Hardwiring truth in functional interpretations (Q6041142)

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.