Satoshi Nakata: A j-translation with Kripke forcing relation

Speaker: Satoshi Nakata (Nagoya University)

Abstract: Syntactic translations such as the negative translation and Friedman's A-translation have found numerous applications in intuitionistic proof theory. These translations are well known to admit a uniform description as j-translations, which provides a bridge to topos theory and realizability theory. In this talk, we introduce a new translation that combines j-translations with the Kripke forcing relation in the internal logic of an elementary topos. We first see that the translation is sound for intuitionistic first-order logic and Heyting arithmetic. We then interpret it in the effective topos and show that it extends the sheaf model of realizability introduced by de Jongh and Goodman.