Course by L. D. Beklemishev and T. L. Yavorskaya "Provability and Formal Arithmetic II" September 12–December 26, 2023, Steklov Mathematical Institute, Room 303 (8 Gubkina)
We kindly ask all participants, including remote ones and those watching recorded videos, to register
at this link.
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
Financial support
The course is supported by the Ministry of Science and Higher Education of the Russian Federation (the grant to the Steklov International Mathematical Center, Agreement no. 075-15-2022-265).
Institutions
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow Steklov International Mathematical Center |
|
Course by L. D. Beklemishev and T. L. Yavorskaya "Provability and Formal Arithmetic II", September 12–December 26, 2023 |
|
|
December 12, 2023 (Tue) |
|
1. |
Lecture 13. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya December 12, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
December 5, 2023 (Tue) |
|
2. |
Lecture 12. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya December 5, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
November 21, 2023 (Tue) |
|
3. |
Lecture 11. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya November 21, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
November 14, 2023 (Tue) |
|
4. |
Lecture 10. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya November 14, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
November 7, 2023 (Tue) |
|
5. |
Lecture 9. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya November 7, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
October 31, 2023 (Tue) |
|
6. |
Lecture 8. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya October 31, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
October 24, 2023 (Tue) |
|
7. |
Lecture 7. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya October 24, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
October 17, 2023 (Tue) |
|
8. |
Lecture 6. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya October 17, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
October 10, 2023 (Tue) |
|
9. |
Lecture 5. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya October 10, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
October 3, 2023 (Tue) |
|
10. |
Lecture 4. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya October 3, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
September 26, 2023 (Tue) |
|
11. |
Lecture 3. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya September 26, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
September 19, 2023 (Tue) |
|
12. |
Lecture 2. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya September 19, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|
September 12, 2023 (Tue) |
|
13. |
Lecture 1. Provability and Formal Arithmetic L. D. Beklemishev, T. L. Yavorskaya September 12, 2023 16:45, Steklov Mathematical Institute, Room 303 (8 Gubkina)
|
|
|
|
|
|