Hardwiring truth in functional interpretations

Dinis, Bruno; Gaspar, Jaime

http://hdl.handle.net/10362/155246

Utilize este identificador para referenciar este registo.

Nome:	Descrição:	Tamanho:	Formato:
Hardwiring_truth_in_functional_interpretations.pdf		371.47 KB	Adobe PDF	Ver/Abrir

Contacte-nos

Autores

Dinis, Bruno

Gaspar, Jaime

Resumo(s)

We present four different approaches to prove the soundness theorem for variants with t-truth of functional interpretations. To showcase our different methods we focus on the intuitionistic nonstandard bounded functional interpretation of the nonstandard extensional Heyting arithmetic in all finite types because a version with t-truth for this interpretation has not been given before. Also, because it is a more involved interpretation than others since it includes both nonstandard principles and majorisability. This leads us to believe that if the approaches work for this more complicated functional interpretation, then they should also work for simpler functional interpretations (and realisabilities).