Herbrand analyses
DOI10.1007/BF01621477zbMATH Open0722.03040OpenAlexW4239618235MaRDI QIDQ2641297FDOQ2641297
Authors: 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
Recommendations
bounded arithmeticpolynomial hierarchysecond-order arithmeticreflection principlePRAprimitive recursive arithmeticrecursive functionalsHerbrand theoremGrzegorczyk hierarchyextractions of relevant functions from proofsHerbrand theoryKalmar elementary classProvably total functionstransformations of proofs
Proof theory in general (including proof-theoretic semantics) (03F03) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35)
Cites Work
- On the scheme of induction for bounded arithmetic formulas
- Title not available (Why is that?)
- On the interpretation of non-finitist proofs–Part II
- Proof theory. 2nd ed
- Title not available (Why is that?)
- Title not available (Why is that?)
- A classification of the ordinal recursive functions
- Countable algebra and set existence axioms
- On the Interpretation of Non-Finitist Proofs--Part I
- Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
- Fragments of arithmetic
- On n-quantifier induction
- Title not available (Why is that?)
- Factorization of polynomials and \(\Sigma ^ 0_ 1\) induction
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Eine Klassifikation der ε0‐Rekursiven Funktionen
- Nested recursion
- Title not available (Why is that?)
- Quantifier-free and one-quantifier systems
- Title not available (Why is that?)
- Classes of recursive functions based on Ackermann's function
- Mathematical significance of consistency proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (26)
- Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
- Local induction and provably total computable functions
- Remarks on Herbrand normal forms and Herbrand realizations
- Induction rules, reflection principles, and provably recursive functions
- On the Herbrand content of LK
- Consistency statements and iterations of computable functions in \(\mathrm{I}\Sigma_1\) and PRA
- A simple proof of Parsons' theorem
- Herbrand's theorem and extractive proof theory
- Title not available (Why is that?)
- Harrington's conservation theorem redone
- Saturated models of universal theories
- Formalizing forcing arguments in subsystems of second-order arithmetic
- On extracting variable Herbrand disjunctions
- Annual meeting of the Association for Symbolic Logic, Notre Dame, 1993
- On nested simple recursion
- A note on the proof theory of the \(\lambda \Pi\)-calculus
- Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
- Unprovability results for clause set cycles
- On the relationship between ATR0 and
- Theories with self-application and computational complexity.
- An approximate Herbrand's theorem and definable functions in metric structures
- Title not available (Why is that?)
- Primitive recursive selection functions for existential assertions over abstract algebras
- Unfolding schematic systems
- Effectiveness and provability
- Term rewriting theory for the primitive recursive functions
This page was built for publication: Herbrand analyses
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2641297)