A proof-theoretical analysis of ptykes (Q1322455): Difference between revisions

Girard introduced the notion of \(n\)-ptykes in terms of the language of category theory. The author reformulates it, in this paper, in the form of relational structures. Namely, a 0-ptyx is a well-ordering; and an \((n+1)\)-ptyx is a structure that results in a 0-ptyx when `applied' to an \(n\)-ptyx (together with further conditions). And, a dilator is an alias of a 1-ptyx. Through coding and representations, the notion and the properties of ptykes are arithmetized in \(\text{ACA}_ 0\), the second- order arithmetic with arithmetical comprehension. The author's main purpose is to exhibit the limitation of \(\text{ACA}_ 0\) in this situation, particularly with respect to dilators and (the next level) 2- ptykes. By proof-theoretic analysis, he shows that if \(\text{ACA}_ 0\) together with true \(\Pi_ 1^ 1\)-sentences shows \(F\) to be a dilator, then \(F(\alpha)\) cannot be too big an ordinal for any primitive recursive ordinal \(\alpha\). A corollary to this shows that there is no provable dilator that sends \(\alpha\) to \(\omega_ \omega^ \alpha\) (= the limit of \(\omega_ n^ \alpha\) where \(\omega_ 2^ \alpha\) is \(\omega^{(\omega^ \alpha)}\), etc.) the situation of 2-ptykes is similar; true \(\Pi_ 2^ 1\)-sentences cannot show, in \(\text{ACA}_ 0\), the existence of a 2-ptyx that sends a dilator \(F\) to \(\sum_{n\in \omega} F^ n (0)\). And these are the best possible limitations: 1- and 2-ptykes of slower growth can be shown to exist. As the author states, these extend ``the traditional proof-theoretic objective of finding a bound on the provable well-orderings [i.e. 0-ptykes] of a theory''.