A proof-theoretical analysis of ptykes (Q1322455): Difference between revisions
From MaRDI portal
Set profile property. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Q4040375 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Π12-logic, Part 1: Dilators / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3690814 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proof theory / rank | |||
Normal rank |
Latest revision as of 15:35, 22 May 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A proof-theoretical analysis of ptykes |
scientific article |
Statements
A proof-theoretical analysis of ptykes (English)
0 references
7 June 1995
0 references
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''.
0 references
ptyx
0 references
\(n\)-ptykes
0 references
relational structures
0 references
dilator
0 references
second-order arithmetic with arithmetical comprehension
0 references
proof-theoretic analysis
0 references
provable well- orderings
0 references