Penn Arts & Sciences Logo

Logic and Computation Seminar

Monday, April 29, 2024 - 3:30pm

Hanul Jeon

Cornell University

Location

University of Pennsylvania

DRL A2

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.