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

• Remarks on Herbrand normal forms and Herbrand realizations
• Herbrand consistency of some arithmetical theories
• Herbrand's theorem and extractive proof theory
• scientific article; zbMATH DE number 440482
• Extracting Herbrand disjunctions by functional interpretation

zbMATH Keywords

bounded arithmeticpolynomial hierarchysecond-order arithmeticreflection principlePRAprimitive recursive arithmeticrecursive functionalsHerbrand theoremGrzegorczyk hierarchyextractions of relevant functions from proofsHerbrand theoryKalmar elementary classProvably total functionstransformations of proofs

Mathematics Subject Classification ID

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 ε₀‐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 ATR₀ 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)