Herbrand analyses

DOI10.1007/BF01621477zbMath0722.03040MaRDI QIDQ2641297

Wilfried Sieg

Publication date: 1991

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

zbMATH Keywords

bounded arithmetic; primitive recursive arithmetic; polynomial hierarchy; PRA; reflection principle; second-order arithmetic; recursive functionals; Herbrand theorem; Grzegorczyk hierarchy; extractions of relevant functions from proofs; Herbrand theory; Kalmar elementary class; Provably total functions; transformations of proofs

Mathematics Subject Classification ID

03F30: First-order arithmetic and fragments

03F35: Second- and higher-order arithmetic and fragments

03F03: Proof theory in general (including proof-theoretic semantics)

Related Items

Annual meeting of the Association for Symbolic Logic, Notre Dame, 1993, Effectiveness and provability, On the relationship between ATR₀ and, A simple proof of Parsons' theorem, Term rewriting theory for the primitive recursive functions, Consistency statements and iterations of computable functions in \(\mathrm{I}\Sigma_1\) and PRA, Primitive recursive selection functions for existential assertions over abstract algebras, Harrington's conservation theorem redone, Induction rules, reflection principles, and provably recursive functions, Theories with self-application and computational complexity., Remarks on Herbrand normal forms and Herbrand realizations, Saturated models of universal theories, A note on the proof theory of the \(\lambda \Pi\)-calculus, Formalizing forcing arguments in subsystems of second-order arithmetic, Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fragments of arithmetic
• Countable algebra and set existence axioms
• Factorization of polynomials and \(\Sigma ^ 0_ 1\) induction
• Proof theory. 2nd ed
• On the scheme of induction for bounded arithmetic formulas
• Nested recursion
• Classes of recursive functions based on Ackermann's function
• Quantifier-free and one-quantifier systems
• Mathematical significance of consistency proofs
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• A classification of the ordinal recursive functions
• Eine Klassifikation der ε₀‐Rekursiven Funktionen
• On n-quantifier induction
• On the Interpretation of Non-Finitist Proofs--Part I
• On the interpretation of non-finitist proofs–Part II