Proof theory. The first step into impredicativity

DOI10.1007/978-3-540-69319-2zbMath1153.03001OpenAlexW4239393213MaRDI QIDQ930618

Publication date: 1 July 2008

Published in: Universitext (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-69319-2

zbMATH Keywords

complexity recursion proof theory formal systems predicativity ordinals inductive definitions infinitary language subsystems of analysis

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Proof theory in general (including proof-theoretic semantics) (03F03) Recursive ordinals and ordinal notations (03F15) Relative consistency and interpretations (03F25)

Related Items (54)

, , AND REINHARDT’S PROGRAM ⋮ On elementary theories of ordinal notation systems based on reflection principles ⋮ Relative Truth Definability of Axiomatic Truth Theories ⋮ De Finettian logics of indicative conditionals. II: Proof theory and algebraic semantics ⋮ A MATHEMATICAL COMMITMENT WITHOUT COMPUTATIONAL STRENGTH ⋮ Simplified Cut Elimination for Kripke-Platek Set Theory ⋮ On the Performance of Axiom Systems ⋮ Well-Ordering Principles in Proof Theory and Reverse Mathematics ⋮ Epsilon substitution for $ID_1$ via cut-elimination ⋮ A note on the theory SID<ω of stratified induction ⋮ Pure patterns of order 2 ⋮ Hyperations, Veblen progressions and transfinite iteration of ordinal functions ⋮ Deducibility and independence in Beklemishev's autonomous provability calculus ⋮ Reducing ω-model reflection to iterated syntactic reflection ⋮ NONCLASSICAL TRUTH WITH CLASSICAL STRENGTH. A PROOF-THEORETIC ANALYSIS OF COMPOSITIONAL TRUTH OVER HYPE ⋮ Systems for non-reflexive consequence ⋮ Well ordering principles for iterated $\Pi^1_1$-comprehension ⋮ A note on ordinal exponentiation and derivatives of normal functions ⋮ Characterizations of ordinal analysis ⋮ The omega-rule interpretation of transfinite provability logic ⋮ The Π21$\Pi ^1_2$ consequences of a theory ⋮ Predicatively unprovable termination of the Ackermannian Goodstein process ⋮ Notes on models of (partial) Kripke-Feferman truth ⋮ Provably true sentences across axiomatizations of Kripke's theory of truth ⋮ Effective cut-elimination for a fragment of modal mu-calculus ⋮ The polytopologies of transfinite provability logic ⋮ A NOTE ON PREDICATIVE ORDINAL ANALYSIS I: ITERATED COMPREHENSION AND TRANSFINITE INDUCTION ⋮ More on Systems of Truth and Predicative Comprehension ⋮ Proof Theoretic Analysis by Iterated Reflection ⋮ A disquotational theory of truth as strong as $Z_2^-$ ⋮ About Truth and Types ⋮ From Subsystems of Analysis to Subsystems of Set Theory ⋮ Short note: least fixed points versus least closed points ⋮ An order-theoretic characterization of the Howard-Bachmann-hierarchy ⋮ Axiomatic theories of partial ground. II: Partial ground and hierarchies of typed truth ⋮ Ordinal analysis of non-monotone $\Pi_1^0$-definable inductive definitions ⋮ A Computation of the Maximal Order Type of the Term Ordering on Finite Multisets ⋮ $\Pi_1^1$-comprehension as a well-ordering principle ⋮ Some notes on truths and comprehension ⋮ The Hydra battle and Cichon's principle ⋮ Pure $\Sigma_2$-elementarity beyond the core ⋮ Iterated Inductive Definitions Revisited ⋮ Predicativity and Feferman ⋮ The implicit commitment of arithmetical theories and its semantic core ⋮ The middle ground-ancestral logic ⋮ A Characterisation of Definable NP Search Problems in Peano Arithmetic ⋮ Cut elimination for systems of transparent truth with restricted initial sequents ⋮ Reference and truth ⋮ The Limits of Predicativity Revisited ⋮ A Glimpse of $$ \sum_{3} $$-elementarity ⋮ INFINITARY TABLEAU FOR SEMANTIC TRUTH ⋮ AXIOMATIZING SEMANTIC THEORIES OF TRUTH? ⋮ Ackermannian Goodstein sequences of intermediate growth ⋮ REFLECTION RANKS AND ORDINAL ANALYSIS

This page was built for publication: Proof theory. The first step into impredicativity