- Propositional Logic
- Basic definitions
- Formal definitions: language, formulas
- Sequents and the sequent calculus
- Examples of proofs
- Weakening, structure theorems
- Admissible rules
- Completeness
- Intuitionistic and minimal logic
- Disjunction property
- Double negation translation
- Cut-elimination
- Proof of cut-elimination
- Interpolation theorem
- Lower bounds on cut-elimination
- First-order logic
- Language, terms, expressions
- Free variables, substitutability
- Sequent calculus
- Intuitionistic and minimal versions
- Göodel double negation translation
- Cut-elimination
- Interpolation theorem
- Herbrand's theorem
- Optimality
- First-order arithmetic
- Peano arithmetic
- Primitive recursion
- Primitive recursive arithmetic
- Friedman-Dragalin
- ε0
- Cut-elimination for PA
- Goodstein sequences
- Logics in higher types
- Functional interpretation