2.1 The internal language of a topos

The proofs in Sections 3, 4, and 6 are formalizable within a certain higher-order logic. To make this explicit, we review the internal language $\mathcal {L}_{\mathcal {E}}$ of an elementary topos $\mathcal {E}$ in detail. While various conventions exist in the literature, we follow the notation of the type theory based on equality introduced in [Reference Lambek and Scott26, Part II].

Each type in $\mathcal {L}_{\mathcal {E}}$ corresponds to an object of $\mathcal {E}$ . In particular, $1$ , $\Omega $ , and $PX$ denote the terminal object, the subobject classifier, and the power object of an object X, respectively. We assume that each type is associated with countably many free variables. A context is a finite list of typed variables, typically written as $\Gamma = [x_1:X_1, \dots , x_n:X_n]$ . The concatenation of contexts $\Gamma $ and $\Gamma '$ is denoted by $\Gamma \cup \Gamma '$ . Given a context $\Gamma $ , we define terms in context $\Gamma $ (written as $(t:X\quad \Gamma )$ or $t[\vec {x}]$ ) inductively as follows:

• • $*:1$ ;

• • $x:X$ for each variable x in $\Gamma $ ;

• • $\langle t, t'\rangle : X\times Y$ if $t:X$ and $t':Y$ ;

• • $f(t):Y$ for a morphism $f\colon X\to Y$ in $\mathcal {E}$ and a term $t:X$ ;

• • $\{\, x:X \mid \varphi \,\}:PX$ if $\varphi :\Omega $ is a term in $\Gamma \cup [x:X]$ .

A term of type $\Omega $ is called an ( $\mathcal {L}_{\mathcal {E}}$ -)formula, and one with no free variables is called a sentence. The primitive formulas in the type theory based on equality are the following:

$$\begin{align*}\top \ {:}{=}\ \mathrm{true}(*):\Omega, \quad (t =_X t') \ {:}{=}\ (=_X(\langle t, t' \rangle)):\Omega, \end{align*}$$

$$\begin{align*}(t \in_X u) \ {:}{=}\ (\in_X(\langle t, u \rangle)):\Omega,\end{align*}$$

where $\mathrm {true} \colon 1 \to \Omega $ is the subobject classifier, $=_X \colon X \times X \to \Omega $ is the characteristic map of the diagonal map $\Delta _X \colon X \rightarrowtail X \times X$ , and $\in _X \colon X \times PX \to \Omega $ is the evaluation map associated with the power object. Other logical symbols, such as the bottom symbol $\bot $ , the logical connectives $\land $ , $\lor $ , $\rightarrow $ , and the quantifiers $\forall $ , $\exists $ are defined in terms of these primitive formulas. For example, universal quantification is defined by

$$\begin{align*}\forall x:X. \varphi[x] \ {:}{=}\ (\{\, x:X \mid \varphi[x]\,\} =_{PX} \{\, x:X \mid \top\,\}).\end{align*}$$

See [Reference Lambek and Scott26, Part II Section 2] for more details. A term $t:X$ in a context $[x_1:X_1, \dots , x_n:X_n]$ is interpreted as a morphism $t\colon X_1\times \dots \times X_n \to X$ in $\mathcal {E}$ in the standard way. For any morphism $\varphi \colon X\to \Omega $ , we denote its corresponding subobject by $[\![ \varphi ]\!] \rightarrowtail X$ .

We say that a formula $\varphi $ holds in $\mathcal {E}$ , denoted by $\mathcal {E}\models \varphi $ , if its interpretation is the morphism $\top \colon X_1\times \dots \times X_n \to \Omega $ . This is equivalent to saying that the corresponding subobject $[\![ \varphi ]\!] $ is top in the subobject lattice. This interpretation is sound for the type theory based on equality and, in particular, for intuitionistic logic.

2.2 Other notation

We collect some notation used throughout this article. We often omit the subscript X of the membership relation $\in _{X}$ when it is clear from the context. For any object X, terms t, $s:PX$ , and formula $\varphi $ , we use the following abbreviations:

• • $\forall x\in t. \varphi \ {:}{=}\ \forall x:X. (x\in _{} t \rightarrow \varphi )$ .

• • $t\subseteq s \ {:}{=}\ \forall x\in t. x\in _{} s$ .

• • $\forall u\subseteq t. \varphi \ {:}{=}\ \forall u:PX. (u\subseteq t \rightarrow \varphi )$ .

Unless stated otherwise, $\mathcal {E}$ denotes an arbitrary elementary topos. Given a local operator $j\colon \Omega \to \Omega $ in $\mathcal {E}$ , we write $\mathcal {E}_{j}$ for the associated subtopos and $L_{j}\colon \mathcal {E}\to \mathcal {E}_{j}$ for the associated sheaf functor.

2.3 Arithmetic

In this article, we also consider translations for first-order intuitionistic arithmetic. We here follow the conventions in [Reference Akama, Berardi, Hayashi and Kohlenbach2, Reference Troelstra and van Dalen38]. Let $\mathcal {L}_{\mathrm {Arith}}$ denote the language of arithmetic consisting of a constant $0$ , the successor $\mathrm {s}$ , and function symbols for all primitive recursive functions. Heyting arithmetic $\mathbf {HA}$ is a first-order intuitionistic theory consisting of the successor axiom $\forall x. \lnot (\mathrm {s}(x)=0)$ , defining equations for all primitive recursive functions, and the induction axiom scheme for all $\mathcal {L}_{\mathrm {Arith}}$ -formulas. If an elementary topos $\mathcal {E}$ has a natural numbers object $N = (N, 0\colon 1\to N, \mathrm {s}\colon N\to N)$ , then any $\mathcal {L}_{\mathrm {Arith}}$ -formula $\varphi [\vec {x}]$ can be canonically interpreted as an $\mathcal {L}_{\mathcal {E}}$ -formula whose variables range over N:

$$\begin{align*}\varphi [\vec{x}] \quad\mapsto\quad \varphi:\Omega \quad [\vec{x}:N].\end{align*}$$

We call the $\mathcal {L}_{\mathcal {E}}$ -formula the standard interpretation of $\varphi $ in $\mathcal {E}$ . It is well known that all axioms of $\mathbf {HA}$ hold in $\mathcal {E}$ under this interpretation.

3.1 The j-translation in the internal language

To begin with, we introduce the j-translation in the internal language of a topos. Unlike arguments in locale theory or in proof theory, we emphasize that the internal logic of a topos can formalize quantification ranging over local operators. To this end, we first recall the basics of nucleus and the associated j-translation in locale theory (see, e.g., [Reference Johnstone19]).

Let $H = (H, \land , \lor , \rightarrow , \leq )$ be a locale. A monotone map $j\colon H\to H$ is called a nucleus if it satisfies the following conditions: (1) $a \leq j(a)$ , (2) $jj(a) \leq j(a)$ , and (3) $j(a \land b) = j(a) \land j(b)$ . Note that the third condition can be replaced by $(3)'\ (a \rightarrow b) \leq (j(a)\rightarrow j(b))$ . Each nucleus j on H induces the associated sublocale $H_{j}\ {:}{=}\ \{\, a \in H \mid j(a) = a\,\}$ of j-closed elements. Now, let us define an $\mathcal {L}_{H}$ -formula as a propositional formula over H constructed from $\land $ , $\lor $ , and $\rightarrow $ (this terminology is used only in this section). Then, the j-translation ${\varphi }^{j}$ for an $\mathcal {L}_{H}$ -formula $\varphi $ is defined as follows:

$$\begin{align*}{p}^{j}\ {:}{=}\ jp \text{ if } p \text{ is an atomic } \mathcal{L}_{H}\text{-formula };\end{align*}$$

$$\begin{align*}{(\varphi\land \psi)}^{j}\ {:}{=}\ {\varphi}^{j}\land{\psi}^{j}; \qquad {(\varphi\lor \psi)}^{j}\ {:}{=}\ j({\varphi}^{j}\lor{\psi}^{j}); \qquad {(\varphi\rightarrow \psi)}^{j}\ {:}{=}\ {\varphi}^{j}\rightarrow{\psi}^{j}. \end{align*}$$

This translation provides a uniform way to transform $\mathcal {L}_{H}$ -formulas into $\mathcal {L}_{H_{j}}$ -formulas.

We can apply a similar argument to the subobject classifier $\Omega $ of an elementary topos $\mathcal {E}$ and $\mathcal {L}_{\mathcal {E}}$ -formulas. In a topos $\mathcal {E}$ , $\Omega $ is an internal locale. An endomorphism $j\colon \Omega \to \Omega $ in $\mathcal {E}$ is called a local operator if j is an internal nucleus on $\Omega $ . However, a crucial difference is that the internal language $\mathcal {L}_{\mathcal {E}}$ can formalize endomorphisms on $\Omega $ using the power object $P\Omega $ , which is isomorphic to the exponential $\Omega ^{\Omega }$ . That is, we can treat local operators as terms of type $P\Omega $ (note that in a presheaf topos, this data is internally equivalent to a Grothendieck coverage). This treatment enables us to handle not only local operators but also quantification over them in $\mathcal {E}$ .

Remark 3.2. Let $j\colon \Omega \to \Omega $ be an endomorphism in $\mathcal {E}$ , and let $\widehat {j}\colon 1\to P\Omega $ denote its transpose. One can check that j is a local operator in $\mathcal {E}$ if and only if $\mathcal {E}\models (\widehat {j} \in _{} \mathrm {Lop})$ holds. The closed term $\mathrm {Lop}$ naturally induces a subobject of $P\Omega $ :

$$\begin{align*}\mathrm{Lop} = [\![ \mathrm{is}\textrm{-}\mathrm{lop}[j] ]\!] \rightarrowtail P\Omega.\end{align*}$$

This can be regarded as an object of all local operators in $\mathcal {E}$ . In our arguments below, the universal quantification $\forall j\in \mathrm {Lop}.\varphi [j]$ can be read as the universal quantification $\forall j:\mathrm {Lop}. \varphi [j]$ over this object $\mathrm {Lop}$ .

Here, we list some basic facts on nucleus (cf. [Reference van den Berg3, Lemma 1]).

Based on these facts, we also have the following equivalences:

$$\begin{align*}j\forall x:X. (\varphi\rightarrow j\psi) \leftrightarrow \forall x:X. (\varphi\rightarrow j\psi), \quad j\exists x:X. j\varphi \leftrightarrow j\exists x:X.\varphi.\end{align*}$$

For example, [Reference van den Berg3] studies a j-translation for first-order formulas. For simplicity, we restrict our attention to one-sorted first-order formulas.

Definition 3.4 ( $\mathcal {L}_{X}$ -formula)

Let X be an object in a topos $\mathcal {E}$ . An $\mathcal {L}_{X}$ -formula is defined inductively as follows:

$$\begin{align*}\varphi, \psi \ {:}{:}{=}\ R[\vec{x}] \mid \varphi\land\psi \mid \varphi\lor\psi \mid \varphi\rightarrow\psi \mid \exists x:X. \varphi \mid \forall x:X. \varphi,\end{align*}$$

where R is a morphism from $X^{m}$ to $\Omega $ in $\mathcal {E}$ , and m is the length of $\vec {x}$ . Here, $\bot $ is also considered an $\mathcal {L}_{X}$ -formula, and $\lnot \varphi $ stands for $\varphi \rightarrow \bot $ .

In other words, an $\mathcal {L}_{X}$ -formula is an $\mathcal {L}_{\mathcal {E}}$ -formula whose atomic formulas are given by morphisms $R\colon X^{m}\to \Omega $ in $\mathcal {E}$ and whose variables range over X. For instance, if $\mathcal {E}$ has a natural numbers object N, the standard interpretation (see Section 2.3) of each $\mathcal {L}_{\mathrm {Arith}}$ -formula is an $\mathcal {L}_N$ -formula.

Then, the j-translation for $\mathcal {L}_{X}$ -formulas is defined internally as follows. Note that j in the following definition is a variable of type $P\Omega $ intended to represent an internal local operator.

Definition 3.5. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ , we inductively define ${\varphi }^{*}$ as follows:

$$\begin{align*}\begin{aligned} {(R[\vec{x}])}^{*} &\ {:}{=}\ jR[\vec{x}]; \\ {(\varphi\land\psi)}^{*} &\ {:}{=}\ {\varphi}^{*}\land {\psi}^{*}; \\ {(\varphi\lor\psi)}^{*} &\ {:}{=}\ j({\varphi}^{*}\lor {\psi}^{*}); \\ {(\varphi\rightarrow\psi)}^{*} &\ {:}{=}\ {\varphi}^{*}\rightarrow {\psi}^{*}; \\ {(\exists y:X. \varphi[\vec{x}, y])}^{*} &\ {:}{=}\ j(\exists y:X. {\varphi}^{*}[j, \vec{x}, y]); \\ {(\forall y:X. \varphi[\vec{x}, y])}^{*} &\ {:}{=}\ \forall y:X. {\varphi}^{*}[j, \vec{x}, y]. \end{aligned}\end{align*}$$

We call ${\varphi }^{*}$ the (internal) j-translation of $\varphi $ :

$$\begin{align*}\varphi:\Omega \quad [\vec{x}:X] \quad\mapsto\quad {\varphi}^{*}:\Omega \quad [j:P\Omega, \vec{x}:X].\end{align*}$$

In addition, given a local operator $j\colon \Omega \to \Omega $ in $\mathcal {E}$ , we write ${\varphi }^{j}$ for ${\varphi }^{*}[\widehat {j}, \vec {x}]$ , which is obtained by substituting the transpose $\widehat {j}\colon 1\to P\Omega $ into ${\varphi }^{*}$ .

3.2 Relationship to the associated subtopos

It is well known that for any topos $\mathcal {E}$ , each local operator j induces the associated subtopos $\mathcal {E}_{j}$ of j-sheaves. This is analogous to the associated sublocale in locale theory. Recall that for a locale H, the j-translation transforms an $\mathcal {L}_{H}$ -formula into an $\mathcal {L}_{H_{j}}$ -formula. However, this does not hold for the j-translation of $\mathcal {L}_{X}$ -formulas. Since an object X is not necessarily a j-sheaf, the j-translation ${\varphi }^{j}$ of an $\mathcal {L}_{X}$ -formula $\varphi $ is not an $\mathcal {L}_{\mathcal {E}_{j}}$ -formula in general. Therefore, [Reference Hyland15] defined j-translations that modify not only logical connectives but also the types of variables. For comparison with our j-translation, let us briefly look at the translation based on the associated sheaf functor $L_{j}\colon \mathcal {E} \to \mathcal {E}_{j}$ , introduced as $[\![ \varphi ]\!] _{j}$ in [Reference Hyland15, Section 5].

Definition 3.6. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ and any local operator j in $\mathcal {E}$ , we inductively define ${\varphi }^{L_{j}}$ as follows:

$$\begin{align*}\begin{aligned} {(R[\vec{x}])}^{L_{j}} &\ {:}{=}\ \chi_{L_{j} {[\![ R ]\!] }} [\vec{r}]; \\ {(\varphi\land\psi)}^{L_{j}} &\ {:}{=}\ {\varphi}^{L_{j}}\land {\psi}^{L_{j}}; \\ {(\varphi\lor\psi)}^{L_{j}} &\ {:}{=}\ j({\varphi}^{L_{j}}\lor {\psi}^{L_{j}}); \\ {(\varphi\rightarrow\psi)}^{L_{j}} &\ {:}{=}\ {\varphi}^{L_{j}}\rightarrow {\psi}^{L_{j}}; \\ {(\exists y:X. \varphi[\vec{x}, y])}^{L_{j}} &\ {:}{=}\ j(\exists s:L_{j} {X}. {\varphi}^{L_{j}}[\vec{r}, s]); \\ {(\forall y:X. \varphi[\vec{x}, y])}^{L_{j}} &\ {:}{=}\ \forall s:L_{j} {X}. {\varphi}^{L_{j}}[\vec{r}, s], \end{aligned}\end{align*}$$

where $\chi _{L_{j} {[\![ R ]\!] }}\colon L_{j} {X^{m}}\to \Omega $ denotes the characteristic map of $L_{j} {[\![ R ]\!] }\rightarrowtail L_{j} {X^{m}}$ . We call ${\varphi }^{L_{j}}$ the $L_{j}$ -translation of $\varphi $ :

$$\begin{align*}\varphi:\Omega \quad [\vec{x}:X] \quad\mapsto\quad {\varphi}^{L_{j}}:\Omega \quad [\vec{r}:L_{j} {X}]. \end{align*}$$

The $L_{j}$ -translation provides a uniform way to transform $\mathcal {L}_{X}$ -formulas in $\mathcal {E}$ into $\mathcal {L}_{L_{j} {X}}$ -formulas in $\mathcal {E}_{j}$ . For instance, the $L_{j}$ -translation for specific atomic formulas or $\mathcal {L}_{\mathrm {Arith}}$ -formulas is coherent with the structure of the associated subtopos, as shown below.

Example 3.7. Let us consider an atomic $\mathcal {L}_{X}$ -formula $(f(\vec {x}) =_{X} g(\vec {x}))$ , where $f, g\colon X^{m}\rightarrow X$ are morphisms in $\mathcal {E}$ . Since the associated sheaf functor $L_{j}$ preserves equalizers, its $L_{j}$ -translation coincides with the equality between the morphisms $L_{j} {f}, L_{j} {g}\colon L_{j} {X^{m}}\rightarrow L_{j} {X}$ :

$$\begin{align*}{(f(\vec{x}) =_{X} g(\vec{x}))}^{L_{j}} = (L_{j} {f}(\vec{r}) =_{L_{j} {X}} L_{j} {g}(\vec{r})) \quad [\vec{r}:L_{j} {X}].\end{align*}$$

Example 3.8. Let us consider an $\mathcal {L}_{\mathrm {Arith}}$ -sentence $\varphi $ and its standard interpretation on a natural numbers object in $\mathcal {E}$ . Since the associated sheaf functor $L_{j}$ preserves the natural numbers object, the $L_{j}$ -translation ${\varphi }^{L_{j}}$ corresponds to the standard interpretation of $\varphi $ in $\mathcal {E}_{j}$ . That is, the following equivalence follows from the definitions:

$$\begin{align*}\mathcal{E}\models {\varphi}^{L_{j}} \iff \mathcal{E}_{j}\models \varphi.\end{align*}$$

On the other hand, it can be shown that the $L_{j}$ -translation ${\varphi }^{L_{j}}$ and the j-translation ${\varphi }^{j}$ are equivalent in $\mathcal {E}$ . While this is probably a folklore among topos theorists, we have not found literature where the proof is explicitly written. Therefore, we clarify this fact here. The verification relies on the following lemmas.

The former statement is a basic fact found in various literature. The latter isomorphism is proved in [Reference Caramello6, Proposition 2.3]. In particular, for an atomic $\mathcal {L}_{X}$ -formula R, Lemma 3.9(1) immediately gives the following equality in $\mathrm {Cl}_{j}\mathrm {Sub}_{\mathcal {E}}(X)$ :

$$\begin{align*}\eta_{X}^{-1} ([\![ {R}^{L_{j}} ]\!] ) = \eta_{X}^{-1} (L_{j} {[\![ R ]\!] }) = j[\![ R ]\!] = [\![ {R}^{j} ]\!] .\end{align*}$$

Furthermore, by combining Lemma 3.9(2) with basic calculations for the associated sheaf functor (e.g., [Reference Hyland15, Theorem 5.1(f)] for universal quantification), we can prove the equality above holds for any $\mathcal {L}_{X}$ -formula $\varphi $ . This implies the following equivalence in the internal logic.

Proposition 3.10. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ and any local operator $j\colon \Omega \to \Omega $ in $\mathcal {E}$ , the following equivalence holds:

$$\begin{align*}\mathcal{E}\models \forall \vec{x}:X. ({\varphi}^{L_{j}}[\eta_{X}(x_1), \dots, \eta_{X}(x_{m})] \leftrightarrow {\varphi}^{j}[\vec{x}] ),\end{align*}$$

where $\eta _{X}\colon X \to L_{j} {X}$ is the component of the unit.

In fact, as we will see later in Section 4.2, this equivalence can also be proven directly using the internal logic (see the discussion following Proposition 4.10).

4.1 Lop-frame

There is a standard partial order on local operators. It is well known that this order admits numerous characterizations, such as the reverse inclusion between the associated subtoposes. What is important here is that the order can also be defined in the internal language. We first introduce a formula expressing the standard order on local operators.

Definition 4.1. The formula $j\leq k$ with variables j, $k:P\Omega $ is defined by

$$\begin{align*}j\leq k\ {:}{=}\ \forall p:\Omega. (jp\rightarrow kp). \end{align*}$$

The formula $j\leq k$ defines an internal poset $(P\Omega , \leq )$ in $\mathcal {E}$ , as well as an internal poset $(\mathrm {Lop}, \leq )$ of internal local operators. Thus, each subobject $\mathbb {P}$ of $\mathrm {Lop}$ induces an internal subposet of local operators:

$$\begin{align*}(\mathbb{P}, \leq_{\mathbb{P}}) \rightarrowtail (\mathrm{Lop}, \leq).\end{align*}$$

Definition 4.2. Let $\mathbb {P}$ denote a variable of type $P(P\Omega )$ . We say that $\mathbb {P}$ is a lop-frame Footnote ¹ if the formula $\mathbb {P}\subseteq \mathrm {Lop}$ holds in $\mathcal {E}$ . For any formula $\varphi [k]$ with a free variable $k:P\Omega $ , we use the following abbreviation:

$$\begin{align*}\forall k\geq_{\mathbb{P}} {j}. \varphi[k] \ {:}{=}\ \forall k\in\mathbb{P}. (j\leq k \rightarrow \varphi[k]). \end{align*}$$

Remark 4.3. Similarly to Remark 3.2, the formula $\mathbb {P}\subseteq \mathrm {Lop}$ defines a closed term $\mathrm {LopFrm} \ {:}{=}\ \{\, \mathbb {P}: P(P\Omega ) \mid \mathbb {P}\subseteq \mathrm {Lop} \,\}$ and induces an object $\mathrm {LopFrm}$ of all lop-frames in $\mathcal {E}$ . This object $\mathrm {LopFrm}$ is isomorphic to the power object of $\mathrm {Lop}$ :

$$\begin{align*}\mathrm{LopFrm} = [\![ \mathbb{P}\subseteq\mathrm{Lop} ]\!] \cong P(\mathrm{Lop}) \rightarrowtail P(P\Omega).\end{align*}$$

Therefore, the universal quantification $\forall \mathbb {P}\subseteq \mathrm {Lop}. \varphi [\mathbb {P}]$ can be read as the universal quantification $\forall \mathbb {P}:\mathrm {LopFrm}. \varphi [\mathbb {P}]$ over this object $\mathrm {LopFrm}$ . In Section 5, we will provide an explicit description of the objects $\mathrm {Lop}$ and $\mathrm {LopFrm}$ in the effective topos $\mathcal {E}\textit{ff}$ .

Each lop-frame gives rise to a translation that combines the j-translation with Kripke forcing.

Definition 4.4. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ , we inductively define $j\Vdash _{\mathbb {P}} \varphi [\vec {x}]$ as follows:

$$\begin{align*}\begin{aligned} j\Vdash_{\mathbb{P}} (R[\vec{x}]) &\ {:}{=}\ jR[\vec{x}]; \\ j\Vdash_{\mathbb{P}} (\varphi\land \psi) &\ {:}{=}\ (j\Vdash_{\mathbb{P}} \varphi) \land (j\Vdash_{\mathbb{P}} \psi); \\ j\Vdash_{\mathbb{P}} (\varphi\lor \psi) &\ {:}{=}\ j((j\Vdash_{\mathbb{P}} \varphi) \lor (j\Vdash_{\mathbb{P}} \psi)); \\ j\Vdash_{\mathbb{P}} (\varphi\rightarrow \psi [\vec{x}]) &\ {:}{=}\ \forall k\geq_{\mathbb{P}} {j}. ((k\Vdash_{\mathbb{P}} \varphi [\vec{x}]) \rightarrow (k\Vdash_{\mathbb{P}} \psi [\vec{x}])); \\ j\Vdash_{\mathbb{P}} (\exists y:X.\varphi[\vec{x}, y]) &\ {:}{=}\ j(\exists y:X. j\Vdash_{\mathbb{P}} \varphi[\vec{x}, y]); \\ j\Vdash_{\mathbb{P}} (\forall y:X.\varphi[\vec{x}, y]) &\ {:}{=}\ \forall k \geq_{\mathbb{P}} {j} \forall y:X. k\Vdash_{\mathbb{P}} \varphi[\vec{x}, y]. \end{aligned}\end{align*}$$

$$\begin{align*}\varphi:\Omega \quad[\vec{x}:X] \quad\mapsto\quad j\Vdash_{\mathbb{P}} \varphi:\Omega \quad [\mathbb{P}:P(P\Omega), j:P\Omega, \vec{x}:X]. \end{align*}$$

First, we observe that this translation generalizes the j-translation. In fact, it is straightforward to verify that if j is a maximal element in a lop-frame $\mathbb {P}$ internally, the translation $j\Vdash _{\mathbb {P}}\varphi $ coincides with the j-translation ${\varphi }^{*}[j]$ .

Proposition 4.5. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ ,

$$\begin{align*}\begin{aligned} \mathcal{E}\models \forall&\mathbb{P}\subseteq\mathrm{Lop} \forall j\in\mathrm{Lop}. \\ &(\forall k\geq_{\mathbb{P}} {j}. (j=_{P\Omega} k)) \rightarrow \forall \vec{x}:X. (j\Vdash_{\mathbb{P}} \varphi [\vec{x}] \leftrightarrow {\varphi}^{*}[j, \vec{x}]). \end{aligned}\end{align*}$$

We also verify that j-closedness, a fundamental property of j-translations, holds for our translation as well.

Lemma 4.6 (j-closedness)

For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ ,

$$\begin{align*}\mathcal{E}\models \forall \mathbb{P}\subseteq\mathrm{Lop} \forall j\in\mathrm{Lop} \forall x:X. (j(j\Vdash_{\mathbb{P}}\varphi[\vec{x}]) \leftrightarrow j\Vdash_{\mathbb{P}}\varphi[\vec{x}] ).\end{align*}$$

4.2 Internal Kripke frame

In Section 3.2, we observed that the relationship between the $L_{j}$ -translation ${\varphi }^{L_{j}}$ and the j-translation ${\varphi }^{j}$ . In fact, we can define a variant $j\Vdash _{\mathbb {P}}^{\mathrm {L}}\varphi $ of our translation $j\Vdash _{\mathbb {P}}\varphi $ that corresponds to the $L_{j}$ -translation. This variant gives us a semantic intuition that our translation describes an internal Kripke frame in $\mathcal {E}$ . Although its practical benefit may not be apparent due to the equivalence of the translations, we discuss this variant in detail to prepare for future extensions.

To define this, let us recall the internal construction of the associated sheaf functor $L_{j}\colon \mathcal {E} \to \mathcal {E}_{j}$ found in numerous literature [Reference Johnstone18, Reference MacLane and Moerdijk30, Reference Veit39]. This is referred to as Lawvere’s construction in [Reference Johnstone18, Exercise 3.4]. See the introduction of [Reference Johnstone17] for the history of this construction. The key idea is to define the j-sheafification $L_{j} {X}$ of an object X as a subobject of the power object $PX$ .

Definition 4.7. We define the following $\mathcal {L}_{\mathcal {E}}$ -terms:

$$ \begin{align*} \{\, x\,\}_{X} &\ {:}{=}\ \{\, y:X \mid (y =_{X} x)\,\}:PX \quad [x:X] \\ \eta_{X} [j, u] &\ {:}{=}\ \{\, x:X \mid j(x \in_{X} u)\,\}:PX \quad [j:P\Omega, u:PX] \\ \Lambda_{X} [j, u] &\ {:}{=}\ j( \exists x:X. u=_{PX} \eta_{X} [j, \{\, x\,\}_{X}] ):\Omega \quad [j:P\Omega, u:PX] \\ L_{*}{X} [j] &\ {:}{=}\ \{\, u:PX \mid \Lambda_{X} [j, u] \,\}:P(PX) \quad [j:P\Omega]. \end{align*} $$

Then, for a local operator $j\colon \Omega \to \Omega $ in $\mathcal {E}$ , the j-sheafification $L_{j} {X}$ is given by the subobject $L_{*}{X} [\widehat {j}] = [\![ \Lambda _{X} [\widehat {j}, \cdot ] ]\!] \rightarrowtail PX$ . Moreover, the component $\eta _{X}\colon X \to L_{j} {X}$ of the unit of the geometric inclusion $\mathcal {E}_{j} \hookrightarrow \mathcal {E}$ is the unique morphism such that the following diagram commutes (see, e.g., [Reference Veit39]):

Furthermore, from standard calculations of internal logic, the following lemmas on the term $\eta $ are verified.

In particular, Lemma 4.8(1) implies that for any local operators j, $k\colon \Omega \to \Omega $ with $j\leq k$ , the unit $\eta _{X}^{j, k}\colon L_{j}X \to L_{k}X$ of the geometric inclusion $\mathcal {E}_{k} \hookrightarrow \mathcal {E}_{j}$ is induced by the term $\eta _{X} [\widehat {k}, \cdot ] \colon PX \to PX$ as follows:

This allows us to describe all information on the j-sheafification $L_{j} {X}$ and the unit $\eta _{X}^{j, k}\colon L_{j}X \to L_{k}X$ by embedding them into $PX$ .

Based on this description, it is natural to define a formula $j\Vdash _{\mathbb {P}}^{\mathrm {L}} \varphi $ that intuitively represents a Kripke frame semantics: the order structure is a lop-frame $\mathbb {P}$ , each possible world is $L_{j} {X}$ for $j\in \mathbb {P}$ , each restriction map is $\eta _{X}^{j, k}\colon L_{j}X \to L_{k}X$ , and the logical connectives and the quantifiers are interpreted in $\mathcal {E}_{j}$ :

$$\begin{align*}(\mathbb{P}, \, \leq_{\mathbb{P}}, \, \{\, L_{j} {X} \mid j\in\mathbb{P} \,\}, \, \{\, \eta_{X}^{j, k}\colon L_{j}X \to L_{k}X \mid j\leq k \,\}).\end{align*}$$

Definition 4.9. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ , we inductively define $j\Vdash _{\mathbb {P}}^{\mathrm {L}} \varphi [\vec {u}]$ as follows:

$$\begin{align*}\begin{aligned} j\Vdash_{\mathbb{P}}^{\mathrm{L}} (R[\vec{x}]) &\ {:}{=}\ \forall \vec{x}:X. \left(\left(\bigwedge_{1\leq i\leq m}(x_{i}\in_{X} u_{i})\right) \rightarrow jR[\vec{x}]\right); \\ j\Vdash_{\mathbb{P}}^{\mathrm{L}} (\varphi\land \psi) &\ {:}{=}\ (j\Vdash_{\mathbb{P}}^{\mathrm{L}} \varphi) \land (j\Vdash_{\mathbb{P}}^{\mathrm{L}} \psi); \\ j\Vdash_{\mathbb{P}}^{\mathrm{L}} (\varphi\lor \psi) &\ {:}{=}\ j((j\Vdash_{\mathbb{P}}^{\mathrm{L}} \varphi) \lor (j\Vdash_{\mathbb{P}}^{\mathrm{L}} \psi)); \\ j\Vdash_{\mathbb{P}}^{\mathrm{L}} (\varphi\rightarrow \psi [\vec{x}]) &\ {:}{=}\ \forall k\geq_{\mathbb{P}} {j}. ((k\Vdash_{\mathbb{P}}^{\mathrm{L}} \varphi [\eta_{X} [k, \vec{u}]] ) \rightarrow (k\Vdash_{\mathbb{P}}^{\mathrm{L}} \psi [\eta_{X} [k, \vec{u}]] )); \\ j\Vdash_{\mathbb{P}}^{\mathrm{L}} (\exists y:X.\varphi[\vec{x}, y]) &\ {:}{=}\ j(\exists v\in L_{*}{X} [j]. j\Vdash_{\mathbb{P}}^{\mathrm{L}} \varphi[\vec{u}, v]); \\ j\Vdash_{\mathbb{P}}^{\mathrm{L}} (\forall y:X.\varphi[\vec{x}, y]) &\ {:}{=}\ \forall k \geq_{\mathbb{P}} {j} \forall v\in L_{*}{X} [k]. k\Vdash_{\mathbb{P}}^{\mathrm{L}} \varphi[\eta_{X} [k, \vec{u}], v], \end{aligned}\end{align*}$$

where $[\eta _{X} [k, \vec {u}]]$ denotes $[\eta _{X} [k, u_1], \dots , \eta _{X} [k, u_{m}] ]$ :

$$\begin{align*}\varphi:\Omega \quad[\vec{x}:X] \quad\mapsto\quad j\Vdash_{\mathbb{P}}^{\mathrm{L}} \varphi:\Omega \quad [\mathbb{P}:P(P\Omega), j:P\Omega, \vec{u}:PX]. \end{align*}$$

As expected, this translation is equivalent to our original translation $j\Vdash _{\mathbb {P}}\varphi $ .

Proposition 4.10. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ , the following equivalence holds:

$$\begin{align*}\begin{aligned} \mathcal{E}\models \forall &\mathbb{P}\subseteq\mathrm{Lop} \forall j\in\mathrm{Lop} \\ &\forall \vec{x}:X. ( j\Vdash_{\mathbb{P}}^{\mathrm{L}}\varphi[\eta_{X} [j, \{\, x_{1}\,\}_{X}], \dots, \eta_{X} [j, \{\, x_{m}\,\}_{X}]] \leftrightarrow j\Vdash_{\mathbb{P}}\varphi[\vec{x}] ). \end{aligned}\end{align*}$$

Proof. By induction on the complexity of $\varphi $ . The atomic case follows from Lemma 3.3. The induction steps for $\land $ and $\lor $ are trivial. Let us show the step for existential quantification $\exists y:X. \varphi [x, y]$ . Using Lemma 3.3(4), we have the following equivalence:

$$\begin{align*}\begin{aligned} &j\Vdash_{\mathbb{P}}(\exists y:X. \varphi) [ \eta_{X} [j, \{\, x\,\}_{X}] ] \\ = &j(\exists v:PX. j( \exists y:X. v=_{PX} \eta_{X} [j, \{\, y\,\}_{X}] ) \land j\Vdash_{\mathbb{P}}^{\mathrm{L}} \varphi[\eta_{X} [j, \{\, x\,\}_{X}], v]) \\ \leftrightarrow &j(\exists v:PX. ( \exists y:X. v=_{PX} \eta_{X} [j, \{\, y\,\}_{X}] ) \land j\Vdash_{\mathbb{P}}^{\mathrm{L}} \varphi[\eta_{X} [j, \{\, x\,\}_{X}], v] ) \\ \leftrightarrow &j(\exists y:X. j\Vdash_{\mathbb{P}}^{\mathrm{L}} \varphi[\eta_{X} [j, \{\, x\,\}_{X}], \eta_{X} [j, \{\, y\,\}_{X}]] ). \end{aligned}\end{align*}$$

By the induction hypothesis, the last formula is equivalent to $j\Vdash _{\mathbb {P}} (\exists y:X. \varphi [x, y])$ .

Next, consider the step for universal quantification $\forall y:X. \varphi [x, y]$ . Note that $j\Vdash _{\mathbb {P}}^{\mathrm {L}}\varphi $ is j-closed similarly to Lemma 4.6. Then, by Lemma 4.8(2) and the induction hypothesis, we obtain the following equivalence:

$$\begin{align*}\begin{aligned} &j\Vdash_{\mathbb{P}}^{\mathrm{L}}(\forall y:X. \varphi) [ \eta_{X} [j, \{\, x\,\}_{X}] ] \\ = &\forall k\geq_{\mathbb{P}} {j} \forall v\in L_{*}{X} [k]. k\Vdash_{\mathbb{P}}^{\mathrm{L}}\varphi [ \eta_{X} [k, \eta_{X} [j, \{\, x\,\}_{X}]], v ] \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j} \forall y:X. k\Vdash_{\mathbb{P}}^{\mathrm{L}}\varphi [\eta_{X} [k, \{\, x\,\}_{X}], \eta_{X} [k, \{\, y\,\}_{X}]] \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j} \forall y:X. k\Vdash_{\mathbb{P}}^{\mathrm{L}}\varphi[x, y] \\ = &j\Vdash_{\mathbb{P}}(\forall y:X. \varphi) [x]. \end{aligned}\end{align*}$$

The step for implication $\rightarrow $ can be shown similarly.

Using this proposition, we can give an alternative proof of Proposition 3.10 based on the internal logic.

Proof of Proposition 3.10

Let $j\colon \Omega \to \Omega $ be a local operator, and consider the singleton lop-frame $\mathbb {P} \ {:}{=}\ \{\, \widehat {j} \,\}_{P\Omega }$ . Similarly to Proposition 4.5, we can verify the following equivalence by induction on the complexity of $\varphi $ :

$$\begin{align*}\forall \vec{r}:L_{j} {X}. ( {\varphi}^{L_{j}}[\vec{r}] \leftrightarrow j\Vdash_{\mathbb{P}}^{\mathrm{L}}\varphi [m(r_{1}), \dots, m(r_{m})] ), \end{align*}$$

where $m\colon L_{j} {X} \rightarrowtail PX$ (for the atomic case, note Lemma 3.9(1)). Letting ${r}_{i} \ {:}{=}\ \eta _{X}({x}_{i})$ , we have $m(\eta _{X}(x_{i})) = \eta _{X} [\widehat {j}, \{\, x_{i}\,\}_{X}]$ . Then, by Proposition 4.10, we obtain

$$\begin{align*}\begin{aligned} &{\varphi}^{L_{j}}[\eta_{X}(x_{1}), \dots, \eta_{X}(x_{m})] \\ \leftrightarrow &\widehat{j}\Vdash_{\mathbb{P}}^{\mathrm{L}}\varphi [m(\eta_{X}(x_{1})), \dots, m(\eta_{X}(x_{m}))] \\ \leftrightarrow &\widehat{j}\Vdash_{\mathbb{P}}^{\mathrm{L}}\varphi [\eta_{X} [\widehat{j}, \{\, x_{1}\,\}_{X}], \dots, \eta_{X} [\widehat{j}, \{\, x_{m}\,\}_{X}]] \\ \leftrightarrow &\widehat{j}\Vdash_{\mathbb{P}}\varphi[\vec{x}]. \end{aligned}\end{align*}$$

By Proposition 4.5, the last formula is equivalent to ${\varphi }^{j}[\vec {x}]$ .

4.3 Soundness

We now establish the soundness theorem of our translation for $\mathrm {IQC}$ . First, we observe that our translation satisfies monotonicity, a fundamental property of Kripke models for intuitionistic logic. It is worth noting that the following results do not require the assumption $j\in \mathbb {P}$ , except for Corollaries 4.12 and 4.13.

Lemma 4.11 (Monotonicity)

For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ ,

$$\begin{align*}\begin{aligned} \mathcal{E}\models \forall&\mathbb{P}\subseteq\mathrm{Lop} \forall j\in\mathrm{Lop} \forall k\geq_{\mathbb{P}} {j} \\ &\forall \vec{x}:X. (j\Vdash_{\mathbb{P}}\varphi[\vec{x}] \rightarrow k\Vdash_{\mathbb{P}}\varphi[\vec{x}]). \end{aligned}\end{align*}$$

Furthermore, if $j\in \mathbb {P}$ , monotonicity can be expressed by the following equivalence.

Corollary 4.12. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ ,

$$\begin{align*}\begin{aligned} \mathcal{E}\models \forall&\mathbb{P}\subseteq\mathrm{Lop} \forall j\in\mathbb{P} \\ &\forall \vec{x}:X. (j\Vdash_{\mathbb{P}}\varphi[\vec{x}] \leftrightarrow (\forall k\geq_{\mathbb{P}} {j}. k\Vdash_{\mathbb{P}}\varphi[\vec{x}])). \end{aligned}\end{align*}$$

This corollary implies that our translation behaves analogously to Kripke frame with constant domain.

Corollary 4.13. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ , the following equivalence holds:

$$\begin{align*}\begin{aligned} \mathcal{E}\models \forall&\mathbb{P}\subseteq\mathrm{Lop} \forall j\in\mathbb{P}. \\ &(\forall \vec{x}:X. j\Vdash_{\mathbb{P}} \varphi[\vec{x}]) \leftrightarrow j\Vdash_{\mathbb{P}} (\forall \vec{x}:X. \varphi). \end{aligned}\end{align*}$$

Consequently, assuming $j\in \mathbb {P}$ , the clause for universal quantification in Definition 4.4 admits a simpler formulation given above. With these preparations, we prove the soundness of our translation for the intuitionistic predicate calculus $\mathrm {IQC}$ . Here, we adopt a Hilbert-style axiomatization, often referred to as Gödel’s system [Reference Kohlenbach24, Chapter 3].

Proof. (1) We first verify the axioms.

The translation $j\Vdash _{\mathbb {P}} (\varphi \rightarrow \varphi \lor \psi )$ is expressed as

$$\begin{align*}\forall k\geq_{\mathbb{P}} {j}. ((k\Vdash_{\mathbb{P}} \varphi) \rightarrow k(k\Vdash_{\mathbb{P}} \varphi \lor k\Vdash_{\mathbb{P}} \psi)).\end{align*}$$

Since $\forall p, q:\Omega. (p \rightarrow k(p\lor q))$ holds for any $k\in \mathrm {Lop}$ , the above formula is valid in $\mathcal {E}$ . Similarly, one can easily verify the cases for $\varphi \land \psi \rightarrow \varphi $ , the axioms for contraction $\varphi \lor \varphi \rightarrow \varphi $ and $\varphi \rightarrow \varphi \land \varphi $ , and the axioms for exchange $\varphi \lor \psi \rightarrow \psi \lor \varphi $ and $\varphi \land \psi \rightarrow \psi \land \varphi $ .

By $(k\Vdash _{\mathbb {P}} \bot ) \leftrightarrow k\bot $ and Lemma 4.6, we have the following equivalence:

$$\begin{align*}\begin{aligned} &j\Vdash_{\mathbb{P}} (\bot\rightarrow\varphi) \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j}. (k\bot\rightarrow k\Vdash_{\mathbb{P}} \varphi) \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j}. (\bot\rightarrow k\Vdash_{\mathbb{P}} \varphi). \end{aligned}\end{align*}$$

The last formula follows from ex falso quodlibet in the internal logic of $\mathcal {E}$ .

Note that the translation $j\Vdash _{\mathbb {P}}\varphi [{x}]$ commutes with substitution, that is, $j\Vdash _{\mathbb {P}}(\varphi [t])$ coincides with $j\Vdash _{\mathbb {P}}(\varphi [x]) [t/x]$ . By Corollary 4.13, we obtain the following equivalence:

$$\begin{align*}\begin{aligned} &j\Vdash_{\mathbb{P}}(\forall x:X. \varphi[x]\rightarrow \varphi[t[y]]) \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}}(\forall x:X. \varphi[x]) \rightarrow k\Vdash_{\mathbb{P}}(\varphi[t[y]])) \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j}. ( (\forall x:X. k\Vdash_{\mathbb{P}}\varphi[x]) \rightarrow k\Vdash_{\mathbb{P}}\varphi [t[y]/x]). \end{aligned}\end{align*}$$

The last formula is clearly valid in $\mathcal {E}$ . The axiom $(\varphi [t[\vec {y}]] \rightarrow \exists x:X. \varphi [x])$ is verified similarly.

(2) Next, we verify the inference rules for logical connectives.

By definition, $j\Vdash _{\mathbb {P}} \varphi \land \psi \rightarrow \chi $ is expressed as

$$\begin{align*}\forall k\geq_{\mathbb{P}} {j}. ((k\Vdash_{\mathbb{P}}\varphi) \land (k\Vdash_{\mathbb{P}}\psi) \rightarrow k\Vdash_{\mathbb{P}}\chi).\end{align*}$$

From Lemma 4.11, $k\Vdash _{\mathbb {P}}\varphi $ is equivalent to $\forall \ell \geq _{\mathbb {P}} {k}. (\ell \Vdash _{\mathbb {P}}\varphi )$ . Hence, the above formula is equivalent to

$$\begin{align*}\forall k\geq_{\mathbb{P}} {j} \forall \ell\geq_{\mathbb{P}} {k}. ((k\Vdash_{\mathbb{P}}\varphi \land \ell\Vdash_{\mathbb{P}}\psi) \rightarrow \ell\Vdash_{\mathbb{P}}\chi).\end{align*}$$

This formula is intuitionistically equivalent to

$$\begin{align*}\forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}}\varphi \rightarrow \forall \ell\geq_{\mathbb{P}} {k}. (\ell\Vdash_{\mathbb{P}}\psi \rightarrow \ell\Vdash_{\mathbb{P}}\chi)),\end{align*}$$

which coincides with $j\Vdash _{\mathbb {P}} \varphi \rightarrow (\psi \rightarrow \chi )$ . Similarly, the rules for modus ponens and cut are verified:

Noting that $\forall p,q:\Omega. (p\rightarrow q) \rightarrow (kp\rightarrow kq)$ holds for any $k\in \mathrm {Lop}$ , we can verify the following implication:

$$\begin{align*}\begin{aligned} &j\Vdash_{\mathbb{P}} (\varphi\rightarrow\psi) \\ = &\forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}}\varphi \rightarrow k\Vdash_{\mathbb{P}}\psi) \\ \rightarrow &\forall k\geq_{\mathbb{P}} {j}. ((k\Vdash_{\mathbb{P}}\varphi \lor k\Vdash_{\mathbb{P}}\chi) \rightarrow (k\Vdash_{\mathbb{P}}\psi \lor k\Vdash_{\mathbb{P}}\chi)) \\ \rightarrow &\forall k\geq_{\mathbb{P}} {j}. (k(k\Vdash_{\mathbb{P}}\varphi \lor k\Vdash_{\mathbb{P}}\chi) \rightarrow k(k\Vdash_{\mathbb{P}}\psi \lor k\Vdash_{\mathbb{P}}\chi)) \\ = &\forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}}(\varphi\lor\chi) \rightarrow k\Vdash_{\mathbb{P}}(\psi\lor\chi)). \end{aligned}\end{align*}$$

The last formula is precisely the definition of $j\Vdash _{\mathbb {P}} (\varphi \lor \chi \rightarrow \psi \lor \chi )$ .

(3) Finally, we verify the inference rules for quantifiers. For simplicity, assume that $\psi $ is an $\mathcal {L}_{X}$ -sentence and $\varphi [y]$ is an $\mathcal {L}_{X}$ -formula where y is the only free variable. Note that the implications in (3) are, in fact, equivalences.

By Corollary 4.13, we obtain the following equivalence:

$$\begin{align*}\begin{aligned} &\forall y:X. j\Vdash_{\mathbb{P}} (\psi\rightarrow \varphi[y]) \\ = &\forall y:X \forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}}\psi \rightarrow k\Vdash_{\mathbb{P}} \varphi[y]) \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}}\psi \rightarrow \forall y:X. k\Vdash_{\mathbb{P}} \varphi[y]) \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}}\psi \rightarrow k\Vdash_{\mathbb{P}} (\forall y:X. \varphi)). \end{aligned}\end{align*}$$

The last formula is nothing but $j\Vdash _{\mathbb {P}} (\psi \rightarrow \forall y:X. \varphi )$ .

By applying Lemma 4.6, we have the following equivalence:

$$\begin{align*}\begin{aligned} &\forall y:X. j\Vdash_{\mathbb{P}} (\varphi[y]\rightarrow\psi) \\ = &\forall y:X \forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}}\varphi[y] \rightarrow k\Vdash_{\mathbb{P}}\psi) \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j}. ((\exists y:X. k\Vdash_{\mathbb{P}} \varphi[y] ) \rightarrow k\Vdash_{\mathbb{P}}\psi) \\ \leftrightarrow &\forall k\geq_{\mathbb{P}} {j}. (k(\exists y:X. k\Vdash_{\mathbb{P}} \varphi[y] ) \rightarrow k\Vdash_{\mathbb{P}}\psi) \\ = &\forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}} (\exists y:X. \varphi[y]) \rightarrow k\Vdash_{\mathbb{P}}\psi). \end{aligned}\end{align*}$$

The last formula coincides with the definition of $j\Vdash _{\mathbb {P}}(\exists y:X. \varphi [y] \rightarrow \psi )$ . This completes the proof.

4.4 Heyting arithmetic

We show that our translation is sound for Heyting arithmetic $\mathbf {HA}$ under the standard interpretation on a natural numbers object N. The axioms to be verified consist not only of the induction axiom scheme but also of the universal closures of literals, such as the successor axiom and defining equations for primitive recursive functions. To this end, we first consider a subclass of formulas which includes the latter.

Definition 4.15. Let $\mathcal {R}$ denote the subclass of $\mathcal {L}_{X}$ -formulas generated by the following rules:

$$\begin{align*}\varphi, \psi \ {:}{:}{=}\ R[\vec{x}] \mid \lnot R[\vec{x}] \mid \varphi\land\psi \mid \forall x:X. \varphi. \end{align*}$$

Then the following property holds for any formula in $\mathcal {R}$ .

Proposition 4.16. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ in $\mathcal {R}$ ,

$$\begin{align*}\mathcal{E}\models \forall \vec{x}:X. (\varphi[\vec{x}] \leftrightarrow \forall \mathbb{P}\subseteq\mathrm{Lop} \forall j\in\mathrm{Lop}. j\Vdash_{\mathbb{P}} \varphi[\vec{x}] ).\end{align*}$$

Thus, it suffices to show that the induction axiom is forced. A key fact for this proof is that induction over the natural numbers object holds for arbitrary formula with parameters (the proof is essentially contained in [Reference Lambek and Scott26, Theorem 4.1]).

Theorem 4.17 (Soundness for $\mathbf {HA}$ )

Let $\mathcal {E}$ be an elementary topos with a natural numbers object $(N, 0, \mathrm {s})$ . Let $\varphi $ be an $\mathcal {L}_{\mathrm {Arith}}$ -formula. If $\varphi $ is an axiom of $\mathbf {HA}$ , then the following holds under the standard interpretation on N:

$$\begin{align*}\mathcal{E}\models \forall\mathbb{P}\subseteq\mathrm{Lop} \forall j\in\mathrm{Lop}. j\Vdash_{\mathbb{P}}\varphi.\end{align*}$$

Proof. If $\varphi $ is the successor axiom $\forall x:N. \lnot (\mathrm {s}(x)=_{N}0)$ or a defining equation $\forall \vec {x}:N. (f(\vec {x}) =_{N} g(\vec {x}))$ for a primitive recursive function, the claim follows from Proposition 4.16 and the fact that $\varphi $ holds in $\mathcal {E}$ . It remains to show that the induction axiom scheme:

$$\begin{align*}(\mathrm{Ind}_{\psi}) \ {:}{=}\ \psi[0] \land \forall x:N. (\psi[x]\rightarrow \psi[\mathrm{s}(x)]) \rightarrow \forall x:N.\psi[x].\end{align*}$$

Let $k\in \mathrm {Lop}$ satisfy $j\leq k$ and $k\in \mathbb {P}$ . Since $k\in \mathbb {P}$ , Corollary 4.12 implies that $k\Vdash _{\mathbb {P}}(\psi [0])$ is equivalent to $\forall \ell \geq _{\mathbb {P}} {k}. \ell \Vdash _{\mathbb {P}}\psi [0]$ . Similarly, $k\Vdash _{\mathbb {P}} (\forall x:N. (\psi [x]\rightarrow \psi [\mathrm {s}(x)]))$ is equivalent to

$$\begin{align*}\forall \ell\geq_{\mathbb{P}} {k} \forall x:N. ( \ell\Vdash_{\mathbb{P}}\psi[x] \rightarrow \ell\Vdash_{\mathbb{P}} \psi[\mathrm{s}(x)] ).\end{align*}$$

Since N is a natural numbers object, the induction holds for the formula $\ell \Vdash _{\mathbb {P}}\psi [x]$ . Therefore, we obtain $\forall \ell \geq _{\mathbb {P}} {k} \forall x:X. (\ell \Vdash _{\mathbb {P}}\psi [x])$ from $k\Vdash _{\mathbb {P}}(\psi [0])$ and $k\Vdash _{\mathbb {P}} (\forall x:N. (\psi [x]\rightarrow \psi [\mathrm {s}(x)]))$ . This means the following implication:

$$\begin{align*}\begin{aligned} \forall k\geq_{\mathbb{P}} {j}. &(k\Vdash_{\mathbb{P}}(\psi[0]) \land k\Vdash_{\mathbb{P}} (\forall x:N. (\psi[x]\rightarrow \psi[\mathrm{s}(x)])) \\ &\rightarrow k\Vdash_{\mathbb{P}}(\forall x:N. \psi[x]) ), \end{aligned}\end{align*}$$

which is precisely the definition of $j\Vdash _{\mathbb {P}} (\mathrm {Ind}_{\psi })$ .

4.5 Kuroda-style translation

We conclude this section by pointing out that our translation admits an alternative definition based on the Kuroda-style j-translation. In intuitionistic proof theory, there are several variations of double negation translation, such as the Gödel–Gentzen-style, the Kuroda-style, and the Kolmogorov-style (see, e.g., [Reference Troelstra and van Dalen38, Chapter 2, Section 3]). A similar situation holds for the j-translation. In particular, [Reference van den Berg3] provides a syntactic study of the Kuroda-style j-translation.

While Definition 4.4 is based on the Gödel–Gentzen-style, one can define a variant $j\Vdash _{\mathbb {P}}^{\mathrm {K}}\varphi $ corresponding to the Kuroda-style j-translation:

$$\begin{align*}\begin{aligned} j\Vdash_{\mathbb{P}}^{\mathrm{K}} (R[\vec{x}]) &\ {:}{=}\ R[\vec{x}]; \\ j\Vdash_{\mathbb{P}}^{\mathrm{K}} (\varphi\land \psi) &\ {:}{=}\ (j\Vdash_{\mathbb{P}}^{\mathrm{K}} \varphi) \land (j\Vdash_{\mathbb{P}}^{\mathrm{K}} \psi); \\ j\Vdash_{\mathbb{P}}^{\mathrm{K}} (\varphi\lor \psi) &\ {:}{=}\ (j\Vdash_{\mathbb{P}}^{\mathrm{K}} \varphi) \lor (j\Vdash_{\mathbb{P}}^{\mathrm{K}} \psi); \\ j\Vdash_{\mathbb{P}}^{\mathrm{K}} (\varphi\rightarrow \psi [\vec{x}]) &\ {:}{=}\ \forall k\geq_{\mathbb{P}} {j}. ((k\Vdash_{\mathbb{P}}^{\mathrm{K}} \varphi [\vec{x}]) \rightarrow k(k\Vdash_{\mathbb{P}}^{\mathrm{K}} \psi [\vec{x}])); \\ j\Vdash_{\mathbb{P}}^{\mathrm{K}} (\exists y:X.\varphi[\vec{x}, y]) &\ {:}{=}\ \exists y:X. j\Vdash_{\mathbb{P}}^{\mathrm{K}} \varphi[\vec{x}, y]; \\ j\Vdash_{\mathbb{P}}^{\mathrm{K}} (\forall y:X. \varphi[\vec{x}, y]) &\ {:}{=}\ \forall k \geq_{\mathbb{P}} {j} \forall y:X. k(k\Vdash_{\mathbb{P}}^{\mathrm{K}} \varphi[\vec{x}, y]). \end{aligned}\end{align*}$$

The Kuroda-style translation is then given by $j(j\Vdash _{\mathbb {P}}^{\mathrm {K}}\varphi )$ . As is the case for the usual j-translation, this is indeed equivalent to the original translation.

Proposition 4.18. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ ,

$$\begin{align*}\begin{aligned} \mathcal{E}\models &\forall\mathbb{P}\subseteq\mathrm{Lop} \forall j\in\mathrm{Lop} \\ &\forall \vec{x}:X. (j(j\Vdash_{\mathbb{P}}^{\mathrm{K}}\varphi [\vec{x}]) \leftrightarrow j\Vdash_{\mathbb{P}} \varphi[\vec{x}]). \end{aligned}\end{align*}$$

4.6 A corresponding internal sheaf topos

Benno van den Berg pointed out the existence of a topos corresponding to our translation (private communication). Here, we sketch a candidate for the construction based on discussion with him.

We work in an elementary topos $\mathcal {E}$ . Let $\mathbb {P}\subseteq \mathrm {Lop}$ be a lop-frame, and assume that $j\in \mathbb {P}$ . Then the opposite poset $\mathbb {P}^{\mathrm {op}}$ can be regarded as an internal category in $\mathcal {E}$ , and we can define the internal presheaf topos $\mathbf {PSh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}})$ for $\mathbb {P}^{\mathrm {op}}$ in $\mathcal {E}$ . We consider the following:

$$\begin{align*}\begin{aligned} {\mathbb{P}}\vert_{j} &\ {:}{=}\ \{\, k\in_{} \mathbb{P} \mid j\leq k \,\}; \\ \Omega_{\mathbb{P}}(j) &\ {:}{=}\ \{\, U\subseteq {\mathbb{P}}\vert_{j} \mid \forall k\in U \forall \ell\geq_{\mathbb{P}} {k}. (\ell\in_{} U) \,\}; \\ J_{\mathbb{P}}(j) &\ {:}{=}\ \{\, U \in_{} \Omega_{\mathbb{P}}(j) \mid \forall k\geq_{\mathbb{P}} {j}. j(k\in_{} U) \,\}. \end{aligned}\end{align*}$$

Here, $\Omega _{\mathbb {P}}(j)$ represents the family of all sieves on j in $\mathbb {P}^{\mathrm {op}}$ , and defines the subobject classifier of $\mathbf {PSh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}})$ . Note that ${\mathbb {P}}\vert _{j}$ is the maximal sieve on j. In this setting, we can verify that $(\mathbb {P}^{\mathrm {op}}, J_{\mathbb {P}})$ forms an internal site in $\mathcal {E}$ . This defines the internal sheaf topos $\mathbf {Sh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}}, J_{\mathbb {P}})$ in $\mathcal {E}$ (for details on internal sites and internal sheaf toposes, see [Reference Johnstone20, Section C2.4]).

It can be observed that the internal logic of this topos $\mathbf {Sh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}}, J_{\mathbb {P}})$ corresponds to our translation. First, for $U \in _{} \Omega _{\mathbb {P}}(j)$ , we define $C_{\mathbb {P}}(j) (U)$ as follows:

$$\begin{align*}C_{\mathbb{P}}(j) (U) \ {:}{=}\ \{\, k\in_{} {\mathbb{P}}\vert_{j} \mid j(k\in_{} U) \,\}.\end{align*}$$

This defines a local operator $C_{\mathbb {P}}\colon \Omega _{\mathbb {P}} \to \Omega _{\mathbb {P}}$ corresponding to the Grothendieck coverage $J_{\mathbb {P}}$ . (Indeed, for any $U\in _{} \Omega _{\mathbb {P}}(j)$ , $U \in _{}J_{\mathbb {P}}(j)$ if and only if $C_{\mathbb {P}}(j) (U) = {\mathbb {P}}\vert _{j}$ .) Now, let us look at the structure of the lattice of subterminals in $\mathbf {Sh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}}, J_{\mathbb {P}})$ . Each subterminal $U \rightarrowtail 1$ in $\mathbf {Sh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}}, J_{\mathbb {P}})$ is determined by an upper set U of $\mathbb {P}$ such that $C_{\mathbb {P}}(j)({U}\vert _{j}) = {U}\vert _{j}$ holds for any $j\in \mathbb {P}$ , where ${U}\vert _{j}$ is defined similarly to ${\mathbb {P}}\vert _{j}$ . Therefore, for subterminals U, $V\rightarrowtail 1$ , the join $\lor _{J_{\mathbb {P}}}$ and the Heyting implication $\Rightarrow _{J_{\mathbb {P}}}$ in $\mathbf {Sh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}}, J_{\mathbb {P}})$ are calculated using those $\lor $ and $\Rightarrow $ in $\mathbf {PSh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}})$ : for any $j\in \mathbb {P}$ ,

$$\begin{align*}\begin{aligned} {(U \lor_{J_{\mathbb{P}}} V)}\vert_{j} &= C_{\mathbb{P}}(j) ({U}\vert_{j} \lor {V}\vert_{j}) \\ &= \{\, \ell\in_{} {\mathbb{P}}\vert_{j} \mid j( \ell \in_{} {U}\vert_{j} \lor \ell \in_{} {V}\vert_{j} )\,\} \\ {(U \Rightarrow_{J_{\mathbb{P}}} V)}\vert_{j} &= ({U}\vert_{j} \Rightarrow {V}\vert_{j}) \\ &= \{\, \ell\in_{} {\mathbb{P}}\vert_{j} \mid \forall k\geq_{\mathbb{P}} {j}. ( \ell \in_{} {U}\vert_{k} \rightarrow \ell \in_{} {V}\vert_{k} )\,\}. \end{aligned}\end{align*}$$

These coincide with the clauses for disjunction and implication in Definition 4.2, respectively.

In Section 3.2, we saw that the usual j-translation ${\varphi }^{j}$ is exactly related to the internal logic of the subtopos $\mathcal {E}_{j}$ via the $L_{j}$ -translation (Proposition 3.10). Similarly, we expect that any $\mathcal {L}_{X}$ -sentence $\varphi $ induces a subterminal $[\![ \varphi ]\!] _{J_{\mathbb {P}}} \rightarrowtail 1$ in $\mathbf {Sh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}}, J_{\mathbb {P}})$ , and that $j\Vdash _{\mathbb {P}}\varphi $ in $\mathcal {E}$ describes ${[\![ \varphi ]\!] _{J_{\mathbb {P}}}}\vert _{j}$ in $\mathbf {Sh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}}, J_{\mathbb {P}})$ . Through this correspondence, categorical observations on $\mathbf {Sh}_{\mathcal {E}} (\mathbb {P}^{\mathrm {op}}, J_{\mathbb {P}})$ could also yield the results established in this section, such as the soundness for Heyting arithmetic. However, we leave further investigation of this topos for future work. We will briefly discuss future problems concerning our translation and its relation to this topos in Section 7.

5.1 Preliminaries on $\mathcal {E}\textit{ff}$

We begin by introducing the notation for the effective tripos $X \mapsto (\mathcal {P}(\mathbb {N})^X, \sqsubseteq )$ . We refer readers interested in the basics of the effective topos to the standard text [Reference van Oosten34].

Definition 5.1. We fix a primitive recursive pairing function $\langle -, -\rangle \colon \mathbb {N}^{2}\to \mathbb {N}$ . For natural numbers e and n, we write $e\cdot n$ for the result of applying the e-th partial computable function to n, and write $e\cdot n \downarrow $ if the computation terminates. A $\mathcal {P}(\mathbb {N})$ -valued function $\Phi \colon X\to \mathcal {P}(\mathbb {N})$ on a set X is called a predicate (on X). Given a set X, we define the following logical operations on the set of predicates on X: for any $\Phi (x)$ , $\Psi (x)\colon X\to \mathcal {P}(\mathbb {N})$ ,

$$\begin{align*}\begin{aligned} \Phi\land\Psi (x) &\ {:}{=}\ \{\, \langle n, m\rangle \mid n\in \Phi(x) \text{ and } m\in \Psi(x) \,\}; \\ \Phi\lor\Psi (x) &\ {:}{=}\ \{\, \langle 0, n\rangle \mid n\in \Phi(x) \,\} \cup \{\, \langle 1, m\rangle \mid m\in \Psi(x) \,\}; \\ \Phi\rightarrow\Psi (x) &\ {:}{=}\ \{\, e \mid \forall n\in \Phi(x). (e\cdot n\downarrow \text{ and } e\cdot n\in \Psi(x)) \,\}. \end{aligned}\end{align*}$$

We write $\top (x)\ {:}{=}\ \mathbb {N}$ , $\bot (x)\ {:}{=}\ \emptyset $ , $\lnot \Phi \ {:}{=}\ \Phi \rightarrow \bot $ , and $(\Phi \leftrightarrow \Psi ) \ {:}{=}\ (\Phi \rightarrow \Psi ) \land (\Psi \rightarrow \Phi )$ . The same operations are introduced on $\mathcal {P}(\mathbb {N})$ .

A realizer of $\Phi (x)$ is a natural number contained in $\Phi (x)$ . We say that $\Phi (x)$ is realizable if $\Phi (x)\neq \emptyset $ . We define the preorder predicate $(\Phi \sqsubseteq \Psi ) \ {:}{=}\ \bigcap _{x\in X} (\Phi \rightarrow \Psi ) (x)$ , and the equivalence predicate $(\Phi \equiv \Psi ) \ {:}{=}\ \bigcap _{x\in X} (\Phi \leftrightarrow \Psi ) (x)$ between predicates on X. If $(\Phi \equiv \Psi )$ (resp. $(\Phi \sqsubseteq \Psi )$ ) is realizable, we simply write $\Phi \equiv \Psi $ (resp. $\Phi \sqsubseteq \Psi $ ). We say that $\Phi $ and $\Psi $ are equivalent if $\Phi \equiv \Psi $ .

We next recall the structure of objects in $\mathcal {E}\textit{ff}$ . An object X in $\mathcal {E}\textit{ff}$ is a pair $(|X|, =_{X})$ of a set $|X|$ and a partial equivalence relation $=_{X}\colon |X|\times |X| \to \mathcal {P}(\mathbb {N})$ (see [Reference van Oosten34, Section 3.1]). For instance, the subobject classifier is given by $\Omega \ {:}{=}\ (\mathcal {P}(\mathbb {N}), =_{\Omega })$ with $(p=_{\Omega } q) \ {:}{=}\ (p\leftrightarrow q)$ . The natural numbers object is defined as $N \ {:}{=}\ (\mathbb {N}, =_{N})$ , where $(n =_{N} m) \ {:}{=}\ \{\, n\,\}$ if $n=m$ and $\ {:}{=}\ \emptyset $ otherwise.

Let us clarify the object $\mathrm {Lop}$ of local operators and $\mathrm {LopFrm}$ of lop-frames in $\mathcal {E}\textit{ff}$ . The power object $PX$ of an object $X = (|X|, =_{X})$ in $\mathcal {E}\textit{ff}$ is defined by an object $({\mathcal {P}(\mathbb {N})}^{|X|}, =_{PX})$ of strict relational predicates with respect to $=_{X}$ (see [Reference van Oosten34, p. 70]). Furthermore, if X is a uniform object (such as $\Omega $ or $P\Omega $ ), the strictness condition can be omitted [Reference van Oosten34, Proposition 3.2.6].

Definition 5.2. Let $X = (|X|, =_{X})$ be an object in $\mathcal {E}\textit{ff}$ . We introduce the predicate $\mathrm {Rel}_{=_{X}}$ on $\mathcal {P}(\mathbb {N})^{|X|}$ as follows:

$$\begin{align*}\mathrm{Rel}_{=_{X}}(\Phi) \ {:}{=}\ \bigcap_{x, y\in |X|} (\Phi(x) \land (x=_{X} y) \rightarrow \Phi(y)).\end{align*}$$

We say that a predicate $\Phi $ on $|X|$ is $=_{X}$ -relational if $\mathrm {Rel}_{=_{X}}(\Phi )$ is realizable. Similarly, for $\equiv $ in Definition 5.1, we define the predicate $\mathrm {Rel}_{\equiv }$ and the notion of $\equiv $ -relationality.

Let us recall that $\mathrm {Lop}$ and $\mathrm {LopFrm}$ were defined as subobjects $[\![ \mathrm {is}\textrm {-}\mathrm {lop}[j] ]\!] \rightarrowtail P\Omega $ (Remark 3.2) and $[\![ \mathbb {P}\subseteq \mathrm {Lop} ]\!] \rightarrowtail P(P\Omega )$ (Remark 3.2), respectively. These definitions imply that local operators and lop-frames in $\mathcal {E}\textit{ff}$ correspond to specific predicates, as below.

Definition 5.4. For predicates j, $k\colon \mathcal {P}(\mathbb {N})\to \mathcal {P}(\mathbb {N})$ , we define

$$\begin{align*}\begin{aligned} [\![ \mathrm{is}\textrm{-}\mathrm{lop}[j]]\!] &\ {:}{=}\ \bigcap_{p\subseteq \mathbb{N}} (p \rightarrow j(p)) \land \bigcap_{p\subseteq \mathbb{N}} (jj(p) \rightarrow j(p)) \\ &\land \bigcap_{p, q\subseteq \mathbb{N}} ((p\rightarrow q) \rightarrow (j(p)\rightarrow j(q))), \\ (j =_{\mathrm{Lop}} k) &\ {:}{=}\ [\![ \mathrm{is}\textrm{-}\mathrm{lop}[j]]\!] \land (j \equiv k). \end{aligned}\end{align*}$$

A predicate j on $\mathcal {P}(\mathbb {N})$ is called a local operator in the effective topos if $[\![ \mathrm {is}\textrm {-}\mathrm {lop}[j]]\!] $ is realizable. We write $\mathrm {Lop}(\mathcal {E}\textit{ff})$ for the set of all local operators in $\mathcal {E}\textit{ff}$ . The standard order between local operators is interpreted as $[\![ j\leq k]\!] \ {:}{=}\ (j \sqsubseteq k)$ .

A local operator equivalent to the largest element $\top (p)\ {:}{=}\ \mathbb {N}$ in the preordered set $(\mathrm {Lop}(\mathcal {E}\textit{ff}), \sqsubseteq )$ is called degenerate. In addition, the double negation operator is interpreted as follows: $\lnot \lnot (p) \ {:}{=}\ \mathbb {N}$ if $p\neq \emptyset $ and $\ {:}{=}\ \emptyset $ otherwise. We say that j is dense if $j\sqsubseteq \lnot \lnot $ , and write $\mathrm {DLop}(\mathcal {E}\textit{ff})$ for the set of all dense local operators in $\mathcal {E}\textit{ff}$ .

Definition 5.6. For predicates $\mathbb {P}$ , $\mathbb {Q} \colon \mathcal {P}(\mathbb {N})^{\mathcal {P}(\mathbb {N})} \to \mathcal {P}(\mathbb {N})$ , we define

$$\begin{align*}\begin{aligned} [\![ \mathbb{P}\subseteq\mathrm{Lop}]\!] &\ {:}{=}\ \bigcap_{j\in \mathcal{P}(\mathbb{N})^{\mathcal{P}(\mathbb{N})}} (\mathbb{P}(j) \rightarrow [\![ \mathrm{is}\textrm{-}\mathrm{lop}[j]]\!] ), \\ (\mathbb{P} =_{\mathrm{LopFrm}} \mathbb{Q}) &\ {:}{=}\ [\![ \mathbb{P}\subseteq\mathrm{Lop}]\!] \land \mathrm{Rel}_{\equiv}(\mathbb{P}) \land (\mathbb{P} \equiv \mathbb{Q}). \end{aligned}\end{align*}$$

A predicate $\mathbb {P}$ on $\mathcal {P}(\mathbb {N})^{\mathcal {P}(\mathbb {N})}$ is called a lop-frame in the effective topos if it is $\equiv $ -relational and $[\![ \mathbb {P}\subseteq \mathrm {Lop}]\!] $ is realizable.

In summary, the internal objects $\mathrm {Lop}$ and $\mathrm {LopFrm}$ are given by the following:

$$\begin{align*}\mathrm{Lop} \ {:}{=}\ (\mathcal{P}(\mathbb{N})^{\mathcal{P}(\mathbb{N})}, =_{\mathrm{Lop}}), \quad \mathrm{LopFrm} \ {:}{=}\ (\mathcal{P}(\mathbb{N})^{(\mathcal{P}(\mathbb{N})^{\mathcal{P}(\mathbb{N})})}, =_{\mathrm{LopFrm}}).\end{align*}$$

We conclude this section by noting that each lop-frame in $\mathcal {E}\textit{ff}$ can be constructed as an $\equiv $ -relational predicate on $\mathcal {P}(\mathbb {N})^{\mathcal {P}(\mathbb {N})}$ weighted by $[\![ \mathrm {is}\textrm {-}\mathrm {lop}[j]]\!] $ .

Proposition 5.8. Let $\mathbb {P}\colon \mathcal {P}(\mathbb {N})^{\mathcal {P}(\mathbb {N})}\to \mathcal {P}(\mathbb {N})$ be an $\equiv $ -relational predicate. Then the predicate $\overline {\mathbb {P}}$ defined as follows is a lop-frame in $\mathcal {E}\textit{ff}$ :

$$\begin{align*}\overline{\mathbb{P}}(j) \ {:}{=}\ \mathbb{P}(j) \land [\![ \mathrm{is}\textrm{-}\mathrm{lop}[j]]\!] .\end{align*}$$

Conversely, any lop-frame in $\mathcal {E}\textit{ff}$ is equivalent to a predicate of this form.

5.2 $\mathbb {P}$ -realizability

Given a lop-frame $\mathbb {P}$ and a local operator j in $\mathcal {E}\textit{ff}$ , the translation $j\Vdash _{\mathbb {P}}\varphi $ for an $\mathcal {L}_{\mathrm {Arith}}$ -formula $\varphi [{x}]$ induces a predicate $[\![ {j}\Vdash _{\mathbb {P}} {\varphi } ]\!] \colon \mathbb {N}\to \mathcal {P}(\mathbb {N})$ . Based on the Kuroda-style translation, we provide the following description.

Definition 5.9. Let $\mathbb {P}$ be a lop-frame and j be a local operator in $\mathcal {E}\textit{ff}$ . For an $\mathcal {L}_{\mathrm {Arith}}$ -formula $\varphi [\vec {x}]$ , we inductively define the predicate $[\![ {j}\Vdash _{\mathbb {P}} {\varphi } ]\!] \colon \mathbb {N}^{m}\to \mathcal {P}(\mathbb {N})$ as follows:

$$\begin{align*}\begin{aligned} [\![ {j}\Vdash_{\mathbb{P}} {(f(\vec{x}) = g(\vec{x}))} ]\!] &\ {:}{=}\ \begin{cases} \mathbb{N} & \text{ if } (f(\vec{n}) = g(\vec{n})) \text{ holds in }\mathbb{N} \\ \emptyset & \text{ otherwise; } \end{cases} \\ [\![ {j}\Vdash_{\mathbb{P}} {(\varphi\land \psi)} ]\!] &\ {:}{=}\ [\![ {j}\Vdash_{\mathbb{P}} {\varphi} ]\!] \land [\![ {j}\Vdash_{\mathbb{P}} {\psi} ]\!] ; \\ [\![ {j}\Vdash_{\mathbb{P}} {(\varphi\lor \psi)} ]\!] &\ {:}{=}\ [\![ {j}\Vdash_{\mathbb{P}} {\varphi} ]\!] \lor [\![ {j}\Vdash_{\mathbb{P}} {\psi} ]\!] ; \\ [\![ {j}\Vdash_{\mathbb{P}} {(\varphi\rightarrow \psi)} ]\!] &\ {:}{=}\ \\ \bigcap_{k\in\mathcal{P}(\mathbb{N})^{\mathcal{P}(\mathbb{N})}} &( \mathbb{P}(k)\land [\![ j\leq k]\!] \land [\![ {k}\Vdash_{\mathbb{P}} {\varphi} ]\!] \rightarrow k([\![ {k}\Vdash_{\mathbb{P}} {\psi} ]\!] ) ); \\ [\![ {j}\Vdash_{\mathbb{P}} {(\exists y.\varphi[\vec{x}, y])} ]\!] (\vec{n}) &\ {:}{=}\ \bigcup_{m\in\mathbb{N}} ( \{\, m\,\} \land [\![ {j}\Vdash_{\mathbb{P}} {\varphi} ]\!] (\vec{n}, m) ); \\ [\![ {j}\Vdash_{\mathbb{P}} {(\forall y.\varphi[\vec{x}, y])} ]\!] (\vec{n}) &\ {:}{=}\ \\ \bigcap_{k\in\mathcal{P}(\mathbb{N})^{\mathcal{P}(\mathbb{N})}} \bigcap_{m\in\mathbb{N}} &( \mathbb{P}(k)\land [\![ j\leq k]\!] \land \{\, m\,\} \rightarrow k([\![ {k}\Vdash_{\mathbb{P}} {\varphi} ]\!] (\vec{n}, m)) ). \end{aligned}\end{align*}$$

For an $\mathcal {L}_{\mathrm {Arith}}$ -sentence $\varphi $ , we say that $\varphi $ is $\mathbb {P}$ -realizable at j if $[\![ {j}\Vdash _{\mathbb {P}} {\varphi } ]\!] $ is realizable.

The predicate $[\![ {j}\Vdash _{\mathbb {P}} {\varphi } ]\!] $ corresponds to the subobject induced by the Kuroda-style translation $j\Vdash _{\mathbb {P}}^{\mathrm {K}}\varphi $ defined in Section 4.5. As noted in Remark 5.5, if j is non-degenerate, the following equivalence holds externally:

$$\begin{align*}\mathcal{E}\textit{ff}\models j(j\Vdash_{\mathbb{P}}^{\mathrm{K}}\varphi) \iff j([\![ {j}\Vdash_{\mathbb{P}} {\varphi} ]\!] )\neq\emptyset \iff [\![ {j}\Vdash_{\mathbb{P}} {\varphi} ]\!] \neq\emptyset.\end{align*}$$

Thus, Proposition 4.18 implies that the validity of the Gödel–Gentzen-style translation $j\Vdash _{\mathbb {P}}\varphi $ in $\mathcal {E}\textit{ff}$ coincides with $\mathbb {P}$ -realizability at j as long as j is non-degenerate.

Theorem 5.10. Let $\mathbb {P}$ be a lop-frame and j be a non-degenerate local operator in $\mathcal {E}\textit{ff}$ . Then, for any $\mathcal {L}_{\mathrm {Arith}}$ -formula $\varphi [\vec {x}]$ and any list $\vec {n}$ of natural numbers, the following equivalence holds:

$$\begin{align*}\mathcal{E}\textit{ff}\models (j\Vdash_{\mathbb{P}}(\varphi[\vec{n}])) \iff [\![ {j}\Vdash_{\mathbb{P}} {\varphi} ]\!] (\vec{n}) \neq \emptyset,\end{align*}$$

where $\varphi [\vec {n}]$ denotes the sentence obtained by substituting the numerals $\vec {n}$ into $\varphi $ .

As a corollary of Theorems 4.14 and 4.17, $\mathbb {P}$ -realizability is sound for Heyting arithmetic. Furthermore, recalling Corollary 4.13, we can simplify the clause for universal quantification if $\mathbb {P}(j) = [\![ j\in _{} \mathbb {P}]\!] $ is realizable.

Corollary 5.11. Suppose that a lop-frame $\mathbb {P}$ and a non-degenerate local operator j in $\mathcal {E}\textit{ff}$ satisfy $\mathbb {P}(j)\neq \emptyset $ . Then, for any $\mathcal {L}_{\mathrm {Arith}}$ -formula $\varphi [{y}]$ , the following equivalence holds:

$$\begin{align*}[\![ {j}\Vdash_{\mathbb{P}} {(\forall {y}. \varphi[{y}])} ]\!] \equiv \bigcap_{m\in\mathbb{N}} (\{\, m\,\} \rightarrow j([\![ {j}\Vdash_{\mathbb{P}} {\varphi} ]\!] ({m}))). \end{align*}$$

Observe that the usual j-translation ${\varphi }^{j}$ also corresponds to the predicate $[\![ {\varphi }^{j} ]\!] \colon \mathbb {N}^{m}\to \mathcal {P}(\mathbb {N})$ defined by

$$\begin{align*}[\![ {(\varphi\rightarrow \psi)}^{j} ]\!] \ {:}{=}\ [\![ {\varphi}^{j} ]\!] \rightarrow j([\![ {\psi}^{j} ]\!] ), \quad [\![ {(\forall {y}. \varphi[{y}])}^{j} ]\!] \ {:}{=}\ \bigcap_{m\in\mathbb{N}} (\{\, m\,\} \rightarrow j[\![ {\varphi}^{j} ]\!] ({m})).\end{align*}$$

The other steps are defined analogously to Definition 5.9. This predicate is clearly the set of realizers for the j-realizability found in the literature [Reference Kihara22, Reference Lee and van Oosten27, Reference van Oosten35]. Henceforth, we also say that $\varphi $ is j-realizable if $[\![ {\varphi }^{j} ]\!] $ is realizable.

Next, let us consider a simple example of lop-frame. Given a subset $S\subseteq \mathrm {Lop}(\mathcal {E}\textit{ff})$ externally, we can naturally define a lop-frame associated with it.

The primary reason why we call $\mathbb {P}_{S}$ standard is that the internal universal quantification over $\mathbb {P}_{S}$ corresponds to the external universal quantification over S, as shown below. The same applies to the property that S is a subset of dense local operators.

Proof. We show (1). By the definition of the standard lop-frame $\mathbb {P}_{S}$ , the left-hand side is equivalent to

$$\begin{align*}\bigcap_{k\in \mathcal{P}(\mathbb{N})^{\mathcal{P}(\mathbb{N})}} \bigcap_{\ell \in S} ((\ell \equiv k) \rightarrow ([\![ \mathrm{is}\textrm{-}\mathrm{lop}[k]]\!] \land [\![ j\leq k]\!] \rightarrow \Phi(k))).\end{align*}$$

Note that $[\![ j\leq k]\!] $ , $[\![ \mathrm {is}\textrm {-}\mathrm {lop}[k]]\!] $ , and $\Phi (k)$ are $\equiv $ -relational. Using the fact $((\bigcup _{x} \Psi (x)) \rightarrow p) = \bigcap _{x} (\Psi (x) \rightarrow p)$ , the above predicate is also equivalent to

$$\begin{align*}\bigcap_{\ell \in S} ( (\bigcup_{k\in \mathcal{P}(\mathbb{N})^{\mathcal{P}(\mathbb{N})}} (\ell \equiv k) ) \rightarrow ([\![ \mathrm{is}\textrm{-}\mathrm{lop}[\ell]]\!] \land [\![ j\leq \ell]\!] \rightarrow \Phi(\ell)) ).\end{align*}$$

Since $\bigcup _{k} (\ell \equiv k)$ contains a code for the identity function on $\mathbb {N}$ which is independent of $\ell $ , we obtain the right-hand side.

For (2), if $\ell $ is a dense operator, the claim follows from the fact that $[\![ \ell \leq \lnot \lnot ]\!] $ contains a code for the identity function on $\mathbb {N}$ .

Moreover, assuming that S is uniform, the equivalence in Lemma 5.13(1) can be simplified. In addition, maximality and minimumness are also characterized.

Consequently, for a uniform subset S, the clause for implication in Definition 5.9 admits a simpler form. Also, it follows from Lemma 5.14(2) and Proposition 4.5 that $\mathbb {P}_{S}$ -realizability at a maximal element j in S coincides with j-realizability.

Corollary 5.15. Suppose that $S\subseteq \mathrm {Lop}(\mathcal {E}\textit{ff})$ is uniform. Then, for the standard lop-frame $\mathbb {P}_{S}$ , the following equivalence holds: for any $j\in \mathrm {Lop}(\mathcal {E}\textit{ff})$ and any $\mathcal {L}_{\mathrm {Arith}}$ -formulas $\varphi $ and $\psi ,$

$$\begin{align*}[\![ j\Vdash_{\mathbb{P}_{S}} (\varphi\rightarrow\psi)]\!] \equiv \bigcap_{k \in S\cap\uparrow(j)} ([\![ k\Vdash_{\mathbb{P}_{S}} \varphi]\!] \rightarrow k([\![ k\Vdash_{\mathbb{P}_{S}} \psi]\!] ) ).\end{align*}$$

Furthermore, if j is maximal in S, the equivalence $[\![ j\Vdash _{\mathbb {P}_{S}} \varphi ]\!] \equiv [\![ {\varphi }^{j} ]\!] $ holds.

5.3 De Jongh–Goodman realizability

As mentioned in Section 1, the idea of combining realizability with forcing dates back to de Jongh and Goodman. Their realizability is defined using a partial function on $\mathbb {N}$ as an oracle and a set of partial functions on $\mathbb {N}$ as a forcing poset [Reference Goodman14]. To compare this with our $\mathbb {P}$ -realizability, let us focus on the formulation given in [Reference van Oosten34, Section 4.6.2].

Definition 5.16. Let $\mathrm {PF}$ denote the set of all partial functions on $\mathbb {N}$ , and let $\subseteq $ denote the extension relation on $\mathrm {PF}$ . Let the symbol $\cdot ^{f}$ denote a partial computable application using oracle $f\in \mathrm {PF}$ .

For a subset $T\subseteq \mathrm {PF}$ , a partial function $f\in T$ , a natural number $e\in \mathbb {N}$ , and an $\mathcal {L}_{\mathrm {Arith}}$ -sentence $\varphi $ , we define the relation ${f} \Vdash _{T} {e} \mathrel {\mathbf {r}} \varphi $ inductively as follows:

$$\begin{align*}\begin{aligned} {f} \Vdash_{T} {e} \mathrel{\mathbf{r}} (\varphi\rightarrow\psi) &\stackrel{\text{def}}{\Longleftrightarrow} \forall g\in T \forall n\in\mathbb{N}. \\ &(f \subseteq g \text{ and } {g} \Vdash_{T} {n} \mathrel{\mathbf{r}}\varphi \implies e \cdot^{g} n \downarrow \text{ and } {g} \Vdash_{T} {(e \cdot^{g} n)} \mathrel{\mathbf{r}}\psi), \\ {f} \Vdash_{T} {e} \mathrel{\mathbf{r}} (\forall x. \varphi[x]) &\stackrel{\text{def}}{\Longleftrightarrow} \forall g\in T \forall n\in\mathbb{N}. \\ &(f \subseteq g \implies e \cdot^{g} n \downarrow \text{ and } {g} \Vdash_{T} {(e \cdot^{g} n)} \mathrel{\mathbf{r}} \varphi[n] ). \end{aligned}\end{align*}$$

The other clauses are defined similarly to Kleene realizability relative to f.

It should be noted that this definition is based on Kripke forcing and differs from the definition introduced by Goodman [Reference Goodman14]. However, as pointed out in [Reference van Oosten34, Section 4.6.2], the original definition can be obtained by combining this with the double negation operator. Hence the difference is not essential. In fact, we can connect the above realizability with $\mathbb {P}$ -realizability via a uniform construction of local operators that is well understood in categorical realizability and topos theory.

It is well known that in an elementary topos $\mathcal {E}$ , for any subobject $D\rightarrowtail X$ , there exists the least local operator $j_{D}$ which forces D dense. This theorem was first shown by Joyal [Reference Johnstone18, Theorem 3.57]. While various constructions for such a least local operator are known, we recall the method found in [Reference Hyland15, Proposition 16.3] and [Reference Pitts37, Lemma 5.4]. Here, we restrict our attention to the subobject defined by the graph of a partial function f.

Definition 5.17. Given a partial function $f\in \mathrm {PF}$ , we define a predicate $D_{f}(n)\ {:}{=}\ \{\, \langle n, f(n) \rangle \,\}$ on $\mathbb {N}$ ; if $f(n)$ is undefined, let $D_{f}(n)\ {:}{=}\ \emptyset $ . Then the predicates $m_{f}$ and $j_{f}$ are defined as follows:

$$ \begin{align*} m_{f}(p) &\ {:}{=}\ \bigcup_{n\in\mathbb{N}} (D_{f}(n) \rightarrow p), \\ j_{f}(p) &\ {:}{=}\ \bigcap_{q\subseteq\mathbb{N}} ((p\rightarrow q)\land (m_{f}(q)\rightarrow q) \rightarrow q). \end{align*} $$

Our first observation is that a realizer witnessing that $j_{f}$ is a local operator can be obtained uniformly in f.

This uniform construction of local operator provides a bridge to degree theory. We say that f is $\mathrm {LT}$ -reducible to g, denoted by $f \leq _{\mathrm {LT}} g$ , if there exists $e\in \mathbb {N}$ such that $e\cdot ^{g}n \simeq f(n)$ holds for all $n\in \mathbb {N}$ , where $\simeq $ denotes the Kleene equality. (We adopt this terminology from [Reference Kihara21, Definition 2.14]. Although this definition differs from the original one, the equivalence is easily verified.) When f and g are characteristic functions of subsets of $\mathbb {N}$ , the following equivalences are well known:

1. (1) $j_{f} \sqsubseteq j_{g}$ holds if and only if $f \leq _{\mathrm {LT}} g$ holds (e.g., [Reference Hyland15]).

2. (2) $\varphi $ is $j_{f}$ -realizable if and only if $\varphi $ is Kleene realizable relative to f (e.g., [Reference Phoa36]).

Our second observation is that these two equivalences hold not only for characteristic functions but also for partial functions, and they hold effectively.

Claim (1) is obtained by extending the proof of [Reference Hyland15, Theorem 17.2] to partial functions, and (2) by extending the proof of [Reference Phoa36, Lemma in p. 2]. It is not difficult to verify that these proofs are effective and independent of oracle. Strictly speaking, the original proofs were based not on $j_{f}$ but on the following local operator $j^{\prime }_{f}$ :

$$\begin{align*}j^{\prime}_{f}(p) \ {:}{=}\ \bigcap \{\, q\subseteq \mathbb{N} \mid p\land \{\,\ast\,\} \subseteq q \text{ and } m_{f}(q) \subseteq q \,\},\end{align*}$$

where $\ast \in \mathbb {N}$ is a code of the empty partial function. However, in light of [Reference Pitts37, Proposition 5.6] and our Observation 5.18(1), it is easy to verify that $j_{f}$ and $j^{\prime }_{f}$ are equivalent uniformly in f.

Recently, Kihara provided an excellent framework for understanding the relationship between local operator and oracle [Reference Kihara21, Reference Kihara22]. He introduced the notion of bilayered function, which is a significant generalization of oracle to describe all local operators in $\mathcal {E}\textit{ff}$ . This framework enables us to analyze the order structure of local operators in $\mathcal {E}\textit{ff}$ based on an imperfect information game. In fact, the proof of (1) is essentially contained in [Reference Kihara21, Proposition 2.22 and Theorem 3.1].

Consequently, based on the observations above, we see that de Jongh–Goodman realizability is a special case of $\mathbb {P}$ -realizability under a mild assumption.

Theorem 5.20. Let $T\subseteq \mathrm {PF}$ be a subset satisfying the following assumption $(\mathrm {A})$ :

$$ \begin{align*} \forall f, g\in T. (f\subseteq g \iff f \leq_{\mathrm{LT}} g) \qquad (\mathrm{A}). \end{align*} $$

Then $S_{T}\ {:}{=}\ \{\, j_{f} \mid f\in T\,\}$ is a uniform subset of $\mathrm {Lop}(\mathcal {E}\textit{ff})$ .

Thus, for the standard lop-frame $\mathbb {P}_{T} \ {:}{=}\ \mathbb {P}_{S_{T}}$ , the following equivalence holds: for any partial function $f\in T$ and any $\mathcal {L}_{\mathrm {Arith}}$ -sentence $\varphi $ ,

$$\begin{align*}[\![ j_{f}\Vdash_{\mathbb{P}_{T}} \varphi]\!] \equiv \{\, e\mid {f} \Vdash_{T} {e} \mathrel{\mathbf{r}}\varphi \,\}.\end{align*}$$

Proof. Clearly, there exists a natural number r such that for any f, $g\in \mathrm {PF}$ , r is a code witnessing $f\leq _{\mathrm {LT}} g$ whenever $f \subseteq g$ . That is,

$$\begin{align*}\bigcap_{f \in\mathrm{PF}}\bigcap_{g \in\mathrm{PF} \text{ s.t. } f\subseteq g} (f\leq_{\mathrm{LT}} g) \neq \emptyset.\end{align*}$$

Thus, if T satisfies assumption (A), the uniformity of $S_{T}$ follows from Observations 5.18(2) and 5.19(1).

The latter equivalence can be shown by Corollary 5.15 and Observation 5.19(2).

6.1 Equivalence condition

We begin by discussing the conditions under which our translation $j\Vdash _{\mathbb {P}}\varphi $ is equivalent to the internal j-translation ${\varphi }^{*}[j]$ . In general, this equivalence depends on both the syntactic complexity of $\varphi $ and the structure of the lop-frame $\mathbb {P}$ . In the following, we assume $j\in \mathbb {P}$ for simplicity. For convenience, we introduce a predicate $\mathrm {E}_{\varphi }[\mathbb {P}]$ that expresses the equivalence of these two translations.

Definition 6.1. For an $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ , we define the formula $\mathrm {E}_{\varphi }[\mathbb {P}]$ with a free variable $\mathbb {P}:P(P\Omega )$ as follows:

$$\begin{align*}\mathrm{E}_{\varphi}[\mathbb{P}] \ {:}{=}\ \forall j\in\mathbb{P} \forall \vec{x}:X. (j\Vdash_{\mathbb{P}}\varphi[\vec{x}] \leftrightarrow {\varphi}^{*}[j, \vec{x}]). \end{align*}$$

It is easy to observe that implication-free formulas always satisfy this equivalence.

Proposition 6.2. Let $\varphi [\vec {x}]$ be an implication-free $\mathcal {L}_{X}$ -formula (i.e., a formula containing neither implication $\rightarrow $ nor negation $\lnot $ ). Then,

$$\begin{align*}\mathcal{E}\models \forall \mathbb{P}\subseteq\mathrm{Lop}. \mathrm{E}_{\varphi}[\mathbb{P}].\end{align*}$$

However, non-constructive axioms such as the LEM $\forall \vec {x}:X. \varphi \lor \lnot \varphi $ and the DNE $\forall \vec {x}:X. \lnot \lnot \varphi \rightarrow \varphi $ are not implication-free. Therefore, the equivalence does not hold for them in general. To find the sufficient conditions for these equivalences to hold, we now introduce the following predicates for the internal j-translation.

Definition 6.3. Let $\varphi [\vec {x}]$ be an $\mathcal {L}_{X}$ -formula:

$$\begin{align*}\begin{aligned} \mathrm{M}_{\varphi}[\mathbb{P}]\ {:}{=}\ \forall j\in\mathbb{P} \forall \vec{x}:X. \forall k\geq_{\mathbb{P}} {j}. ({(\varphi)}^{*}[j, \vec{x}] \rightarrow {(\varphi)}^{*}[k, \vec{x}]) \\ \mathrm{N}_{\varphi}[\mathbb{P}]\ {:}{=}\ \forall j\in\mathbb{P} \forall \vec{x}:X. \forall k\geq_{\mathbb{P}} {j}. ({(\varphi)}^{*}[k, \vec{x}] \rightarrow {(\varphi)}^{*}[j, \vec{x}]). \\ \end{aligned}\end{align*}$$

We also define $\lnot _{j}\varphi \ {:}{=}\ \varphi \rightarrow j\bot $ .

Note that ${(\lnot \varphi )}^{*}[j]= \lnot _{j}({\varphi }^{*}[j])$ and $j\Vdash _{\mathbb {P}}(\lnot \varphi ) = \forall k\geq _{\mathbb {P}} {j}.\lnot _{k}(k\Vdash _{\mathbb {P}}\varphi )$ hold. The following lemma summarizes the properties for negated formulas $\lnot \varphi $ and double negated formulas $\lnot \lnot \varphi $ .

Proof. In the following, we fix j, $k\in \mathbb {P}$ with $j\leq k$ and omit the free variables $\vec {x}$ .

For (1), we assume $\mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ and ${(\lnot \varphi )}^{*}[j]$ . Note that $\forall p:\Omega. \lnot _{j}\lnot _{j}\lnot _{j}p \leftrightarrow \lnot _{j}p$ and $\forall p, q:\Omega. (p\rightarrow q) \rightarrow (\lnot _{j}q \rightarrow \lnot _{j}p)$ hold. Then, $\lnot _{j}{(\lnot \lnot \varphi )}^{*}[k]$ follows from $\mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ . Since $\forall p:\Omega. \lnot _{j}p\rightarrow \lnot _{k}p$ , we obtain $\lnot _{k}{(\lnot \lnot \varphi )}^{*}[k]$ , which is equivalent to ${(\lnot \varphi )}^{*}[k]$ . This proves that $\mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ implies ${(\lnot \varphi )}^{*}[j] \rightarrow {(\lnot \varphi )}^{*}[k]$ .

For (2), we assume $\mathrm {E}_{\varphi }[\mathbb {P}]$ and $\mathrm {M}_{\lnot \varphi }[\mathbb {P}]$ . By $\mathrm {M}_{\lnot \varphi }[\mathbb {P}]$ , the formula ${(\lnot \varphi )}^{*}[j]$ is equivalent to $\forall k\geq _{\mathbb {P}} {j}. \lnot _{k} ({\varphi }^{*}[k])$ . It then follows from $\mathrm {E}_{\varphi }[\mathbb {P}]$ that the latter is equivalent to $\forall k\geq _{\mathbb {P}} {j}. \lnot _{k}(k\Vdash _{\mathbb {P}} \varphi )$ , which is also equivalent to $j\Vdash _{\mathbb {P}}\lnot \varphi $ .

For (3), we assume $\mathrm {E}_{\varphi }[\mathbb {P}]$ , $\mathrm {M}_{\lnot \varphi }[\mathbb {P}]$ , and $\mathrm {M}_{\lnot \lnot \varphi }[\mathbb {P}]$ . By (2), the formula $j\Vdash _{\mathbb {P}} \lnot \lnot \varphi $ is equivalent to $\forall k\geq _{\mathbb {P}} {j}. \lnot _{k} {(\lnot \varphi )}^{*}[k]$ . Using the assumption $\mathrm {M}_{\lnot \lnot \varphi }[\mathbb {P}]$ , this becomes equivalent to ${(\lnot \lnot \varphi )}^{*}[j]$ .

To show (4), we assume $\mathrm {E}_{\varphi }[\mathbb {P}]$ , $\mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ , and ${(\lnot \lnot \varphi \rightarrow \varphi )}^{*}[j]$ . First, $\mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ and ${(\lnot \lnot \varphi \rightarrow \varphi )}^{*}[j]$ imply the following implications:

$$\begin{align*}{(\lnot\lnot\varphi)}^{*}[k] \rightarrow {(\lnot\lnot\varphi)}^{*}[j] \rightarrow {(\varphi)}^{*}[j].\end{align*}$$

Using $\mathrm {E}_{\varphi }[\mathbb {P}]$ and Lemma 4.11, ${(\varphi )}^{*}[k]$ follows from ${(\varphi )}^{*}[j]$ . This shows the implication ${(\lnot \lnot \varphi )}^{*}[k] \rightarrow {\varphi }^{*}[k]$ , which is precisely ${(\lnot \lnot \varphi \rightarrow \varphi )}^{*}[k]$ . Therefore, $\mathrm {M}_{\lnot \lnot \varphi \rightarrow \varphi }[\mathbb {P}]$ follows from $\mathrm {E}_{\varphi }[\mathbb {P}]$ and $\mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ .

These lemmas provide sufficient conditions for $\mathrm {E}_{\forall \vec {x}:X. (\varphi \lor \lnot \varphi )}[\mathbb {P}]$ and $\mathrm {E}_{\forall \vec {x}:X. (\lnot \lnot \varphi \rightarrow \varphi )}[\mathbb {P}]$ .

Proof. Claim (1) follows immediately from Corollary 4.13 and Lemma 6.4(2).

We show (2). By Corollary 4.13, $j\Vdash _{\mathbb {P}} \forall \vec {x}:X. (\lnot \lnot \varphi \rightarrow \varphi )$ is equivalent to

$$\begin{align*}\forall \vec{x}:X \forall k\geq_{\mathbb{P}} {j}. (k\Vdash_{\mathbb{P}}\lnot\lnot\varphi [\vec{x}] \rightarrow k\Vdash_{\mathbb{P}} \varphi[\vec{x}] ).\end{align*}$$

We now apply Lemma 6.4(1) and (3). Under the assumptions $\mathrm {E}_{\varphi }[\mathbb {P}]$ , $\mathrm {M}_{\lnot \lnot \varphi }[\mathbb {P}]$ , and $\mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ , the above formula is equivalent to

$$\begin{align*}\forall \vec{x}:X \forall k\geq_{\mathbb{P}} {j}. ({(\lnot\lnot\varphi)}^{*}[k, \vec{x}] \rightarrow {\varphi}^{*}[k, \vec{x}]).\end{align*}$$

By Lemma 6.4(4), the last formula is equivalent to ${(\forall \vec {x}:X. (\lnot \lnot \varphi \rightarrow \varphi ))}^{*}[j]$ .

6.2 Transparency, closedness, and denseness

Lemma 6.4(1) ensures that the condition $\mathrm {E}_{\varphi }[\mathbb {P}]\land \mathrm {M}_{\lnot \lnot \varphi }[\mathbb {P}]\land \mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ suffices to establish both $\mathrm {E}_{\forall \vec {x}:X. (\lnot \lnot \varphi \rightarrow \varphi )}[\mathbb {P}]$ and $\mathrm {E}_{\forall \vec {x}:X. (\varphi \lor \lnot \varphi )}[\mathbb {P}]$ . However, it remains unclear which formulas satisfy $\mathrm {M}_{\lnot \lnot \varphi }[\mathbb {P}]\land \mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ . Here, we reveal that transparency, a notion introduced in the author’s previous study [Reference Nakata, Murano and Silva31], provides a sufficient condition for this property.

The notion of transparency was originally found in the investigation of the least local operator for a given formula [Reference Nakata, Murano and Silva31]. In that study, j-transparency with respect to a local operator j in a topos $\mathcal {E}$ was defined via the associated sheaf functor $L_{j}$ as follows:

$$ \begin{align*} L_{j} {[\![ \varphi ]\!] } = [\![ {\varphi}^{L_{j}} ]\!] \text{ in } \mathrm{Sub}_{\mathcal{E}_{j}}(L_{j} {X}) \quad\quad [j\text{-transparency}]. \end{align*} $$

In other words, a formula $\varphi $ is j-transparent if its $L_{j}$ -translation ${\varphi }^{L_{j}}$ (Definition 3.6) corresponds to the subobject obtained by a single application of $L_{j}$ to $[\![ \varphi ]\!] $ .

Recalling the correspondence observed in Section 3.2, the pullback functor along the unit $\eta _{X}\colon X\to L_{j} {X}$ shows that the equation above is equivalent to $j[\![ \varphi ]\!] = [\![ {\varphi }^{j} ]\!] $ in $\mathrm {Cl}_{j}\mathrm {Sub}_{\mathcal {E}}(X)$ . Thus, j-transparency can be expressed in the internal language as the following equivalence:

$$\begin{align*}\forall \vec{x}:X. (j\varphi[\vec{x}] \leftrightarrow {\varphi}^{j}[\vec{x}]).\end{align*}$$

This property may be seen as an analogue of Glivenko’s theorem for the double negation translation (which states that for any propositional formula $\varphi $ , the translation $\varphi ^{\lnot \lnot }$ is equivalent to $\lnot \lnot \varphi $ in intuitionistic propositional logic; see [Reference Troelstra and van Dalen38]). While [Reference Nakata, Murano and Silva31] utilized this property to discuss the existence of the least local operator for some semi-classical axioms, Proposition 6.11 below shows that transparency, combined with certain conditions, also implies $\mathrm {M}_{\lnot \lnot \varphi }[\mathbb {P}]\land \mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ .

For the sake of generality, let us introduce a formula $\mathrm {Trp}_{\varphi }^{j}[k]$ expressing that $\varphi $ is k-transparent relative to j. We also consider a corresponding closedness condition $\mathrm {Cl}_{\varphi }^{j}[k]$ .

Definition 6.6. For an $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ , we define

$$ \begin{align*} \mathrm{Trp}_{\varphi}^{j}[k] &\ {:}{=}\ \forall \vec{x}:X. (k{\varphi}^{*}[j, \vec{x}] \leftrightarrow {\varphi}^{*}[k, \vec{x}]), \\ \mathrm{Cl}_{\varphi}^{j}[k] &\ {:}{=}\ \forall \vec{x}:X. ({\varphi}^{*}[j, \vec{x}] \leftrightarrow k{\varphi}^{*}[j, \vec{x}]). \end{align*} $$

We first verify that the following closure properties, shown in [Reference Nakata, Murano and Silva31, Lemma 25], also hold in the internal logic.

Proof. Since the other cases can be shown similarly, we only see the case of $\lor $ in (3) and the case of $\rightarrow $ in (4). In the following, we assume that $\mathcal {L}_{X}$ -formulas do not contain free variables.

For the case of $\lor $ in (3), assume that $\mathrm {Trp}_{\varphi }^{j}[k]$ , $\mathrm {Trp}_{\psi }^{j}[k]$ , and $j\leq k$ . Then we have the following equivalences for $k{(\varphi \lor \psi )}^{*}[j]$ :

$$\begin{align*}\begin{aligned} &k{(\varphi\lor\psi)}^{*}[j] = kj ({\varphi}^{*}[j] \lor {\psi}^{*}[j]) \\ \leftrightarrow &k({\varphi}^{*}[j] \lor {\varphi}^{*}[j]) \leftrightarrow k(k{\varphi}^{*}[j] \lor k{\varphi}^{*}[j]). \end{aligned}\end{align*}$$

Since $\mathrm {Trp}_{\varphi }^{j}[k]$ and $\mathrm {Trp}_{\psi }^{j}[k]$ hold, the last formula is equivalent to ${(\varphi \lor \psi )}^{*}[k]$ .

Next, consider the case of $\rightarrow $ in (4). Suppose that $\mathrm {Trp}_{\varphi }^{j}[k]$ , $\mathrm {Trp}_{\psi }^{j}[k]$ , and $\mathrm {Cl}_{\psi }^{j}[k]$ . By $\mathrm {Cl}_{\psi }^{j}[k]$ , we obtain the following equivalence for $k{(\varphi \rightarrow \psi )}^{*}[j]$ :

$$\begin{align*}\begin{aligned} k{(\varphi\rightarrow\psi)}^{*}[j] &= k ({\varphi}^{*}[j] \rightarrow {\psi}^{*}[j]) \\ &\leftrightarrow ( k{\varphi}^{*}[j] \rightarrow k{\psi}^{*}[j]). \end{aligned}\end{align*}$$

Since $\mathrm {Trp}_{\varphi }^{j}[k]$ and $\mathrm {Trp}_{\psi }^{j}[k]$ hold, the last formula is equivalent to ${(\varphi \rightarrow \psi )}^{*}[k]$ .

Lemma 6.7 ensures that under the assumption $(j\leq k)$ , all coherent formulas (i.e., formulas containing only $\land $ , $\lor $ , and $\exists $ ) are k-transparent relative to j. Furthermore, as observed in [Reference Nakata, Murano and Silva31] and essentially in [Reference Caramello5], denseness allows us to extend transparency to a broader class of formulas.

In light of Remarks 4.3 and 6.9, we immediately obtain the following lemma.

Consequently, transparency and denseness can guarantee the condition $\mathrm {M}_{\lnot \lnot \varphi }[\mathbb {P}]\land \mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ as follows.

Proposition 6.11. For any $\mathcal {L}_{X}$ -formula $\varphi [\vec {x}]$ ,

$$\begin{align*}\mathcal{E}\models \forall \mathbb{P}\subseteq\mathrm{DLop} \forall j\in\mathrm{Lop}. ((\forall k\in\mathbb{P}. \mathrm{Trp}_{\varphi}^{j}[k]) \rightarrow \mathrm{M}_{\lnot\lnot\varphi}[\mathbb{P}]\land \mathrm{N}_{\lnot\lnot\varphi}[\mathbb{P}]).\end{align*}$$

Proof. Suppose that $\mathbb {P}\subseteq \mathrm {DLop}$ satisfies the antecedent. For $k\in \mathbb {P}$ , we have the following equivalences:

$$\begin{align*}\begin{aligned} &{(\lnot\lnot\varphi)}^{*}[k] \leftrightarrow \lnot\lnot{\varphi}^{*}[k] \\ \leftrightarrow &\lnot\lnot k{\varphi}^{*}[j] \leftrightarrow \lnot\lnot {\varphi}^{*}[j], \end{aligned}\end{align*}$$

where the first and third equivalences follow from the denseness of k, and the second follows from $\mathrm {Trp}_{\varphi }^{j}[k]$ . Therefore, for any k, $\ell \in \mathbb {P}$ , the equivalence ${(\lnot \lnot \varphi )}^{*}[k] \leftrightarrow \lnot \lnot {\varphi }^{*}[j] \leftrightarrow {(\lnot \lnot \varphi )}^{*}[\ell ]$ holds. This proves $\mathrm {M}_{\lnot \lnot \varphi }[\mathbb {P}]\land \mathrm {N}_{\lnot \lnot \varphi }[\mathbb {P}]$ .

6.3 Semiclassical axioms over HA

We now investigate the equivalence $\mathrm {E}[\mathbb {P}]$ for semi-classical axioms over Heyting arithmetic $\mathbf {HA}$ . Typical examples are the restricted versions of the $\mathbf {DNE}$ and the $\mathbf {LEM}$ , which were systematically investigated in [Reference Akama, Berardi, Hayashi and Kohlenbach2, Reference Fujiwara and Kurahashi12]. We begin by recalling the standard notation.

Definition 6.12. We inductively define the classes $\Sigma _n$ , $\Pi _n$ of $\mathcal {L}_{\mathrm {Arith}}$ -formulas as follows: $\Sigma _0 = \Pi _0$ is the set of all quantifier-free formulas, while $\Sigma _{n+1}$ and $\Pi _{n+1}$ are defined by $\Sigma _{n+1} \ {:}{=}\ \{\, \exists x_1 \dots \exists x_k \varphi \mid \varphi \in \Pi _{n}, \, 0\leq k\,\}$ and $\Pi _{n+1} \ {:}{=}\ \{\, \forall x_1 \dots \forall x_k \varphi \mid \varphi \in \Sigma _{n}, \, 0\leq k\,\}$ . The class $\Pi _n \lor \Pi _n$ denotes the set of formulas of the form $\varphi \lor \psi $ where $\varphi $ , $\psi \in \Pi _n$ . For a class $\Gamma $ of $\mathcal {L}_{\mathrm {Arith}}$ -formulas, the following axiom schemes restricted to $\Gamma $ are defined:

$$ \begin{align*} {\Gamma}\text{-}\mathbf{DNE} &\ {:}{=}\ \{\, \forall \vec{x}. (\lnot\lnot\varphi \rightarrow \varphi) \mid \varphi[\vec{x}] \in \Gamma \,\}, \\ {\Gamma}\text{-}\mathbf{LEM} &\ {:}{=}\ \{\, \forall \vec{x}. (\varphi \lor \lnot\varphi) \mid \varphi[\vec{x}] \in \Gamma \,\}. \end{align*} $$

Since the classes $\Sigma _{n}$ and $\Pi _{n}$ in Definition 6.12 consist of prenex normal formulas, Proposition 6.2 immediately implies the following corollary.

Furthermore, the following lemma can be proven internally. This result is a j-relativized version of [Reference Nakata, Murano and Silva31, Lemma 29].

Proposition 6.15. Let $\mathcal {E}$ be an elementary topos with a natural numbers object. For any natural number n, the following implication holds:

$$\begin{align*}\mathcal{E}\models \forall j, k\in\mathrm{DLop}. ( {({\Sigma_{n}}\text{-}\mathbf{DNE})}^{*}[j] \land (j\leq k) \rightarrow (\mathrm{Trp}_{\Pi_{n+1}}^{j}[k] \land \mathrm{Trp}_{\Sigma_{n+1}}^{j}[k]) ). \end{align*}$$

Our goal has been to characterize the conditions under which a lop-frame $\mathbb {P}$ satisfies $\mathrm {E}[\mathbb {P}]$ for semi-classical axioms over $\mathbf {HA}$ . Combining the results above, we obtain the following sufficient condition.

Theorem 6.16. Let $\mathcal {E}$ be an elementary topos with a natural numbers object and n be a natural number. Suppose that $\Gamma $ is one of the classes $\{\, \Sigma _{n+1}, \Pi _{n+1}, \Pi _{n+1}\lor \Pi _{n+1}, \Sigma _{n+2}\,\}$ and $\mathrm {Ax}$ denote the axiom scheme $\mathbf {DNE}$ or $\mathbf {LEM}$ . Then the following implication holds:

$$\begin{align*}\mathcal{E}\models \forall \mathbb{P}\subseteq\mathrm{DLop} \forall j\in\mathbb{P}. ({({\Sigma_{n}}\text{-}\mathbf{DNE})}^{*}[j] \land \forall k\in\mathbb{P}. (j\leq k) \rightarrow \mathrm{E}_{\Gamma\text{-}\mathrm{Ax}}[\mathbb{P}]).\end{align*}$$

6.4 Separation by $\mathbb {P}$ -realizability

Using the results establishing so far, we now demonstrate a separation proof for semi-classical axioms via $\mathbb {P}$ -realizability. We here emphasize the distinction between our approach and the usual j-realizability. Regarding j-realizability, the following result is well known (see, e.g., [Reference Akama, Berardi, Hayashi and Kohlenbach2]; a more detailed analysis appears in [Reference Nakata, Murano and Silva31, Corollary 47]).

Combining the soundness of j-realizability for $\mathbf {HA}$ , this result implies that $\mathbf {HA} + {\Sigma _{n+1}}\text {-}\mathbf {DNE}$ does not prove ${\Pi _{n+1}\lor \Pi _{n+1}}\text {-}\mathbf {DNE}$ . In this way, j-realizabilities apply to separation problems. Indeed, Kihara [Reference Kihara23] establishes numerous separation results for axioms over intuitionistic set theory $\mathbf {IZF}$ by combining j-realizability with McCarty realizability.

However, the following proposition indicates a limitation of j-realizability regarding the double negated variants of axioms.

Proposition 6.18. For any $\mathcal {L}_{\mathrm {Arith}}$ -sentence $\varphi $ and any local operator j in $\mathcal {E}\textit{ff}$ , the following implication holds externally:

$$\begin{align*}\mathcal{E}\textit{ff} \models {(\lnot\lnot \varphi)}^{j} \implies \mathcal{E}\textit{ff}\models {\varphi}^{j}.\end{align*}$$

This limitation reflects the fact that if j is non-degenerate, the lattice $\mathrm {Sub}_{\mathcal {E}\textit{ff}_{j}}(1)$ of subterminal objects is boolean. In constructive mathematics, the double negated variant $\lnot \lnot T \ {:}{=}\ \{\, \lnot \lnot \varphi \mid \varphi \in T\,\}$ of an axiom scheme T often arises naturally. For instance, [Reference Fujiwara and Kohlenbach10] provides a systematic study on such variants. Despite their importance, Proposition 6.18 shows that j-realizability is not effective for separating these variants.

In contrast, our $\mathbb {P}$ -realizability can separate such double negated variant, as shown below.

Theorem 6.19. For any natural number n, there exists a lop-frame $\mathbb {P}_{n}$ and a local operator $j_{n}$ in $\mathcal {E}\textit{ff}$ such that ${\Sigma _{n+1}}\text {-}\mathbf {DNE} + \lnot \lnot ({\Pi _{n+1}\lor \Pi _{n+1}}\text {-}\mathbf {DNE})$ is $\mathbb {P}_{n}$ -realizable at $j_{n}$ , while ${\Pi _{n+1}\lor \Pi _{n+1}}\text {-}\mathbf {DNE}$ is not. Therefore, the following underivability result holds:

$$\begin{align*}\mathbf{HA} + {\Sigma_{n+1}}\text{-}\mathbf{DNE} + \lnot\lnot({\Pi_{n+1}\lor\Pi_{n+1}}\text{-}\mathbf{DNE}) \not\vdash {\Pi_{n+1}\lor\Pi_{n+1}}\text{-}\mathbf{DNE}.\end{align*}$$

This theorem indicates not only that $\mathbb {P}$ -realizability is useful for separation problems but also that it is a genuine generalization of j-realizability.

Most lemmas required for the proof of Theorem 6.19 have already been established in the previous sections. It remains only to note the following lemma.

Proof. Recall from Lemma 5.13(2) that $\mathcal {E}\textit{ff} \models (\mathbb {P}_{S} \subseteq \mathrm {DLop})$ holds. Then $j\Vdash _{\mathbb {P}_{S}} \lnot \lnot \varphi $ is equivalent to the following formula internally:

$$\begin{align*}\forall k\geq_{\mathbb{P}_{S}} j. \lnot\lnot (\exists \ell\in\mathrm{Lop}. (\ell\in_{}\mathbb{P}_{S} \land k\leq \ell \land \ell\Vdash_{\mathbb{P}_{S}} \varphi) ).\end{align*}$$

Furthermore, since S is uniform, Lemma 5.14(1) implies that $[\![ j\Vdash _{\mathbb {P}_{S}} \lnot \lnot \varphi ]\!] $ is equivalent to the following predicate:

$$\begin{align*}\bigcap_{k\in S \cap\uparrow(j)} \lnot\lnot (\bigcup_{\ell\in S \cap\uparrow(k)} [\![ \ell\Vdash_{\mathbb{P}_{S}} \varphi]\!] ).\end{align*}$$

The assumption on S and j ensures that this last predicate is realizable.

Proof of Theorem 6.19

We define a sequence of partial functions $\{\, f_{n} \,\}_{n\in \mathbb {N}}$ such that each $f_{n}$ has the Turing degree corresponding $\emptyset ^{(n)}$ , and satisfies $f_{n}\subseteq f_{n+1}$ for all n. Let $j_{n}\ {:}{=}\ j_{f_{n}}$ by the construction in Definition 5.17. By the first part of Theorem 5.20, the set $S_{n} \ {:}{=}\ \{\, j_{n}, j_{n+1}\,\}$ forms a uniform subset of $\mathrm {Lop}(\mathcal {E}\textit{ff})$ . Therefore, regarding the standard lop-frame $\mathbb {P}_{n}\ {:}{=}\ \mathbb {P}_{S_{n}}$ for $S_{n}$ , we observe the following:

1. (1) Since $S_{n}\subseteq \mathrm {DLop}(\mathcal {E}\textit{ff})$ , Lemma 5.13(2) implies that $\mathcal {E}\textit{ff}\models \mathbb {P}_{n}\subseteq \mathrm {DLop}$ .

2. (2) Since $j_{n}$ is minimum in $S_{n}$ , Lemma 5.14(3) implies that $\mathcal {E}\textit{ff}\models \forall k\in \mathbb {P}_{n}.$ $(j_{n}\leq k)$ .

3. (3) Furthermore, as we have seen in Example 6.17, $\mathcal {E}\textit{ff}\models {({\Sigma _{n}}\text {-}\mathbf {DNE})}^{*}[j_{n}]$ holds.

Thus, by Theorem 6.16, for any $j\in S_{n}$ and any T in $\{\, {\Sigma _{n+1}}\text {-}\mathbf {DNE},\, \Pi _{n+1}$ $\lor \Pi _{n+1}\text {-}\mathbf {DNE} \,\}$ , the following equivalence holds:

$$\begin{align*}T \text{ is } \mathbb{P}_{n}\text{-realizable at } j \iff T \text{ is } j\text{-realizable}.\end{align*}$$

In particular, by Example 6.17, we obtain that ${\Sigma _{n+1}}\text {-}\mathbf {DNE}$ is $\mathbb {P}_{n}$ -realizable at $j_{n}$ , while ${\Pi _{n+1}\lor \Pi _{n+1}}\text {-}\mathbf {DNE}$ is not. On the other hand, since ${\Pi _{n+1}\lor \Pi _{n+1}}\text {-}\mathbf {DNE}$ is $\mathbb {P}_{n}$ -realizable at $j_{n+1}$ , it follows from Lemma 6.21 that $\lnot \lnot ({\Pi _{n+1}\lor \Pi _{n+1}}\text {-}\mathbf {DNE})$ is $\mathbb {P}_{n}$ -realizable at $j_{n}$ . Thus, combining these with the soundness of $\mathbb {P}$ -realizability for $\mathbf {HA}$ , we obtain the desired separation.