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
    0 references
    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

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references