Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies

DOI10.1007/BFb0091894zbMath0489.03022OpenAlexW1579817075MaRDI QIDQ1166517

Wilfried Buchholz, Wilfried Sieg, Wolfram Pohlers, Solomon Feferman

Publication date: 1981

Published in: Lecture Notes in Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bfb0091894

zbMATH Keywords

set-theoretic models intuitionistic theories collapsing functions inductive generation spectrum of a theory constructive theory of functions and classes accessibility operator double-negation translation impredicative subsystems of analysis inductively defined accessibility class inductively defined classes logical reflection principle mathematical reflection principle method of local predicativity negative arithmetic sentences predicative theories virtual well-orderings

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Functionals in proof theory (03F10) Recursive ordinals and ordinal notations (03F15)

Related Items

Countable sets versus sets that are countable in reverse mathematics ⋮ The Urysohn Extension Theorem for Bishop Spaces ⋮ ON THE UNCOUNTABILITY OF ⋮ Simplified Cut Elimination for Kripke-Platek Set Theory ⋮ On the Performance of Axiom Systems ⋮ European Summer Meeting of the Association for Symbolic Logic ⋮ Type theory as a foundation for computer science ⋮ Well ordering principles for iterated $\Pi^1_1$-comprehension ⋮ Locally hyperarithmetical induction ⋮ The non-normal abyss in Kleene's computability theory ⋮ On the computational properties of the uncountability of the real numbers ⋮ Revisiting the conservativity of fixpoints over intuitionistic arithmetic ⋮ Elementary patterns of resemblance ⋮ Universes in explicit mathematics ⋮ Tiered Arithmetics ⋮ Iterated Inductive Definitions Revisited ⋮ The Operational Penumbra: Some Ontological Aspects ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Predicativity and Feferman ⋮ Feferman’s Skepticism About Set Theory ⋮ MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics ⋮ Induction and inductive definitions in fragments of second order arithmetic ⋮ A NOTE ON THEORIES FOR QUASI-INDUCTIVE DEFINITIONS ⋮ On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics ⋮ A Glimpse of $$ \sum_{3} $$-elementarity ⋮ AXIOMATIZING SEMANTIC THEORIES OF TRUTH? ⋮ THE PREHISTORY OF THE SUBSYSTEMS OF SECOND-ORDER ARITHMETIC ⋮ An intensional fixed point theory over first order arithmetic ⋮ The proof-theoretic analysis of transfinitely iterated fixed point theories ⋮ Hilbert's Programs: 1917–1922 ⋮ 1998 European Summer Meeting of the Association for Symbolic Logic ⋮ How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study ⋮ Realizability interpretation of generalized inductive definitions ⋮ Proof theory of reflection ⋮ Proof Theory in Philosophy of Mathematics ⋮ The strength of admissibility without foundation ⋮ The strength of some Martin-Löf type theories ⋮ Reflecting on incompleteness ⋮ Bounded inductive dichotomy: separation of open and clopen determinacies with finite alternatives in constructive contexts ⋮ The role of parameters in bar rule and bar induction ⋮ An independence result for $(\Pi^ 1_ 1-CA)+BI$ ⋮ Understanding uniformity in Feferman's explicit mathematics ⋮ On the proof-theoretic strength of monotone induction in explicit mathematics ⋮ Betwixt Turing and Kleene ⋮ Between Turing and Kleene ⋮ Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume;Unprovability of certain combinatorial properties of finite trees ⋮ Ordinal notations based on a hierarchy of inaccessible cardinals ⋮ Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones ⋮ Second order theories with ordinals and elementary comprehension ⋮ Error and Predicativity ⋮ How to Compare Buchholz-Style Ordinal Notation Systems with Gordeev-Style Notation Systems ⋮ A theory of formal truth arithmetically equivalent to ID₁ ⋮ Ordinal arithmetic based on Skolem hulling ⋮ Epsilon substitution for $ID_1$ via cut-elimination ⋮ Monotone inductive definitions in a constructive theory of functions and classes ⋮ Book review of: R. Kahle (ed.) and M. Rathjen (ed.), Gentzen's centenary. The quest for consistency ⋮ ABOUT SOME FIXED POINT AXIOMS AND RELATED PRINCIPLES IN KRIPKE–PLATEK ENVIRONMENTS ⋮ Generalizations of the Kruskal-Friedman theorems ⋮ A boundedness theorem in ID₁(W) ⋮ Lifting proofs from countable to uncountable mathematics ⋮ About the proof-theoretic ordinals of weak fixed point theories ⋮ Natural well-orderings ⋮ IN MEMORIAM: SOLOMON FEFERMAN (1928–2016) ⋮ Inductively generated formal topologies. ⋮ A logic of abstraction related to finite constructive number classes ⋮ The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories ⋮ Proof-theoretical analysis: Weak systems of functions and classes ⋮ Ordinal notations based on a weakly Mahlo cardinal ⋮ Intuitionistic fixed point logic ⋮ Between constructive mathematics and PROLOG ⋮ The Possibility of Analysis: Convergence and Proofs of Convergence ⋮ On power set in explicit mathematics ⋮ The Proof Theory of Common Knowledge ⋮ Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa ⋮ From Subsystems of Analysis to Subsystems of Set Theory ⋮ From Mathesis Universalis to Fixed Points and Related Set-Theoretic Concepts ⋮ On Relating Theories: Proof-Theoretical Reduction ⋮ An order-theoretic characterization of the Howard-Bachmann-hierarchy ⋮ Type-theoretic interpretation of iterated, strictly positive inductive definitions ⋮ First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo ⋮ Proofs, programs, processes ⋮ On the unity of duality ⋮ Fixed points in Peano arithmetic with ordinals ⋮ ϱ-inaccessible ordinals, collapsing functions and a recursive notation system ⋮ Choice principles, the bar rule and autonomously iterated comprehension schemes in analysis ⋮ A note on the theory of positive induction, ${{\text{ID}}^*_1}$ ⋮ An ordinal analysis for theories of self-referential truth ⋮ Forcing in Proof Theory ⋮ CZF and second order arithmetic ⋮ Proof theory and ordinal analysis ⋮ Systems of iterated projective ordinal notations and combinatorial statements about binary labeled trees ⋮ On the No-Counterexample Interpretation ⋮ Intuitionistic Fixed Point Theories for Strictly Positive Operators ⋮ TRUTHS, INDUCTIVE DEFINITIONS, AND KRIPKE-PLATEK SYSTEMS OVER SET THEORY ⋮ Elementary inductive dichotomy: separation of open and clopen determinacies with infinite alternatives ⋮ 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08 ⋮ Notes on some second-order systems of iterated inductive definitions and $\Pi_1^1$-comprehensions and relevant subsystems of set theory ⋮ On the Completeness of Dynamic Logic ⋮ Inductive Completeness of Logics of Programs ⋮ Pure $\Sigma_2$-elementarity beyond the core ⋮ The metamathematics of ergodic theory ⋮ Patterns of resemblance of order 2 ⋮ The implicit commitment of arithmetical theories and its semantic core ⋮ Extended bar induction in applicative theories ⋮ Dual Calculus with Inductive and Coinductive Types ⋮ A flexible type system for the small Veblen ordinal ⋮ From Coinductive Proofs to Exact Real Arithmetic ⋮ Fragments of arithmetic ⋮ Functional interpretation and inductive definitions ⋮ The proof-theoretic analysis of transfinitely iterated quasi least fixed points ⋮ Predicativity and constructive mathematics ⋮ Systems of explicit mathematics with non-constructive $\mu$-operator and join ⋮ Predicative functionals and an interpretation of ${\widehat{\text{ID}}_{<\omega}}$ ⋮ Well-ordering proofs for Martin-Löf type theory ⋮ Some results on cut-elimination, provable well-orderings, induction and reflection ⋮ Foundations for analysis and proof theory ⋮ Having a Look Again at Some Theories ofProof-Theoretic Strengths around $$ \varGamma_{0} $$ ⋮ Cut-Elimination for SBL ⋮ Lower bounds on $\beta (\alpha)$ ⋮ Reverse mathematics of the uncountability of $\mathbb{R}$ ⋮ Addendum to ``Countable algebra and set existence axioms ⋮ Systems of explicit mathematics with non-constructive $\mu$-operator. I ⋮ Saturated models of universal theories ⋮ Universes over Frege structures ⋮ Generalizing classical and effective model theory in theories of operations and classes ⋮ The constructive Hilbert program and the limits of Martin-Löf type theory ⋮ Splittings and robustness for the Heine-Borel theorem