Remarks on Herbrand normal forms and Herbrand realizations

DOI10.1007/BF01627504zbMath0742.03021OpenAlexW2086046439MaRDI 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 formHerbrand realization

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35)

Related Items

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

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