Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
From MaRDI portal
Publication:1166517
DOI10.1007/BFb0091894zbMath0489.03022MaRDI QIDQ1166517
Solomon Feferman, Wilfried Buchholz, Wilfried Sieg, Wolfram Pohlers
Publication date: 1981
Published in: Lecture Notes in Mathematics (Search for Journal in Brave)
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
03-02: Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03F05: Cut-elimination and normal-form theorems
03F10: Functionals in proof theory
03F15: Recursive ordinals and ordinal notations
Related Items
Unnamed Item, Forcing in Proof Theory, On power set in explicit mathematics, Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa, On the No-Counterexample Interpretation, Induction and inductive definitions in fragments of second order arithmetic, Elementary patterns of resemblance, Universes in explicit mathematics, European Summer Meeting of the Association for Symbolic Logic, Systems of iterated projective ordinal notations and combinatorial statements about binary labeled trees, Type-theoretic interpretation of iterated, strictly positive inductive definitions, Extended bar induction in applicative theories, Fragments of arithmetic, Foundations for analysis and proof theory, 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, Ordinal arithmetic based on Skolem hulling, A logic of abstraction related to finite constructive number classes, Proof-theoretical analysis: Weak systems of functions and classes, Ordinal notations based on a weakly Mahlo cardinal, The metamathematics of ergodic theory, Patterns of resemblance of order 2, Addendum to ``Countable algebra and set existence axioms, An independence result for \((\Pi^ 1_ 1-CA)+BI\), Ordinal notations based on a hierarchy of inaccessible cardinals, Monotone inductive definitions in a constructive theory of functions and classes, Between constructive mathematics and PROLOG, Fixed points in Peano arithmetic with ordinals, 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, Systems of explicit mathematics with non-constructive \(\mu\)-operator. I, Realizability interpretation of generalized inductive definitions, Proof theory of reflection, The strength of some Martin-Löf type theories, On the proof-theoretic strength of monotone induction in explicit mathematics, Inductively generated formal topologies., Saturated models of universal theories, Universes over Frege structures, An intensional fixed point theory over first order arithmetic, Understanding uniformity in Feferman's explicit mathematics, 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, Proof theory and ordinal analysis, On the unity of duality, CZF and second order arithmetic, Systems of explicit mathematics with non-constructive \(\mu\)-operator and join, First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo, Choice principles, the bar rule and autonomously iterated comprehension schemes in analysis, A theory of formal truth arithmetically equivalent to ID1, ϱ-inaccessible ordinals, collapsing functions and a recursive notation system, The proof-theoretic analysis of transfinitely iterated quasi least fixed points, Generalizations of the Kruskal-Friedman theorems, 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08, On the Completeness of Dynamic Logic, Dual Calculus with Inductive and Coinductive Types, The strength of admissibility without foundation, Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume;Unprovability of certain combinatorial properties of finite trees, A boundedness theorem in ID1(W), Natural well-orderings, Reflecting on incompleteness, The role of parameters in bar rule and bar induction, About the proof-theoretic ordinals of weak fixed point theories, 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
