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