Hardwiring truth in functional interpretations (Q6041142)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 7689242
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| 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
0.8389157652854919
0 references
0.7687926888465881
0 references
0.7675553560256958
0 references
0.7647030353546143
0 references
0.7586058378219604
0 references
