Hardwiring truth in functional interpretations (Q6041142)
From MaRDI portal
scientific article; zbMATH DE number 7689242
Language | Label | Description | Also known as |
---|---|---|---|
English | Hardwiring truth in functional interpretations |
scientific article; zbMATH DE number 7689242 |
Statements
Hardwiring truth in functional interpretations (English)
0 references
26 May 2023
0 references
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.
0 references
interpretations with truth
0 references
functional interpretations
0 references
intuitionism
0 references
bounded interpretations
0 references
nonstandard arithmetic
0 references
0 references