A herbrandized functional interpretation of classical first-order logic

DOI10.1007/s00153-017-0555-6zbMath1417.03290OpenAlexW2614883855MaRDI QIDQ2402958

Gilda Ferreira, Fernando Ferreira

Publication date: 15 September 2017

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

Full work available at URL: http://hdl.handle.net/10400.2/7089

zbMATH Keywords

first-order logicfinite setsfunctional interpretationsHerbrand's theoremtautologiesstar combinatory calculus

Mathematics Subject Classification ID

Classical first-order logic (03B10) Functionals in proof theory (03F10) Combinatory logic and lambda calculus (03B40)

Related Items

On extracting variable Herbrand disjunctions, A parametrised functional interpretation of Heyting arithmetic, The FAN principle and weak König's lemma in Herbrandized second-order arithmetic, Herbrand's theorem as higher order recursion, Weak König's lemma in Herbrandized classical second-order arithmetic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A functional interpretation for nonstandard arithmetic
• On a hitherto unexploited extension of the finitary standpoint
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Extracting Herbrand disjunctions by functional interpretation
• Bounded functional interpretation
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Functional interpretation and inductive definitions
• Lower Bounds on Herbrand's Theorem
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Bounded modified realizability
• Intensional interpretations of functionals of finite type I
• Logical problems of functional interpretations