1. Propositional Logic
    1. Basic definitions
      1. Formal definitions: language, formulas (Avigad 3.1)
      2. Sequents and the sequent calculus (Avigad 6.1, 6.2)
      3. Examples of proofs (Avigad 3.5, 3.6)
      4. Weakening, structure theorems (Avigad 6.1, 6.2)
      5. Admissible rules
      6. Completeness (Avigad 6.3)
    2. Intuitionistic and minimal logic
      1. Disjunction property
      2. Double negation translation (Avigad 3.7)
    3. Cut-elimination
      1. Proof of cut-elimination (Avigad 6.5, 6.6)
      2. Interpolation theorem (Avigad 7.4)
      3. Lower bounds on cut-elimination
  2. First-order logic
    1. Language, terms, expressions (Avigad 4.1, 4.2)
    2. Free variables, substitutability (Avigad 4.1, 4.2)
    3. Sequent calculus (Avigad 6.1, 6.2)
    4. Intuitionistic and minimal versions
    5. G\"odel double negation translation (Avigad 4.6)
    6. Cut-elimination (Avigad 6.5, 6.6)
    7. Interpolation theorem (Avigad 7.4)
    8. Herbrand's theorem (Avigad 7.1, 7.2)
    9. Optimality
  3. First-order arithmetic
    1. Peano arithmetic
    2. Primitive recursion
    3. Primitive recursive arithmetic
    4. Friedman-Dragalin
    5. $\epsilon_0$
    6. Cut-elimination for PA
    7. Goodstein sequences
    8. Logics in higher types
    9. Functional interpretation