Center for Mathematics, Fundamental Applications and Operations Research

Financiador

Organização

Publicações

Hardwiring truth in functional interpretations

Publication . Dinis, Bruno; Gaspar, Jaime; CMA - Centro de Matemática e Aplicações; EMS Press

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).

2023-02-11Artigo científico

Acesso aberto

Ver mais

Entidade financiadora

Fundação para a Ciência e a Tecnologia

Programa de financiamento

6817 - DCRRNI ID

Número da atribuição

UIDB/04561/2020