Hardwiring truth in functional interpretations

DOI10.4171/PM/2094MaRDI QIDQ6041142zbMATH OpenOpenAlexFDO

Authors Bruno Dinis, Jaime Gaspar

Publication date 26 May 2023

Published in Portugaliae Mathematica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.4171/pm/2094

zbMATH Keywords

bounded interpretationsfunctional interpretationsinterpretations with truthintuitionismnonstandard arithmetic

Mathematics Subject Classification ID

Functionals in proof theory (03F10) Relative consistency and interpretations (03F25) Second- and higher-order arithmetic and fragments (03F35)

Review text

This paper, which continues the authors's [Ann. Pure Appl. Logic 169, No. 5, 392--412 (2018; Zbl 1426.03013)], focuses on the reasons why the soundness theorem of intuitionistic nonstandard bounded functional interpretation with t-truth of the nonstandard extensional Heyting arithmetic in all finite types holds. To this end, four different proofs are presented: by induction on the length of derivations (the standard proof), by hardwiring q-truth, by means of the copies-only method and using the t and o translations.

Recommendations

• Proof interpretations with truth
• On the Herbrand functional interpretation
• On bounded functional interpretations
• Nonstandardness and the bounded functional interpretation
• Functional interpretation and the existence property

Cites work

• A functional interpretation for nonstandard arithmetic
• A parametrised functional interpretation of Heyting arithmetic
• Bounded functional interpretation
• Bounded modified realizability
• Constructivism in mathematics. An introduction. Volume I
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Formalized recursive functionals and formalized realizability
• scientific article; zbMATH DE number 956475 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• scientific article; zbMATH DE number 3248792 (Why is no real title available?)
• Injecting uniformities into Peano arithmetic
• Intuitionistic nonstandard bounded modified realisability and functional interpretation
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Proof interpretations with truth
• Unifying functional interpretations
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(2)

• The FAN principle and weak König's lemma in Herbrandized second-order arithmetic
• Proof interpretations with truth

This page was built for publication: Hardwiring truth in functional interpretations

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