On the independence of premiss axiom and rule

Abstract

In this paper, we deal with a relationship among the law of excluded middle, the double negation elimination and the independence of premiss rule ($\mathrm {IPR}$) for (many-sorted) intuitionistic predicate logic. After giving a general machinery, we give, as corollaries, several examples of extensions of $\mathbf {HA}$ and $\mathbf {HA}^\omega$ which are closed under $\mathrm {IPR}$ but do not derive the independence of premiss axiom.

1 Introduction

It has been proved that intuitionistic first order arithmetic $\mathbf {HA}$ is closed under the independence of premiss rule ($\mathrm {IPR}$)

$$\begin{aligned} \vdash A\rightarrow \exists x B \Longrightarrow \;\vdash \exists x(A\rightarrow B),\; (x\text { not free in }A, A\text { Rasiowa}{-}\text {Harrop}), \end{aligned}$$

for sentence A using, for example, Kleene or Aczel slash relation (cf. [9, Ch.3.5.16]). Troelstra [7, 3.7] showed that $\mathbf {HA}^\omega$ is closed under the following $\mathrm {IPR}^\omega$ in $\mathscr {L}(\mathbf {HA}^\omega )$

$$\begin{aligned} \vdash A\rightarrow \exists x^\sigma B \Longrightarrow \;\vdash \exists x^\sigma (A\rightarrow B),\; (x\text { not free in }A, A \text { Rasiowa}{-}\text {Harrop}), \end{aligned}$$

for negative A using the modified realizability interpretation. In [2], we gave a class $\mathscr {S}$ of schemata such that $\mathbf {HA}+\varLambda$ and $\mathbf {HA}^\omega +\varLambda$ are closed under $\mathrm {IPR}$ and $\mathrm {IPR}^\omega$ whenever $\varLambda$ is a subset of $\mathscr {S}$. If an extension $\mathbf{T}$ of $\mathbf {HA}$ or $\mathbf {HA}^\omega$ derives the independence of premiss axiom

$\mathrm {IP}^{(\omega )}$:

$(A{\rightarrow }\exists x^{(\sigma )} B)\rightarrow \exists x^{(\sigma )}(A{\rightarrow }B)$, (x is not free in A, A Rasiowa–Harrop),

then T is closed under $\mathrm {IPR}^{(\omega )}$. Therefore a natural question arises: What theory $\mathbf{T}$ is closed under $\mathrm {IPR}^{(\omega )}$, but does not derive $\mathrm {IP}^{(\omega )}?$

In this paper, we give several examples of extensions of $\mathbf {HA}$ and $\mathbf {HA}^\omega$ which are closed under $\mathrm {IPR}^{(\omega )}$, but do not derive $\mathrm {IP}^{(\omega )}$. In Sect. 2, we give a general relationship among the law of excluded middle ($\mathrm {LEM}$), the double negation elimination ($\mathrm {DNE}$) and $\mathrm {IPR}$:

if $\mathbf{T}\not \vdash \varGamma \text {-}\mathrm {LEM}$ and $\mathbf{T}\vdash \varGamma \text {-}\mathrm {DNE}$, then $\mathbf{T}$ is not closed under $\mathrm {IPR}$, and hence, in particular, $\mathbf{T}$ does not derive $\mathrm {IP}$,

for a class $\varGamma$ of formulae and a theory $\mathbf{T}$ with a certain property. Using the relationship, we show that $\mathbf {HA}+\varSigma _{n}\text {-}\mathrm {LEM}$ is closed under $\mathrm {IPR}$ but does not derive $\mathrm {IP}$. In Sect. 3, we prove that several extensions of $\mathbf {HA}^\omega$ with non-classical axiom schemata in $\mathscr {S}$ are closed under $\mathrm {IPR}^{\omega }$, but do not derive $\mathrm {IP}^{\omega }$. For that, we show that an extension $\mathbf{S}$ of them is consistent relative to an extension of $\mathbf {EL}$, using two interpretations.

2 A general machinery and non-constructive principles

2.1 A general machinery

We use the standard language of (many-sorted) first-order predicate logic containing $\wedge , \vee , \mathbin {\rightarrow }, \bot , \forall$ and $\exists$ as primitive logical operators. Prime formulae are atomic formulae or $\bot$.

Definition 1

We introduce certain predicate symbols ${\varvec{\nu }}_1, {\varvec{\nu }}_2, {\varvec{\nu }}_3, \ldots$ (being outside of our standard language), called place holders, to deal with schemata as syntactic objects similar to formulae. Schemata are inductively defined by

• 1. a prime formula is a schema;

• 2. if ${\varvec{\nu }}$ is an n-ary place holder and $t_1, \ldots , t_n$ are terms, then ${\varvec{\nu }}(t_1, \ldots , t_n)$ is a schema;

• 3. if ${\varvec{\alpha }}$ and ${\varvec{\beta }}$ are schemata, then ${\varvec{\alpha }} \circ {\varvec{\beta }}$ is a schema for $\circ \in \{ \wedge , \vee , \mathbin {\rightarrow }\}$;

• 4. if ${\varvec{\alpha }}$ is a schema, then $Q x {\varvec{\alpha }}$ is a schema for $Q \in \{ \forall , \exists \}$.

Formulae are schemata without place holders.

For example, the induction schema is given by a schema

$$\begin{aligned} {\varvec{\nu }}(0) \wedge \forall x ({\varvec{\nu }}(x) \mathbin {\rightarrow }{\varvec{\nu }}(Sx)) \mathbin {\rightarrow }\forall x {\varvec{\nu }}(x) , \end{aligned}$$

where ${\varvec{\nu }}$ is a unary place holder and x is a numerical variable, and the axiom of choice $\mathrm {AC}_{\sigma ,\tau }$ is given by a schema

$$\begin{aligned} \forall x^{\sigma }\exists y^{\tau }{\varvec{\nu }}(x,y)\rightarrow \exists z^{\sigma \rightarrow \tau }\forall x^{\sigma }{\varvec{\nu }}(x,zx), \end{aligned}$$

where ${\varvec{\nu }}$ is a binary place holder.

Definition 2

Let ${\varvec{\alpha }}$ be a schema, and let $B_1, \ldots , B_k$ be formulae. Let ${\varvec{\nu }}_1, \ldots , {\varvec{\nu }}_k$ be place holders, and let $\vec {x_1}, \ldots , \vec {x_k}$ be sequences of variables with lengths the arities of ${\varvec{\nu }}_1, \ldots , {\varvec{\nu }}_k$, respectively. Then a schema ${\varvec{\alpha }}[{\varvec{\nu }}_1/\lambda \vec {x_1}. B_1, \ldots , {\varvec{\nu }}_k/\lambda \vec {x_k}. B_k]$ is defined by

• 1. $P[{\varvec{\nu }}_1/\lambda \vec {x_1}. B_1, \ldots , {\varvec{\nu }}_k/\lambda \vec {x_k}. B_k] \equiv P$ for P prime;

• 2. ${\varvec{\nu }}(t_1, \ldots , t_n)[{\varvec{\nu }}_1/\lambda \vec {x_1}. B_1, \ldots , {\varvec{\nu }}_k/\lambda \vec {x_k}. B_k] \equiv B_i[y_1/t_1, \ldots , y_n/t_n]$ if ${\varvec{\nu }} \equiv {\varvec{\nu }}_i$ and $\vec {x_i} \equiv y_1, \ldots , y_n$, and ${\varvec{\nu }}(t_1, \ldots , t_n)$ otherwise;

• 3. $({\varvec{\alpha }} \circ {\varvec{\beta }})[{\varvec{\nu }}_1/\lambda \vec {x_1}. B_1, \ldots ,{\varvec{\nu }}_k/\lambda \vec {x_k}. B_k]\equiv {\varvec{\alpha }}[{\varvec{\nu }}_1/\lambda \vec {x_1}. B_1, \ldots , {\varvec{\nu }}_k/\lambda \vec {x_k}. B_k] \circ {\varvec{\beta }}[{\varvec{\nu }}_1/\lambda \vec {x_1}. B_1, \ldots , {\varvec{\nu }}_k/\lambda \vec {x_k}. B_k]$ for $\circ \in \{ \wedge , \vee , \mathbin {\rightarrow }\}$;

• 4. $(Q x {\varvec{\alpha }})[{\varvec{\nu }}_1/\lambda \vec {x_1}.B_1, \ldots , {\varvec{\nu }}_k/\lambda \vec {x_k}. B_k] \equiv Q x ({\varvec{\alpha }}[{\varvec{\nu }}_1/\lambda \vec {x_1}. B_1, \ldots , {\varvec{\nu }}_k/\lambda \vec {x_k}. B_k])$ for $Q \in \{ \forall , \exists \}$.

We write ${\varvec{\alpha }}[{\varvec{\nu }}_1/B_1, \ldots , {\varvec{\nu }}_k/B_k]$ or ${\varvec{\alpha }}[B_1, \ldots , B_k]$ for ${\varvec{\alpha }}[{\varvec{\nu }}_1/\lambda \vec {x_1}. B_1, \ldots , {\varvec{\nu }}_k/\lambda \vec {x_k}. B_k]$, if it does not cause confusion. An instance of a schema ${\varvec{\alpha }}$ with place holders exactly $\vec {{\varvec{\nu }}}$ is a formula ${\varvec{\alpha }}[\vec {{\varvec{\nu }}}/\vec {B}]$ or ${\varvec{\alpha }}[\vec {B}]$.

Remark 3

For the substitution notation ${\varvec{\alpha }}[\vec {{\varvec{\nu }}}/\vec {B}]$, we shall assume that $\vec {B}$ are free for $\vec {{\varvec{\nu }}}$ in ${\varvec{\alpha }}$, or we assume that a suitable renaming of bound variables is carried out. Here $\lambda \vec {x}. B$ is free for ${\varvec{\nu }}$ in P for prime P; $\lambda \vec {x}. B$ is free for ${\varvec{\nu }}$ in ${\varvec{\nu }}'(t_1,\ldots ,t_n)$; $\lambda \vec {x}. B$ is free for ${\varvec{\nu }}$ in ${\varvec{\alpha }}\circ {\varvec{\beta }}$ if $\lambda \vec {x}. B$ is free for ${\varvec{\nu }}$ in ${\varvec{\alpha }}$ and ${\varvec{\beta }}$; $\lambda \vec {x}. B$ is free for ${\varvec{\nu }}$ in $Qy{\varvec{\alpha }}$ if $y\notin \mathrm {FV}(B){\setminus }\{ \vec {x}\}$ and $\lambda \vec {x}. B$ is free for ${\varvec{\nu }}$ in ${\varvec{\alpha }}$.

For a set $\varLambda$ of schemata and a formula A, we write $\varLambda \vdash A$ to express that a set of instances of schemata in $\varLambda$ derives A.

Definition 4

The class $\mathscr {RH}$ of Rasiowa–Harrop schemata is defined as follows. Let P range over prime formulae, ${\varvec{\eta }}$ and ${\varvec{\eta }}'$ over $\mathscr {RH}$, and ${\varvec{\alpha }}$ over arbitrary schemata. Then $\mathscr {RH}$ is inductively generated by the clause

$$\begin{aligned} P, {\varvec{\eta }} \wedge {\varvec{\eta }}', \forall x {\varvec{\eta }}, {\varvec{\alpha }} \mathbin {\rightarrow }{\varvec{\eta }} \in \mathscr {RH} . \end{aligned}$$

Let $\varGamma$ be a class of formulae. Then non-constructive principles $\varGamma \text {-}\mathrm {IP}$, $\varGamma \text {-}\mathrm {LEM}$ and $\varGamma \text {-}\mathrm {DNE}$ for $\varGamma$ are defined as follows:

$\varGamma \text {-}\mathrm {IP}$:

$(A\rightarrow \exists xB(x))\rightarrow \exists x(A\rightarrow B(x))$, where $A\in \varGamma$, B is any formula and x is not free in A;

$\varGamma \text {-}\mathrm {LEM}$:

$A\vee \lnot A$, where $A\in \varGamma$;

$\varGamma \text {-}\mathrm {DNE}$:

$\lnot \lnot A\rightarrow A$, where $A\in \varGamma$.

Note that $\mathrm {IP}$ explained introduction has the restriction on the formula A to Rasiowa–Harrop, but A in $\varGamma \text {-}\mathrm {IP}$ is not always Rasiowa–Harrop.

In what follows, we assume that a class $\varGamma$ of formulae satisfies the following two conditions:

• 1. $A\in \varGamma \Rightarrow A[x/t]\in \varGamma$ (t must be free for x in A);

• 2. $\exists xA\in \varGamma \Rightarrow \exists yA[x/y]\in \varGamma$ (y must be free for x in A, and $y\equiv x$ or $y\not \in \mathrm {FV}(A)$).

For each class $\varGamma$ of formulae, the class $\exists \varGamma$, $\forall \varGamma$ and $\lnot \varGamma$ consist of formulae of the forms $\exists x A$, $\forall xA$ and $\lnot A$ with a formula A in $\varGamma$, respectively.

Proposition 5

If $\mathbf{T}$ is a theory such that $\mathbf{T}\vdash \varGamma \text {-}\mathrm {LEM}$, then $\mathbf{T}\vdash \varGamma \text {-}\mathrm {IP}$.

Proof

Let A be a formula in $\varGamma$ and B(x) a formula and assume $A\rightarrow \exists xB(x)$. Then $\mathbf{T}$ proves $A\vee \lnot A$. If A, then there is x such that B(x) and so we have $\exists x(A\rightarrow B(x))$. If $\lnot A$, then we have $A\rightarrow B(x)$ for any x and so $\exists x(A\rightarrow B(x))$. Therefore $\mathbf{T}$ proves $\varGamma \text {-}\mathrm {IP}$. $\square$

Theorem 6

If $\mathbf{T}$ is a theory such that $\mathbf{T}\vdash \varGamma \text {-}\mathrm {LEM}$ and $\mathbf{T}\vdash \exists \varGamma \text {-}\mathrm {DNE}$, and that $\mathbf{T}$ is closed under $\mathrm {IPR}$, then $\mathbf{T}\vdash \exists \varGamma \text {-}\mathrm {LEM}$ and $\mathbf{T}\vdash \exists \varGamma \text {-}\mathrm {IP}$.

Proof

Assume that $\mathbf{T}$ is a theory such that $\mathbf{T}\vdash \varGamma \text {-}\mathrm {LEM}$ and $\mathbf{T}\vdash \exists \varGamma \text {-}\mathrm {DNE}$, and that $\mathbf{T}$ is closed under $\mathrm {IPR}$. Then, for each formula A in $\varGamma$, we have $\mathbf{T}\vdash \lnot \lnot \exists x A(x)\rightarrow \exists x A(x)$. Since $\lnot \lnot \exists y A[x/y]$ is Rasiowa–Harrop and $\mathbf{T}$ is closed under $\mathrm {IPR}$, we have $\mathbf{T}\vdash \exists x (\lnot \lnot \exists y A[x/y]\rightarrow A(x))$. Assume that $\lnot \lnot \exists yA[x/y]\rightarrow A(x)$. Since $\mathbf{T}\vdash \varGamma \text {-}\mathrm {LEM}$, we have $A(x)\vee \lnot A(x)$. If A(x), then $\exists x A(x)$; if $\lnot A(x)$, then $\lnot \exists yA[x/y]$. Therefore $\mathbf{T}\vdash \exists x A(x)\vee \lnot \exists x A(x)$. The rest follows from Proposition 5. $\square$

Proposition 7

If $\mathbf{T}$ is a theory such that $\mathbf{T}\vdash \varGamma \text {-}\mathrm {LEM}$, $\mathbf{T}\vdash \exists \varGamma \text {-}\mathrm {DNE}$ and $\mathbf{T}\vdash \lnot \lnot \exists \varGamma \text {-}\mathrm {IP}$, then $\mathbf{T}\vdash \exists \varGamma \text {-}\mathrm {LEM}$.

Proof

This can be proved in a similar way to the above theorem, by using $\lnot \lnot \exists \text {-}\mathrm {IP}$ instead of $\mathrm {IPR}$. $\square$

Corollary 8

Let $\mathbf{T}$ be a theory such that $\mathbf{T}\vdash \varGamma \text {-}\mathrm {LEM}$.

• 1. If $\mathbf{T}\not \vdash \exists \varGamma \text {-}\mathrm {LEM}$ and $\mathbf{T}\vdash \exists \varGamma \text {-}\mathrm {DNE}$, then $\mathbf{T}$ is not closed under $\mathrm {IPR}$. In particular, such $\mathbf{T}$ derives $\varGamma \text {-}\mathrm {IP}$ but neither $\exists \varGamma \text {-}\mathrm {IP}$ nor $\mathrm {IP}$.

• 2. If $\mathbf{T}\not \vdash \exists \varGamma \text {-}\mathrm {LEM}$ and $\mathbf{T}$ is closed under $\mathrm {IPR}$, then $\mathbf{T}\not \vdash \exists \varGamma \text {-}\mathrm {DNE}$.

2.2 Heyting arithmetic and non-constructive principles

In this subsection, we apply the results of the previous subsection to intuitionistic first order arithmetic $\mathbf {HA}$ (cf. [7, 1.3.3–1.3.4] and [9, 3.3.1]) with some non-constructive axioms in [1].

In the language $\mathscr {L}(\mathbf {HA})$ of $\mathbf {HA}$, the class $\varDelta _0$ is the smallest class containing prime formulae and closed under $\wedge$, $\vee$, $\rightarrow$, $\forall x<t$ and $\exists x<t$. The class $\varDelta _0$ is called as well as $\varSigma _0$ or $\varPi _0$. The class $\varSigma _{n+1}$ and $\varPi _{n+1}$ are $\exists \varPi _n$ and $\forall \varSigma _n$, respectively.

Akama et al. [1, $\S 3$] proved the following.

Lemma 9

• 1. $\mathbf {HA}+\varSigma _n\text {-}\mathrm {LEM}\vdash \varSigma _n\text {-}\mathrm {DNE}$;

• 2. $\mathbf {HA}+\varSigma _{n+1}\text {-}\mathrm {DNE}\vdash \varSigma _{n}\text {-}\mathrm {LEM}$;

• 3. $\mathbf {HA}+\varSigma _n\text {-}\mathrm {DNE}\not \vdash \varSigma _n\text {-}\mathrm {LEM}$;

• 4. $\mathbf {HA}+\varSigma _{n}\text {-}\mathrm {LEM}\not \vdash \varSigma _{n+1}\text {-}\mathrm {DNE}$.

As for the relationship between $\mathrm {IP}$ and $\mathrm {DNE}$, we have the following:

Proposition 10

$\mathbf {HA}+\mathrm {IP}\not \vdash \varSigma _1\text {-}\mathrm {DNE}$.

Proof

In [7, 3.4.8 and 3.4.12], a model of $\mathbf {HA}^{\omega }+\mathrm {IP}^{\omega }_{\lnot }+\mathrm {AC}$ in which $\mathrm {MP}_\mathrm{PR}$ does not hold, where $\mathrm {IP}^{\omega }_{\lnot }$ and are schemata

$\mathrm {MP}_\mathrm{PR}$:

$\lnot \lnot \exists xA(x)\rightarrow \exists xA(x)$, for any primitive recursive A;

$\mathrm {IP}^{\omega }_{\lnot }$:

$(\lnot A\rightarrow \exists x^{\sigma }B)\rightarrow \exists x(\lnot A\rightarrow B)$, x is not free in A, $\sigma$ is any type.

Note that we can prove, by induction on the formulae, that each Rasiowa–Harrop formulae in the language of $\mathbf {HA}$ is equivalent to some formula of the form $\lnot A$ which is also Rasiowa–Harrrop. Then each of the axioms of $\mathbf {HA}+\mathrm {IP}$ is interpretable in $\mathbf {HA}^{\omega }+\mathrm {IP}^{\omega }_{\lnot }+\mathrm {AC}$ by a standard way, and so the above model shows that $\mathbf {HA}^{\omega }+\mathrm {IP}$ does not derive $\varSigma _1\text {-}\mathrm {DNE}$. $\square$

By the results of the previous section, we have the following:

Corollary 11

$\mathbf {HA}+\varSigma _{n+1}\text {-}\mathrm {DNE}$ is not closed under $\mathrm {IPR}$.

Proof

Let $\varGamma$ be the class $\varPi _n$. Then $\varGamma \text {-}\mathrm {LEM}$, $\exists \varGamma \text {-}\mathrm {LEM}$ and $\exists \varGamma \text {-}\mathrm {DNE}$ are $\varPi _{n}\text {-}\mathrm {LEM}$, $\varSigma _{n+1}\text {-}\mathrm {LEM}$ and $\varSigma _{n+1}\text {-}\mathrm {DNE}$, respectively. Let $\mathbf{T}$ be $\mathbf {HA}+\varSigma _{n+1}\text {-}\mathrm {DNE}$. Note that $\mathbf {HA}+\varSigma _{n}\text {-}\mathrm {LEM}\vdash \varPi _n\text {-}\mathrm {LEM}$ (cf. [1, Theorem 3.1]). Then, by Lemma 9 (2), we have $\mathbf{T}\vdash \varPi _n\text {-}\mathrm {LEM}$. On the other hand we have $\mathbf{T}\not \vdash \varSigma _{n+1}\text {-}\mathrm {LEM}$ by Lemma 9 (3) and $\mathbf{T}\vdash \varSigma _{n+1}\text {-}\mathrm {DNE}$. By Corollary 8 (1), $\mathbf{T}$ is not closed under $\mathrm {IPR}$. $\square$

Definition 12

The classes $\mathscr {S}$ and $\mathscr {W}$ of schemata are simultaneously defined as follows. Let ${\varvec{\eta }}$ range over $\mathscr {RH}$, ${\varvec{\nu }}$ over expressions ${\varvec{\nu }}_k(t_1 \ldots t_n)$ (${\varvec{\nu }}_k$ an n-ary place holder symbol), ${\varvec{\gamma }}$ and ${\varvec{\gamma }}'$ over $\mathscr {S}$, and ${\varvec{\delta }}$ and ${\varvec{\delta }}'$ over $\mathscr {W}$. Then $\mathscr {S}$ and $\mathscr {W}$ are inductively generated by the clauses

$$\begin{aligned}&{\varvec{\eta }}, {\varvec{\nu }}, {\varvec{\gamma }} \wedge {\varvec{\gamma }}', {\varvec{\gamma }} \vee {\varvec{\gamma }}', \forall x {\varvec{\gamma }}, \exists x {\varvec{\gamma }}, {\varvec{\delta }} \mathbin {\rightarrow }{\varvec{\gamma }} \in \mathscr {S} ; \\&{\varvec{\nu }}, {\varvec{\delta }} \wedge {\varvec{\delta }}', {\varvec{\delta }} \vee {\varvec{\delta }}', \forall x {\varvec{\delta }}, \exists x {\varvec{\delta }}, {\varvec{\gamma }} \mathbin {\rightarrow }{\varvec{\delta }} \in \mathscr {W} . \end{aligned}$$

Proposition 13

If $\varLambda$ is a set of schemata in $\mathscr {S}$, then $\mathbf {HA}+\varLambda$ is closed under $\mathrm {IPR}$.

Proof

See [2, Theorem 3.1]. $\square$

Corollary 14

$\mathbf {HA}+\varSigma _n\text {-}\mathrm {LEM}$ is closed under $\mathrm {IPR}$, but does not derive $\mathrm {IP}$.

Proof

Each instance of $\varSigma _n\text {-}\mathrm {LEM}$ is equivalent to a formula of the form

$$\begin{aligned} \exists x_{n}\forall x_{n-1}\ldots Qx_1(t(x_1,\ldots ,x_{n})=0)\vee \lnot \exists x_{n}\forall x_{n-1}\ldots Qx_1(t(x_1,\ldots ,x_{n})=0), \end{aligned}$$

which is in the class $\mathscr {S}$. Therefore $\mathbf {HA}+\varSigma _n\text {-}\mathrm {LEM}$ is closed under $\mathrm {IPR}$ by Proposition 13. If $\mathbf {HA}+\varSigma _n\text {-}\mathrm {LEM}$ proves $\mathrm {IP}$, then so does $\mathbf {HA}+\varSigma _{n+1}\text {-}\mathrm {DNE}$ by Lemma 9 (2), which is impossible, by Corollary 11. $\square$

Although $\mathbf {HA}+\varSigma _n\text {-}\mathrm {LEM}$ does not prove the full $\mathrm {IP}$, some fragments are provable.

Corollary 15

• 1. $\mathbf {HA}+\varSigma _n\text {-}\mathrm {LEM}\vdash \varSigma _n\text {-}\mathrm {IP}$.

• 2. $\mathbf {HA}+\varSigma _{n+1}\text {-}\mathrm {DNE}\vdash \varSigma _n\text {-}\mathrm {IP}$.

Proof

1 follows from Proposition 5. 2 follows from 2 of Lemma 9 and the above 1.    $\square$

Remark 16

Since the system $\mathbf {HA}+\varSigma _n\text {-}\mathrm {LEM}$ proves full induction, it proves $\varDelta (\varSigma _n)\text {-}\mathrm {LEM}$, where $\varDelta (\varSigma _n)$ is the smallest class containg $\varSigma _n$ and closed under $\wedge$, $\vee$, $\rightarrow$, $\forall x<t$ and $\exists x<t$ (cf. [6, Corollary 84]). Hence $\varSigma _n\text {-}\mathrm {IP}$ can be enhanced as $\varDelta (\varSigma _n)\text {-}\mathrm {IP}$ in the above corollary.

3 Non-classical axioms

In this section, we consider intuitionistic finite type arithmetic $\mathbf {HA}^\omega$, which is called $\mathbf {HA}^\omega _{\rightarrow }$ in [9, Ch.9.1.18] and its extensions with non-classical axioms.

The following schemata are in the class $\mathscr {S}$ (cf. [2, Theorem 3.1]), and so $\mathbf {HA}^\omega$ extended by any subset of them is closed under $\mathrm {IPR}^\omega$.

$\mathrm {FAN}$:

$\forall a^1 \exists x^0 {\varvec{\nu }}(\overline{(a \sqcap 1)}x) \mathbin {\rightarrow }\exists z^0 \forall a^1 \exists y^0 ( y \le z \wedge {\varvec{\nu }}(\overline{(a \sqcap 1)}y) ,$ where $(a \sqcap 1) n \equiv \min \{an,1\};$

$\mathrm {BI}_\mathrm {M}$:

$[ \forall a^1 \exists x^0 {\varvec{\nu }}(\overline{a}x) \wedge \forall y^0 \forall z^0 ({\varvec{\nu }}(y) \mathbin {\rightarrow }{\varvec{\nu }}(y *z)) \wedge \forall y^0 (\forall u^0 {\varvec{\nu }}(y *\langle u \rangle ) \mathbin {\rightarrow }{\varvec{\nu }}(y)) ]$ $\mathbin {\rightarrow }{\varvec{\nu }}(\langle \rangle );$

$\mathrm {AC}_{\sigma ,\tau }$:

$\forall x^\sigma \exists y^\tau {\varvec{\nu }}(x,y) \mathbin {\rightarrow }\exists z^{\sigma \rightarrow \tau } \forall x^\sigma {\varvec{\nu }}(x,zx) ;$

$\mathrm {DC}_\sigma$:

$\forall x^\sigma \exists y^\sigma {\varvec{\nu }}(x,y) \mathbin {\rightarrow }\forall x^\sigma \exists z^{0 \rightarrow \sigma } ( z0 = x \wedge \forall n^0 {\varvec{\nu }}(zn,z(Sn)) ) ;$

$\mathrm {WC}\text {-}\mathrm {N}$:

$\forall a^1 \exists x^0 {\varvec{\nu }}(a,x) \mathbin {\rightarrow }\forall a^1 \exists x^0 \exists y^0 \forall b^1 {\varvec{\nu }}(\overline{a}x *b,y) ;$

$\mathrm {C}\text {-}\mathrm {N}$:

$\forall a^1 \exists x^0 {\varvec{\nu }}(a,x) \mathbin {\rightarrow }\exists c^1 [ c \in K_0 \wedge \forall a^1 \exists y^0 \exists z^0 ( c(\overline{a}y) = z+1 \wedge {\varvec{\nu }}(a,z) ) ] ,$ where $c \in K_0 \mathrel {\Leftrightarrow }\forall a^1 \exists y^0 ( c(\overline{a}y) \ne 0) \wedge \forall y^0 \forall z^0 (cn \ne 0 \mathbin {\rightarrow }cy = c(y *z)) .$

Note that $\mathrm {BI}_\mathrm{M}$ implies $\mathrm {FAN}$ (cf. [3, Ch.I, §6.10]) and $\mathrm {C}\text {-}\mathrm {N}$ implies $\mathrm {WC}\text {-}\mathrm {N}$ (cf. [9, Ch.4.6.8]).

We prove that $\mathbf {HA}^\omega$ with any subset of the above schemata does not derive $\mathrm {IP}^\omega$.

The problem is treated as follows.

Let $\mathrm {MP}$ and $\mathrm {LPO}$ be the following non-constructive principles:

$\mathrm {MP}$:

$\forall a^1(\lnot \lnot \exists x^0(a^1(x)=0)\rightarrow \exists x^0(a(x)=0))$;

$\mathrm {LPO}$:

$\forall a^1(\exists x^0(a^1(x)=0)\vee \lnot \exists x^0(a(x)=0))$.

Note that $\mathrm {MP}$ and $\mathrm {LPO}$ are equivalent to $\exists \varDelta \text {-}\mathrm {DNE}$ and $\exists \varDelta \text {-}\mathrm {LEM}$, respectively, where $\varDelta$ is the class of formulae of the form $t^1(x^0)=0$.

Define a theory $\mathbf{S}$ by

$$\begin{aligned} \mathbf{S}\equiv \mathbf {HA}^\omega +\mathrm {BI}_\mathrm{M}+\mathrm {C}\text {-}\mathrm {N}+\mathrm {AC}+\mathrm {DC}+\mathrm {MP}, \end{aligned}$$

where $\mathrm {AC}\equiv \bigcup _{\sigma ,\tau }\mathrm {AC}_{\sigma ,\tau }$ (cf. [7, 3.4.7]) and $\mathrm {DC}\equiv \bigcup _{\sigma }\mathrm {DC}_\sigma$ (cf. [5, 11.2], where $\mathrm {DC}_\sigma$ is called $\mathrm{DAC}^\sigma$). If we have $\mathbf{S}\not \vdash \mathrm {LPO}$, i.e., $\mathbf{S}\not \vdash \exists \varDelta \text {-}\mathrm {LEM}$ then $\mathbf{S}$ is not closed under $\mathrm {IPR}^\omega$ by Corollary 8 (1), and it does not derive $\mathrm {IP}^\omega$.

To prove that $\mathbf{S}\not \vdash \mathrm {LPO}$, we should note that $\mathrm {C}\text {-}\mathrm {N}$ refutes $\mathrm {LPO}$. In fact, $\mathrm {C}\text {-}\mathrm {N}$ refutes $\forall \text {-}\mathrm {PEM}$ (cf. [9, Ch.4.6.4]), and $\mathrm {LPO}$ implies $\forall \text {-}\mathrm {PEM}$ (cf. [9, Ch.4.3.4, Remark], where $\mathrm {LPO}$ is called $\exists \text {-}\mathrm {PEM}$). Therefore, if $\mathbf{S}$ is consistent, then $\mathbf{S}\not \vdash \mathrm {LPO}$.

Thus the problem is reduced to the consistency of $\mathbf{S}$. We show, using two interpretations, the relative consistency of $\mathbf{S}$ to a definitional extension of the system of elementary analysis $\mathbf {EL}$ (cf. [9, Ch.3.6.2]), whose model can be easily constructed in $\mathbf{ZF}$.

In Sect. 3.1, we give the definition of the system $\mathbf {EL}^*$, a definitional extension of $\mathbf {EL}$, and some properties of it for later use. In Sect. 3.2, we show that $\mathbf{S}$ is consistent relative to $\mathbf {EL}^*+\mathrm {BI}_\mathrm{M}+\mathrm {MP}+\mathrm {GC}$, by a modified version of the interpretation $[\![-]\!] _{\mathrm {ICF}^*}$ defined in [9, Ch.9.1.16]. In Sect. 3.3, we combine it with the functional realizability interpretation, and show that $\mathbf {EL}^*+\mathrm {BI}_\mathrm{M}+\mathrm {MP}+\mathrm {GC}$, and hence $\mathbf{S}$, is consistent relative to $\mathbf {EL}+\mathrm {MP}+\mathrm {BI}_\mathrm{D}$.

We fix a surjective pairing function $(-,-):\mathbb {N}\times \mathbb {N}\rightarrow \mathbb {N}$ and projections $(-)_i:\mathbb {N}\rightarrow \mathbb {N}$ such that $((x)_0, (x)_1)=n$, $((x,y))_0=x$ and $((x,y))_1=y$ for all $x^0$ and $y^0$. For each $\alpha$, we define $(\alpha )_i$ by $(\alpha )_i(x)=(\alpha (x))_i$.

3.1 The system $\mathbf {EL}^*$

In the next subsection, we use the language $\mathscr {L}(\mathbf {EL}^*)$ of the definitional extension $\mathbf {EL}^*$ of $\mathbf {EL}$ defined in [8, Section 2.5].

Definition 17

A theory $T'$ in the language $\mathscr {L}'$ such that $\mathscr {L}\subseteq \mathscr {L}'$ is a definitional extension of a theory T in the language $\mathscr {L}$ if there is a mapping $\texttt {s}$ from the set of formulae in $\mathscr {L}'$ to the set of formulae in $\mathscr {L}$ with the following properties.

• 1. $\texttt {s}(A)\equiv A$ for all formulae A in $\mathscr {L}$;

• 2. $T'\vdash \texttt {s}(A)\leftrightarrow A$ for all formulae A in $\mathscr {L}'$;

• 3. if $T'\vdash A$, then $T\vdash \texttt {s}(A)$;

• 4. $\texttt {s}$ commutes all logical operations of $\mathscr {L}$.

Noticing that $\alpha =_1\beta$ is defined by $\forall x(\alpha (x)=\beta (x))$ and that the function $\lambda \text {-}.\text {-}$ is defined on pairs of variables and terms, not pairs of terms, we can prove that the following $\mathbf {EL}^*$ is a definitional extension of $\mathbf {EL}$ in a similar way to [9, Ch.2.7.10–12].

Definition 18

(Description of $\mathbf {EL}^*$) The language $\mathscr {L}(\mathbf {EL}^*)$ contains, in addition to the symbols of $\mathscr {L}(\mathbf {EL})$, binary term constructors $\text {-}|\text {-}$, $\text {-}(\text {-})$, and unary predicate symbols $\text {-}{\downarrow }_{0}$ and $\text {-}{\downarrow }_1$.

Functors (function term) and (numerical) terms are extended by adding the following clauses to (i)–(v) in [9, Ch.3.6.2]:

• if $\phi$ and $\chi$ are functors, then $\phi (\chi )$ is a term,

• if $\phi$ and $\chi$ are functors, then $\phi |\chi$ is a functor.

Atomic formulae are extended by the following clauses:

• if t is a term, then $t{\downarrow }_0$ is an atomic formula,

• if $\phi$ is a functor, then $\phi {\downarrow }_1$ is an atomic formula.

Free variables and bounded variables in terms, functors and formulae are defined as usual. We use, possibly with subscripts, u, v, w, x, y, z for numerical variables, a, b, c for codes of finite sequences of natural numbers, r, s and t for numerical terms, $\alpha$, $\beta$, $\gamma$ and $\delta$ for function variables, and $\phi$, $\chi$ and $\psi$ for functors. Note that, as in $\mathbf {EL}$, the equality $=_1$ between functors is defined by $\phi =_1 \chi \equiv \forall x (\phi (x) = \chi (x))$ (cf. [9, Ch.3.6.3 Notations]).

The logic of $\mathbf {EL}^*$ is two-sorted E$^+$ logic with equality. Here, we follow the formalisation $\mathrm {H}_2\text {-}\mathbf {IQCE}^+$ (cf. [9, Ch.2.4.5]) with the quantifier axioms:

$(\exists \text {-}\mathrm {Ax}^{\mathrm {E},0}_{2})$:

$A[x/t] \wedge t{\downarrow }_0 \mathbin {\rightarrow }\exists x A ,$

$(\forall \text {-}\mathrm {Ax}^{\mathrm {E},0}_{2})$:

$\forall x A \wedge t{\downarrow }_0 \mathbin {\rightarrow }A[x/t] ,$

$(\exists \text {-}\mathrm {Ax}^{\mathrm {E},1}_{2})$:

$A[\alpha /\phi ] \wedge \phi {\downarrow }_1 \mathbin {\rightarrow }\exists \alpha A ,$

$(\forall \text {-}\mathrm {Ax}^{\mathrm {E},1}_{2})$:

$\forall \alpha A \wedge \phi {\downarrow }_1 \mathbin {\rightarrow }A[\alpha /\phi ] ;$

the quantifier rules:

where $x \notin \mathrm {FV}(A)$, and $y \equiv x$ or $y \notin \mathrm {FV}(B)$, and where $\alpha \notin \mathrm {FV}(A)$, and $\beta \equiv \alpha$ or $\beta \notin \mathrm {FV}(B)$.

The axioms for existence, equality and strictness are as follows:

$\mathrm {EAX}$:

$\begin{array}{lll} x{\downarrow }_0, &{} 0{\downarrow }_0, &{} \alpha {\downarrow }_1, \\ t{\downarrow }_0 \mathbin {\leftrightarrow }\exists x (x=t), &{} \phi {\downarrow }_1 \mathbin {\leftrightarrow }\exists \alpha (\alpha =_1 \phi ) , &{} \\ \exists \alpha \forall u (t = \alpha (u)) \mathbin {\leftrightarrow }(\lambda u.t){\downarrow }_1^1;\end{array}$¹

$\mathrm {REFL}$:

$\forall x (x = x) ,$

$\mathrm {REPL}$:

$\begin{array}{l} R \vec {s} \vec {\chi } \wedge \vec {s} = \vec {t} \wedge \vec {\chi } =_1 \vec {\phi }\mathbin {\rightarrow }R \vec {t} \vec {\phi } , \\ (f \vec {s} \vec {\chi }){\downarrow }_k \wedge \vec {s} = \vec {t} \wedge \vec {\chi } =_1 \vec {\phi } \mathbin {\rightarrow }f \vec {s} \vec {\chi } =_k f \vec {t} \vec {\phi } ; \\ \end{array}$

$\mathrm {STR}$:

$\begin{array}{l} R(t_0,\ldots ,t_{n-1}, \phi _0,\ldots ,\phi _{m-1}) \mathbin {\rightarrow }t_i{\downarrow }_0 \wedge \phi _j{\downarrow }_1 , \\ f(t_0,\ldots ,t_{n-1}, \phi _0,\ldots ,\phi _{m-1}){\downarrow }_k \mathbin {\rightarrow }t_i{\downarrow }_0 \wedge \phi _j{\downarrow }_1 , \\ g(t_0,\ldots ,t_{n-1}, \phi _0,\ldots ,\phi _{m-1}){\downarrow }_k \mathbin {\leftrightarrow }t_i{\downarrow }_0 \wedge \phi _j{\downarrow }_1 ; \\ \end{array}$

where R is the equality $=$, ${\downarrow }_0$ or ${\downarrow }_1$, f is $\text {-}(\text {-})$, $\text {-}|\text {-}$ or $\lambda u. \text {-}$ for numerical variable u, and g is the application operator $\mathrm {Ap}$, the recursor ${{\varvec{r}}}$ or a function symbol of $\mathscr {L}(\mathbf {HA})$.

As non-logical axioms, we have the axioms of $\mathbf {HA}$, with induction extended to formulae of $\mathscr {L}(\mathbf {EL}^*)$, and the following modified versions of the axioms ($\mathrm {CON}$), ($\mathrm {REC}$) and ($\mathrm {QF}\text {-}\mathrm {AC}$):

$\mathrm {CON}$:

$(\lambda u. t){\downarrow }_1 \wedge s{\downarrow }_0 \mathbin {\rightarrow }(\lambda u. t) s = t[x/s] ,$

$\mathrm {REC}$:

$\begin{array}{l} \phi {\downarrow }_1 \wedge t{\downarrow }_0 \mathbin {\rightarrow }{{\varvec{r}}}(t,\phi ,0) = t , \\ \phi {\downarrow }_1 \wedge t{\downarrow }_0 \wedge s{\downarrow }_0 \mathbin {\rightarrow }{{\varvec{r}}}(t,\phi , S s) = \phi ({{\varvec{r}}}(t,\phi ,s),s) , \end{array}$

$\mathrm {QF}\text {-}\mathrm {AC}$:

$\forall x \exists y A(x,y) \mathbin {\rightarrow }\exists \alpha \forall x A(x,\alpha (x)) ,$

for quantifier-free A in $\mathscr {L}(\mathbf {EL})$ with $\alpha \notin \mathrm {FV}(A)$; and the following axioms for the function symbols $\text {-}(\text {-})$ and $\text {-}|\text {-}$:

$\mathrm {CFA}$:

$\begin{array}{l} \forall \alpha \beta \forall x [ G_0(\alpha ,\beta ,x) \mathbin {\leftrightarrow }\alpha (\beta ) = x ] , \\ \forall \alpha \beta \gamma [ G_1(\alpha ,\beta ,\gamma ) \mathbin {\leftrightarrow }\alpha |\beta =_1 \gamma ] , \end{array}$

where $G_0(\alpha ,\beta ,x)$ and $G_1(\alpha ,\beta ,\gamma )$ are defined as follows:

$$\begin{aligned} G_{0}(\alpha ,\beta ,x)&\equiv \exists v [ \forall w< v(\alpha (\overline{\beta } w) = 0) \wedge \alpha (\overline{\beta } v) =x+1] , \\ G_{1}(\alpha ,\beta ,\gamma )&\equiv \forall u \exists v [ \forall w < v (\alpha (\langle u \rangle *\overline{\beta } w) = 0) \wedge \alpha (\langle u \rangle *\overline{\beta } v) = \gamma (u)+1 ]. \end{aligned}$$

The function $\text {-}|\text {-}$ is supposed to be left-associative. For example, we write $\alpha |\beta |\gamma$ for $(\alpha |\beta )|\gamma$.

Remark 19

The following are proved by induction on the construction of terms and functors.

• 1. Let t and $\phi$ be a term and a functor in $\mathscr {L}(\mathbf {EL})$, respectively. Then $\mathbf {EL}^*\vdash t{\downarrow }_0$ and $\mathbf {EL}^*\vdash \phi {\downarrow }_1 .$

• 2. If $\phi$ and $\chi$ be functors in $\mathscr {L}(\mathbf {EL})$, then

  $$\begin{aligned} \mathbf {EL}^*\vdash (\phi |\chi ){\downarrow }_1 \mathbin {\leftrightarrow }\forall u \exists v (0 < \phi (\langle u \rangle *\overline{\chi } v)) . \end{aligned}$$

Remark 20

If the following form of $\mathrm {QF}\text {-}\mathrm {AC}$ were included in $\mathbf {EL}^*$, then the resulting system would not be a conservative extension of $\mathbf {EL}$:

$\mathrm {QF}\text {-}\mathrm {AC}^+$:

$\forall x \exists y A(x,y) \mathbin {\rightarrow }\exists \alpha \forall x A(x,\alpha (x)) ,$

for quantifier-free A in $\mathscr {L}(\mathbf {EL}^*)$ with $\alpha \notin \mathrm {FV}(A)$.

To see this, let T be Kleene’s T-predicate, and define a functor $\phi _T$ in $\mathscr {L}(\mathbf {EL})$ by

$$\begin{aligned}&\phi _T (\langle \rangle ) = 0 \quad \phi _T (\langle u \rangle *c) = {\left\{ \begin{array}{ll} 1 &{}\quad \text {if }\exists z < |c|\textit{Tuuz}\\ 0 &{}\quad \text {otherwise.} \end{array}\right. } \end{aligned}$$

Then

$$\begin{aligned} \exists z Txxz \mathbin {\leftrightarrow }\exists z G_0(\phi _T,\lambda u. x,z) \mathbin {\leftrightarrow }\exists z (\phi _T(\lambda u. x) = z) \mathbin {\leftrightarrow }(\phi _T(\lambda u. x)){\downarrow }_0 , \end{aligned}$$

(1)

in $\mathbf {EL}^*$, by $\mathrm {CFA}$ and $\mathrm {EAX}$. Assume that $\forall x (\exists z Txxz \vee \lnot \exists z Txxz) .$ Then

$$\begin{aligned} \forall x ((\phi _T(\lambda u. x)){\downarrow }_0 \vee \lnot (\phi _T(\lambda u. x)){\downarrow }_0) , \end{aligned}$$

and hence

$$\begin{aligned} \forall x \exists y [(y \ne 0 \mathbin {\rightarrow }(\phi _T(\lambda u. x)){\downarrow }_0) \wedge (y = 0 \mathbin {\rightarrow }\lnot (\phi _T(\lambda u. x)){\downarrow }_0)] . \end{aligned}$$

Therefore, applying $\mathrm {QF}\text {-}\mathrm {AC}^+$, we have

$$\begin{aligned} \exists \gamma \forall x [(\gamma (x) \ne 0 \mathbin {\rightarrow }(\phi _T(\lambda u. x)){\downarrow }_0) \wedge (\gamma (x) = 0 \mathbin {\rightarrow }\lnot (\phi _T(\lambda u. x)){\downarrow }_0)] . \end{aligned}$$

Thus

$$\begin{aligned}&\forall x (\exists z Txxz \vee \lnot \exists z Txxz) \\&\quad \mathbin {\rightarrow }\exists \gamma \forall x [(\gamma (x) \ne 0 \mathbin {\rightarrow }(\phi _T(\lambda u. x)){\downarrow }_0) \wedge (\gamma (x) = 0 \mathbin {\rightarrow }\lnot (\phi _T(\lambda u. x)){\downarrow }_0)], \end{aligned}$$

and so, by (1),

$$\begin{aligned}&\forall x (\exists z Txxz \vee \lnot \exists z Txxz) \nonumber \\&\quad \mathbin {\rightarrow }\exists \gamma \forall x [ (\gamma (x) \ne 0 \mathbin {\rightarrow }\exists z(Txxz)) \wedge (\gamma (x) = 0 \mathbin {\rightarrow }\lnot \exists z(Txxz))]. \end{aligned}$$

(2)

If $\mathbf {EL}^*+\mathrm {QF}\text {-}\mathrm {AC}^+$ were a definitional extension of $\mathbf {EL}$, $\mathbf {EL}$ would prove (2) by Definition 17, and hence $\mathbf {EL}$ with classical logic would prove

$$\begin{aligned} \exists \gamma \forall x [(\gamma (x) \ne 0 \mathbin {\rightarrow }\exists z Txxz) \wedge (\gamma (x) = 0 \mathbin {\rightarrow }\lnot \exists z Txxz)] . \end{aligned}$$

This contradicts with the soundness for a standard (classical) model consisting of (total) recursive functions.

In the following, instead of taking the recursor ${{\varvec{r}}}$ as a primitive, we take its special case $\mathrm {It}$ (iterator) satisfying

$$\begin{aligned} \chi {\downarrow }_1 \wedge t{\downarrow }_0 \mathbin {\rightarrow }\mathrm {It}(\chi ,t)(0) = t \wedge \mathrm {It}(\chi ,t)(S z) = \chi (\mathrm {It}(\chi ,t)(z)) . \end{aligned}$$

It is straightforward to show that this set of primitives is interdefinable with the set of the primitives of $\mathbf {EL}^*$.

The following definition and Lemma 23 were given in [8, Section 2.6].

Definition 21

For each term t and functor $\phi$ in $\mathscr {L}(\mathbf {EL}^*)$, and function variable $\alpha$, define functors $\varPhi _{t,\alpha }$ and $\varPhi _{\phi ,\alpha }$ in $\mathscr {L}(\mathbf {EL})$ by simultaneous induction on the complexity of t and $\phi$ as follows. Note that for each y, either $y = 0$ or there exist unique z and c such that $y = \langle z \rangle *c$. In the former case, define $\varPhi _{\phi ,\alpha }(y) = \varPhi _{t,\alpha }(y) = 0$. In the latter case, we divide into the following cases.

Basis

Case 1 $t \equiv 0$:

$$\begin{aligned} (\varPhi _{0,\alpha })(\langle z \rangle *c) = 1 . \end{aligned}$$

Case 2 $t \equiv x$:

$$\begin{aligned} (\varPhi _{x,\alpha })(\langle z \rangle *c) = x+1 . \end{aligned}$$

Case 3 $\phi \equiv \alpha$:

$$\begin{aligned} \varPhi _{\alpha ,\alpha }(\langle z \rangle *c) = {\left\{ \begin{array}{ll} c(z)+1 &{} \quad \text {if }z < |c|, \\ 0 &{} \quad \text {otherwise;} \end{array}\right. } \end{aligned}$$

Case 4 $\phi \equiv \gamma$ and $\gamma \not \equiv \alpha$:

$$\begin{aligned} (\varPhi _{\gamma ,\alpha })(\langle z \rangle *c) = \gamma (z)+1 . \end{aligned}$$

Case 5 $\phi \equiv f$ for some unary function constant f of $\mathbf {EL}$:

$$\begin{aligned} (\varPhi _{f,\alpha })(\langle z \rangle *c) = f(z)+1 . \end{aligned}$$

Induction step

Case 1 $t \equiv \chi (\psi )$:

$$\begin{aligned} \varPhi _{\chi (\psi ),\alpha }(\langle z \rangle *c) = {\left\{ \begin{array}{ll} x + 1 &{} \quad \text {for }x< |c|\text { such that} \\ &{} \qquad 0< \varPhi _{\chi ,\alpha }(\langle z \rangle *c) \wedge 0< \varPhi _{\psi ,\alpha }(\langle z \rangle *c) \\ &{} \qquad \wedge \exists a b< |c| [ \forall i< |a| (\varPhi _{\chi ,\alpha }(\langle i \rangle *c) = a(i) + 1) \\ &{} \qquad \wedge \forall i< |b| (\varPhi _{\psi ,\alpha }(\langle i \rangle *c) = b(i) + 1) \wedge b< |a| \\ &{}\qquad \wedge \forall i < |b| (a(\overline{b} i) = 0) \wedge a(b) = x+ 1 )] , \\ 0 &{}\quad \text {otherwise.} \end{array}\right. } \end{aligned}$$

Case 2 $t \equiv \chi |\psi$:

$$\begin{aligned} \varPhi _{\chi |\psi ,\alpha }(\langle z \rangle *c) = {\left\{ \begin{array}{ll} x + 1 &{}\quad \text {for }x< |c|\text { such that} \\ &{} \qquad 0< \varPhi _{\chi ,\alpha }(\langle z \rangle *c) \wedge 0< \varPhi _{\psi ,\alpha }(\langle z \rangle *c) \\ &{} \qquad \wedge \exists a b< |c| [ \forall i< |a| (\varPhi _{\chi ,\alpha }(\langle i \rangle *c) = a(i) + 1) \\ &{} \qquad \wedge \forall i< |b| (\varPhi _{\psi ,\alpha }(\langle i \rangle *c) = b(i) + 1) \wedge \langle z \rangle *b< |a| \\ &{} \qquad \wedge \forall i < |b| (a(\langle z \rangle *\overline{b} i) = 0) \wedge a(\langle z \rangle *b) = x + 1 ) ] , \\ 0 &{}\quad \text {otherwise.} \end{array}\right. } \end{aligned}$$

Case 3 $\phi \equiv \lambda u. t$:

Case 4 $t \equiv \chi (s)$:

Case 5 $\phi \equiv \mathrm {It}(\chi ,s)$:

Case 6 $t \equiv f(t_0,\ldots ,t_{n-1})$ for function symbol f in $\mathscr {L}(\mathbf {HA})$:

Remark 22

The following are proved by the induction on the construction of terms and functors, using Remark 19 for (3).

• 1. $\mathrm {FV}(\varPhi _{t,\alpha }) = \mathrm {FV}(t) {\setminus } \{\alpha \}$ and $\mathrm {FV}(\varPhi _{\phi ,\alpha }) = \mathrm {FV}(\phi ) {\setminus } \{\alpha \} ,$

• 2. $\mathbf {EL}^*$ proves $\varPhi _{t,\alpha } \in K^*$ and $\varPhi _{\phi ,\alpha } \in K^*$, where

  $$\begin{aligned} \alpha \in K^*\mathrel {\Leftrightarrow }\alpha (0) = 0 \wedge \forall a b (0 < \alpha (a) \mathbin {\rightarrow }\alpha (a *b) = \alpha (a)) . \end{aligned}$$

• 3. $\mathbf {EL}^*$ proves the following:

  $$\begin{aligned}&(\varPhi _{f(t_0,\ldots ,t_{n-1},\phi _0,\ldots ,\phi _{m-1}),\alpha }|\beta ){\downarrow }_1 \\&\quad \mathbin {\rightarrow }(\varPhi _{t_0,\alpha }|\beta ){\downarrow }_1 \wedge \cdots \wedge (\varPhi _{t_{n-1},\alpha }|\beta ){\downarrow }_1 \wedge (\varPhi _{\phi _0,\alpha }|\beta ){\downarrow }_1 \wedge \cdots \wedge (\varPhi _{\phi _{m-1},\alpha }|\beta ){\downarrow }_1, \end{aligned}$$

  where f is $\text {-}(\text {-})$, $\text {-}|\text {-}$, $\lambda u. \text {-}$ for numerical variable u, the application operator $\mathrm {Ap}$, the iterator $\mathrm {It}$ or a function symbol of $\mathscr {L}(\mathbf {HA})$.

Lemma 23

$\mathbf {EL}^*$ proves the following:

• 1. $\forall \beta ((\varPhi _{t,\alpha }|\beta ){\downarrow }_1 \mathbin {\leftrightarrow }(t[\alpha /\beta ]){\downarrow }_0) ,$

• 2. $\forall \beta ((\varPhi _{\phi ,\alpha }|\beta ){\downarrow }_1\mathbin {\leftrightarrow }(\phi [\alpha /\beta ]){\downarrow }_1) ,$

• 3. $\forall \beta [(t[\alpha /\beta ]){\downarrow }_0 \mathbin {\rightarrow }\forall z((\varPhi _{t,\alpha }|\beta )(z) = t[\alpha /\beta ])] ,$

• 4. $\forall \beta [(\phi [\alpha /\beta ]){\downarrow }_1 \mathbin {\rightarrow }\varPhi _{\phi ,\alpha }|\beta =_1 \phi [\alpha /\beta ]] .$

Proof

This can be proved by the induction on the construction of terms and functors. $\square$

Now, we define functors $\varLambda ^0 x. t$, $\varLambda ^1 x. \phi$ $\varLambda ^0 \alpha . t$ and $\varLambda ^1\alpha . \phi$ as follows:

$$\begin{aligned}&\varLambda ^0 x. t \equiv \lambda x. t, \quad \varLambda ^1 x. \phi \equiv \varPhi _{\phi [x/\alpha (0)],\alpha }, \\&\varLambda ^0 \alpha . t \equiv \lambda u. \varPhi _{t,\alpha }(\langle 0 \rangle *u), \quad \varLambda ^1 \alpha . \phi \equiv \varPhi _{\phi ,\alpha }, \end{aligned}$$

where $\alpha \not \in \mathrm {FV}(\phi )$ and $u \not \in \mathrm {FV}(t)$.

Intuitively, the superscript of $\varLambda$ denotes the type of value, and the variable follows $\varLambda ^{\text {-}}$ indicate the type of argument.

Remark 24

Note that, since $\varPhi _{t,\alpha }$ and $\varPhi _{\phi ,\alpha }$ are functors in $\mathscr {L}(\mathbf {EL})$, so are $\varLambda ^1 x.\phi$, $\varLambda ^0 \alpha . t$ and $\varLambda ^1 \alpha . \phi$, and hence $(\varLambda ^1 x. \phi ){\downarrow }_1$, $(\varLambda ^0 \alpha . t){\downarrow }_0$ and $(\varLambda ^1 \alpha . \phi ){\downarrow }_1$, by Remark 19 (1).

We use abbreviations $t \simeq _0 s$ and $\phi \simeq _1 \chi$ defined by

$$\begin{aligned}&t \simeq _0 s \equiv t{\downarrow }_0 \vee s {\downarrow }_0 \mathbin {\rightarrow }t = s , \quad \phi \simeq _1 \chi \equiv \phi {\downarrow }_1 \vee \chi {\downarrow }_1 \mathbin {\rightarrow }\phi =_1 \chi . \end{aligned}$$

Lemma 25

The following are derivable in $\mathbf {EL}^*$.

• 1. $(\varLambda ^0 x. t){\downarrow }_1 \wedge s{\downarrow }_0 \mathbin {\rightarrow }(\varLambda ^0 x. t) s = t[x/s] ,$

• 2. $(\lambda u. s){\downarrow }_1 \mathbin {\rightarrow }(\varLambda ^1 x. \phi )|(\lambda u. s) \simeq _1\phi [x/s] ,$

• 3. $\chi {\downarrow }_1 \wedge (t[\alpha /\chi ]){\downarrow }_0 \mathbin {\rightarrow }(\varLambda ^0\alpha . t)(\chi ) = t[\alpha /\chi ] ,$

• 4. $\chi {\downarrow }_1 \mathbin {\rightarrow }(\varLambda ^1\alpha . \phi )|\chi \simeq _1\phi [\alpha /\chi ] ,$

where $u \not \in \mathrm {FV}(s)$.

Proof

This follows from Lemma 23 and the definitions. $\square$

Lemma 26

There exists a functor $\phi _{{{\varvec{r}}}}$ in $\mathscr {L}(\mathbf {EL}^*)$ such that $\mathbf {EL}^*$ proves

$$\begin{aligned}&\phi _{{{\varvec{r}}}}{\downarrow }_1, \phi _{{{\varvec{r}}}}|\alpha |\beta |(\lambda u.0) \simeq \alpha \;\text { and}\; \phi _{{{\varvec{r}}}}|\alpha |\beta |(\lambda u. Sx) \simeq \beta |(\phi _{{{\varvec{r}}}}|\alpha |\beta |(\lambda u. x)|(\lambda u. x). \end{aligned}$$

Proof

Let $\phi _0$, $\psi _\mathrm{fix}$, $\psi _\mathrm{pred}$ and $\psi _\mathrm{d}$ as follows:

Then it is straightforward to show that

$$\begin{aligned} \phi _{{\varvec{r}}}\equiv \varLambda ^1 \alpha .\varLambda ^1 \beta . (\phi _\mathrm {fix} | \chi ) . \end{aligned}$$

satisfies the desired properties as in [9, Ch.9.3.8]. $\square$

One might think that the axiom

$$\begin{aligned} (\lambda u. t){\downarrow }_1 \mathbin {\leftrightarrow }\forall u (t{\downarrow }_0) \end{aligned}$$

should be included in $\mathbf {EL}^*$ as an axiom. From the left to right follows from $\mathrm {EAX}$ and $\mathrm {STR}$, and the converse is actually derivable in $\mathbf {EL}^*$.

Lemma 27

$\mathbf {EL}^*$ proves that $\forall u (t{\downarrow }_0) \mathbin {\rightarrow }(\lambda u. t){\downarrow }_1 .$

Proof

Suppose that $\forall u (t{\downarrow }_0) .$ Then, since

$$\begin{aligned} \forall u (t{\downarrow }_0 \mathbin {\rightarrow }(\varPhi _{t,\alpha }|\alpha ){\downarrow }_1 \wedge (\varPhi _{t,\alpha }|\alpha )(0) = t) \end{aligned}$$

by Lemma 23, we have $\forall u \exists \gamma (\gamma =_1 \varPhi _{t,\alpha }|\alpha ) ,$ by $\mathrm {EAX}$. Given u, assume that $\gamma =_1 \varPhi _{t,\alpha }|\alpha .$ Then $G_1(\varPhi _{t,\alpha },\alpha ,\gamma ) ,$ by $\mathrm {CFA}$, and hence $\exists v (0 < \varPhi _{t,\alpha }(\langle 0 \rangle *\overline{\alpha } v)) .$ Therefore $\forall u \exists v (0 < \varPhi _{t,\alpha }(\langle 0 \rangle *\overline{\alpha } v)) ,$ and hence there exists $\delta$ such that

$$\begin{aligned} \forall u (0 < \varPhi _{t,\alpha }(\langle 0 \rangle *\overline{\alpha }(\delta (u)))) , \end{aligned}$$

by $\mathrm {QF}\text {-}\mathrm {AC}$. Let . Then $\forall u (\phi (u) = (\varPhi _{t,\alpha }|\alpha )(0)) ,$ and hence $\forall u (\phi (u) = t) .$ Therefore $\exists \gamma \forall u (\gamma (u) = t) ,$ and so $(\lambda u. t){\downarrow }_1 ,$ by $\mathrm {EAX}$. $\square$

3.2 The interpretation $[\![\text {-}]\!]$ of $\mathscr {L}(\mathbf {HA}^{\omega })$ into $\mathscr {L}(\mathbf {EL}^*)$

We use a slightly modified version $[\![\text {-}]\!]$ of the interpretation $[\![\text {-}]\!] _{\mathrm {ICF}^*}$ in [9, Ch.9.1.16]. The main difference between our interpretation $[\![\text {-}]\!]$ and $[\![\text {-}]\!] _{\mathrm {ICF}^*}$ is the interpretation of the type 0 terms. The former interprets them as type 0 terms and the latter interprets them as type 1 terms in $\mathscr {L}(\mathbf {EL}^*)$. In [7, 2.6.2], a model $\mathrm {ICF}[\mathscr {U}]$ of $\mathbf {HA}^{\omega }$ is given in a similar way to $[\![\text {-}]\!]$.

For each type $\sigma$ in $\mathscr {L}(\mathbf {HA}^\omega )$, define a type $[\sigma ]$ in $\mathscr {L}(\mathbf {EL}^*)$ and formulae $x\in [\![0]\!]$ and $\alpha \in [\![\sigma \rightarrow \tau ]\!]$ as follows:

$$\begin{aligned}&[0]\equiv 0; \quad [\rho \rightarrow \tau ]\equiv 1; \quad x\in [\![0]\!] \equiv x=x; \quad \alpha \in [\![0\rightarrow 0]\!] \equiv \forall x(\alpha (x)=\alpha (x));\\&\alpha \in [\![\rho \rightarrow \tau ]\!] \equiv {\left\{ \begin{array}{ll} \forall y(\alpha |\lambda v. y{\downarrow }\wedge \alpha |\lambda v. y\in [\![\tau ]\!] ) &{}\quad \text {if }\rho =0\quad \text { and }\quad \tau \ne 0; \\ \forall \beta (\beta \in [\![\rho ]\!] \rightarrow \alpha (\beta ){\downarrow }) &{}\quad \text {if }\rho \ne 0\quad \text { and }\quad \tau =0; \\ \forall \beta (\beta \in [\![\rho ]\!] \rightarrow \alpha |\beta {\downarrow }\wedge \alpha |\beta \in [\![\tau ]\!] ) &{}\quad \text {if }\rho \ne 0\quad \text { and }\quad \tau \ne 0. \\ \end{array}\right. } \end{aligned}$$

We fix a bijection $[\![\text {-}]\!]$ between the variables of $\mathscr {L}(\mathbf {HA}^\omega )$ and the variables in $\mathscr {L}(\mathbf {EL}^*)$ such that $[\![x^\sigma ]\!]$ is a variable of type $[\sigma ]$ in $\mathscr {L}(\mathbf {EL}^*)$ for each variable $x^\sigma$ in $\mathscr {L}(\mathbf {HA}^\omega )$. Note that for each variable a of type 0 or 1 in $\mathscr {L}(\mathbf {HA}^\omega )$, the variable $[\![a]\!]$ is a variable of type 0 or 1 in $\mathscr {L}(\mathbf {EL}^*)$, respectively.

To define $[\![c]\!]$ for each constant c in $\mathscr {L}(\mathbf {HA}^\omega )$, we use $\varLambda$ operators which are defined in Sect. 3.1. In what follows, we write $\varLambda \text {-}\varLambda \text {-}. \text {-}$ for $\varLambda \text {-}.(\varLambda \text {-}. \text {-})$. Then $[\![c]\!]$ is defined as follows:

$$\begin{aligned}{}[\![0]\!]&\equiv 0; \quad [\![S]\!] =S;\\ [\![{{\varvec{k}}}^{\sigma ,\tau }]\!]&= {\left\{ \begin{array}{ll} \varLambda ^{1}x\varLambda ^{0}y. x &{}\quad \text {if }\sigma \equiv \tau \equiv 0;\\ \varLambda ^1x\varLambda ^0\beta . x &{}\quad \text {if }\sigma \equiv 0\quad \text { and }\quad \tau \not \equiv 0 \\ \varLambda ^1\alpha \varLambda ^1y. \alpha &{}\quad \text {if }\sigma \not \equiv 0\quad \text { and }\quad \tau \equiv 0 \\ \varLambda ^1\alpha \varLambda ^1\beta . \alpha &{}\quad \text {if }\sigma \not \equiv 0\quad \text { and }\quad \tau \not \equiv 0 \end{array}\right. } \\ [\![{{\varvec{s}}}^{\rho ,\sigma ,\tau }]\!]&= {\left\{ \begin{array}{ll} \varLambda ^1\alpha \varLambda ^1\beta \varLambda ^0 z.(\alpha |(\lambda v. z))(\beta (z)) &{} \quad \text {if }\sigma \equiv 0\quad \text { and }\quad \tau \equiv 0;\\ \varLambda ^1\alpha \varLambda ^1\beta \varLambda ^1 z.(\alpha |\lambda v. z)|(\beta |\lambda v. z) &{} \quad \text {if }\sigma \equiv 0\quad \text { and }\quad \tau \equiv 1;\\ \varLambda ^1\alpha \varLambda ^1\beta \varLambda ^0\gamma .(\alpha |\gamma )(\beta |\gamma ) &{} \quad \text {if }\sigma \equiv 1\quad \text { and }\quad \tau \equiv 0;\\ \varLambda ^1\alpha \varLambda ^1\beta \varLambda ^1\gamma .(\alpha |\gamma )|(\beta |\gamma ) &{} \quad \text {if }\sigma \equiv 1\quad \text { and }\quad \tau \equiv 1; \end{array}\right. }\\ [\![{{\varvec{r}}}^{\sigma }]\!]&= {\left\{ \begin{array}{ll} \varLambda ^{1}x \varLambda ^{1}\beta \varLambda ^{0}z. {{\varvec{r}}}(x,\beta ,z) &{}\quad \text {if }[\sigma ]\equiv 0; \\ \varLambda ^{1}\alpha \varLambda ^{1}\beta \varLambda ^{1}z. \phi _{{{\varvec{r}}}}|\alpha |\beta |\lambda v. z &{}\quad \text {if }[\sigma ]\equiv 1, \end{array}\right. } \end{aligned}$$

where ${{\varvec{r}}}$ is the recursor in $\mathscr {L}(\mathbf {EL}^*)$, and where $\phi _{{{\varvec{r}}}}$ is a functor defined in Lemma 26. By Remark 24, $\mathbf {EL}^*$ proves $[\![c^\sigma ]\!] {\downarrow }_{[\sigma ]}$ for each constant c with type $\sigma$ in $\mathscr {L}(\mathbf {HA}^{\omega })$. We use the following notations for a functor $\phi$ such that $\phi \in [\![\sigma \rightarrow \tau ]\!]$ and a variable $a\in [\![\sigma ]\!]$ in $\mathscr {L}(\mathbf {EL})$:

$$\begin{aligned} \phi \cdot a\equiv {\left\{ \begin{array}{ll} \phi (a) &{}\quad \text {if }\sigma \equiv 0\quad \text { and }\quad \tau \equiv 0;\\ \phi |(\lambda x. a) &{}\quad \text {if }\sigma \equiv 0\quad \text { and }\quad \tau \not \equiv 0; \\ \phi (a) &{}\quad \text {if }\sigma \not \equiv 0\quad \text { and }\quad \tau \equiv 0; \\ \phi |a &{}\quad \text {if }\sigma \equiv 0\quad \text { and }\quad \tau \not \equiv 0. \end{array}\right. } \end{aligned}$$

Note that $\phi (a)$ in the first case denotes usual application of a functor $\phi$ to a term a, i.e., $\mathrm {Ap}(\phi ,a)$, but $\phi (a)$ in the third case denotes an application of the partial function $\text {-}(\text {-})$ in $\mathscr {L}(\mathbf {EL}^*)$.

We define $[\![ts]\!]$ by $[\![ts]\!] =[\![t]\!] {\cdot }[\![s]\!]$. By Lemma 25, $\mathbf {EL}^*$ proves the following:

$$\begin{aligned}&[\![0]\!] \equiv 0; \quad [\![Sx^0]\!] =S[\![x]\!] ; \\&[\![x^\sigma ]\!] \in [\![\sigma ]\!] \wedge [\![y^\tau ]\!] \in [\![\tau ]\!] \rightarrow [\![{{\varvec{k}}}^{\sigma ,\tau }x y]\!] =[\![x]\!] ; \\&[\![x^{\rho \rightarrow (\sigma \rightarrow \tau )}]\!] \in [\![\rho \rightarrow (\sigma \rightarrow \tau )]\!] \wedge [\![y^{\rho \rightarrow \sigma }]\!] \in [\![\rho \rightarrow \sigma ]\!] \wedge [\![z^{\rho }]\!] \in {[\![\rho ]\!] }\\&\quad \rightarrow [\![{{\varvec{s}}}^{\rho ,\sigma ,\tau }x^{\rho \rightarrow (\sigma \rightarrow \tau )}y^{\rho \rightarrow \sigma }z^{\rho }]\!] =[\![xz(yz)]\!] ; \\&[\![x^{\sigma }]\!] \in [\![\sigma ]\!] \wedge [\![y^{\sigma \rightarrow (0\rightarrow \sigma )}]\!] \in [\![\sigma \rightarrow (0\rightarrow \sigma )]\!] \\&\quad \rightarrow [\![{{\varvec{r}}}^{\sigma }x^{\sigma }y^{\sigma \rightarrow (0\rightarrow \sigma )}0]\!] =[\![x]\!] \wedge [\![{{\varvec{r}}}^{\sigma }x^{\sigma }y^{\sigma \rightarrow (0\rightarrow \sigma )}({S}z^{0})]\!] = [\![y({{\varvec{r}}}^{\sigma }xyz)z]\!] . \end{aligned}$$

Furthermore, we can prove the following by induction on the construction of a term: For each term $t^{\rho }\in \mathscr {L}(\mathbf {HA}^{\omega })$ whose all free variables are listed in $x_0^{\sigma _0},\ldots ,x_{i-1}^{\sigma _i}$, $\alpha _{0}^{\tau _0},\ldots ,\alpha _{j-1}^{\tau _{j-1}}$, $\mathbf {EL}^*$ proves that

$$\begin{aligned} \bigwedge _{k<i} [\![x_k]\!] \in [\![\sigma _k]\!] \wedge \bigwedge _{k<j}[\![\alpha _k]\!] \in [\![\tau _k]\!] \rightarrow [\![t]\!] {\downarrow }_{[\rho ]}\wedge [\![t]\!] \in [\![\sigma ]\!] . \end{aligned}$$

For a formula A in $\mathscr {L}(\mathbf {HA}^\omega )$, a formula $[\![A]\!]$ in $\mathscr {L}(\mathbf {EL}^*)$ is defined as follows:

$$\begin{aligned}{}[\![t=_\sigma s]\!]&\equiv {\left\{ \begin{array}{ll} [\![t]\!] =[\![s]\!] &{}\quad \text {if }[\sigma ]\equiv 0;\\ \forall n([\![t]\!] (n)=[\![s]\!] (n)) &{}\quad \text {if }[\sigma ]\equiv 1; \end{array}\right. } \quad [\![\bot ]\!] \equiv \bot ; \\ [\![A\circ B]\!]&\equiv [\![A]\!] \circ [\![B]\!] ,\text { where }\circ \in \{ \wedge ,\vee ,\rightarrow \};\\ [\![\forall x^\sigma A]\!]&\equiv \forall x^{[\sigma ]}(x\in [\![\sigma ]\!] \rightarrow [\![A]\!] ); \quad [\![\exists x^\sigma A]\!] \equiv \exists x^{[\sigma ]}(x\in [\![\sigma ]\!] \wedge [\![A]\!] ). \end{aligned}$$

We often use the abbreviations $\forall x\in [\![\sigma ]\!] A$ and $\exists x\in [\![\sigma ]\!] A$ for $\forall x^{[\sigma ]}(x\in [\![\sigma ]\!] \rightarrow A)$ and $\exists x^{[\sigma ]}(x\in [\![\sigma ]\!] \wedge A)$, respectively.

A schema in $\mathscr {L}(\mathbf {EL})$ or $\mathscr {L}(\mathbf {HA}^\omega )$ is a schema whose terms and quantifiers are all in $\mathscr {L}(\mathbf {EL})$ or $\mathscr {L}(\mathbf {HA}^\omega )$, respectively. Note that the schemata $\mathrm {BI}_\mathrm{M}$, $\mathrm {C}\text {-}\mathrm {N}$ and $\mathrm {MP}$ are in $\mathscr {L}(\mathbf {EL})$ and that $\mathrm {AC}$ and $\mathrm {DC}$ are in $\mathscr {L}(\mathbf {HA}^{\omega })$. The standard translation $\iota$ from $\mathscr {L}(\mathbf {EL})$ into $\mathscr {L}(\mathbf {HA}^\omega )$ can be extended on the schemata in $\mathscr {L}(\mathbf {EL})$ in a natural way. For each term t and schema ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL})$, assign a term $(t)_E$ and a schema $({\varvec{\alpha }})_E$ in $\mathscr {L}(\mathbf {EL}^*)$ as follows:

$$\begin{aligned} {\begin{array}{ll} (c)_E\equiv [\![\iota (c)]\!] &{}\quad (x^i)_E\equiv [\![\iota (x^i)]\!] ; \\ (ft_1\ldots t_{n})_E\equiv f(t_1)_E\ldots (t_{n})_E; &{}\quad ({{\varvec{r}}}(t_1,t_2,t_3))_E\equiv {{\varvec{r}}}(t_1)_E(t_2)_E(t_3)_E;\\ (a^1(t^0))_E\equiv (a)_E((t)_E); &{}\quad (\lambda x. t)_E\equiv \lambda (x)_E. (t)_E; \\ (s=_0t)_E\equiv (s)_E=_0(t)_E; \quad (\bot )_E\equiv \bot ; &{}\quad ({\varvec{\nu }}(t_1,\ldots ,t_n))_E\equiv {\varvec{\nu }}((t_1)_E, \ldots , (t_n)_E); \\ ({\varvec{\beta }}_1\circ {\varvec{\beta }}_2)_E\equiv ({\varvec{\beta }}_1)_E\circ ({\varvec{\beta }}_2)_E; &{}\quad (Qx^i{\varvec{\beta }})_E\equiv Q(x)_E({\varvec{\beta }})_E,\end{array}} \end{aligned}$$

for $\circ \in \{\wedge ,\vee ,\rightarrow \}$ and $Q\in \{ \exists ,\forall \}$. Note that the interpretation $[\![\text {-}]\!]$ satisfies the following properties (P0)–(P5).

• (P0) For each variable $x^\sigma \in \mathscr {L}(\mathbf {HA}^\omega )$, $[\![x^\sigma ]\!]$ is a variable of type $[\sigma ]$ in $\mathscr {L}(\mathbf {EL}^*)$;

• (P1) $[\![\iota (t)]\!] \equiv (t)_E$;

• (P2) $[\![t^0 = s^0]\!] \equiv [\![t^0]\!] = [\![s^0]\!]$;

• (P3) $\mathbf {EL}^*\vdash [\![A\circ B]\!] \leftrightarrow [\![A]\!] \circ [\![B]\!]$ for $\circ \in \{ \wedge ,\vee ,\rightarrow \}$;

• (P4) $\mathbf {EL}^*\vdash [\![Q u^\sigma A]\!] \leftrightarrow \forall [\![u^\sigma ]\!] [\![A]\!]$, for $Q\in \{ \exists , \forall \}$ and $\sigma \equiv 0$ or 1;

• (P5) $\mathbf {EL}^*\vdash [\![A [u^\sigma / t^\sigma ]]\!] \leftrightarrow [\![A]\!] [ [\![u^\sigma ]\!] / [\![t^\sigma ]\!] ]$.

Remark 28

For the property (P4), note that $\mathbf {EL}^*\vdash x^0\in [\![0]\!] \wedge a^1\in [\![1]\!]$. To show the property (P5), we first prove $[\![t[x^\sigma /s^\sigma ]]\!] \equiv [\![t]\!] [[\![x^\sigma ]\!] /[\![s^\sigma ]\!] ]$ by induction on the construction of t, and then prove (P5), by the induction on the construction of A.

The following propositions show that, for any schema ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL})$, any instance ${\varvec{\alpha }}[\vec {\nu }/\vec {B}]$ of ${\varvec{\alpha }}$ as a schema in $\mathscr {L}(\mathbf {HA}^{\omega })$ with $\vec {B}$ in $\mathscr {L}(\mathbf {HA}^{\omega })$ is interpreted into an instance of ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL}^*)$.

Proposition 29

Let ${\varvec{\alpha }}[{\varvec{\nu }}_1,\ldots {\varvec{\nu }}_k]$ be a schema with exactly the displayed place holders in $\mathscr {L}(\mathbf {EL})$ and let $B_1, \ldots , B_k$ be formulae in $\mathscr {L}(\mathbf {HA}^\omega )$. Then

$$\begin{aligned}&\mathbf {EL}^* \vdash {[\![\iota ({\varvec{\alpha }})[{\varvec{\nu }}_1/\lambda \vec {u_1}. B_1, \ldots , {\varvec{\nu }}_k/\lambda \vec {u_k}. B_k]]\!] } \\&\quad \leftrightarrow {({\varvec{\alpha }})_E[{\varvec{\nu }}_1/\lambda \vec {[\![u_1]\!] }. [\![B_1]\!] , \ldots , {\varvec{\nu }}_k/\lambda \vec {[\![u_k]\!] }. [\![B_k]\!] ]}. \end{aligned}$$

Proof

We show by induction on the complexity of ${\varvec{\alpha }}$. It is clear if ${\varvec{\alpha }}$ is $\bot$. If ${\varvec{\alpha }}$ is an atomic formula $P\equiv s=_0t$, then s and t are terms in $\mathscr {L}(\mathbf {EL})$, and hence $[\![\iota (s=_0t)]\!] \equiv [\![\iota (s)]\!] =_0[\![\iota (t)]\!] \equiv (s)_E=_0(t)_E\equiv (s=_0t)_E$, by (P1), (P2) and the definition of $(\text {-})_E$. Let ${\varvec{\alpha }} \equiv {\varvec{\nu }}_i(t_1, \ldots , t_n)$ for some $i=0,\ldots , k$ and $\vec {u_i}\equiv v_1^{\sigma _1},\ldots ,v_n^{\sigma _n}$. Then

$$\begin{aligned} {[\![B_i [v_1^{\sigma _1} / \iota (t_1), \ldots , v_n^{\sigma _n} / \iota (t_n)]]\!] }&\equiv {[\![B_i]\!] [[\![v_1^{\sigma _1}]\!] /[\![\iota (t_1)]\!] , \ldots , [\![v_n^{\sigma _n}]\!] /[\![\iota (t_n)]\!] ]} \\&\equiv {[\![B_i]\!] [[\![v_1^{\sigma _1}]\!] /(t_1)_E, \ldots , [\![v_n^{\sigma _n}]\!] /(t_n)_E]}, \end{aligned}$$

by (P5) and (P1). It is straightforward to see the induction steps for the connectives by (P3) and (P4). $\square$

For a schema ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL})$, the set $\mathrm {FV}({\varvec{\alpha }})$ of free variables in ${\varvec{\alpha }}$ is defined in the usual way. A schema is closed if $\mathrm {FV}({\varvec{\alpha }})=\emptyset$.

Proposition 30

Let ${\varvec{\alpha }}$ be a closed schema in $\mathscr {L}(\mathbf {EL})$ with place holders ${\varvec{\nu }}_1,\ldots , {\varvec{\nu }}_k$, and let $B_1,\ldots , B_k$ be formulae in $\mathscr {L}(\mathbf {HA}^\omega )$. Then

$$\begin{aligned} \mathbf {EL}^*\vdash [\![\iota ({\varvec{\alpha }})[B_1,\ldots , B_k]]\!] \leftrightarrow {\varvec{\alpha }}[[\![B_1]\!] ,\ldots , [\![B_k]\!] ]. \end{aligned}$$

Proof

Since, for any closed schema ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL})$ and formulae $\vec {C}$ in $\mathscr {L}(\mathbf {EL}^*)$, $({\varvec{\alpha }})_E[\vec {C}]$ is obtained from ${\varvec{\alpha }}[\vec {C}]$ by renaming of bound variables in $\mathbf {\alpha }$, we have $\mathbf {EL}^*\vdash ({\varvec{\alpha }})_E[\vec {C}]\leftrightarrow {\varvec{\alpha }}[\vec {C}]$. Then it follows from Proposition 29. $\square$

The above proposition shows that, for each schema ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL})$, each instance of ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {HA}^{\omega })$ is interpreted by $[\![\text {-}]\!]$ as an instance of the same schema ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL}^*)$. In particular, we have the following.

Corollary 31

For each instance A of $\mathrm {BI}_\mathrm{M}$, $\mathrm {C}\text {-}\mathrm {N}$ or $\mathrm {MP}$ in $\mathscr {L}(\mathbf {HA}^\omega )$, there exists an instance B of $\mathrm {BI}_\mathrm{M}$, $\mathrm {C}\text {-}\mathrm {N}$ or $\mathrm {MP}$ in $\mathscr {L}(\mathbf {EL}^*)$, respectively, such that

$$\begin{aligned} \mathbf {EL}^*\vdash [\![A]\!] \leftrightarrow B. \end{aligned}$$

Proof

Let a schema ${\varvec{\alpha }}$ be $\mathrm {BI}_\mathrm{M}$, $\mathrm {C}\text {-}\mathrm {N}$ or $\mathrm {MP}$ in $\mathscr {L}(\mathbf {EL})$. Then, since ${\varvec{\alpha }}$ is closed, $\iota ({\varvec{\alpha }})$ is a closed schema in $\mathscr {L}(\mathbf {HA}^\omega )$ corresponding to $\mathrm {BI}_\mathrm{M}$, $\mathrm {C}\text {-}\mathrm {N}$ or $\mathrm {MP}$. $\square$

Note that, although we have used the particular interpretation $[\![\text {-}]\!]$, we can prove Proposition 30 for any interpretation with the properties (P0)–(P5).

The classes $\varDelta _0$, $\varSigma _n$ and $\varPi _n$ of formulae in $\mathscr {L}(\mathbf {HA})$ are naturally extended into ones of formulae in $\mathscr {L}(\mathbf {EL})$, which are often written $\varDelta ^0_0$, $\varSigma ^0_n$ and $\varPi ^0_n$ in the literature. A formula A in $\mathscr {L}(\mathbf {EL})$ is almost negative if it is built up from formulae of the form $\exists x^{\sigma }B$ with B in $\varDelta _0$ in $\mathscr {L}(\mathbf {EL})$ (not B in $\mathscr {L}(\mathbf {EL}^*)$) by means of $\wedge$, $\rightarrow$ and $\forall x^\sigma$ for $\sigma \equiv 0$ or 1.

Troelstra’s generalized continuity principle ($\mathrm {GC}$, cf. [7, 3.3.9 Definition]) is as follows:

$$\begin{aligned} \forall \alpha (B(\alpha )\rightarrow \exists \beta C(\alpha ,\beta ))\rightarrow \exists \gamma \forall \alpha (B(\alpha )\rightarrow \gamma |\alpha {\downarrow }\wedge C(\alpha ,\gamma |\alpha )), \end{aligned}$$

where B is almost negative (cf. [7, 3.3.9] or [9, Ch.9.6.9]). The following proposition is well known, and we omit a proof.

Proposition 32

$\mathbf {EL}^*+\mathrm {GC}\vdash \mathrm {C}\text {-}\mathrm {N}$.

For each type $\sigma$ in $\mathscr {L}(\mathbf {HA}^\omega )$, we use the following functors in $\mathscr {L}(\mathbf {EL})$:

$$\begin{aligned}&\phi _{\sigma }\equiv {\left\{ \begin{array}{ll} \varLambda ^0\alpha . \alpha (0) &{}\quad \text {if }\sigma \equiv 0;\\ \varLambda ^1\alpha . \alpha &{}\quad \text {otherwise}; \end{array}\right. }&\chi _{\sigma }\equiv {\left\{ \begin{array}{ll} \varLambda ^1x.(\lambda y. x) &{}\quad \text {if }\sigma \equiv 0,\\ \varLambda ^1\alpha . \alpha &{} \quad \text {otherwise}. \end{array}\right. } \end{aligned}$$

By Remark 24, we have $\phi _{\sigma }{\downarrow }_1$ and $\chi _{\sigma }{\downarrow }_1$ for any $\sigma$. Furthermore, we have $\phi _{\sigma }(\alpha )=\alpha (0)$ for $\sigma \equiv 0$ and $\phi _{\sigma }|\alpha =\alpha$ for $\sigma \not \equiv 0$, and so $\phi _{0}\in [\![\tau \rightarrow 0]\!]$ for any $\tau$ with $\tau \not \equiv 0$ and $\phi _{\sigma }\in [\![\sigma \rightarrow \sigma ]\!]$ for any $\sigma \not \equiv 0$. We also have $\chi _{0}(x)=\lambda y. x$ and $\chi _{\sigma }|\alpha =\alpha$ for $\sigma \not \equiv 0$ and so $\chi _{0}\in [\![0\rightarrow 1]\!]$ and $\chi _{\sigma }\in [\![\sigma \rightarrow \sigma ]\!]$ for $\sigma \not \equiv 0$.

Hence, using the notation $\beta {\cdot }a$ used to define $[\![ts]\!]$, we have the following:

$$\begin{aligned} \phi _{\sigma }{\cdot }\alpha = {\left\{ \begin{array}{ll} \alpha (0) &{}\quad \text {if }\sigma \equiv 0;\\ \alpha &{}\quad \text {otherwise}; \end{array}\right. }\quad \chi _{\sigma }{\cdot }a^{[\sigma ]}= {\left\{ \begin{array}{ll} \lambda y. a &{}\quad \text {if }\sigma \equiv 0; \\ a &{} \quad \text {otherwise}. \end{array}\right. } \end{aligned}$$

Note that $\phi _{\sigma }{\cdot }\alpha$ has type $[\sigma ]$ but $\chi _{\sigma }{\cdot }a^{[\sigma ]}$ has always type 1.

Lemma 33

For any $\sigma$ with $\sigma \not \equiv 0$, there is an almost negative formula $A_{\sigma }(\alpha )$ such that $\mathbf {EL}^*$ proves $\forall \alpha (\alpha \in [\![\sigma ]\!] \leftrightarrow A_{\sigma }(\alpha ))$.

Proof

We prove by induction on types.

For $\sigma \equiv 0\rightarrow 0$, $A_{1}(\alpha )\equiv \forall x(\alpha (x)=\alpha (x))$ has the desired property.

Since the other cases can be proved in a similar way, we only prove the case with $\sigma \equiv \rho \rightarrow \tau$ and for some $\rho \not \equiv 0$ and $\tau \not \equiv 0$. Assume that $A_{\rho }(\alpha )$ and $A_{\tau }(\alpha )$ are almost negative and that $\mathbf {EL}^*$ proves

$$\begin{aligned} \forall \alpha (\alpha \in [\![\rho ]\!] \leftrightarrow A_{\rho }(\alpha )) \quad \text {and} \quad \forall \alpha (\alpha \in [\![\tau ]\!] \leftrightarrow A_{\rho }(\tau )). \end{aligned}$$

By Remark 19 (2), $\alpha |\beta {\downarrow }$ is equivalent to $\forall u\exists v(\alpha (\langle u\rangle *\overline{\beta }v)>0)$. Then

$$\begin{aligned}&\alpha \in [\![\rho \rightarrow \tau ]\!] \\&\quad \leftrightarrow \forall \beta (\beta \in [\![\rho ]\!] \rightarrow \alpha |\beta {\downarrow }\wedge \alpha |\beta \in [\![\tau ]\!] ) \\&\quad \leftrightarrow \forall \beta (\beta \in [\![\rho ]\!] \rightarrow \forall x\exists y(\alpha (\langle x\rangle *\overline{\beta }y)>0)\wedge \forall \gamma (\forall x((\alpha |\beta )(x)=\gamma (x))\\&\quad \rightarrow \gamma \in [\![\tau ]\!] )) \\&\quad \leftrightarrow \forall \beta (\beta \in [\![\rho ]\!] \rightarrow \forall x\exists y(\alpha (\langle x\rangle *\overline{\beta }y)>0)\wedge \forall \gamma (G_1(\alpha ,\beta ,\gamma )\rightarrow \gamma \in [\![\tau ]\!] )) \\&\quad \leftrightarrow \forall \beta (A_{\rho }(\beta )\rightarrow \forall x\exists y(\alpha (\langle x\rangle *\overline{\beta }y)>0)\wedge \forall \gamma (G_1(\alpha ,\beta ,\gamma )\rightarrow A_{\tau }(\gamma ))), \end{aligned}$$

and so we can take the almost negative formula in the last line as $A_{\rho \rightarrow \tau }(\alpha )$. $\square$

The above lemma shows that for any $\alpha$, $\mathbf {EL}^*$ proves that $\phi _{\sigma }{\cdot }\alpha \in [\![\sigma ]\!]$ is equivalent to some almost negative formula in $\mathscr {L}(\mathbf {EL})$, since $\phi _{\sigma }{\cdot }\alpha =\alpha (0)$ and so $\phi _{\alpha }{\cdot }\alpha \in [\![0]\!] \leftrightarrow \alpha (0)=\alpha (0)$ for $\sigma \equiv 0$, and $\phi _{\sigma }{\cdot }\alpha =\alpha$ for $\sigma \not \equiv 0$ and so $\phi _{\sigma }{\cdot }\alpha \in [\![\sigma ]\!] \leftrightarrow A_{\sigma }(\alpha )$.

Hence the interpretation $[\![\text {-}]\!]$ also satisfies the following properties:

• (P6) $\phi _{\sigma }{\cdot }\alpha \in [\![\sigma ]\!]$ is equivalent to an almost negative formula in $\mathscr {L}(\mathbf {EL})$;

• (P7) $\mathbf {EL}^*\vdash [\![\forall a^\sigma A]\!] \leftrightarrow (\forall a\in [\![\sigma ]\!] )[\![A]\!]$ and $\mathbf {EL}^*\vdash [\![\exists a^{\sigma } A]\!] \leftrightarrow (\exists a\in [\![\sigma ]\!] )[\![A]\!]$;

• (P8) $\mathbf {EL}^* \vdash \forall a \in [\![ \sigma ]\!] (\phi _\sigma {\cdot }(\chi _\sigma {\cdot }a) = a)$;

• (P9) $\mathbf {EL}^* \vdash \forall \alpha [ {\forall a \in [\![\sigma ]\!] ({\alpha |(\chi _\sigma (a))}{\downarrow }_1 \wedge \phi _\tau {\cdot }(\alpha |(\chi _\sigma {\cdot }a)) \in [\![ \tau ]\!] )} \rightarrow \exists \beta \in [\![ \sigma \rightarrow \tau ]\!] \forall a\in [\![\sigma ]\!] (\beta {\cdot }a = \phi _\tau {\cdot }(\alpha |(\chi _\sigma {\cdot }a))) ]$.

Remark 34

To prove the property (P9), we have to consider four cases depending on types $\sigma$ and $\tau$. If $\sigma \equiv \tau \equiv 0$, the assumption

$$\begin{aligned} \forall a\in [\![\sigma ]\!] ({\alpha |(\chi _\sigma (a))}{\downarrow }_1 \wedge \phi _\tau {\cdot }(\alpha |(\chi _\sigma (a))) \in [\![ \tau ]\!] ) \end{aligned}$$

implies that $\forall a\in [\![\sigma ]\!] [\psi {\cdot }a=\phi _{\tau }{\cdot }(\alpha |(\chi _{\sigma }{\cdot }a))]$ for $\psi \equiv \varLambda ^0x. \alpha {|}(\chi _{\sigma }(x))(0)$. Other cases are proved in a similar way.

Proposition 35

For each instance A of $\mathrm {AC}_{\sigma ,\tau }$ in $\mathscr {L}(\mathbf {HA}^\omega )$,

$$\begin{aligned} \mathbf {EL}^* + \mathrm {GC}\vdash [\![ A ]\!] . \end{aligned}$$

Proof

Let

$$\begin{aligned} {\forall x^\sigma \exists y^\tau B(x,y)} \rightarrow {\exists z^{\sigma \rightarrow \tau } \forall x^\sigma B(x,zx)} \end{aligned}$$

be an instance of $\mathrm {AC}_{\sigma ,\tau }$, and suppose $(\forall a \in [\![ \sigma ]\!] ) (\exists b \in [\![ \tau ]\!] ) [\![ B ]\!] (a,b)$ for $[\![x]\!] =a$ and $[\![y]\!] =b$. Then we have

$$\begin{aligned} \forall \alpha [ {\phi _\sigma {\cdot }\alpha \in [\![ \sigma ]\!] } \rightarrow \exists b(\phi _\tau {\cdot }(\chi _\tau {\cdot }b) \in [\![\tau ]\!] \wedge [\![ B ]\!] (\phi _\sigma {\cdot }\alpha ,\phi _\tau {\cdot }(\chi _\tau {\cdot }b)))], \end{aligned}$$

by (P8). Since $\forall b^{[\tau ]}(\chi _{\tau }{\cdot }b{\downarrow }_1)$, we have

$$\begin{aligned} \forall \alpha [ {\phi _\sigma {\cdot }\alpha \in [\![ \sigma ]\!] } \rightarrow \exists \beta (\phi _\tau {\cdot }\beta \in [\![ \tau ]\!] \wedge [\![ B ]\!] (\phi _\sigma {\cdot }\alpha ,\phi _\tau {\cdot }\beta ))] . \end{aligned}$$

Since $\phi _\sigma {\cdot }\alpha \in [\![\sigma ]\!]$ is almost negative by (P6), we have $\psi _0$ such that $\psi _0{\downarrow }_1$ and

$$\begin{aligned} \forall \alpha [ {\phi _\sigma {\cdot }\alpha \in [\![ \sigma ]\!] } \rightarrow {{\psi _0|\alpha }{\downarrow }\wedge \phi _\tau {\cdot }(\psi _0|\alpha ) \in [\![ \tau ]\!] \wedge [\![B]\!] (\phi _\sigma {\cdot }\alpha ,\phi _\tau {\cdot }(\psi _0|\alpha ))} ], \end{aligned}$$

by $\mathrm {GC}$. Therefore

$$\begin{aligned}&\forall a \in [\![ \sigma ]\!] [ {\phi _\sigma {\cdot }(\chi _\sigma {\cdot }a) \in [\![ \sigma ]\!] } \\&\quad \rightarrow {\psi _0|(\chi _\sigma {\cdot }a)}{\downarrow }\wedge \phi _\tau |(\psi _0|(\chi _\sigma {\cdot }a)) \in [\![ \tau ]\!] \wedge [\![ B ]\!] (\phi _\sigma {\cdot }(\chi _\sigma {\cdot }a),\phi _\tau {\cdot }(\psi _0|(\chi _\sigma {\cdot }a))) ] , \end{aligned}$$

and so

$$\begin{aligned} \forall a\in [\![ \sigma ]\!] [ {\psi _0|(\chi _\sigma {\cdot }a)}{\downarrow }\wedge \phi _\tau {\cdot }(\psi _0|(\chi _\sigma {\cdot }a)) \in [\![ \tau ]\!] \wedge [\![B]\!] (a,\phi _\tau {\cdot }(\psi _0|(\chi _\sigma {\cdot }a))) ] , \end{aligned}$$

by (P8). Take $\psi _1\equiv \varLambda ^{[\tau ]}a. \phi _{\tau }\cdot (\psi _0|(\chi _{\sigma }\cdot a))$. Then $\psi _1{\downarrow }_1$ by $\forall \alpha \in [\![\sigma ]\!] (\psi _1|(\chi _{\sigma }{\cdot }\alpha ){\downarrow }_1)$ and by $\forall \delta ((\phi _{\sigma }{\cdot }\delta ){\downarrow }_{[\sigma ]})$. Hence we have $\psi _1\in [\![\sigma \rightarrow \tau ]\!] \wedge (\forall z\in [\![\sigma ]\!] )[\![B]\!] (a,\psi _1{\cdot }a)$, which implies

$$\begin{aligned} (\exists \beta \in [\![ \sigma \rightarrow \tau ]\!] ) (\forall a \in [\![ \sigma ]\!] ) [\![ B ]\!] (a,\beta {\cdot }a) , \end{aligned}$$

by (P9). Note that, since $\beta {\cdot }a=[\![z^{\sigma \rightarrow \tau }x^{\sigma }]\!] [[\![z]\!] /\beta , [\![x]\!] /a]$, this is equivalent to

$$\begin{aligned}{}[\![\exists z^{\sigma \rightarrow \tau }\forall x^\sigma B(x, zx)]\!] , \end{aligned}$$

in $\mathbf {EL}^*$ by (P5) and (P7). The rest of the proof is easy by (P3) and (P7). $\square$

Proposition 36

For each instance A of $\mathrm {DC}_\sigma$ in $\mathscr {L}(\mathbf {HA}^\omega )$,

$$\begin{aligned} \mathbf {EL}^*+ \mathrm {GC}\vdash [\![ A ]\!] . \end{aligned}$$

Proof

Let

$$\begin{aligned} \forall x^\sigma \exists y^\sigma B(x,y)\rightarrow \forall x^\sigma \exists z^{0\rightarrow \sigma }(z0=x\wedge \forall w^0B(zw, z(w+1))) \end{aligned}$$

be an instance of $\mathrm {DC}_\sigma$, and suppose that $(\forall a\in [\![\sigma ]\!] )(\exists b\in [\![\sigma ]\!] )[\![B]\!] (a,b)$. As in the proof of Proposition 35, there exists $\beta$ such that

$$\begin{aligned} \beta \in [\![\sigma \rightarrow \sigma ]\!] \wedge \forall a\in [\![\sigma ]\!] [\![B]\!] (a, \beta {\cdot }a). \end{aligned}$$

For each $a\in [\![\sigma ]\!]$, let $\chi \equiv \lambda w. [\![{{\varvec{r}}}^\sigma ]\!] (a,\beta , w)$ if $[\sigma ]\equiv 0$, and $\chi \equiv \lambda w. [\![{{\varvec{r}}}^\sigma ]\!] |a|\beta |(\lambda v. w)$, otherwise. Then, by induction on w, we can show that

$$\begin{aligned} \chi \in [\![0\rightarrow \sigma ]\!] \wedge \chi {\cdot }0=a\wedge \forall w[\chi \cdot w{\downarrow }_{[\sigma ]}\wedge [\![B]\!] (\chi {\cdot }w, \chi {\cdot }(w+1))], \end{aligned}$$

which implies

$$\begin{aligned}{}[\![\exists \alpha ^{0\rightarrow \sigma }(\alpha {\cdot }0=a\wedge \forall w B(\alpha {\cdot }w, \alpha {\cdot }(w+1)))]\!] , \end{aligned}$$

in $\mathbf {EL}^*$. $\square$

Corollary 37

$\mathbf{S}\vdash A$ implies $\mathbf {EL}^*+\mathrm {BI}_\mathrm{M}+\mathrm {MP}+\mathrm {GC}\vdash [\![A]\!]$ for any sentence A in $\mathscr {L}(\mathbf {HA}^{\omega })$.

Proof

It is trivial that $\exists x(x\in [\![0]\!] )$. By induction on types, we can also prove that $\exists \alpha (\alpha \in [\![\sigma ]\!] )$ for any type $\sigma \not \equiv 0$. Using this fact, we can prove that $\mathbf {HA}^{\omega }+\varGamma \vdash A$ yields $\mathbf {EL}^*+\{ [\![B^c]\!] :B\in \varGamma \}\vdash A^c$ by induction on derivations, where $B^c$ is the universal closure of B. The rest of the proof follows from Corollary 31, Lemmas 32, 35 and 36. $\square$

Note that we can prove Propositions 35 and 36 for any interpretation and terms $\phi _\sigma$ and $\chi _\sigma$ satisfying (P3) and (P6)–(P9).

3.3 Combining with the functional realizability interpretation

In this subsection, we interpret $\mathbf {EL}^*+\mathrm {BI}_\mathrm{M}+\mathrm {MP}+\mathrm {GC}$ into $\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}$, using Kleene’s function realizability [4, §5.1] or $r^1$-realizability in [7, 3.3.1–3.3.13]. By combining Troelstra’s characterization theorem and the self-realizability of $\mathrm {BI}!$, we show that $\mathbf {EL}+\mathrm {BI}_\mathrm{M}+\mathrm {MP}+\mathrm {GC}$ is consistent relative to $\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}$ and so is $\mathbf{S}$ to $\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}$.

Take a mapping $\mathtt {s}$ from the set of formulae in $\mathscr {L}(\mathbf {EL}^*)$ to the one of formulae in $\mathscr {L}(\mathbf {EL})$ satisfying the condition in Definition 17. For each schema ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL})$ and formulae $\vec {A}$ in $\mathscr {L}(\mathbf {EL}^*)$, $\mathbf {EL}$ proves $\mathtt {s}({\varvec{\alpha }}[\vec {\nu }/\vec {A}])\leftrightarrow {\varvec{\alpha }}[\vec {\nu }/\vec {\mathtt {s}(A)}]$, i.e., each instance of a schema ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL}^*)$ is mapped into an instance of the same ${\varvec{\alpha }}$ in $\mathscr {L}(\mathbf {EL})$. Therefore, $\mathbf {EL}^*+\mathrm {BI}_\mathrm{M}+\mathrm {MP}+\mathrm {GC}\vdash A$ yields

$$\begin{aligned} \mathbf {EL}+\{\mathtt {s}(B):B\text { is an instance of }\mathrm {BI}_\mathrm{M}, \mathrm {MP}\text { or } \mathrm {GC}\text { in }\mathscr {L}(\mathbf {EL}^*)\} \vdash \mathtt {s}(A), \end{aligned}$$

which is equivalent to, by Proposition 30,

$$\begin{aligned} \mathbf {EL}+\mathrm {BI}_\mathrm{M}+\mathrm {MP}+\{\mathtt {s}(B):B\text { is an instance of }\mathrm {GC}\text { in }\mathscr {L}(\mathbf {EL}^*)\} \vdash \mathtt {s}(A). \end{aligned}$$

Following the literature on the functional realizability interpretation such as [7], we write $\mathbf {EL}+\varDelta +\varGamma \vdash A$ if $\mathbf {EL}+\varDelta +\{ \mathtt {s}(B):B\in \varGamma \}\vdash \mathtt {s}(A)$, for a set $\varDelta$ of formulae in $\mathscr {L}(\mathbf {EL})$, a set $\varGamma$ of formulae in $\mathscr {L}(\mathbf {EL}^*)$ and a formula A in $\mathscr {L}(\mathbf {EL}^*)$.

Definition 38

(Kleene’s function realizability, [4, §5.1]) For each formula A and a functional variable $\alpha$, define a formula $\alpha {\mathbf{r}} A$ in $\mathscr {L}(\mathbf {EL}^*)$ as follows:

$$\begin{aligned}&\alpha {\mathbf{r}} A\equiv A \;\text { for prime }A\text { in }\mathscr {L}(\mathbf {EL}); \\&\alpha {\mathbf{r}} B\wedge C\equiv (\alpha )_0 {\mathbf{r}} B \wedge (\alpha )_1{\mathbf{r}} C; \\&\alpha {\mathbf{r}} B\vee C\equiv ((\alpha )_0(0)=0\rightarrow (\alpha )_1{\mathbf{r}} B)\wedge ((\alpha )_0(0)\ne 0\rightarrow (\alpha )_1{\mathbf{r}} C); \\&\alpha {\mathbf{r}} B\rightarrow C \equiv \forall \beta (\beta \mathbf{r}B \rightarrow a|b{\downarrow }\wedge \alpha |\beta {\mathbf{r}} C); \\&\alpha {\mathbf{r}} \forall x^0\mathbf{r}B(x) \equiv \forall x((\alpha |\lambda y. x){\downarrow }\wedge (\alpha |\lambda y. x){\mathbf{r}} B(x)); \\&\alpha {\mathbf{r}} \exists x^0 B(x) \equiv (\alpha )_1 {\mathbf{r}} B((\alpha )_0(0)); \\&\alpha {\mathbf{r}} \forall x^1{\mathbf{r}} B(x) \equiv \forall \beta ^1(\alpha |\beta {\downarrow }\wedge \alpha |\beta {\mathbf{r}} B(\beta )); \\&\alpha {\mathbf{r}} \exists x^1 B(x) \equiv (\alpha )_1 {\mathbf{r}} B((\alpha )_0). \end{aligned}$$

The bar induction for decidable bars ($\mathrm {BI}_\mathrm{D}$) is given as follows (cf. [7, 1.9.20]):

$$\begin{aligned}&[\forall \alpha \exists xC(\overline{\alpha }x)\wedge \forall x(C(x)\vee \lnot C(x))\wedge \forall x(C(x)\rightarrow D(x))\wedge \\&\quad \forall x(\forall yD(x*\langle y\rangle )\rightarrow D(x))] \rightarrow D(\langle \rangle ). \end{aligned}$$

Lemma 39

$\mathrm {BI}_\mathrm{M}$ and $\mathrm {BI}_\mathrm{D}$ are equivalent over $\mathbf {EL}+\mathrm {GC}$.

Proof

In [9, Ch.4.8.13], it is proved that $\mathrm {BI}_\mathrm{M}$ and $\mathrm {BI}_{D}$ are equivalent over $\mathbf {EL}+\mathrm {C}\text {-}\mathrm {N}$. Since $\mathbf {EL}+\mathrm {GC}$ implies $\mathrm {C}\text {-}\mathrm {N}$ by Proposition 32, we have the desired equivalence. $\square$

Lemma 40

$\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}+\mathrm {GC}\vdash A$ if and only if $\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}\vdash \exists \alpha (\alpha \mathbf{r}A)$.

Proof

Note that $\mathrm {MP}$ is almost negative. Then $\mathbf {EL}+\mathrm {MP}\vdash \exists \alpha (\alpha \mathbf{r}A)$ for each instance A of $\mathrm {MP}$, by [7, 3.3.8 Lemma]. A variant $\mathrm {BI}!$ of $\mathrm {BI}_\mathrm{D}$ is given by replacing $\exists$ with $\exists !$ in $\mathrm {BI}_\mathrm{D}$. By the self-realizability of $\mathrm {BI}!$ [7, 3.3.4 Theorem and Remark], we have that $\mathbf {EL}+\mathrm {BI}!\vdash \exists \alpha (\alpha \mathbf{r}A)$ for each instance A of $\mathrm {BI}!$.

Therefore we have

$$\begin{aligned} \mathbf {EL}+\mathrm {BI}!+\mathrm {MP}\vdash A\Longrightarrow \mathbf {EL}+\mathrm {BI}!+\mathrm {MP}\vdash \exists \alpha (\alpha \mathbf{r}A), \end{aligned}$$

by [7, 3.3.3 Corollary (ii)]. Thus we have

$$\begin{aligned} \mathbf {EL}+\mathrm {BI}!+\mathrm {MP}+\mathrm {GC}\vdash A \Longleftrightarrow \mathbf {EL}+\mathrm {BI}!+\mathrm {MP}\vdash \exists \alpha (\alpha \mathbf{r}A) \end{aligned}$$

for each formula A in $\mathscr {L}(\mathbf {EL})$, by Troelstra’s characterization theorem [7, 3.3.11 Theorem (ii)].

Since it is easy to see that $\mathrm {BI}!$ is equivalent to $\mathrm {BI}_\mathrm{D}$ over $\mathbf {EL}$ by replacing C(x) with $C(x)\wedge (\forall y<|x|)\lnot C(\overline{x}y)$ in $\mathrm {BI}_\mathrm{D}$, the above implies

$$\begin{aligned} \mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}+\mathrm {GC}\vdash A \Longleftrightarrow \mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}\vdash \exists \alpha (\alpha \mathbf{r}A). \end{aligned}$$

$\square$

Corollary 41

$\mathbf {EL}+\mathrm {BI}_\mathrm{M}+\mathrm {MP}+\mathrm {GC}\vdash A$ if and only if $\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}\vdash \exists a^1(a\mathbf{r}A)$.

Finally, we have the following:

Theorem 42

$\mathbf{S}\vdash A$ implies $\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}\vdash \exists \alpha (\alpha \mathbf{r}[\![A]\!] )$, for any sentence A in $\mathscr {L}(\mathbf {HA}^{\omega })$.

Proof

By Corollaries 37 and 41. $\square$

Corollary 43

$\mathbf{S}$ is consistent relative to $\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}$.

In $\mathbf{ZF}$, the standard structure ${\mathbf {N}}^{{\mathbf {N}}}\cup {\mathbf {N}}$ is a model of $\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}$. Therefore $\mathbf {EL}+\mathrm {BI}_\mathrm{D}+\mathrm {MP}$ is consistent, and so is $\mathbf{S}$. Thus, we have the following by the Corollary 8.

Theorem 44

• 1. $\mathbf{S}$ is not closed under $\mathrm {IPR}^\omega$, and so it does not derive $\mathrm {IP}^\omega$.

• 2. $\mathbf {HA}^\omega +\mathrm {BI}_\mathrm{M}+\mathrm {C}\text {-}\mathrm {N}+\mathrm {AC}+\mathrm {DC}$ derives neither $\mathrm {IP}^\omega$ nor $\mathrm {MP}$.