Extracting Herbrand disjunctions by functional interpretation

DOI10.1007/S00153-005-0275-1zbMATH Open1081.03056OpenAlexW2082381286MaRDI QIDQ2486989FDOQ2486989

Philipp Gerhardy, Ulrich Kohlenbach

Publication date: 17 August 2005

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

Full work available at URL: https://doi.org/10.1007/s00153-005-0275-1

Recommendations

• On extracting variable Herbrand disjunctions
• A sequent-calculus based formulation of the extended first epsilon theorem
• On the Herbrand functional interpretation
• Herbrand's theorem and extractive proof theory
• A herbrandized functional interpretation of classical first-order logic

zbMATH Keywords

Herbrand's theoremfunctional interpretationHerbrand terms

Mathematics Subject Classification ID

Classical first-order logic (03B10) Functionals in proof theory (03F10)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• Exact bounds for lengths of reductions in typed \(\lambda\)-calculus
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Lower Bounds on Herbrand's Theorem
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Computer Science Logic
• A complexity analysis of functional interpretations
• A note on Spector's quantifier-free rule of extensionality
• Cut elimination and automatic proof procedures
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logical problems of functional interpretations

Cited In (17)

• Title not available (Why is that?)
• Herbrand's theorem as higher order recursion
• On the Herbrand content of LK
• A herbrandized functional interpretation of classical first-order logic
• Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
• Title not available (Why is that?)
• A complexity analysis of functional interpretations
• Herbrand complexity and the epsilon calculus with equality
• Herbrand's theorem and extractive proof theory
• Title not available (Why is that?)
• Herbrand's theorem and term induction
• On extracting variable Herbrand disjunctions
• On the practical value of Herbrand disjunctions
• On the non-confluence of cut-elimination
• Herbrand analyses
• Title not available (Why is that?)
• Herbrand Sequent Extraction

This page was built for publication: Extracting Herbrand disjunctions by functional interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2486989)