Herbrand analyses

DOI10.1007/BF01621477zbMath0722.03040OpenAlexW4239618235MaRDI QIDQ2641297

Wilfried Sieg

Publication date: 1991

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

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

zbMATH Keywords

bounded arithmeticprimitive recursive arithmeticpolynomial hierarchyPRAreflection principlesecond-order arithmeticrecursive functionalsHerbrand theoremGrzegorczyk hierarchyextractions of relevant functions from proofsHerbrand theoryKalmar elementary classProvably total functionstransformations of proofs

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

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

Cites Work

• 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
• 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