Remarks on Herbrand normal forms and Herbrand realizations

DOI10.1007/BF01627504zbMath0742.03021MaRDI QIDQ1813063

Ulrich Kohlenbach

Publication date: 25 June 1992

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

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

zbMATH Keywords

Herbrand normal form; Herbrand realization

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03F30: First-order arithmetic and fragments

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

Related Items

On uniform weak König's lemma, Primitive recursive selection functions for existential assertions over abstract algebras, Harrington's conservation theorem redone, Arithmetical conservation results, Saturated models of universal theories, Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization

Cites Work

• Unnamed Item
• Unnamed Item
• Fragments of arithmetic
• Goodman's theorem and beyond
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• Herbrand analyses
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• The theory of the Gödel functionals
• Relativized realizability in intuitionistic arithmetic of all finite types
• Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
• On n-quantifier induction
• On the Interpretation of Non-Finitist Proofs--Part I