The course presents an introduction to one of the most important formal theories - Peano arithmetic - and some classical results related to it, which are fundamental to structural proof theory. The following topics will be covered:

Topic 1: Sequent Calculus for Predicate Logic

• Sequent calculus for predicate logic in Tate format.
• The cut elimination theorem.
• Consequences of the cut elimination theorem: subformula property, Herbrand's theorem (for existential formulas), Craig's interpolation theorem.
• Formalization of Peano arithmetic in the sequent calculus. The system of arithmetic with free predicate variables $\mathrm{РА(Х)}$.

Topic 2: Ordinal Arithmetic

• Well-ordered sets, operations of addition, multiplication, exponentiation.
• Cantor's normal form and the canonical ordinal notation system for the ordinal $\epsilon_0$.

Topic 3: Omega-logic

• Omega rule and omega-logic.
• $\mathrm{РА}\omega$, arithmetic with the omega rule.
• Provability of true $\Pi_1^1$ sentences in $\mathrm{РА}\omega$.
• Embedding of proofs in $\mathrm{РА(Х)}$ into $\mathrm{РА}\omega$.

Topic 4: Cut Elimination in Arithmetic with the Omega-Rule

• Height and rank of omega-derivations.
• Elimination of the cut rule in $\mathrm{РА}\omega$ with rank and height bounds.
• Transfinite induction principle; transfinite induction schema for arithmetically definable well-orders.
• Lemma on the lower bound on the height of cut-free derivations of transfinite induction formulas in $\mathrm{РА}\omega$.
• Unprovability of transfinite induction for the ordinal $\epsilon_0$ in Peano arithmetic (Gentzen's theorem).
• Provability of transfinite induction for initial segments of ordinal $\epsilon_0$ in Peano arithmetic (Gentzen's theorem).

Topic 5: Proof-Theoretic Ordinals

• Second-order arithmetic system $\mathrm{АСА}_0$.
• The ordinal of a theory as the supremum of all order types of provably well-founded total orderings.
• Theorem: For any $\Pi_1^1$ sentence $\pi$, there exists a primitive recursive tree $T$ such that $\pi$ is equivalent to the well-foundedness of $T$.
• Kleene-Brouwer order on an omega-tree. Equivalence of its well-foundedness and the well-foundedness of the tree. Formalizability in $\mathrm{АСА}_0$.
• Construction of a recursive well-ordering universal for the set of all provably well- founded total orderings of a theory $T$. Coincidence of its order type with the ordinal of the theory.
• Corollary: The ordinal of a $\Pi_1^1$-sound theory is less than the supremum of the ordinals of all recursively enumerable well-orderings (Church-Kleene ordinal).
• Preservation of the ordinal of a $\Pi_1^1$-sound theory under extensions by true $\Sigma_1^1$ sentences.
• Every recursively enumerable ordinal is primitive recursive.

References:
[1] W. Pohlers, Proof theory: First steps into impredicativity. Springer-Verlag Berlin Heidelberg, 2009 (topics 1-4).
[2] M. Rathjen, The realm of ordinal analysis. S.B. Cooper and J.K. Truss (eds.): Sets and Proofs. (Cambridge University Press, 1999) 219–279. (topic 5).
[3] H. Schwichtenberg, Some applications of cut elimination. In: Handbook of Mathematical Logic (eds. J. Barwise), Part IV (Ch. 2). Studies in Logic and the Foundations of Mathematics, Volume 90, 1977, Pages 867-895 (topics 1-4).

Fall Semester Schedule of 2023/2024:

Time: Tuesday 16:45 – 18:15

First lecture: September 12

Lecturers
Beklemishev Lev Dmitrievich
Yavorskaya Tatiana Leonidovna

Organizations
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow
Steklov International Mathematical Center