Logic Seminar

Hanul JeonCornell University
Proof theory for higher pointclasses

Friday, February 16, 2024 - 2:55pm
Malott 205

Gentzen initiated Ordinal analysis to answer the question of Hilbert whether arithmetic is consistent. Ordinal analysis produces a proof-theoretic ordinal of a theory, which is the least ordinal whose well-foundness is unprovable by the theory. While the current ordinal analysis successfully establishes a way to gauge the strength of fragments of arithmetic, it has a weakness in that it only gauges $\Pi^1_1$ consequences of a theory. Thus, we can ask whether there is another characteristic gauging the theorems of a more complex form. On the other side, Girard developed the notion of dilators and ptykes to develop the proof theory for $\Pi^1_n$ formulas, and recent works by Aguilera and Pakhomov illustrate how to use dilators and ptykes to capture \Pi^1_n consequences of a theory. However, dilators and ptykes are not linearly comparable, unlike ordinals.

In my talk, I will present ordinal characteristics capturing the $\Sigma^1_2$ and $\Pi^1_3$ consequences of theories, and prove Walsh's characterizations to these characteristics. The $\Sigma^1_2$ case is captured by what is called s^1_2 ordinal, and the $\Pi^1_3$ case is captured by the proof-theoretic ptyx with a special argument. Walsh-styled characterization only works for sufficiently strong theories, and especially, the $\Pi^1_3$ case only applies to theories extending $\mathbf{\Delta}^1_2$-determinacy.