Well ordering principles for iterated \(\Pi^1_1\)-comprehension (Q6080077): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
ReferenceBot (talk | contribs)
Changed an Item
 
Property / cites work
 
Property / cites work: Reverse mathematics and well-ordering principles: a pilot study / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4075450 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4109654 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A new system of proof-theoretic ordinal functions / rank
 
Normal rank
Property / cites work
 
Property / cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5622162 / rank
 
Normal rank
Property / cites work
 
Property / cites work: \(\Pi_1^1\)-comprehension as a well-ordering principle / rank
 
Normal rank
Property / cites work
 
Property / cites work: A categorical construction of Bachmann–Howard fixed points / rank
 
Normal rank
Property / cites work
 
Property / cites work: Computable aspects of the Bachmann–Howard principle / rank
 
Normal rank
Property / cites work
 
Property / cites work: From Kruskal’s theorem to Friedman’s gap condition / rank
 
Normal rank
Property / cites work
 
Property / cites work: PREDICATIVE COLLAPSING PRINCIPLES / rank
 
Normal rank
Property / cites work
 
Property / cites work: Set-theoretic reflection is equivalent to induction over well-founded classes / rank
 
Normal rank
Property / cites work
 
Property / cites work: Patterns of resemblance and Bachmann-Howard fixed points / rank
 
Normal rank
Property / cites work
 
Property / cites work: Bachmann-Howard derivatives / rank
 
Normal rank
Property / cites work
 
Property / cites work: Derivatives of normal functions in reverse mathematics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Minimal bad sequences are necessary for a uniform Kruskal theorem / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5619071 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4111536 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Π12-logic, Part 1: Dilators / rank
 
Normal rank
Property / cites work
 
Property / cites work: Introduction to \(\Pi^1_2\)-logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3773876 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Reverse mathematics and ordinal exponentiation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Beweistheorie vonKPN / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3968923 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Zur Beweistheorie Der Kripke-Platek-Mengenlehre Über Den Natürlichen Zahlen / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3778746 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Bar induction and \(\omega\) model reflection / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5625138 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Well-quasiordering finite trees with gap-condition. Proof of Harvey Friedman's conjecture / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3837736 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Veblen functions for computability theorists / rank
 
Normal rank
Property / cites work
 
Property / cites work: Open Questions in Reverse Mathematics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5734436 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Cut elimination for impredicative infinitary systems. Part II ordinal analysis for iterated inductive definitions / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4215633 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof theory. The first step into impredicativity / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3809793 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3081650 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3464624 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Well-Ordering Principles in Proof Theory and Reverse Mathematics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Well-ordering Principles, ω-models and $$ \varPi_{1}^{1} $$-comprehension / rank
 
Normal rank
Property / cites work
 
Property / cites work: Gentzen's Centenary / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof-theoretic investigations on Kruskal's theorem / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2906572 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Ein System des Verknüpfenden Schliessens / rank
 
Normal rank
Property / cites work
 
Property / cites work: Eine Grenze Für die Beweisbarkeit der Transfiniten Induktion in der Verzweigten Typenlogik / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4143279 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3395521 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Galvin-Prikry theorem and set existence axioms / rank
 
Normal rank
Property / cites work
 
Property / cites work: Weak axioms of determinacy and subsystems of analysis I: δ20 games / rank
 
Normal rank

Latest revision as of 08:31, 3 August 2024

scientific article; zbMATH DE number 7756888
Language Label Description Also known as
English
Well ordering principles for iterated \(\Pi^1_1\)-comprehension
scientific article; zbMATH DE number 7756888

    Statements

    Well ordering principles for iterated \(\Pi^1_1\)-comprehension (English)
    0 references
    0 references
    0 references
    30 October 2023
    0 references
    The authors present new reverse mathematical equivalences between ordinal collapsing principles, iterated \(\Pi^1_1\)-comprehension, and the existence of admissible sets. A central result is that, over \(\mathsf{RCA}_0\), the following are equivalent for any infinite well-ordering \(\nu\): (1) \(\Pi^1_1\)-recursion along \(\nu\); (2) any dilator has a well founded \(\nu\)-fixed point; and (3) if \(D\) is a dilator, then \(\psi_\nu (D)\) is well founded. Using \(\mathsf{ATR}_0^{\mathsf{set}}\) as a base system, (1) and (3) are shown to be equivalent to: (4) for any set \(u\), there is a sequence of admissible sets \(\mathsf{Ad}_\alpha \owns u\) for \(\alpha < \nu\) such that \(\alpha < \beta < \nu\) entails \(\mathsf{Ad}_\alpha \in\mathsf{Ad}_\beta\) (where \(\nu\) is viewed as an ordinal). The result has consequences in the characterization of \(\beta\)-models of \(\Pi^1_1\)-comprehension, including a result promised in a paper of \textit{M. Rathjen} [in: Axiomatic thinking II. Cham: Springer. 89--127 (2022; Zbl 07632450)]. \textit{A. Freund} has applied the work presented here to prove the equivalence of \(\Pi^1_1\)-transfinite recursion and a uniform Kruskal-Friedman theorem with gap condition [``Reverse mathematics of a uniform Kruskal-Friedman theorem'', Preprint, \url{arXiv:2112.08727}]. These new iterated results build on earlier results on the equivalence of \(\Pi^1_1\)-comprehension and fixed points of dilators in the work of \textit{A. Freund} [J. Math. Log. 20, No. 2, Article ID 2050006, 26 p. (2020; Zbl 1457.03027)].
    0 references
    well ordering principles
    0 references
    ordinal collapsing functions
    0 references
    iterated \(\Pi^1_1\)-comprehension
    0 references
    transfinite recursion
    0 references
    admissible sets
    0 references
    dilators
    0 references
    ordinal analysis
    0 references
    reverse mathematics
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references