A $j$-translation with Kripke forcing relation

TL;DR

This paper introduces a novel translation combining the $j$-translation with Kripke forcing within an elementary topos, extending realizability models and analyzing semi-classical axioms to establish new separation results.

Contribution

It presents a new translation method that unifies $j$-translation and Kripke forcing, extending realizability models and providing insights into semi-classical arithmetic.

Findings

Translation is sound for intuitionistic logic and Heyting arithmetic.

Interpretation extends the sheaf model of realizability.

Establishes a separation result for semi-classical arithmetics.

Abstract

In this paper, we introduce a translation that combines the $j$-translation with Kripke forcing in the internal logic of an elementary topos. First, we show that our translation is sound for intuitionistic first-order logic and Heyting arithmetic. Furthermore, its interpretation in the effective topos provides an extension of the sheaf model of realizability introduced by de Jongh and Goodman. As an application, we systematically investigate translations for semi-classical axioms. Based on this investigation, we establish a separation result on semi-classical arithmetics, which cannot be obtained using the usual $j$-realizability.