1 Introduction
Recursive realizability introduced by Kleene [Reference Kleene4] can be considered as an interpretation of the informal intuitionistic meaning of arithmetical sentences on the basis of the theory of recursive functions. The main idea of recursive realizability is to replace the vague intuitionistic concept of an effective operation by the exact notion of a partial recursive function. On the other hand, many other more restrictive classes of computable functions are studied in mathematics. It is of interest to consider variants of realizability based on subrecursive classes of functions. One of them is the class of primitive recursive functions.
Damnjanovic [Reference Damnjanovic2] introduced the notion of strictly primitive recursive realizability for the language of formal arithmetic. This kind of realizability combines the ideas of recursive realizability and Kripke models. Strictly primitive recursive realizability can be considered as a kind of constructive semantics of arithmetical sentences. For any semantics, it is of interest to study the corresponding logic. The predicate logic of Kleene’s recursive realizability was considered by the author. It was proved that the set of recursively realizable predicate formulas is not arithmetical [Reference Plisko11].
A similar result for the strictly primitive recursive realizability was obtained by Park [Reference Park7]. His proof of the nonarithmeticity of the predicate logic of strictly primitive recursive realizability is essentially based on the claim [Reference Damnjanovic2] that every predicate formula deducible in the intuitionistic predicate calculus is strictly primitive recursively realizable (Lemma 4.3 and Theorem 5.1). Later this claim was disproved by the author [Reference Plisko, Grigoriev, Harrison and Hirsch8, Reference Plisko10]. Nevertheless the result of Park remains valid. The aim of this paper is to present a correct proof of this result.
Another primitive recursive realizability was introduced by Salehi [Reference Salehi12], which was compared with the strictly primitive recursive realizability of Damnjanovic in [Reference Plisko, Grigoriev, Harrison and Hirsch8–Reference Plisko10]. It was proved that there exists an arithmetical formula that is primitive recursively realizable, in the sense of [Reference Salehi12], but not strictly primitive recursively realizable, in the sense of [Reference Damnjanovic2]; while its negation is strictly primitive recursively realizable but not primitive recursively realizable.
2 Indexing of primitive recursive functions
Definition 2.1.
Primitive recursive functions are obtained by substitution and recursion from the basic functions
$O(x)=0$
,
$S(x)=x+1$
,
$I^m_i(x_1,\ldots ,x_m)=x_i$
(
$m =1,2,\ldots $
;
$1\le i\le m$
).
Definition 2.2. The class of elementary functions is the least class containing the functions
$x\mapsto 1$
,
$I^m_i$
,
$+$
,
$\div $
, where
$x\div y=\begin {cases} 0 & \text {if}\ x<y,\\ x-y & \text {if}\ x\ge y, \end {cases}$
and closed under substitution, summation
$(\mathbf x,y)\mapsto \sum \limits _{i=0}^y\psi (\mathbf x,i),$
and multiplication
$(\mathbf x,y)\mapsto \prod \limits _{i=0}^y\psi (\mathbf x,i),$
$\mathbf x$
being the list
$x_1,\ldots ,x_m$
.
If
$a_0,a_1,\ldots ,a_n$
are natural numbers, then
$\langle a_0,a_1,\ldots ,a_n\rangle $
denotes the number
$p_0^{a_0}\cdot p_1^{a_1}\cdot \ldots \cdot p_n^{a_n}$
, where
$p_0,p_1,\ldots ,p_n$
are sequential prime numbers (
$p_0=2$
,
$p_1=3$
,
$p_2 =5,\ldots $
). The functions
$\pi (i)=p_i$
and
$(x,y)\mapsto \langle x,y\rangle $
are elementary. In what follows, for
$a\ge 1$
and
$i\ge 0$
, let
$[a]_i$
denote the exponent of
$p_i$
under decomposition of a into prime factors. Therefore,
$[a]_i = a_i$
if
$a=\langle a_0,\ldots ,a_n\rangle $
. For definiteness, let
$[0]_i =0$
for every i. Note that the function
$(x,i)\mapsto [x]_i$
is elementary.
Definition 2.3. An
$(m+1)$
-ary function f is obtained by bounded recursion from an m-ary function g, an
$(m+2)$
-ary function h, and an
$(m+1)$
-ary function j if the following conditions are fulfilled for any
$x_1,\ldots ,x_m,y$
:
$$ \begin{align*}f(0,x_1,\ldots,x_m)= g(x_1,\ldots,x_m),\end{align*} $$
$$ \begin{align*}f(y+1,x_1,\ldots,x_m)= h(y,f(y,x_1,\ldots,x_m),x_1,\ldots,x_m),\end{align*} $$
$$ \begin{align*}f(y,x_1,\ldots,x_m)\le j(y,x_1,\ldots,x_m).\end{align*} $$
Thus f is obtained by bounded recursion from
$g,h,j$
if f is obtained by primitive recursion from
$g,h$
and is bounded by j.
For given functions
$\theta _1,\ldots ,\theta _k$
, let
${\mathbf E}[\theta _1,\ldots ,\theta _k]$
be the least class containing
$\theta _1,\ldots ,\theta _k$
, S,
$I^m_i$
, the constant functions and closed under substitution and bounded recursion. Consider the following sequence of functions:
$$ \begin{align*}f_0(x,y)= y+1,\end{align*} $$
$$ \begin{align*}f_1(x,y)= x+ y,\end{align*} $$
$$ \begin{align*}f_2(x,y)=(x+1)\cdot(y+1),\end{align*} $$
$$ \begin{align*}f_{n+1}(0,y) = f_n(y+1,y+1),\end{align*} $$
$$ \begin{align*}f_{n+1}(x+1,y)=f_{n+1}(x,f_{n+1}(x,y)),\end{align*} $$
for
$n\ge 2$
. Grzegorczyk [Reference Grzegorczyk3] introduced a hierarchy of classes
${\mathcal E}^n$
, where
${\mathcal E}^n={\mathbf E}[f_n]$
. The class
${\mathcal E}^3$
contains all elementary functions. It was shown by Grzegorczyk [Reference Grzegorczyk3] that
$\bigcup \limits _{n=0}^\infty {\mathcal E}^n$
is exactly the class of primitive recursive functions.
Axt [Reference Axt1] has shown that in the definition of the classes
${\mathcal E}^n$
for
$n\ge 4$
, the usual bounded recursion can be replaced by the following scheme applicable to every triple of functions
$g,h,j$
of appropriate arities:
$$ \begin{align*}\left\{ \begin{array}{l} f(0,\mathbf x)= g(\mathbf x),\\ f(y+1,\mathbf x)= h(y,f(y,\mathbf x),\mathbf x)\cdot\mathsf{sg}(j(y,\mathbf x)\div f(y,\mathbf x))\cdot\mathsf{sg}(f(y,\mathbf x)), \end{array}\right. \end{align*} $$
where
$\mathsf {sg}(x)=\begin {cases} 0 & \text {if}\ x=0,\\ 1 & \text {if}\ x>0. \end {cases}$
For any collection of functions
$\Theta =\{\theta _1,\ldots ,\theta _m\}$
, let
${\mathbf E}^4[\Theta ]$
be the least class including
$\Theta $
, containing S, the constant functions,
$I^m_i$
,
$\mathsf {sg}$
,
$\div $
,
$f_4$
and closed under substitution and Axt’s bounded recursion. A way of indexing the functions which are primitive recursive relative to
$\theta _1,\ldots ,\theta _m$
is proposed in [Reference Kleene6]. It can be adapted to an indexing of the class
${\mathbf E}^4[\Theta ]$
. The functions in
${\mathbf E}^4[\Theta ]$
get indexes according to their definition from the initial functions by substitution and Axt’s bounded recursion. We list below the possible defining schemes for a function
$\varphi $
and indicate on the right its index.
$$ \begin{align*}\begin{array}{ccc} (\,) & \varphi(x_1,\ldots,x_{k_i})=\theta_i(x_1,\ldots,x_{k_i}) & \langle0,k_i,i\rangle,\\ (\mathrm{I}) & \varphi(x)=x+1 & \langle1,1\rangle,\\ (\mathrm{II}) & \varphi(x_1,\ldots,x_n)=q & \langle2,n,q\rangle,\\ (\mathrm{III}) & \varphi(x_1,\ldots,x_n)=x_i\mbox{ (where }1\le i\le n) & \langle3,n,i\rangle,\\ (\mathrm{IV}) & \varphi(x)=\mathsf{sg}(x) & \langle4,1\rangle,\\ (\mathrm{V}) & \varphi(x,y)=x\div y & \langle5,2\rangle,\\ (\mathrm{VI}) & \varphi(x,y)=f_4(x,y) & \langle6,2\rangle,\\ (\mathrm{VII}) & \varphi(\mathbf x)= \psi(\chi_1(\mathbf x),\ldots,\chi_k(\mathbf x)) & \langle7,m,g,h_1,\ldots,h_k\rangle,\\ (\mathrm{VIII}) & \left\{ \begin{array}{l} \varphi(0,\mathbf x)=\psi(\mathbf x)\\ \varphi(y+1,\mathbf x)=\chi(y,f(y,\mathbf x),\mathbf x)\cdot\\ \cdot\mathsf{sg}(\zeta(y,x)\div\varphi(y,\mathbf x))\cdot\mathsf{sg}(\varphi(y,\mathbf x)) \end{array} \right. & \langle8,m+1,g,h,j\rangle. \end{array}\end{align*} $$
Here
$\mathbf x$
is the list
$x_1,\ldots ,x_m$
and
$g,h_1,\ldots ,h_k,h,j$
are indexes of the functions
$\psi ,\chi _1,\ldots ,\chi _k,\chi ,\zeta $
respectively.
Let
$In^\Theta (b)$
mean that b is an index of a function in the class
${\mathbf E}^4[\Theta ]$
. It is shown in [Reference Axt1] that
$In^\Theta (b)$
is an elementary predicate. If
$In^\Theta (b)$
holds, then
$\mathsf {ef}^\Theta _b$
denotes a
$[b]_1$
-ary function in
${\mathbf E}^4[\Theta ]$
indexed by b. Following [Reference Axt1], we set
$$ \begin{align*}\mathsf{ef}^\Theta(b,a)=\begin{cases} \mathsf{ef}^\Theta_b([a]_0,\ldots,[a]_{[b]_1\div1}) & \text{if}\ In^\Theta(b),\\ 0 & \text{else}. \end{cases}\end{align*} $$
The function
$\mathsf {ef}^\Theta $
is universal for the class
${\mathbf E}^4[\Theta ]$
and is not in this class. Following [Reference Axt1], a binary function
$\mathsf {e}_n$
is defined inductively as follows:
$$ \begin{align*}\mathsf{e}_0(b,a)=0,\;\mathsf{e}_{n+1}(b,a)=\mathsf{ef}^{[\mathsf{e}_0,\ldots,\mathsf{e}_n]}(b,a).\end{align*} $$
Finally, the class
${\mathbf E}_n$
is defined as
${\mathbf E}^4[\mathsf {e}_0,\ldots ,\mathsf {e}_n]$
. It is proved (see [Reference Axt1]) that for any
$n\ge 0$
,
${\mathbf E}_n={\mathcal E}^{n+4}$
.
Let
$In(n,b)$
mean that b is an n-index, i.e., an index of a function in
${\mathbf E}_n$
. It is shown in [Reference Axt1] that the predicate
$In(n,b)$
is elementary. It follows immediately from the definition of the indexing that
$In(n,b)$
and
$m>n$
imply
$In(m,b)$
. Note that if an n-index b of a function
$\varphi (\mathbf x)$
is given, then for any
$\mathbf m$
, we can compute the value
$\varphi (\mathbf m)$
. Indeed, computing the value
$\varphi (\mathbf x)$
is reduced to computing the values of a finite number of functions whose indexes are less than b. Thus the process of computing should be terminated.
Notation. If n is a natural number, then
$\Lambda x.n$
will denote the number
$\langle 2,1,n\rangle $
,
$\mathsf a_k$
will denote the number
$\Lambda j.\Lambda x.k$
, and
$\mathsf a$
will denote the number
$\mathsf a_0$
. Thus
$\Lambda x.n$
is a 0-index of the constant function
$x\mapsto n$
,
$\mathsf a_k$
is a 0-index of the function
$x\mapsto \Lambda x.k$
, and
$\mathsf a$
is a 0-index of the function
$x\mapsto \Lambda x.0$
.
3 Strictly primitive recursively realizable arithmetical formulas
We consider arithmetical sentences in a purely predicate language. Namely, the language of formal arithmetic
$Ar$
is a first-order language without any functional symbols and individual constants consisting of a unary predicate symbol Z, binary predicate symbols E and S, and ternary predicate symbols A and M. In the standard model of arithmetic
$\mathfrak N$
these predicate symbols have the following meaning:
$Z(x)$
means
$x=0$
,
$E(x,y)$
means
$x=y$
,
$S(x,y)$
means
$x+1=y$
,
$A(x,y,z)$
means
$x+y=z$
, and
$M(x,y,z)$
means
$x\cdot y=z$
. Besides, we consider an extended arithmetical language
$Ar^*$
obtained by adding to
$Ar$
individual constants
$0,1,2,\ldots $
for all natural numbers.
$Ar$
-formulas and
$Ar^*$
-formulas are built from atomic ones by means of the connectives
$\&$
,
$\lor $
,
$\to $
,
$\neg $
and the quantifiers
$\forall $
,
$\exists $
. The expression
$\Phi \equiv \Psi $
is an abbreviation for the formula
$(\Phi \to \Psi )\,\&\,(\Psi \to \Phi )$
. If a formula A does not contain any free variables except
$x_1,\ldots ,x_n$
, we denote this formula
$A(x_1,\ldots ,x_n)$
. In this case,
$A(k_1,\ldots ,k_n)$
denotes the
$Ar^*$
-formula obtained from A by substituting the constants
$k_1,\ldots ,k_n$
for
$x_1,\ldots ,x_n$
respectively. For brevity, we sometimes write
$\forall \mathbf x$
instead of
$\forall x_1\ldots \forall x_n$
and
$\exists \mathbf x$
instead of
$\exists x_1\ldots \exists x_n$
, where
$\mathbf x$
is the list of variables
$x_1,\ldots ,x_n$
.
We say that a closed
$Ar^*$
-formula
$\Phi $
is true iff
$\mathfrak N\models \Phi $
in the usual classical sense.
The notion of strictly primitive recursive realizability for arithmetical formulas is introduced by Damnjanovic [Reference Damnjanovic2]. The relation “a natural number e strictly primitive recursively realizes a closed
$Ar^*$
-formula A at level n” (
$e\Vdash _nA$
) is defined by induction on the number of logical symbols in A.
-
1) If A is an atomic formula, then
$e\Vdash _nA$
means that
$e=0$
and A is true. -
2) If A is
$B\,\&\,C$
, then
$e\Vdash _nA$
means that
$[e]_0\Vdash _nB$
and
$[e]_1\Vdash _nC$
. -
3) If A is
$B\lor C$
, then
$e\Vdash _nA$
means that either
$[e]_0=0$
and
$[e]_1\Vdash _nB$
or
$[e]_0\not =0$
and
$[e]_1\Vdash _nC$
. -
4) If A is
$B\to C$
, then
$e\Vdash _nA$
means that
$In(n,e)$
holds and for any
$j\ge n$
,
$In(j,\mathsf {e}_{n+1}(e,\langle j\rangle ))$
holds, and for any y, if
$y\Vdash _jB$
, then
$\mathsf {e}_{j+1}(\mathsf {e}_{n+1}(e,\langle j\rangle ),\langle y\rangle )\Vdash _jC$
. -
5) If A is
$\neg B$
, then
$e\Vdash _nA$
means that
$e\Vdash _n(B\to E(0,1))$
. -
6) If A is
$\exists x\,B(x)$
, then
$e\Vdash _nA$
means that
$[e]_1\Vdash B([e]_0)$
. -
7) If A is
$\forall x\,B(x)$
, then
$e\Vdash _nA$
means that
$In(n,e)$
holds and for any m,
$\mathsf {e}_{n+1}(e,\langle m\rangle )\Vdash _nB(m)$
.
A closed
$Ar^*$
-formula A is called strictly primitive recursively realizable (spr-realizable) iff there are e and n such that
$e\Vdash _nA$
. It is proved in [Reference Damnjanovic2] that
$e\Vdash _mA$
if
$e\Vdash _nA$
and
$m\ge n$
. Since any closed
$Ar$
-formula is a closed
$Ar^*$
-formula, it follows that the notion of strictly primitive recursive realizability is defined for closed
$Ar$
-formulas too.
The following properties of spr-realizability immediately follow from the definition.
Proposition 3.4. For any closed
$Ar^*$
-formulas A and B,
-
1)
$A\,\&\,B$
is spr-realizable iff A and B are both spr-realizable; -
2)
$A\lor B$
is spr-realizable iff at least one of A, B is spr-realizable; -
3) if A is spr-realizable and B is not spr-realizable, then
$A\to B$
is not spr-realizable; -
4) if
$k\Vdash _nB$
, then
$\mathsf a_k\Vdash _n(A\to B)$
(see Notation); -
5) if A is not spr-realizable, then for any k,
$\mathsf a_k\Vdash _0(A\to B)$
; -
6) if
$\neg A$
is spr-realizable, then
$\mathsf a\Vdash _0\neg A$
.
Proof. The statements 1)–3) are obvious.
4) Suppose
$k\Vdash _nB$
. Then
$k\Vdash _jB$
for any
$j\ge n$
. We prove that
$\mathsf a_k\Vdash _n(A\to B)$
, i.e., that (a)
$In(n,\mathsf a_k)$
holds, (b)
$In(j,\mathsf e_{n+1}(\mathsf a_k,\langle j\rangle ))$
holds for any
$j\ge n$
, and (c) for any
$j\ge n$
and any y, if
$y\Vdash _jA$
, then
$\mathsf e_{j+1}(\mathsf e_{n+1}(\mathsf a_k,\langle j\rangle ),\langle y\rangle )\Vdash _jB$
. Note, that
$\Lambda x.k$
is a
$0$
-index of the constant function with the only value k and
$\mathsf a_k$
is a
$0$
-index of the constant function whose only value is
$\langle 2,1,k\rangle $
. Thus the conditions (a) and (b) are fulfilled. The condition (c) is also obvious, because for any j and y, we have
$\mathsf e_{j+1}(\mathsf e_{n+1}(\mathsf a_k,\langle j\rangle ),\langle y\rangle )=\mathsf e_{j+1}(\Lambda x.k,\langle y\rangle )=k$
, and
$k\Vdash _jB$
.
5) Assume that A is not spr-realizable. This means that for any
$y,j$
, the condition
$y\Vdash _jA$
does not hold. We have to prove that
$\mathsf a_k\Vdash _0(A\to E(0,1))$
. It was shown above that
$In(0,\mathsf a_k)$
holds and for any j,
$In(j,\mathsf e_{1}(\mathsf a_k,\langle j\rangle ))$
holds. Thus it is enough to prove that for any y,
$y\Vdash _jA\Rightarrow \mathsf e_{j+1}(\mathsf e_{1}(\mathsf a_k,\langle j\rangle ),\langle y\rangle )\Vdash _jB$
, but this is obvious because the premise is false.
The statement 6) follows from 5) because A is not spr-realizable if
$\neg A$
is spr-realizable.□
Proposition 3.5. Suppose that an
$Ar^*$
-formula
$A(x,y)$
is such that for any m and n, the
$Ar^*$
-formula
$\neg A(m,n)$
is spr-realizable. Then the formula
$\forall x\forall y\,\neg A(x,y)$
is spr-realizable at level
$0$
.
Proof. For any m and n, if
$\neg A(m,n)$
is spr-realizable, then by Proposition 3.4,
$\mathsf a\Vdash _0\neg A(m,n)$
. We show that
$\Lambda x.\Lambda y.\mathsf a\Vdash _0\forall x\forall y\,\neg A(x,y)$
, i.e.,
$In(0,\Lambda x.\Lambda y.\mathsf e)$
holds (this is obvious) and for any m,
$\mathsf e_1(\Lambda x.\Lambda y.\mathsf a,\langle m\rangle )\Vdash _0\forall y\,\neg A(m,y)$
. Note that
$\mathsf e_1(\Lambda x.\Lambda y.\mathsf a,\langle \ m\rangle )=\Lambda y.\mathsf a$
. Thus we have to prove that
$\Lambda y.\mathsf a\Vdash _0\forall y\,\neg A(m,y)$
, i.e.,
$In(0,\Lambda y.\mathsf a)$
holds (this is evident) and for any n,
$\mathsf e_1(\Lambda y.\mathsf a,\langle n\rangle \Vdash _0\neg A(m,n)$
. This is also evident because
$\mathsf e_1(\Lambda y.\mathsf a,\langle n\rangle )=\mathsf a$
.□
Definition 3.6. An
$Ar^*$
-formula
$\Phi $
will be called completely negative iff it does not contain logical symbols
$\lor $
and
$\exists $
and every atom
$\Psi $
occurs in
$\Phi $
only in subformulas of the form
$\neg \Psi $
.
An inductive definition of a completely negative
$Ar^*$
-formula is the following:
-
• if
$\Phi $
is an atomic
$Ar^*$
-formula, then
$\neg \Phi $
is completely negative; -
• if
$\Phi $
and
$\Psi $
are completely negative
$Ar^*$
-formulas, then
$\neg \Phi $
,
$(\Phi \,\&\,\Psi )$
, and
$(\Phi \to \Psi )$
are completely negative; -
• if
$\Phi $
is a completely negative
$Ar^*$
-formula and x is an individual variable, then
$\forall x\,\Phi $
is completely negative.
Proposition 3.7. If
$A(x_1,\ldots ,x_n)$
is a completely negative
$Ar^*$
-formula, then there exists a natural number
$n_A$
such that for any natural numbers
$k_1,\ldots ,k_n$
, the following conditions are equivalent:
-
1) the formula
$A(k_1,\ldots ,k_n)$
is true; -
2)
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
; -
3) the formula
$A(k_1,\ldots ,k_n)$
is spr-realizable.
Proof. We construct the number
$n_A$
inductively. Obviously, it is enough to verify two conditions:
-
(i)
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
iff the formula
$A(k_1,\ldots ,k_n)$
is true; -
(ii) if the formula
$A(k_1,\ldots ,k_n)$
is spr-realizable, then
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
.
If
$A(x_1,\ldots ,x_n)$
is of the form
$\neg \Phi (x_1,\ldots ,x_n)$
for an atomic formula
$\Phi $
, let
$n_A=\mathsf a$
. We now verify the item (i). Assume that
$\mathsf a\Vdash _0\neg \Phi (k_1,\ldots ,k_n)$
. Then the formula
$\Phi (k_1,\ldots ,k_n)$
is not spr-realizable. It follows from the definition of spr-realizability for atomic formulas that
$\Phi (k_1,\ldots ,k_n)$
is not true. Then the formula
$\neg \Phi (k_1,\ldots ,k_n)$
is true. Conversely, assume that the formula
$\neg \Phi (k_1,\ldots ,k_n)$
is true. Then
$\Phi (k_1,\ldots ,k_n)$
is not true. It follows from the definition of spr-realizability for atomic formulas that
$\Phi (k_1,\ldots ,k_n)$
is not spr-realizable. Then by Proposition 3.4,
$\mathsf a\Vdash _0\neg \Phi (k_1,\ldots ,k_n)$
. The item (ii) follows from Proposition 3.4
Suppose that for formulas
$B(x_1,\ldots ,x_n)$
and
$C(x_1,\ldots ,x_n)$
we have found the numbers
$n_B$
and
$n_C$
such that for any
$k_1,\ldots ,k_n$
, the following conditions hold:
-
(ib)
$n_B\Vdash _0B(k_1,\ldots ,k_n)$
iff the formula
$B(k_1,\ldots ,k_n)$
is true; -
(ic)
$n_C\Vdash _0C(k_1,\ldots ,k_n)$
iff the formula
$C(k_1,\ldots ,k_n)$
is true; -
(iib) if the formula
$B(k_1,\ldots ,k_n)$
is spr-realizable, then
$n_B\Vdash _0B(k_1,\ldots ,k_n)$
; -
(iic) if the formula
$C(k_1,\ldots ,k_n)$
is spr-realizable, then
$n_C\Vdash _0C(k_1,\ldots ,k_n)$
.
If
$A(x_1,\ldots ,x_n)$
is
$B(x_1,\ldots ,x_n)\,\&\,C(x_1,\ldots ,x_n)$
, let
$n_A=\langle n_B,n_C\rangle $
. We prove that
$n_A$
is a required number. Let us show the item (i). Assume that
$A(k_1,\ldots ,k_n)$
is true. Then
$B(k_1,\ldots ,k_n)$
and
$C(k_1,\ldots ,k_n)$
are both true. By (ib) and (ic), we have
$n_B\Vdash _0B(k_1,\ldots ,k_n)$
and
$n_C\Vdash _0C(k_1,\ldots ,k_n)$
. Then
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
by the definition of spr-realizability because
$[n_A]_0=n_B$
,
$[n_A]_1=n_C$
. Conversely, if
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
, then
$n_B\Vdash _0B(k_1,\ldots ,k_n)$
and
$n_C\Vdash _0C(k_1,\ldots ,k_n)$
by the definition of spr-realizability for the conjunction. In this case, by the items (ib) and (ic), the formulas
$B(k_1,\ldots ,k_n)$
and
$C(k_1,\ldots ,k_n)$
are both true; therefore,
$A(k_1,\ldots ,k_n)$
is also true.
We now prove the item (ii). Assume that
$A(k_1,\ldots ,k_n)$
is spr-realizable. Then
$B(k_1,\ldots ,k_n)$
and
$C(k_1,\ldots ,k_n)$
are spr-realizable. It follows from (iib) and (iic) that
$n_B\Vdash _0B(k_1,\ldots ,k_n)$
and
$n_C\Vdash _0C(k_1,\ldots ,k_n)$
. This gives
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
by the definition of spr-realizability.
If
$A(x_1,\ldots ,x_n)$
is
$B(x_1,\ldots ,x_n)\to C(x_1,\ldots ,x_n)$
, then we set
$n_A=\mathsf a_{n_C}$
and prove that
$n_A$
is a required number. Let us verify the item (i). Assume that the formula
$A(k_1,\ldots ,k_n)$
is true. Then either the formula
$B(k_1,\ldots ,k_n)$
is false or the formula
$C(k_1,\ldots ,k_n)$
is true. In the first case,
$B(k_1,\ldots ,k_n)$
is not spr-realizable. Indeed, suppose the opposite; then it should follow from (iib) that
$n_B\Vdash _0B(k_1,\ldots ,k_n)$
and by (ib),
$B(k_1,\ldots ,k_n)$
should be true. By Proposition 3.4,
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
. If
$C(k_1,\ldots ,k_n)$
is true, then by (ic),
$n_C\Vdash _0C(k_1,\ldots ,k_n)$
. By Proposition 3.4,
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
. Now assume that
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
. We prove that
$A(k_1,\ldots ,k_n)$
is true. Suppose the opposite. Then the formula
$B(k_1,\ldots ,k_n)$
is true and the formula
$C(k_1,\ldots ,k_n)$
is false. By (ib), the formula
$B(k_1,\ldots ,k_n)$
is spr-realizable. Therefore, the formula
$C(k_1,\ldots ,k_n)$
should be spr-realizable. But in this case, by the item (iic),
$n_C\Vdash _0C(k_1,\ldots ,k_n)$
and by (ic), the formula
$C(k_1,\ldots ,k_n)$
is true. This contradiction shows that the formula
$A(k_1,\ldots ,k_n)$
is true.
We now show the item (ii). Assume that
$A(k_1,\ldots ,k_n)$
is spr-realizable. In this case, if the formula
$B(k_1,\ldots ,k_n)$
is not spr-realizable, then by Proposition 3.4,
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
. If
$B(k_1,\ldots ,k_n)$
is spr-realizable, then
$C(k_1,\ldots ,k_n)$
is also spr-realizable. It follows from (iic) that
$n_C\Vdash _0C(k_1,\ldots ,k_n)$
. Then by Proposition 3.4,
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
.
The case when the formula
$A(x_1,\ldots ,x_n)$
is of the form
$\neg B(x_1,\ldots ,x_n)$
is reduced to the case of the implication
$B(x_1,\ldots ,x_n)\to E(0,1)$
. In this case we can set
$n_A=\mathsf a$
.
Finally, assume that
$A(x_1,\ldots ,x_n)$
is of the form
$\forall y\,B(y,x_1,\ldots ,x_n)$
and there is a number
$n_B$
such that for any natural numbers
$m,k_1,\ldots ,k_n$
, the following conditions are fulfilled:
-
(iB)
$n_B\Vdash _0B(m,k_1,\ldots ,k_n)$
iff the formula
$B(m,k_1,\ldots ,k_n)$
is true; -
(iiB) if
$B(m,k_1,\ldots ,k_n)$
is spr-realizable, then
$n_B\Vdash _0B(m,k_1,\ldots ,k_n)$
.
Let
$n_A=\Lambda x.n_B$
. Obviously,
$In(0,n_A)$
holds. We prove the item (i). Assume that the formula
$A(k_1,\ldots ,k_n)$
is true. Then for any m, the formula
$B(m,k_1,\ldots ,k_n)$
is true and by (iB),
$n_B\Vdash _0B(m,k_1,\ldots ,k_n)$
. Since
$\mathsf e_1(n_A,\langle m\rangle )=n_B$
, it follows that for any m,
$\mathsf e_1(n_A,\langle m\rangle )\Vdash _0B(m,k_1,\ldots ,k_n)$
. This means that
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
.
Conversely, suppose
$n_A\Vdash _0A(k_1,\ldots ,k_n)$
. Thus
$\mathsf e_1(n_A,\langle m\rangle )\Vdash _0B(m,k_1,\ldots ,k_n),$
i.e.,
$n_B\Vdash _0B(m,k_1,\ldots ,k_n)$
, for any m. By (iB), the formula
$B(m,k_1,\ldots ,k_n)$
is true for any m; therefore, the formula
$A(k_1,\ldots ,k_n)$
is true.
We now show the item (ii). Assume that
$A(k_1,\ldots ,k_n)$
is spr-realizable. Then for any m, the formula
$B(m,k_1,\ldots ,k_n)$
is spr-realizable and by the condition (iiB),
$n_B\Vdash _0B(m,k_1,\ldots ,k_n)$
. It follows that for any m,
$\mathsf e_1(n_A,\langle m\rangle )\Vdash _0B(m,k_1,\ldots ,k_n)$
. This means that
$n_A\Vdash _0A(y,k_1,\ldots ,k_n)$
what we wanted to prove.□
Proposition 3.8. Suppose that
$A(\mathbf x)$
is an
$Ar*$
-formula of the form
$\exists \mathbf y\,\Psi (\mathbf x,\mathbf y)$
, where
$\mathbf x$
is the list of variables
$x_1,\ldots ,x_n$
,
$\mathbf y$
is the list of variables
$y_1,\ldots ,y_m$
, and
$\Psi (\mathbf x,\mathbf y)$
is a completely negative quantifier-free
$Ar^*$
-formula. Then for any list of natural numbers
$\mathbf k=k_1,\ldots ,k_n$
, the formula
$A(\mathbf k)$
is spr-realizable iff it is true.
Proof. Assume that the formula
$A(\mathbf k)$
is spr-realizable. This means that there is the list of natural numbers
$\mathbf l=l_1,\ldots ,l_m$
such that the formula
$\Psi (\mathbf k,\mathbf l)$
is spr-realizable. By Proposition 3.7, this formula is true. It follows that the formula
$A(\mathbf k)$
is also true. Conversely, if the formula
$A(\mathbf k)$
is true, then there exists the list of natural numbers
$\mathbf l$
such that the formula
$\Psi (\mathbf k,\mathbf l)$
is true. By Proposition 3.7, this formula is spr-realizable. It follows that the formula
$A(\mathbf k)$
is also realizable.□
4 An arithmetical theory sound with respect to spr-realizability
Let
$\beta $
be Gödel’s Beta Function (see [Reference Kleene5]). This ternary function has the following property: for any list of natural numbers
$k_0,k_1,\ldots ,k_n$
, there exist natural numbers a and b such that
$\beta (a,b,i)=k_i$
for all
$i\le n$
. The predicate
$\beta ([x]_0,[x]_1,y)=0$
is recursively enumerable. By Matiyasevich Theorem, it can be defined in
$\mathfrak N$
by an arithmetical formula
$B(x,y)$
of the form
$\exists \mathbf z\,\Phi (x,y,\mathbf z)$
, where
$\Phi (x,y,\mathbf z)$
is an atomic arithmetical formula. It follows easily that the predicate
$\beta ([x]_0,[x]_1,y)=0$
can be defined in
$\mathfrak N$
by an
$Ar$
-formula of the form
$\exists \mathbf z\,\Phi (x,y,\mathbf z)$
, where
$\Phi (x,y,\mathbf z)$
is a completely negative quantifier-free
$Ar$
-formula. Thus for any natural numbers a and i,
$$ \begin{align*}\beta([a]_0,[a]_1,i)=0\Rightarrow\mathfrak N\models B(a,i);\end{align*} $$
$$ \begin{align*}\beta([a]_0,[a]_1,i)\not=0\Rightarrow\mathfrak N\models\neg B(a,i).\end{align*} $$
Let a be a natural number. Then
$\{a\}$
will denote a unary primitive recursive function g defined as follows:
$g(n)=\mathsf e_{[a]_0+1}([a]_1,\langle n\rangle ).$
Since the predicate
$\{x_1\}(x_2)=x_3$
is recursively enumerable, it follows that it can be defined in
$\mathfrak N$
by an
$Ar$
-formula
$G(x_1,x_2,x_3)$
of the form
$\exists \mathbf y\,\Psi (\mathbf y,x_1,x_2,x_3)$
, where
$\Psi (\mathbf y,x_1,x_2,x_3)$
is a completely negative quantifier-free
$Ar$
-formula.
Definition 4.9. Let
$H(x_1,x_2)$
be the formula
$\exists z\,(\neg \neg Z(z)\,\&\,G(x_1,x_2,z)).$
Obviously, this formula
$H(x_1,x_2)$
defines in
$\mathfrak N$
the predicate
$\{x_1\}(x_2)=0$
.
Definition 4.10. Let Q be the conjunction of the following formulas:
$\begin {array}{ll} A_1. & \forall x\,\neg \neg E(x,x);\\ A_2. & \forall x\forall y\,(\neg \neg E(x,y)\to \neg \neg E(y,x));\\ A_3. & \forall x\forall y\forall z\,(\neg \neg E(x,y)\,\&\,\neg \neg E(y,z)\to \neg \neg E(x,z));\\ A_4. & \exists x\,\neg \neg Z(x);\\ A_5. & \forall x\forall y\,(\neg \neg Z(x)\,\&\,\neg \neg Z(y)\to \neg \neg E(x,y));\\ A_6. & \forall x\forall y\,(\neg \neg E(x,y)\,\&\,\neg \neg Z(x)\to \neg \neg Z(y));\\ A_7. & \forall x\exists y\,\neg \neg S(x,y);\\ A_8. & \forall x\forall y\forall z\,(\neg \neg S(x,y)\,\&\,\neg \neg S(x,z)\to \neg \neg E(y,z));\\ A_9. & \forall x_1\forall x_2\forall y_1\forall y_2\,(\neg \neg E(x_1,x_2)\,\&\,\neg \neg E(y_1,y_2)\,\& \,\neg \neg S(x_1,y_1)\to \neg \neg S(x_2,y_2));\\ A_{10}. & \forall x\forall y\forall z\,(\neg \neg S(x,z)\,\&\,\neg \neg S(y,z)\to \neg \neg E(x,y));\\ A_{11}. & \forall x\forall y\,(\neg \neg S(x,y)\to \neg Z(y));\\ A_{12}. & \forall x\,(\neg \neg Z(x)\lor \exists y\,\neg \neg S(y,x));\\ A_{13}. & \forall x\forall y\exists z\,\neg \neg A(x,y,z);\\ A_{14}. & \forall x\forall y\forall z_1\forall z_2\,(\neg \neg A(x,y,z_1)\,\&\,\neg \neg A(x,y,z_2)\to \neg \neg E(z_1,z_2));\\ A_{15}. & \forall x_1\forall x_2\forall y_1\forall y_2\forall z_1\forall z_2\,(\neg \neg E(x_1,x_2)\,\&\,\neg \neg E(y_1,y_2)\,\&\, \neg \neg E(z_1,z_2)\\ &\qquad \qquad \qquad \qquad \qquad \qquad \&\,\neg \neg A(x_1,y_1,z_1)\to \neg \neg A(x_2,y_2,z_2));\\ A_{16}. & \forall x\forall y\,(\neg \neg Z(y)\to \neg \neg A(x,y,x));\\ A_{17}. & \forall x\forall y\forall z\forall u\forall v\,(\neg \neg S(y,z)\,\&\,\neg \neg A(x,y,u)\,\&\,\neg \neg S(u,v)\to \neg \neg A(x,z,v));\\ A_{18}. & \forall x\forall y\exists z\,\neg \neg M(x,y,z);\\ A_{19}. & \forall x\forall y\forall z_1\forall z_2\,(\neg \neg M(x,y,z_1)\,\&\,\neg \neg M(x,y,z_2)\to \neg \neg E(z_1,z_2));\\ A_{20}. & \forall x_1\forall x_2\forall y_1\forall y_2\forall z_1\forall z_2\,(\neg \neg E(x_1,x_2)\,\&\,\neg \neg E(y_1,y_2)\,\&\,\neg \neg E(z_1,z_2)\\ &\qquad \qquad \qquad \qquad \qquad \qquad \&\,\neg \neg M(x_1,y_1,z_1)\to \neg \neg M(x_2,y_2,z_2));\\ A_{21}. & \forall x\forall y\,(\neg \neg Z(y)\to \neg \neg M(x,y,y));\\ A_{22}. & \forall x\forall y\forall z\forall u\forall v(\neg \neg S(y,z)\&\neg \neg M(x,y,u)\&\neg \neg A(u,x,v)\to \neg \neg M(x,z,v));\\ A_{23}. & \forall x\forall y\forall z_1\forall z_2\,(G(x,y,z_1)\,\&\,G(x,y,z_2)\to \neg \neg E(z_1,z_2));\\ A_{24}. & \forall y\forall z\,\neg \neg \exists v\forall x\,(x\le z\to (\neg \neg B(v,x)\equiv \neg \neg H(y,x)));\\ A_{25}. & \forall x\forall y\,(\neg B(x,y)\lor \neg \neg B(x,y)). \end {array}$
Theorem 4.11. The
$Ar$
-formula Q is spr-realizable.
Proof. We prove that everyone of the formulas
$A_1$
–
$A_{25}$
is spr-realizable. All these formulas are evidently true. All of them except
$A_4$
,
$A_7$
,
$A_{12}$
,
$A_{13}$
,
$A_{18}$
,
$A_{23}$
,
$A_{24}$
, and
$A_{25}$
are completely negative. Therefore they are spr-realizable at level 0 by Proposition 3.7
Recall that
$\mathsf a$
is a 0-index of the function
$x\mapsto \Lambda x.0$
(see Notation in Section 2).
Consider the formula
$A_4$
. Let
$a=3^{\mathsf a}$
. Obviously,
$a\Vdash _0\exists x\,\neg \neg Z(x)$
.
Consider the formula
$A_7$
. The function
$f(x)=2^{x+1}\cdot 3^{\mathsf a}$
is in the class
$\mathbf E_0$
. Let a be its 0-index. We prove that
$a\Vdash _0\forall x\exists y\,\neg \neg S(x,y)$
, i.e.,
$In(0,a)$
holds (this condition is obviously fulfilled) and for any k,
$[f(k)]_1\Vdash _0\neg \neg S(k,[f(k)]_0)$
, i.e.,
$\mathsf a\Vdash _0\neg \neg S(k,k+1)$
, but this easily follows from Proposition 3.4 Thus the formula
$A_7$
is spr-realizable.
Consider the formula
$A_{12}$
. The function
$f(x)=2^{\mathsf {sg}(x)}\cdot 3^{\overline {\mathsf {sg}}(x)\cdot \mathsf a+\mathsf {sg}(x)\cdot 2^{x\div 1}\cdot 3^{\mathsf a}}$
is in the class
$\mathbf E_0$
. Let a be its 0-index. We prove that
$a\Vdash _0\forall x\,(\neg \neg Z(x)\lor \exists y\,\neg \neg S(y,x)),$
i.e.,
$In(0,a)$
holds (this condition is fulfilled) and for any k, either
$[f(k)]_0=0$
and
$[f(k)]_1\Vdash _0\neg \neg Z(k)$
or
$[f(k)]_0\not =0$
and
$[f(k)]_1\Vdash _0\exists y\,\neg \neg S(y,k)$
. Note, that
$$ \begin{align*}f(k)=\begin{cases} 3^{\mathsf a} & \text{if}\ k=0,\\ 2\cdot3^{2^{k-1}\cdot3^{\mathsf a}} & \text{if}\ k>0. \end{cases}\end{align*} $$
If
$k=0$
, then
$[f(k)]_0=0$
,
$[f(k)]_1=\mathsf a$
. In this case,
$[f(0)]_1\Vdash _0\neg \neg Z(0)$
by Proposition 3.4 because
$Z(0)$
is true and spr-realizable. If
$k>0$
, then
$[f(k)]_0=1$
,
$[f(k)]_1=2^{k-1}\cdot 3^{\mathsf a}$
. Since the formula
$S(k-1,k)$
is true and spr-realizable, it follows by Proposition 3.4, that
$\mathsf a\Vdash _0\neg \neg S(k-1,k)$
. Therefore
$[f(k)]_1\Vdash _0\exists y\,\neg \neg S(y,k)$
what we wanted to prove. Thus the formula
$A_{12}$
is spr-realizable.
Consider the formula
$A_{13}$
. The function
$f(x,y)=2^{x+y}\cdot 3^{\mathsf a}$
is in the class
$\mathbf E_0$
. Let a be its 0-index and
$g(x)=\langle 7,1,a,\langle 2,1,x\rangle ,\langle 3,1,1\rangle \rangle $
. Obviously,
$g\in \mathbf E_0$
. Let b be a 0-index of g. We prove that
$b\Vdash _0\forall x\forall y\exists z\,\neg \neg A(x,y,z),$
i.e.,
$In(0,b)$
holds (this condition is fulfilled) and for any k,
$$ \begin{align} \mathsf e_1(b,\langle k\rangle)\Vdash_0\forall y\exists z\,\neg\neg A(k,y,z). \end{align} $$
Note that
$\mathsf e_1(b,\langle k\rangle )=g(k)=\langle 7,1,a,\langle 2,1,k\rangle ,\langle 3,1,1\rangle \rangle $
. Thus
$g(k)$
is a 0-index of the function h obtained by substituting the unary constant function with the only value k and the identity function to the function f, i.e., for any
$\ell $
,
$h(\ell )=f(k,\ell )$
. Thus (1) means that
$f(k,\ell )\Vdash _0\exists z\,\neg \neg A(k,\ell ,z)$
, i.e.,
$[f(k,\ell )]_1\Vdash _0\neg \neg A(k,\ell ,[f(k,\ell )]_0)$
. Note that
$[f(k,\ell )]_0=k+\ell $
,
$[f(k,\ell )]_1=\mathsf a$
. We have to prove that
$\mathsf a\Vdash _0\neg \neg A(k,\ell ,k+\ell )$
, but this easily follows from Proposition 3.4 Thus the formula
$A_{13}$
is spr-realizable.
The case of the formula
$A_{18}$
is considered in the same way with the function
$f(x,y)=2^{x\cdot y}\cdot 3^{\mathsf a}$
.
Consider the formula
$A_{23}$
. Let natural numbers
$k,\ell ,m_1,m_2$
be fixed. Suppose that the formula
$G(k,\ell ,m_1)\,\&\,G(k,\ell ,m_2)$
is realizable. It follows that
$G(k,\ell ,m_1)$
and
$G(k,\ell ,m_2)$
are both spr-realizable. By Proposition 3.8, they are true. This means that
$\{k\}(\ell )=m_1$
and
$\{k\}(\ell )=m_2$
. Then
$m_1=m_2$
and by Proposition 3.4,
$\mathsf a\Vdash _0\neg \neg E(m_1,m_2)$
,
$\Lambda w.\mathsf a\Vdash _0G(k,\ell ,m_1)\,\&\,G(k,\ell ,m_2)\to \neg \neg E(m_1,m_2)$
. Then the number
$\Lambda x.\Lambda y.\Lambda z_1.\Lambda z_2.\Lambda w.\mathsf a$
spr-realizes the formula
$A_{23}$
at level 0.
Consider the formula
$A_{24}$
. By Proposition 3.5, it is enough to prove that for any fixed natural numbers m and n, the formula
$$ \begin{align*}\neg\exists v\forall x\,(x\le n\to(\neg\neg B(v,x)\equiv\neg\neg H(m,x)))\end{align*} $$
is not spr-realizable. We prove that the formula
$$ \begin{align} \exists v\forall x\,(x\le n\to(\neg\neg B(v,x)\equiv\neg\neg H(m,x))) \end{align} $$
is spr-realizable. Consider the list of natural numbers
$k_0,k_1,\ldots ,k_n$
, where
$k_i=0$
iff
$\neg \neg H(m,i)$
is spr-realizable, i.e.,
$\{m\}(i)=0$
. By the property of the function
$\beta $
, there exists a natural number a such that
$\beta ([a]_0,[a]_1,i)=k_i$
for all
$i\le n$
. Assume that
$i\le n$
. If
$k_i=0$
, then both formulas
$\neg \neg B(a,i)$
and
$\neg \neg H(m,i)$
are spr-realizable by
$\mathsf a$
at level 0. By Proposition 3.4, we have
$$ \begin{align} \mathsf a_{\mathsf a}\Vdash_0(\neg\neg B(a,i)\to\neg\neg H(m,i)) \end{align} $$
and
$$ \begin{align} \mathsf a_{\mathsf a}\Vdash_0(\neg\neg H(m,i)\to\neg\neg B(a,i)). \end{align} $$
If
$k_i\not =0$
, then
$\neg \neg B(a,i)$
and
$\neg \neg H(m,i)$
are not spr-realizable. In this case, (3) and (4) hold by Proposition 3.4. It follows that
$\mathsf b\Vdash _0(\neg \neg B(a,i)\equiv \neg \neg H(m,i))$
, where
$\mathsf b=\langle \mathsf a_{\mathsf a},\mathsf a_{\mathsf a}\rangle .$
Then by Proposition 3.4,
$\mathsf a_{\mathsf b}\Vdash _0(i\le n\to (\neg \neg B(a,i)\equiv \neg \neg H(m,i)))$
for any i. It follows that
$\Lambda x.\mathsf a_{\mathsf b}\Vdash _0\forall x\,(x\le n\to ((\neg \neg B(a,x)\equiv \neg \neg H(m,x))).$
This means that the formula (2) is spr-realizable, what we wanted to prove.
Consider the formula
$A_{25}$
. Let
$$ \begin{align*}\phi(x,y)=\mathsf{sg}(\beta([x]_0,[x]_1,y))\cdot3^{\mathsf a}+ \overline{\mathsf{sg}}(\beta([x]_0,[x]_1,y))\cdot2\cdot3^{\mathsf a}.\end{align*} $$
The function
$\phi $
is primitive recursive. Thus there is n such that
$\phi \in \mathbf E_n$
. Let a be an n-index of
$\phi $
and
$g(x)=\langle 7,1,a,\langle 2,1,x\rangle ,\langle 3,1,1\rangle \rangle $
. Obviously,
$g\in \mathbf E_0$
. Let b be a 0-index of g. We prove that
$b\Vdash _n\forall x\forall y\,(\neg B(x,y)\lor \neg \neg B(x,y))$
, i.e.,
$In(n,b)$
holds (this condition is fulfilled) and for any k,
$$ \begin{align} \mathsf e_{n+1}(b,\langle k\rangle)\Vdash_n\forall y\,(\neg B(k,y)\lor\neg\neg B(k,y)). \end{align} $$
Note that
$\mathsf e_{n+1}(b,\langle k\rangle )=g(k)=\langle 7,1,a,\langle 2,1,k\rangle ,\langle 3,1,1\rangle \rangle $
. Thus
$g(k)$
is an n-index of the unary function h obtained by substituting the unary constant function with the only value k and the identity function to the function
$\phi $
, i.e., for any
$\ell $
,
$h(\ell )=\phi (k,\ell )$
. Thus (5) means that
$\phi (k,\ell )\Vdash _n(\neg B(k,\ell )\lor \neg \neg B(k,\ell ))$
, i.e., if
$[\phi (k,\ell )]_0=0$
, then
$[\phi (k,\ell )]_1\Vdash _n\neg B(k,\ell )$
, and
$[\phi (k,\ell )]_1\Vdash _n\neg \neg B(k,\ell )$
if
$[\phi (k,\ell )]_0\not =0$
. Note that
$[\phi (k,\ell )]_0=\begin {cases} 0 & \text {if}\ \beta ([k]_0,[k]_1,\ell )\not =0,\\ 1 & \text {if}\ \beta ([k]_0,[k]_1,\ell )=0; \end {cases}$
$[\phi (k,\ell )]_1=\mathsf a$
. Therefore, if
$[\phi (k,\ell )]_0=0$
, then
$\beta ([k]_0,[k]_1,\ell )\not =0$
. In this case,
$\neg B(k,\ell )$
is spr-realizable. By Proposition 3.4,
$\mathsf a\Vdash _0\neg B(k,\ell )$
, i.e.,
$[\phi (k,\ell )]_1\Vdash _n\neg B(k,\ell )$
. If
$[\phi (k,\ell )]_0\not =0$
, then
$\beta ([k]_0,[k]_1,\ell )=0$
. In this case,
$\neg \neg B(k,\ell )$
is spr-realizable. By Proposition 3.4,
$\mathsf a\Vdash _0\neg \neg B(k,\ell )$
, i.e.,
$[\phi (k,\ell )]_1\Vdash _n\neg \neg B(k,\ell )$
. Thus the formula
$A_{25}$
is realizable.□
5 Strictly primitive recursively realizable predicate formulas
The language of predicate logic consists of individual variables
$x_0,x_1,x_2,\ldots $
, predicate symbols
$P_i^{n_i}$
(
$i,n_i\in \mathbb N$
) (
$P_i^{n_i}$
is called an
$n_i$
-ary predicate symbol), logical symbols
$\neg ,\&,\lor ,\to ,\forall ,\exists $
, and auxiliary symbols ,, (,). Predicate symbols are also called predicate variables and individual variables are called terms.
Atomic formulas have the form
$P(t_1,\ldots ,t_n)$
, where P is an n-ary predicate symbol, and
$t_1,\ldots ,t_n$
are terms.
Sometimes we use a notation
$\mathbf x$
for the list of individual variables
$x_1,\ldots ,x_n$
.
Definition 5.12. Predicate formulas are defined inductively as follows:
-
1) atomic formulas are formulas;
-
2) if A is a formula, then
$\neg A$
is a formula; -
3) if A and B are formulas, then
$(A\,\&\,B)$
,
$(A\lor B)$
, and
$(A\to B)$
are formulas; -
4) if A is a formula, x is an individual variable, then
$\forall x\,A$
and
$\exists x\,A$
are formulas.
Free and bound occurrences of a variable in a formula are defined as usual. A formula A is closed if no variable is free in A. If
$A(x_1,\ldots ,x_n)$
is a formula, then
$A(t_1,\ldots ,t_n)$
denotes the result of substituting terms
$t_1,\ldots ,t_n$
for free occurrences of the variables
$x_1,\ldots ,x_n$
in A. An expression
$(A\equiv B)$
is an abbreviation for
$(A\to B)\,\&\,(B\to A)$
.
A predicate formula A will be referred as
$A(P_1,\ldots ,P_n,y_1,\ldots ,y_m)$
if it does not contain any predicate variables except
$P_1,\ldots ,P_n$
and any free individual variables except
$y_1,\ldots ,y_m$
.
Let
$A(P_1,\ldots ,P_n)$
be a predicate formula. We say that the list of
$Ar^*$
-formulas
$\Phi _1,\ldots ,\Phi _n$
is admissible for substituting in A, if for any
$i=1,\ldots ,n$
, the formula
$\Phi _i$
does not contain free variables except
$x_1,\ldots ,x_m$
, where m is arity of the predicate variable
$P_i$
. In this case,
$A(\Phi _1,\ldots ,\Phi _n)$
will denote the result of substituting the formulas
$\Phi _1,\ldots ,\Phi _n$
for the predicate variables
$P_1,\ldots ,P_n$
in A (bound individual variables should be renamed in order to avoid any collision). The formula
$A(\Phi _1,\ldots ,\Phi _n)$
will be referred as an arithmetical instance of a predicate formula
$A(P_1,\ldots ,P_n)$
.
A closed predicate formula
$A(P_1,\ldots ,P_n)$
is called strictly primitive recursively realizable (spr-realizable) if for any list of
$Ar^*$
-formulas
$\Phi _1,\ldots ,\Phi _k$
admissible for substituting in A, the closed
$Ar^*$
-formula
$A(\Phi _1\ldots \Phi _k)$
is spr-realizable.
A predicate formula
$A(P_1,\ldots ,P_n)$
will be called completely negative if it does not contain logical symbols
$\lor $
and
$\exists $
and each predicate variable
$P_i$
occurs in A only in subformulas of the form
$\neg P_i(y_1,\ldots ,y_k)$
, i.e., an inductive definition of a completely negative predicate formula is the following:
-
• if A is an atomic formula, then
$\neg A$
is a completely negative predicate formula; -
• if A and B are completely negative predicate formulas, then
$\neg A$
,
$(A\,\&\, B)$
, and
$(A\to B)$
are completely negative predicate formulas; -
• if A is a completely negative predicate formula, x is an individual variable, then
$\forall x\,A$
is a completely negative predicate formula.
Proposition 5.13. If
$F(P_1,\ldots ,P_n,y_1,\ldots ,y_m)$
is a completely negative predicate formula, then there exists a natural number
$a_F$
such that for any list of
$Ar^*$
-formulas
$\Phi _1,\ldots ,\Phi _n$
admissible for substituting in F and any natural
$k_1,\ldots ,k_m$
, the following conditions are equivalent:
-
1) the formula
$F(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m)$
is spr-realizable; -
2)
$a_F\Vdash _0F(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m)$
.
Proof. Induction on the complexity of a completely negative predicate formula F. Let F be of the form
$\neg P(y_1,\ldots ,y_m)$
, where P is an m-ary predicate variable,
$\Phi (x_1,\ldots ,x_m)$
is an
$Ar^*$
-formula admissible for substituting in F, and
$k_1,\ldots ,k_m$
are natural numbers. Then
$F(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m)$
is
$\neg \Phi (k_1,\ldots ,k_m)$
. By Proposition 3.4, in this case we can define
$a_F$
as
$\mathsf a$
.
Let
$F(P_1,\ldots ,P_n,y_1,\ldots ,y_m)$
be of the form
$$ \begin{align*}G(P_1,\ldots,P_n,y_1,\ldots,y_m)\,\&\,H(P_1,\ldots,P_n,y_1,\ldots,y_m),\end{align*} $$
and for the formulas G are H the corresponding numbers
$a_G$
and
$a_H$
are defined. Then one can define
$a_F$
as
$\langle a_G,a_H\rangle $
.
If
$F(P_1,\ldots ,P_n,y_1,\ldots ,y_m)$
is of the form
$$ \begin{align*}G(P_1,\ldots,P_n,y_1,\ldots,y_m)\to H(P_1,\ldots,P_n,y_1,\ldots,y_m),\end{align*} $$
we can define
$a_F$
as
$\mathsf a_{a_H}$
. Let
$\Phi _1,\ldots ,\Phi _n$
be the list of
$Ar^*$
-formulas admissible for substituting in F and
$k_1,\ldots ,k_m$
be natural numbers. Assume that the formula
$F(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m)$
is spr-realizable. We prove that
$$ \begin{align*}a_F\Vdash_0F(\Phi_1,\ldots,\Phi_n,k_1,\ldots,k_m).\end{align*} $$
If
$G(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m)$
is not spr-realizable, then by Proposition 3.4,
$$ \begin{align} a_F\Vdash_0G(\Phi_1,\ldots,\Phi_n,k_1,\ldots,k_m)\to H(\Phi_1,\ldots,\Phi_n,k_1,\ldots,k_m). \end{align} $$
If
$G(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m)$
is spr-realizable, then
$H(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m)$
is spr-realizable. By the inductive hypothesis,
$a_H\Vdash _0H(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m).$
Then, by Proposition 3.4, (6) holds.
If F is
$\neg G(P_1,\ldots ,P_n,y_1,\ldots ,y_m)$
, then for any list of
$Ar^*$
-formulas
$\Phi _1,\ldots ,\Phi _n$
admissible for substituting in F and any
$k_1,\ldots ,k_m$
,
$\neg G(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m)$
can be replaced by
$G(\Phi _1,\ldots ,\Phi _n,k_1,\ldots ,k_m)\to E(0,1).$
Thus this case is reduced to the case of implication and we can define
$a_F$
as
$\mathsf a$
.
If F is
$\forall y\,G(P_1,\ldots ,P_n,y,y_1,\ldots ,y_m)$
and the number
$a_G$
is defined for the formula
$G(P_1,\ldots ,P_n,y,y_1,\ldots ,y_m)$
, then we define
$a_F$
as
$\Lambda y.a_G$
. The fact that this number satisfies the conclusion of the theorem is proved by the same argument as in the proof of Proposition 3.7□
6 Simulating arithmetic in the predicate language
Let A be an
$Ar$
-formula. Then A can be considered as a predicate formula if we treat the predicate symbols as predicate variables. In this case, we refer to A as a predicate
$Ar$
-formula.
The predicate
$Ar$
-formula Q defined in Section 4 does not contain any predicate variables except
$Z,S,A,M,E$
; thus it will be denoted
$Q(Z,S,A,M,E)$
. The list of
$Ar$
-formulas
${{\boldsymbol\Phi}} ={\mathcal Z}(x_1),{\mathcal S}(x_1,x_2),{\mathcal A}(x_1,x_2,x_3),{\mathcal M}(x_1,x_2,x_3),{\mathcal E}(x_1,x_2)$
admissible for substituting in
$Q(Z,S,A,M,E)$
will be called an interpretation of Q iff the
$Ar$
-formula
$Q({\mathcal Z},{\mathcal S},{\mathcal A},{\mathcal M},{\mathcal E})$
is spr-realizable.
Assume that an interpretation
${{\boldsymbol\Phi} }$
of the formula Q is fixed. If
$F(Z,S,A,M,E)$
is a predicate formula, then the
$Ar$
-formula
$F({\mathcal Z},{\mathcal S},{\mathcal A},{\mathcal M},{\mathcal E})$
will be denoted
$\widetilde F$
. This is the meaning we attach to the expression
$\widetilde {Q}$
.
Proposition 6.14. If
${{\boldsymbol\Phi} }$
is an interpretation of Q, then for any completely negative
$Ar$
-formula
$\Psi (x_1,\dots ,x_n)$
, the
$Ar$
-formula
$$ \begin{align} \forall\mathbf x,\mathbf y\,(\neg\neg{\mathcal E}(x_1,y_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(x_n,y_n)\,\&\, \widetilde{\Psi}(\mathbf x)\to\widetilde{\Psi}(\mathbf y)), \end{align} $$
where
$\mathbf x$
is the list
$x_1,\ldots ,x_n$
and
$\mathbf y$
is
$y_1,\ldots ,y_n$
is spr-realizable.
Proof. See Appendix A.□
For a natural number n, a predicate
$Ar$
-formula
$[n](x)$
is defined inductively:
-
•
$[0](x)$
is
$\neg \neg Z(x)$
; -
•
$[n+1](x)$
is
$\neg Z(x)\,\&\,\forall y\,(\neg \neg S(y,x)\to [n](y))$
.
Note that for any n, the formula
$[n](x)$
is completely negative.
Proposition 6.15. If
${\boldsymbol\Phi }$
is an interpretation of Q, then for any n, the
$Ar$
-formula
$$ \begin{align} \forall x\forall y\,(\widetilde{[n]}(x)\,\&\,\widetilde{[n]}(y)\to\neg\neg{\mathcal E}(x,y)) \end{align} $$
is spr-realizable.
Proof. We prove spr-realizability of (8) by induction on n. If
$n=0$
, then
$[n](x)$
is
$\neg \neg Z(x)$
. Thus we have to prove that
$\forall x\forall y\,(\neg \neg \mathcal Z(x)\,\&\,\neg \neg \mathcal Z(y)\to \neg \neg {\mathcal E}(x,y))$
is spr-realizable. But this is the formula
$\widetilde {A_5}$
, which is spr-realizable because
${\boldsymbol\Phi} $
is an interpretation of Q. Now assume that the formula (8) is spr-realizable for a given n. We verify that the formula
$$ \begin{align} \forall x\forall y\,(\widetilde{[n+1]}(x)\,\&\,\widetilde{[n+1]}(y)\to\neg\neg{\mathcal E}(x,y)) \end{align} $$
is spr-realizable. First we prove that for any
$k,\ell $
, the formula
$$ \begin{align} \widetilde{[n+1]}(k)\,\&\,\widetilde{[n+1]}(\ell)\to\neg\neg{\mathcal E}(k,\ell) \end{align} $$
is spr-realizable. Assume that the premise of the formula (10) is spr-realizable. Then
$\neg \mathcal Z(k)\,\&\,\forall y\,(\neg \neg \mathcal S(y,k)\to \widetilde {[n]}(y))$
and
$\neg \mathcal Z(\ell )\,\&\,\forall y\,(\neg \neg \mathcal S(y,\ell )\to \widetilde {[n]}(y))$
are spr-realizable. We prove that the formula
$\neg \neg {\mathcal E}(k,\ell )$
is spr-realizable. Since the formula
$\widetilde {A_{12}}$
is spr-realizable, it follows that the formula
$\exists y\,\neg \neg \mathcal S(y,k)$
is spr-realizable. This means that there exists a natural number p such that
$\neg \neg \mathcal S(p,k)$
is realizable. It follows that the formula
$\widetilde {[n]}(p)$
is spr-realizable. By the same reason, there exists a natural number q such that the formulas
$\neg \neg \mathcal S(q,\ell )$
and
$\widetilde {[n]}(q)$
are spr-realizable. By the inductive hypothesis, the formula
$\neg \neg \mathcal E(p,q)$
is spr-realizable. Since the formulas
$\neg \neg \mathcal E(k,k)$
and
$\widetilde {A_9}$
are spr-realizable, it follows that the formula
$\neg \neg \mathcal S(q,k)$
is realizable. Since the formula
$\widetilde {A_8}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(k,\ell )$
is spr-realizable. By Proposition 3.4,
$\mathsf a\Vdash _0\neg \neg \mathcal E(k,\ell )$
and
$\mathsf a_{\mathsf a}$
spr-realizes the formula (10) at level 0. If the premise of the formula (10) is not spr-realizable, then by Proposition 3.4,
$\mathsf a_{\mathsf a}$
spr-realizes the formula (10). Thus we have proved that for any
$k,\ell $
the number
$\mathsf a_{\mathsf a}$
spr-realizes the formula (10). Now it is evident that the number
$\Lambda x.\Lambda y.\mathsf a_{\mathsf a}$
spr-realizes the formula (9).□
Proposition 6.16. If
${\boldsymbol\Phi }$
is an interpretation of Q and
$e\Vdash _m\widetilde {Q}$
, then for any natural numbers k and n we can effectively determine whether the
$Ar^*$
-formula
$\widetilde {[n]}(k)$
is spr-realizable.
Proof. The proof is by induction on n. If
$n=0$
, then
$\widetilde {[n]}(k)$
is the formula
$\neg \neg \mathcal Z(k)$
. Let a natural number k be given. We can extract an spr-realization of the formula
$\widetilde {A_{12}}$
from e. Thus we can determine which of the formulas
$\neg \neg \mathcal Z(k)$
and
$\exists y\,\neg \neg \mathcal S(y,k)$
is spr-realizable. If the first one is spr-realizable, then the formula
$\widetilde {[0]}(k)$
is spr-realizable. If the formula
$\exists y\,\neg \neg \mathcal S(y,k)$
is spr-realizable, then there exists a natural number
$\ell $
such that the formula
$\neg \neg \mathcal S(\ell ,k)$
is spr-realizable. Since the formula
$\widetilde {A_{11}}$
is spr-realizable, it follows that
$\neg \mathcal Z(k)$
is spr-realizable. This means that the formula
$\widetilde {[0]}(k)$
is not spr-realizable. Now suppose that for a given n and any
$\ell $
we can effectively determine whether the formula
$\widetilde {[n]}(\ell )$
is spr-realizable. Let a natural number k be given and we want to determine whether the formula
$\widetilde {[n+1]}(k)$
, i.e.,
$\neg \mathcal Z(k)\,\&\,\forall y\,(\neg \neg \mathcal S(y,k)\to \widetilde {[n]}(y))$
, is realizable. Using an spr-realization of the formula
$\widetilde {A_{12}}$
we determine which of the formulas
$\neg \neg \mathcal Z(k)$
and
$\exists y\,\neg \neg \mathcal S(y,k)$
is spr-realizable. If the formula
$\neg \neg \mathcal Z(k)$
is spr-realizable, then the formula
$\widetilde {[n+1]}(k)$
is not spr-realizable. Assume that the formula
$\exists y\,\neg \neg \mathcal S(y,k)$
is spr-realizable. Then we have a natural number
$\ell $
such that the formula
$\neg \neg \mathcal S(\ell ,k)$
is spr-realizable. We determine whether the formula
$\widetilde {[n]}(\ell )$
is spr-realizable. If this formula is not realizable, then obviously the formula
$\widetilde {[n+1]}(k)$
is not spr-realizable. Assume that the formula
$\widetilde {[n]}(\ell )$
is spr-realizable. We show that the formula
$\widetilde {[n+1]}(k)$
is spr-realizable. It is enough to prove that the formula
$\forall y\,(\neg \neg \mathcal S(y,k)\to \widetilde {[n]}(y))$
is spr-realizable. First we prove that for any p the formula
$\neg \neg \mathcal S(p,k)\to \widetilde {[n]}(p)$
is spr-realizable. First consider the case when the formula
$\neg \neg \mathcal S(p,k)$
is spr-realizable. Recall that the formula
$\neg \neg \mathcal S(\ell ,k)$
is spr-realizable as well. Since the formula
$\widetilde {A_{10}}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(\ell ,p)$
is spr-realizable. Recall that the formula
$\widetilde {[n]}(\ell )$
is spr-realizable. Since the formula
$[n](x)$
is completely negative, it follows from Proposition 6.14 that the formula
$\widetilde {[n]}(p)$
is spr-realizable. By Proposition 5.13,
$a_{[n](x)}\Vdash _0\widetilde {[n]}(p)$
. By Proposition 3.4,
$$ \begin{align} \mathsf a_{a_{[n](x)}}\Vdash_0\neg\neg\mathcal S(p,k)\to\widetilde{[n]}(p). \end{align} $$
If the formula
$\neg \neg \mathcal S(p,k)$
is not spr-realizable, then (11) holds by Proposition 3.4 Thus (11) holds for any p. Then
$\Lambda y.\mathsf a_{a_{[n](x)}}\Vdash _0\forall y\,(\neg \neg \mathcal S(y,k)\to \widetilde {[n]}(y))$
. This means that the formula
$\widetilde {[n+1]}(k)$
is spr-realizable.□
Proposition 6.17. If
${\boldsymbol\Phi }$
is an interpretation of Q, then there exists a primitive recursive function
$\mathsf f$
such that for any natural number n, the
$Ar^*$
-formula
$\widetilde {[n]}(\mathsf f(n))$
is spr-realizable.
Proof. Let
${\boldsymbol\Phi }$
be an interpretation of the formula Q. So, there exist natural numbers e and m such that
$e\Vdash _m\widetilde {Q}$
. It follows from the definition of spr-realizability, that the formula
$\widetilde {A_4}$
is realizable at level m. Thus, there exists a natural number
$a_4$
such that
$a_4\Vdash _m\exists x\,\neg \neg {\mathcal Z}(x)$
. Then
$$ \begin{align} [a_4]_1\Vdash_m\neg\neg{\mathcal Z}([a_4]_0). \end{align} $$
Let
$\mathsf f(0)=[a_4]_0$
. Note that by Proposition 3.4, we have
$\mathsf a\Vdash _0\widetilde {[0]}(\mathsf f(0))$
.
Suppose that the value
$\mathsf f(n)$
is defined for a given n. Since
$\widetilde {A_7}$
is spr-realizable, it follows that there exists a natural number
$a_7$
such that
$a_7\Vdash _m\forall x\exists y\,\neg \neg {\mathcal S}(x,y)$
. Then
$\mathsf {e}_{m+1}(a_7,\langle \mathsf f(n)\rangle )\Vdash _m\exists y\,\neg \neg {\mathcal S}(\mathsf f(n),y)$
. Therefore,
$$ \begin{align*}[\mathsf{e}_{m+1}(a_7,\langle\mathsf f(n)\rangle)]_1\Vdash_m \neg\neg{\mathcal S}(\mathsf f(n),[\mathsf{e}_{m+1}(a_7,\langle\mathsf f(n)\rangle)]_0).\end{align*} $$
Let
$\mathsf f(n+1)=[\mathsf {e}_{m+1}(a_7,\langle \mathsf f(n)\rangle )]_0$
. Note that the formula
$$ \begin{align} \neg\neg{\mathcal S}(\mathsf f(n),\mathsf f(n+1)) \end{align} $$
is spr-realizable. Thus we have the following definition of the function
$\mathsf f$
:
$$ \begin{align*}\left\{ \begin{array}{l} \mathsf f(0)=[a_4]_0;\\ \mathsf f(n+1)=[\mathsf{e}_{m+1}(a_7,\langle\mathsf f(n)\rangle)]_0, \end{array}\right.\end{align*} $$
where the numbers
$a_4$
,
$a_7$
, and m depend only on the formula
$\widetilde {Q}$
. The function
$\mathsf {e}_{m+1}$
is primitive recursive. Obviously, the function
$\mathsf f$
is primitive recursive.
Let us prove that for any n, the formula
$\widetilde {[n]}(\mathsf f(n))$
is spr-realizable. The proof is by induction on n. If
$n=0$
, this condition follows from (12) because
$\neg \neg {\mathcal Z}(x)$
is
$\widetilde {[0]}(x)$
and
$\mathsf f(0)=[a_4]_0$
. Now suppose that for a given n, the formula
$\widetilde {[n]}(\mathsf f(n))$
is spr-realizable. Then by Proposition 5.13,
$a_F\Vdash _0\widetilde {[n]}(\mathsf f(n))$
, where F is
$[n](x)$
. We prove that the formula
$\widetilde {[n+1]}(\mathsf f(n+1))$
is spr-realizable. This means that the formulas
$$ \begin{align} \neg\mathcal Z(\mathsf f(n+1)) \end{align} $$
and
$$ \begin{align} \forall y\,(\neg\neg{\mathcal S}(y,\mathsf f(n+1))\to\widetilde{[n]}(y)) \end{align} $$
are spr-realizable. Since the formulas (13) and
$\widetilde {A_{11}}$
are spr-realizable, it follows that the formula (14) is spr-realizable. Now we prove that the formula (15) is spr-realizable. First we prove that for any k, the formula
$$ \begin{align} \neg\neg{\mathcal S}(k,\mathsf f(n+1))\to\widetilde{[n]}(k) \end{align} $$
is spr-realizable. Assume that the premise of the formula (16), i.e.,
$\neg \neg {\mathcal S}(k,\mathsf f(n+1))$
, is spr-realizable. Since the formulas (13) and
$\widetilde {A_{10}}$
are spr-realizable, it follows that the formula
$\neg \neg {\mathcal E}(\mathsf f(n),k)$
is spr-realizable. By the inductive hypothesis,
$\widetilde {[n]}(\mathsf f(n))$
is spr-realizable. By Proposition 6.14,
$\widetilde {[n]}(k)$
is spr-realizable and by Proposition 5.13,
$a_F\Vdash _0\widetilde {[n]}(k)$
. By Proposition 3.4, the number
$\mathsf a_{a_F}$
spr-realizes the formula (16) at level 0. If the premise of the formula (16) is not spr-realizable, then by Proposition 3.4, the number
$\mathsf a_{a_F}$
spr-realizes the formula (16) at level 0. Thus we have proved that for any k, the number
$\mathsf a_{a_F}$
spr-realizes the formula (16) at level 0. Now it is evident that
$\Lambda x.\mathsf a_{a_F}$
spr-realizes the formula (15) at level 0.□
Proposition 6.18. If
${\boldsymbol\Phi }$
is an interpretation of Q, then for any natural numbers n, m, and a, if the
$Ar^*$
-formulas
$\widetilde {[n]}(a)$
and
$\widetilde {[m]}(a)$
are spr-realizable, then
$m=n$
.
Proof. Assume that
$\widetilde {[n]}(a)$
and
$\widetilde {[m]}(a)$
are spr-realizable. We prove that
$n<m$
is impossible by induction on n. Let
$n=0$
,
$m=k+1$
. Thus we have that the formulas
$\widetilde {[0]}(a)$
, i.e.,
$\neg \neg \mathcal Z(a)$
, and
$\widetilde {[k+1]}(a)$
, i.e.,
$\neg \mathcal Z(a)\,\&\,\forall y\,(\neg \neg \mathcal S(y,a)\to \widetilde {[k]}(y))$
, are spr-realizable. This is obviously impossible. Now let
$m=k+1>n+1$
, and assume that the formulas
$\widetilde {[n+1]}(a)$
, i.e.,
$\neg \mathcal Z(a)\,\&\,\forall y\,(\neg \neg \mathcal S(y,a)\to \widetilde {[n]}(y))$
, and
$\widetilde {[k+1]}(a)$
, i.e.,
$\neg \mathcal Z(a)\,\&\,\forall y\,(\neg \neg \mathcal S(y,a)\to \widetilde {[k]}(y))$
, are spr-realizable. Since the formulas
$\neg \mathcal Z(a)$
and
$\widetilde {A_{12}}$
are spr-realizable, it follows that there exists a number b such that the formula
$\neg \neg \mathcal S(b,a)$
is spr-realizable. Then the formulas
$\widetilde {[n]}(b)$
and
$\widetilde {[k]}(b)$
are spr-realizable. This is impossible by the inductive hypothesis.□
For any n, let
$\tilde n$
denote the number
$\mathsf f(n)$
.
Proposition 6.19. Let
${\boldsymbol\Phi} $
be an interpretation of Q. Then for any quantifier-free completely negative
$Ar$
-formula
$\Psi (y_1,\ldots ,y_m)$
without any free variables except
$y_1,\ldots ,y_m$
and any natural numbers
$k_1,\ldots ,k_m$
, the
$Ar^*$
-formula
$\Psi (k_1,\ldots ,k_m)$
is true iff the
$Ar^*$
-formula
$\widetilde {\Psi }(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable.
Proof. See Appendix B.□
Recall that
$\{a\}$
denotes the function
$g(n)=\mathsf e_{[a]_0+1}([a]_1,\langle n\rangle )$
and the
$Ar$
-formula
$G(x_1,x_2,x_3)$
of the form
$\exists \mathbf y\,\Psi (\mathbf y,x_1,x_2,x_3)$
, where
$\Psi (\mathbf y,x_1,x_2,x_3)$
is a completely negative quantifier-free
$Ar$
-formula, defines in
$\mathfrak N$
the predicate
$\{x_1\}(x_2)=x_3$
.
Proposition 6.20. If
${\boldsymbol\Phi} $
is an interpretation of Q, then for any natural numbers e, n, and k, the
$Ar^*$
-formula
$\widetilde {G}(\tilde e,\tilde n,\tilde k)$
is spr-realizable iff
$\{e\}(n)=k$
.
Proof. Assume that
$\{e\}(n)=k$
. Then the formula
$G(e,n,k)$
is true. This means that there exists the list of natural numbers
$\mathbf b=b_1,\ldots ,b_m$
such that the quantifier-free
$Ar^*$
-formula
$\Psi (\mathbf b,e,n,k)$
is true. By Proposition 6.19, the formula
$\widetilde {\Psi }(\widetilde {\mathbf b},\tilde e,\tilde n,\tilde k)$
, where
$\widetilde {\mathbf b}=\widetilde {b_1},\ldots ,\widetilde {b_m}$
, is spr-realizable. Then the formula
$\exists \mathbf y\,\widetilde {\Psi }(y,\tilde e,\tilde n,\tilde k)$
, i.e.,
$\widetilde {G}(\tilde e,\tilde n,\tilde k)$
, is spr-realizable.
Conversely, assume that the formula
$\widetilde {G}(\tilde e,\tilde n,\tilde k)$
is spr-realizable. Obviously, there exists a natural number
$\ell $
such that
$\{e\}(n)=\ell $
. Then the formula
$G(e,n,\ell )$
is true. Arguing as above, we conclude that the formula
$\widetilde {G}(\tilde e,\tilde n,\tilde \ell )$
is realizable. Since the formula
$\widetilde {A_{23}}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(\tilde \ell ,\tilde k)$
is realizable. By Proposition 6.17, the formula
$\widetilde {[k]}(\tilde k)$
is spr-realizable. It follows from Proposition 6.14 that the formula
$\widetilde {[k]}(\tilde \ell )$
is spr-realizable. On the other hand, the formula
$\widetilde {[\ell ]}(\tilde \ell )$
is spr-realizable. Then, by Proposition 6.18,
$k=\ell $
. Thus we have proved that
$\{e\}(n)=k$
.□
Recall that
$H(x_1,x_2)$
is the formula
$\exists z\,(\neg \neg Z(z)\,\&\,G(x_1,x_2,z)).$
Proposition 6.21. If
${\boldsymbol\Phi} $
is an interpretation of Q, then for any natural numbers e and n, the
$Ar^*$
-formula
$\widetilde {H}(\tilde e,\tilde n)$
is spr-realizable iff
$\{e\}(n)=0$
.
Proof. Assume that
$\{e\}(n)=0$
. Then by Proposition 6.21,
$\widetilde {G}(\tilde e,\tilde n,\tilde 0)$
is spr-realizable. On the other hand,
$\neg \neg \mathcal Z(\tilde 0)$
is also spr-realizable. Then the formula
$\neg \neg \mathcal Z(\tilde 0)\,\&\,\widetilde {G}(\tilde e,\tilde n,\tilde 0)$
is spr-realizable. It follows that
$\exists z\,(\neg \neg \mathcal Z(z)\,\&\,\widetilde {G}(\tilde e,\tilde n,z))$
, i.e.,
$\widetilde {H}(\tilde e,\tilde n)$
, is realizable. Conversely, assume that the formula
$\widetilde {H}(\tilde e,\tilde n)$
is spr-realizable. Then there is a natural number k such that the formulas
$\neg \neg \mathcal Z(k)$
, i.e.,
$\widetilde {[0]}(k)$
, and
$\widetilde {G}(\tilde e,\tilde n,k)$
are spr-realizable. Since the formula
$\widetilde {[0]}(\tilde 0)$
is also spr-realizable, it follows from Proposition 6.15 that the formula
$\neg \neg \mathcal E(k,\tilde 0)$
is spr-realizable. Then it follows from Proposition 6.14 that the formula
$\widetilde {G}(\tilde e,\tilde n,\tilde 0)$
is spr-realizable. By Proposition 6.21,
$\{e\}(n)=0$
.□
Definition 6.22. Assume that an interpretation
${\boldsymbol\Phi }$
of the formula Q is fixed. A natural number a will be called
${\boldsymbol\Phi }$
-standard if there exists a natural number n such that the formula
$\widetilde {[n]}(a)$
is spr-realizable.
Note that the numbers
$\tilde 0,\tilde 1,\tilde 2,\ldots $
are
${\boldsymbol\Phi }$
-standard.
Proposition 6.23. If a natural number a is
${\boldsymbol\Phi }$
-standard and b is a natural number such that the
$Ar^*$
-formula
$\neg \neg {\mathcal S}(a,b)$
is spr-realizable, then the number b is
${\boldsymbol\Phi }$
-standard.
Proof. Assume that the formula
$\widetilde {[n]}(a)$
is spr-realizable. Since the predicate
$Ar$
-formula
$[n](x)$
is completely negative, it follows from Proposition 5.13 that there exists a number d, namely
$a_{[n](x)}$
, such that
$d\Vdash _0\widetilde {[n]}(a)$
. Assume that b is a natural number such that the formula
$\neg \neg {\mathcal S}(a,b)$
is spr-realizable. We prove that the formula
$\widetilde {[n+1]}(b)$
, i.e.,
$\neg \mathcal Z(b)\,\&\,\forall y\,(\neg \neg \mathcal S(y,b)\to \widetilde {[n]}(y))$
, is spr-realizable. Since the formula
$\widetilde {A_{11}}$
is spr-realizable, it follows that the formula
$\neg \mathcal Z(b)$
is spr-realizable. We prove that the formula
$\forall y\,(\neg \neg \mathcal S(y,b)\to \widetilde {[n]}(y))$
is spr-realizable at level 0. Let c be an arbitrary natural number. We prove that
$$ \begin{align} \mathsf a_d\Vdash_0\neg\neg\mathcal S(c,b)\to\widetilde{[n]}(c). \end{align} $$
If the formula
$\neg \neg \mathcal S(c,b)$
is not spr-realizable, then (17) holds by Proposition 3.4 Assume that the formula
$\neg \neg \mathcal S(c,b)$
is spr-realizable. Since the formulas
$\neg \neg {\mathcal S}(a,b)$
,
$\neg \neg \mathcal S(c,b)$
, and
$\widetilde {A_{10}}$
are spr-realizable, it follows that the formula
$\neg \neg \mathcal E(a,c)$
is spr-realizable. Since the formula
$\widetilde {[n]}(a)$
is realizable, it follows from Proposition 6.14 that the formula
$\widetilde {[n]}(c)$
is spr-realizable. By Proposition 5.13,
$d\Vdash _0\widetilde {[n]}(c)$
. Now (17) follows from Proposition 3.4 Then
$\Lambda y.\mathsf a_d\Vdash _0\forall y\,(\neg \neg \mathcal S(y,b)\to \widetilde {[n]}(y))$
.□
Definition 6.24. Let
$x\le y$
be the formula
$\exists z\,\neg \neg A(z,x,y)$
.
Proposition 6.25. Suppose that
${\boldsymbol\Phi }$
is an interpretation of the formula Q. For any natural numbers n and b, if b is not
${\boldsymbol\Phi }$
-standard, then the
$Ar^*$
-formula
$\tilde n\widetilde {\le }b$
is spr-realizable.
Proof. Induction on n. Let
$n=0$
. Since the formula
$\widetilde {A_{16}}$
is spr-realizable, it follows that the formula
$\neg \neg {\mathcal Z}(\tilde 0)\to \neg \neg {\mathcal A}(b,\tilde 0,b)$
is spr-realizable. Since the formula
$\neg \neg {\mathcal Z}(\tilde 0)$
is realizable, it follows that the formula
$\neg \neg {\mathcal A}(b,\tilde 0,b)$
is spr-realizable. Therefore the formula
$\exists z\,\neg \neg {\mathcal A}(z,\tilde 0,b)$
, i.e.,
$\tilde 0\widetilde {\le }b$
, is spr-realizable.
Now suppose that for any natural number b which is not
${\boldsymbol\Phi }$
-standard, the formula
$\tilde n\widetilde {\le }b$
is spr-realizable. We have to prove that for any such number b, the formula
$\widetilde {n+1}\widetilde {\le }b$
is spr-realizable. Since the number b is not
${\boldsymbol\Phi }$
-standard, it follows that the formula
$\neg \neg {\mathcal Z}(b)$
is not spr-realizable. Since the formula
$\widetilde {A_{12}}$
is realizable, it follows that the formula
$\exists y\,\neg \neg {\mathcal S}(y,b)$
is spr-realizable. This means that there exists a natural number a such that the formula
$\neg \neg {\mathcal S}(a,b)$
is spr-realizable. By Proposition 6.23, the number a cannot be
${\boldsymbol\Phi }$
-standard. By the inductive hypothesis, the formula
$\exists z\,\neg \neg {\mathcal A}(z,\tilde n,a)$
is spr-realizable. This means that there exists a natural number c such that the formula
$\neg \neg {\mathcal A}(c,\tilde n,a)$
is spr-realizable. Since the formula
$\neg \neg S(n,n+1)$
is true, it follows from Proposition 6.19 that the formula
$\neg \neg \mathcal S(\tilde n,\widetilde {n+1})$
is realizable. Since the formula
$\widetilde {A_{17}}$
is spr-realizable, it follows that the formula
$\neg \neg {\mathcal A}(c,\widetilde {n+1},b)$
is spr-realizable. Therefore the formula
$\exists z\,\neg \neg {\mathcal A}(z,\widetilde {n+1},b)$
, i.e.,
$\widetilde {n+1}\widetilde {\le }b$
, is spr-realizable.□
7 Non-arithmeticity of the spr-realizability
Theorem 7.26. If
${\boldsymbol\Phi } $
is an interpretation of the formula Q, then every natural number is
${\boldsymbol\Phi } $
-standard.
Proof. Let an interpretation
${\boldsymbol\Phi } $
of Q be given. Then
$\widetilde {A_{25}}$
is spr-realizable. This means that there are natural numbers q and p such that
$q\Vdash _p\forall x\forall y\,(\neg \tilde B(x,y)\lor \neg \neg \tilde B(x,y)).$
Then for any
$k,\ell $
, we have
$\mathsf e_{p+1}(\mathsf e_{p+1}(q,\langle k\rangle )),(\langle \ell \rangle )\Vdash _p\neg \tilde B(k,\ell )\lor \neg \neg \tilde B(k,\ell ))$
, i.e., if
$[\mathsf e_{p+1}(\mathsf e_{p+1}(q,\langle k\rangle )),(\langle \ell \rangle )]_0=0$
, then the formula
$\neg \tilde B(k,\ell )$
is spr-realizable, else the formula
$\neg \neg \tilde B(k,\ell )$
is spr-realizable. Let a unary function g be defined as follows:
$$ \begin{align*}g(n)=\begin{cases} 0 & \text{if the formula}\ \neg\tilde B(n,\tilde n)\ \text{is {\sl spr}-realizable,}\\ 1 & \text{otherwise}. \end{cases}\end{align*} $$
By Proposition 6.17, the number
$\tilde n$
can be found from n by means of a primitive recursive function
$\mathsf f$
. Thus we can represent the function g in the following form:
$$ \begin{align*}g(n)=\mathsf{sg}((\mathsf e_{p+1}([\mathsf e_{p+1}(q,\langle n\rangle),\langle\mathsf f(n)\rangle]_0).\end{align*} $$
It is obvious that the function g is primitive recursive. Therefore, there exists a natural number e such that for all n,
$g(n)=\mathsf e_{[e]_0+1}(\langle [e]_1,n\rangle )$
.
Since
${\boldsymbol\Phi } $
is an interpretation of the formula Q, it follows that the formula
$\widetilde {A_{24}}$
, i.e.,
$$ \begin{align} \forall y\forall z\,\neg\neg\exists v\forall x\,(x\widetilde{\le}z\to(\neg\neg\widetilde{B}(v,x)\equiv\neg\neg\widetilde{H}(y,x))), \end{align} $$
is spr-realizable. Suppose that there exists a natural number b which is not
${\boldsymbol\Phi } $
-standard. Since the formula (18) is spr-realizable, it follows that the formula
$$ \begin{align} \neg\neg\exists v\forall x\,(x\widetilde{\le}b\to(\neg\neg\widetilde{B}(v,x)\equiv\neg\neg\widetilde{H}(\tilde e,x))) \end{align} $$
is spr-realizable. Now suppose that the formula
$$ \begin{align} \exists v\forall x\,(x\widetilde{\le}b\to(\neg\neg\widetilde{B}(v,x)\equiv\neg\neg\widetilde{H}(\tilde e,x))) \end{align} $$
is spr-realizable. Then there exists a natural number a such that the formula
$$ \begin{align*}\forall x\,(x\widetilde{\le}b\to(\neg\neg\widetilde{B}(a,x)\equiv\neg\neg\widetilde{H}(\tilde e,x)))\end{align*} $$
is spr-realizable. It follows that for any n, the formula
$$ \begin{align*}\tilde n\widetilde{\le}b\to(\neg\neg\widetilde{B}(a,\tilde n)\equiv\neg\neg\widetilde{H}(\tilde e,\tilde n))\end{align*} $$
is spr-realizable. By Proposition 6.25, the formula
$\tilde n\widetilde {\le }b$
is spr-realizable. Then for any n, the formula
$\neg \neg \widetilde {B}(a,\tilde n)\equiv \neg \neg \widetilde {H}(\tilde e,\tilde n))$
is spr-realizable. Thus we have that for any n,
(a) the formula
$\neg \neg \widetilde {B}(a,\tilde n)$
is spr-realizable iff the formula
$\neg \neg \widetilde {H}(\tilde e,\tilde n)$
is realizable.
On the other hand, by Proposition 6.21, for any n,
(b) the formula
$\neg \neg \widetilde {H}(\tilde e,\tilde n)$
is spr-realizable iff
$g(n)=0$
.
Further, by the definition of the function g, we have
(c)
$g(n)=0$
iff the formula
$\neg \widetilde {B}(n,\tilde n)$
is spr-realizable.
It follows from the statements (a), (b), and (c) that for a given natural number a and any natural number n, the following equivalence holds: the formula
$\neg \neg \widetilde {B}(a,\tilde n)$
is spr-realizable iff the formula
$\neg \widetilde {B}(n,\tilde n)$
is spr-realizable, and we have a contradiction if
$n=a$
. This contradiction means that the formula (20) is not spr-realizable. Then its negation is spr-realizable contrary to the fact that the formula (19) is spr-realizable. Thus we have proved that there exists no natural number which is not
${\boldsymbol\Phi } $
-standard.□
Proposition 7.27. If
${\boldsymbol\Phi }$
is an interpretation of Q and
$e\Vdash _m\widetilde {Q}$
, then for any natural number k, we can effectively find a natural number n such that the formula
$\widetilde {[n]}(k)$
is spr-realizable.
Proof. Assume that
${\boldsymbol\Phi }$
is an interpretation of Q and numbers e and m such that
$e\Vdash _m\widetilde {Q}$
are given. Let a natural number k be given. By Proposition 6.16, for any natural number n we can effectively determine whether the formula
$\widetilde {[n]}(k)$
is spr-realizable. Sequentially iterating over natural numbers starting from 0, we find n such that the formula
$\widetilde {[k]}(n)$
is spr-realizable because otherwise the number k should be not
${\boldsymbol\Phi } $
-standard in contradiction with Theorem 7.26.□
Proposition 7.28. Suppose that
${\boldsymbol\Phi }$
is an interpretation of the formula Q. Then for any completely negative
$Ar$
-formula
$\Psi (y_1,\ldots ,y_n)$
without any free variables except
$y_1,\ldots ,y_n$
and any natural numbers
$k_1,\ldots ,k_n$
, the
$Ar^*$
-formula
$\Psi (k_1,\ldots ,k_n)$
is true iff the
$Ar^*$
-formula
$\widetilde {\Psi }(\widetilde {k_1},\ldots ,\widetilde {k_n})$
is spr-realizable.
Proof. Induction on the logical complexity of a completely negative
$Ar$
-formula
$\Psi (y_1,\ldots ,y_n)$
.
The case of an atomic formula
$\Psi (y_1,\ldots ,y_n)$
is considered in Proposition 6.19 The proof of Proposition 6.19 contains also a consideration of the cases when the formula
$\Psi $
is of the form
$\Psi _1\,\&\,\Psi _2$
,
$\Psi _1\to \Psi _2$
or
$\neg \Psi _1$
and the statement is true for the formulas
$\Psi _1$
and
$\Psi _2$
.
Assume that
$\Psi (y_1,\ldots ,y_n)$
is of the form
$\forall y\,\Psi _0(y,y_1,\ldots ,y_n)$
. Then
$\widetilde {\Psi }(y_1,\ldots ,y_n)$
is the formula
$\forall y\,\widetilde {\Psi _0}(y,y_1,\ldots ,y_n)$
. The inductive hypothesis states that for any natural numbers
$k,k_1,\ldots ,k_n$
, the
$Ar^*$
-formula
$\Psi _0(k,k_1,\ldots ,k_n)$
is true iff the
$Ar^*$
-formula
$\widetilde {\Psi _0}(\tilde k,\widetilde {k_1},\ldots ,\widetilde {k_n})$
is realizable. Assume that
$\Psi (k_1,\ldots ,k_n)$
is true. It follows that for any natural number k, the formula
$\Psi _0(k,k_1,\ldots ,k_n)$
is true and by the inductive hypothesis, the formula
$\widetilde {\Psi _0}(\tilde k,\widetilde {k_1},\ldots ,\widetilde {k_n})$
is spr-realizable. We prove that
$\forall y\,\widetilde {\Psi _0}(y,\widetilde {k_1},\ldots ,\widetilde {k_n})$
is spr-realizable. Let
$\ell $
be an arbitrary natural number. By Theorem 7.26, the number
$\ell $
is
${\boldsymbol\Phi }$
-standard. This means that there exists a natural number k such that
$\widetilde {[k]}(\ell )$
is spr-realizable. (Moreover, by Proposition 7.27, we can find k effectively.) It follows from Proposition 6.15 that
${\mathcal E}(\tilde k,\ell )$
is spr-realizable. By Proposition 6.14,
${\mathcal E}(\tilde k,\ell )\,\&\,\widetilde {\Psi _0}(\tilde k,\tilde k_1,\ldots ,\tilde k_n)\to \widetilde {\Psi _0}(\ell ,\tilde k_1,\ldots ,\tilde k_n)$
is spr-realizable. Since the premise of this formula is spr-realizable, it follows that its conclusion
$\widetilde {\Psi _0}(\ell ,\tilde k_1,\ldots ,\tilde k_n)$
is spr-realizable. Note that
$\Psi _0$
is completely negative. By Proposition 5.13, there exists a number
$a_{\Psi _0}$
such that
$a_{\Psi _0}\Vdash _0\widetilde {\Psi _0}(\ell ,\tilde k_1,\ldots ,\tilde k_n)$
for any number
$\ell $
. Then
$\Lambda y.a_{\Psi _0}\Vdash _0\forall y\widetilde {\Psi _0}(y,\tilde k_1,\ldots ,\tilde k_n)$
, i.e., the formula
$\widetilde {\Psi }(\tilde k_1,\ldots ,\tilde k_n)$
is spr-realizable, what we wanted to prove.
Conversely, assume that
$\widetilde {\Psi }(\tilde k_1,\ldots ,\tilde k_n)$
is spr-realizable. This implies that for any natural number k, the formula
$\widetilde {\Psi _0}(\tilde k,\tilde k_1,\ldots ,\tilde k_n)$
is spr-realizable. By the inductive hypothesis, for any k, the formula
$\Psi _0(k,k_1,\ldots ,k_n)$
is true. This means that the formula
${\Psi }(k_1,\ldots ,k_n)$
is true.□
Theorem 7.29. For any closed completely negative
$Ar$
-formula
$\Psi $
one can effectively construct a closed predicate formula
$\Psi ^*$
such that
$\Psi ^*$
is spr-realizable iff
$\Psi $
is true.
Proof. If
$\Psi $
is a closed completely negative
$Ar$
-formula, let
$\Psi ^*$
be the predicate
$Ar$
-formula
$Q\to \Psi $
. We show that
$\Psi ^*$
is the required predicate formula.
Claim I. If the predicate formula
$\Psi ^*$
is spr-realizable, then the
$Ar$
-formula
$\Psi $
is true.
Proof. Assume that
$\Psi ^*$
is spr-realizable. This means that for any list of
$Ar$
-formulas
${\boldsymbol\Phi } $
admissible for substituting in
$\Psi ^*$
, the formula
$\widetilde {\Psi ^*}$
is spr-realizable. In particular, this holds if
${\boldsymbol\Phi } $
is the list of the formulas
$Z(x)$
,
$S(x,y)$
,
$A(x,y,z)$
,
$M(x,y,z)$
, and
$E(x,y)$
. In this case,
$\widetilde {\Psi ^*}$
is just the formula
$Q\to \Psi $
. By Theorem 4.11, the formula Q is spr-realizable. Thus the formula
$\Psi $
is also spr-realizable. Since
$\Psi $
is a completely negative formula, it follows from Proposition 3.7 that
$\Psi $
is true, what we wanted to prove. □
$_{\mathrm {I}}$
Claim II. If a closed completely negative
$Ar$
-formula
$\Psi $
is true, then the predicate formula
$\Psi ^*$
is spr-realizable.
Proof. Assume that a closed completely negative
$Ar$
-formula
$\Psi $
is true. We prove that the predicate
$Ar$
-formula
$\Psi ^*$
is spr-realizable. Assume that the list of
$Ar$
-formulas
${\boldsymbol\Phi }$
is admissible for substituting in
$\Psi ^*$
. Since
$\Psi $
is completely negative, it follows from Proposition 5.13 that there exists a number
$a_{\Psi }$
such that the formula
$\widetilde {\Psi }$
is spr-realizable iff
$a_{\Psi }\Vdash _0\widetilde {\Psi }$
. We prove that
$\Lambda n.\Lambda y.a_{\Psi }\Vdash _0\widetilde {\Psi ^*}$
. By the definition of spr-realizability, it is enough to prove that for any n and any b such that
$b\Vdash _n\widetilde Q$
, we have
$a_{\Psi }\Vdash _n\widetilde {\Psi }$
. Assume that
$b\Vdash _n\widetilde Q$
. This means that
${\boldsymbol\Phi } $
is an interpretation of the formula Q. By Proposition 7.28, the formula
$\widetilde {\Psi }$
is spr-realizable because the formula
$\Psi $
is true. As it was remarked above, in this case
$a_{\Psi }\Vdash _0\widetilde {\Psi }$
. It follows that
$a_{\Psi }\Vdash _n\widetilde {\Psi }$
, what we wanted to prove. □
$_{\mathrm {{II}}}$
Claims I and II yield the statement of Theorem 7.29.
Theorem 7.30. The set of spr-realizable predicate formulas is not arithmetical.
Proof. It is obvious that the set of true completely negative closed
$Ar$
-formulas is recursively isomorphic to the set of true closed
$Ar$
-formulas which is not arithmetical by Tarski’s Undefinability Theorem. It follows that the set of true completely negative closed
$Ar$
-formulas is not arithmetical too. By Theorem 7.29, the set of true completely negative closed
$Ar$
-formulas is 1-1-reducible to the set of spr-realizable predicate formulas. It follows that the set of spr-realizable predicate formulas is not arithmetical.□
A Appendix: Proof of Proposition 6.14
Let
$$ \begin{align*}{{\boldsymbol\Phi }}={\mathcal Z}(x_1),{\mathcal S}(x_1,x_2),{\mathcal A}(x_1,x_2,x_3),{\mathcal M}(x_1,x_2,x_3),{\mathcal E}(x_1,x_2)\end{align*} $$
be an interpretation of the formula Q. Note that the formula
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is built from the formulas
$\neg \mathcal E(x_i,x_j)$
,
$\neg \mathcal Z(x_i)$
,
$\neg {\mathcal S}(x_i,x_j)$
,
$\neg \mathcal A(x_i,x_j,x_k)$
, and
$\neg \mathcal M(x_i,x_j,x_k),$
where
$1\le i,j,k\le n$
, using the logical symbols
$\neg $
,
$\&$
,
$\to $
, and
$\forall $
. Note that (7) is an arithmetical instance of the completely negative predicate
$Ar$
-formula
$$ \begin{align} \forall\mathbf x,\mathbf y\,(\neg\neg E(x_1,y_1)\,\&\cdots\&\,\neg\neg E(x_n,y_n)\,\&\,\Psi(\mathbf x)\to\Psi(\mathbf y)). \end{align} $$
By Proposition 5.13, there exists a number that spr-realizes at level
$0$
every spr-realizable arithmetical instance of (A.1). Thus it is enough to prove that the formula (7) is spr-realizable at level
$0$
without paying any attention to the construction of a concrete spr-realization.
We prove that the formula (7) is spr-realizable by induction on the complexity of
$\Psi (x_1,\dots ,x_n)$
.
1) If
$\Phi (x_1,\dots ,x_n)$
is
$\neg E(x_i,x_j)$
, where
$1\le i,j\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \mathcal E(x_i,x_j)$
and in this case the formula (7) is
$$ \begin{align} \forall\mathbf x,\mathbf y\, (\neg\neg\mathcal E(x_1,y_1)\,\&\cdots\&\,\neg\neg\mathcal E(x_n,y_n)\,\&\,\neg\mathcal E(x_i,x_j)\to\neg\mathcal E(y_i,y_j)). \end{align} $$
First we prove that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the
$Ar^*$
-formula
$$ \begin{align} \neg\neg\mathcal E(k_1,\ell_1)\,\&\cdots\&\,\neg\neg\mathcal E(k_n,\ell_n)\,\&\,\neg\mathcal E(k_i,k_j)\to\neg\mathcal E(\ell_i,\ell_j) \end{align} $$
is spr-realizable.
Suppose
$i=j$
. Since the formula
$\widetilde {A_1}$
is spr-realizable, it follows that
$\neg \neg \mathcal E(k_i,k_j)$
is spr-realizable. In this case, the premise of the formula (A.3) is not spr-realizable, and by Proposition 3.4, the number
$\mathsf a_{\mathsf a}$
spr-realizes the formula (A.3) at level 0.
Now suppose
$i\not =j$
. If the premise of the formula (A.3) is not spr-realizable, then by Proposition 3.4, the number
$\mathsf a_{\mathsf a}$
spr-realizes the formula (A.3) at level 0. Suppose that the premise of the formula (A.3) is spr-realizable. Then the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
,
$\neg \neg \mathcal E(k_j,\ell _j)$
, and
$\neg \mathcal E(k_i,k_j)$
are spr-realizable. We prove that the conclusion of the formula (A.3), i.e.,
$\neg \mathcal E(\ell _i,\ell _j)$
, is spr-realizable as well. By Proposition 3.4, it is enough to prove that the formula
$\neg \neg \mathcal E(\ell _i,\ell _j)$
is not spr-realizable. Suppose that this formula is spr-realizable. Thus we have that the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
,
$\neg \neg \mathcal E(k_j,\ell _j)$
, and
$\neg \neg \mathcal E(\ell _i,\ell _j)$
are spr-realizable. Since the formula
$\widetilde {A_3}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(k_i,\ell _j)$
is also spr-realizable. Since the formula
$\widetilde {A_2}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(\ell _j,k_j)$
is spr-realizable. Since the formula
$\widetilde {A_3}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(k_i,kj)$
is also spr-realizable in contradiction with the assumption that the formula
$\neg \mathcal E(k_i,k_j)$
is spr-realizable. Thus
$\neg \mathcal E(\ell _i,\ell _j)$
is spr-realizable. By Proposition 3.4,
$\mathsf a\Vdash _0\neg \mathcal E(\ell _i,\ell _j)$
and the number
$\mathsf a_{\mathsf a}$
spr-realizes the formula (A.3) at level 0. Thus we have proved that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the number
$\mathsf a_{\mathsf a}$
spr-realizes (A.3) at level
$0$
. Evidently, the number
$\Lambda x_1.\ldots \Lambda x_n.\Lambda y_1.\ldots \Lambda y_n.\mathsf a_{\mathsf a}$
spr-realizes the formula (A.2) at level
$0$
.
2) If
$\Psi (x_1,\dots ,x_n)$
is
$\neg Z(x_i)$
, where
$1\le i\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \mathcal Z(x_i)$
and in this case the formula (7) is
$$ \begin{align} \forall\mathbf x,\mathbf y\,(\neg\neg\mathcal E(x_1,y_1)\,\&\cdots\&\,\neg\neg\mathcal E(x_n,y_n)\,\&\,\neg\mathcal Z(x_i)\to\neg\mathcal Z(y_i)). \end{align} $$
First we prove that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the
$Ar^*$
-formula
$$ \begin{align} \neg\neg\mathcal E(k_1,\ell_1)\,\&\cdots\&\,\neg\neg\mathcal E(k_n,\ell_n)\,\&\,\neg\mathcal Z(k_i)\to\neg\mathcal Z(\ell_i) \end{align} $$
is spr-realizable.
If the premise of the formula (A.5) is not spr-realizable, then by Proposition 3.4, the number
$\mathsf a_{\mathsf a}$
spr-realizes the formula (A.5) at level 0. Suppose that the premise of the formula (A.5) is spr-realizable. Then the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
and
$\neg \mathcal Z(k_i)$
are spr-realizable. We prove that the conclusion of the formula (A.5), i.e.,
$\neg \mathcal Z(\ell _i)$
, is spr-realizable as well. By Proposition 3.4, it is enough to prove that the formula
$\neg \neg \mathcal Z(\ell _i)$
is not spr-realizable. Suppose that this formula is spr-realizable. Thus we have that the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
and
$\neg \neg \mathcal Z(\ell _i)$
are spr-realizable. Since the formula
$\widetilde {A_2}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(\ell _i,k_i)$
is also spr-realizable. Note that the formula
$\widetilde {A_6}$
is spr-realizable. It follows that
$\neg \neg \mathcal E(\ell _i,k_i)\,\&\,\neg \neg \mathcal Z(\ell _i)\to \neg \neg \mathcal Z(k_i)$
is realizable. Since the premise of this implication is spr-realizable, it follows that its conclusion
$\neg \neg \mathcal Z(k_i)$
is realizable in contradiction with the assumption that the formula
$\neg \mathcal Z(k_i)$
is spr-realizable. Thus
$\neg \mathcal Z(\ell _i)$
is spr-realizable. By Proposition 3.4,
$\mathsf a\Vdash _0\neg \mathcal Z(\ell _i)$
and the number
$\mathsf a_{\mathsf a}$
spr-realizes (A.5) at level
$0$
. We have proved that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the number
$\mathsf a_{\mathsf a}$
spr-realizes (A.5) at level
$0$
. Evidently, the number
$\Lambda x_1.\ldots \Lambda x_n.\Lambda y_1.\ldots \Lambda y_n.\mathsf a_{\mathsf a}$
spr-realizes the formula (A.4) at level
$0$
.
3) If
$\Psi (x_1,\dots ,x_nx)$
is
$\neg S(x_i,x_j)$
, where
$1\le i,j\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \mathcal S(x_i,x_j)$
and in this case the formula (7) is
$$ \begin{align} \forall\mathbf x,\mathbf y\, (\neg\neg\mathcal E(x_1,y_1)\,\&\cdots\&\,\neg\neg\mathcal E(x_n,y_n)\,\&\,\neg\mathcal S(x_i,x_j)\to\neg\mathcal S(y_i,y_j)). \end{align} $$
First we prove that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the formula
$$ \begin{align} \neg\neg\mathcal E(k_1,\ell_1)\,\&\cdots\&\,\neg\neg\mathcal E(k_n,\ell_n)\,\&\,\neg\mathcal S(k_i,k_j)\to\neg\mathcal S(\ell_i,\ell_j) \end{align} $$
is spr-realizable.
If the premise of the formula (A.7) is not spr-realizable, then by Proposition 3.4, the number
$\mathsf a_{\mathsf a}$
spr-realizes the formula (A.7) at level 0. Suppose that the premise of the formula (A.7) is spr-realizable. Then the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
,
$\neg \neg \mathcal E(k_j,\ell _j)$
, and
$\neg \mathcal S(k_i,k_j)$
are spr-realizable. We prove that the conclusion of the formula (A.7), i.e.,
$\neg \mathcal S(\ell _i,\ell _j)$
, is spr-realizable as well. By Proposition 3.4, it is enough to prove that the formula
$\neg \neg \mathcal S(\ell _i,\ell _j)$
is not spr-realizable. Suppose that this formula is spr-realizable. Thus we have that the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
,
$\neg \neg \mathcal E(k_j,\ell _j)$
, and
$\neg \neg \mathcal S(\ell _i,\ell _j)$
are spr-realizable. Since the formula
$\widetilde {A_2}$
is spr-realizable, it follows that the formulas
$\neg \neg \mathcal E(\ell _i,k_i)$
and
$\neg \neg \mathcal E(\ell _j,k_j)$
are also spr-realizable. Note that the formula
$\widetilde {A_9}$
is spr-realizable. It follows that
$\neg \neg \mathcal E(\ell _i,k_i)\,\&\,\neg \neg \mathcal E(\ell _j,k_j)\,\&\,\neg \neg \mathcal S(\ell _i,\ell _j)\to \neg \neg \mathcal S(k_i,k_j)$
is spr- realizable. Since the premise of this implication is spr-realizable, it follows that its conclusion
$\neg \neg \mathcal S(k_i,k_j)$
is spr-realizable in contradiction with the assumption that
$\neg \mathcal S(k_i,k_j)$
is spr-realizable. Thus
$\neg \mathcal S(\ell _i,\ell _j)$
is spr-realizable. By Proposition 3.4,
$\mathsf a\Vdash _0\neg \mathcal S(\ell _i,\ell _j)$
and the number
$\mathsf a_{\mathsf a}$
spr-realizes (A.7) at level
$0$
. We have proved that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the number
$\mathsf a_{\mathsf a}$
spr-realizes (A.7) at level
$0$
. Evidently, the number
$\Lambda x_1.\ldots \Lambda x_n.\Lambda y_1.\ldots \Lambda y_n.\mathsf a_{\mathsf a}$
spr-realizes the formula (A.6) at level
$0$
.
4) If
$\Psi (x_1,\dots ,x_n)$
is the formula
$\neg A(x_i,x_j,x_m)$
, where
$1\le i,j,m\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \mathcal A(x_i,x_j,x_m)$
and in this case the formula (7) is
$$ \begin{align} \forall\mathbf x,\mathbf y\, (\neg\neg\mathcal E(x_1,y_1)\,\&\cdots\&\,\neg\neg\mathcal E(x_n,y_n)\,\&\,\neg\mathcal A(x_i,x_j,x_m)\to\neg\mathcal A(y_i,y_j,y_m)). \end{align} $$
First we prove that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
the formula
$$ \begin{align} \neg\neg\mathcal E(k_1,\ell_1)\,\&\cdots\&\,\neg\neg\mathcal E(k_n,\ell_n)\,\&\,\neg\mathcal A(k_i,k_j,k_m)\to\neg\mathcal A(\ell_i,\ell_j,\ell_m) \end{align} $$
is spr-realizable.
If the premise of the formula (A.9) is not spr-realizable, then by Proposition 3.4, the number
$\mathsf a_{\mathsf a}$
spr-realizes the formula (A.9) at level 0. Suppose that the premise of the formula (A.9) is spr-realizable. Then the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
,
$\neg \neg \mathcal E(k_j,\ell _j)$
,
$\neg \neg \mathcal E(k_m,\ell _m)$
, and
$\neg \mathcal A(k_i,k_j,k_m)$
are realizable. We prove that the conclusion of the formula (A.9), i.e.,
$\neg \mathcal A(\ell _i,\ell _j,\ell _m)$
, is realizable as well. By Proposition 3.4, it is enough to prove that the formula
$\neg \neg \mathcal A(\ell _i,\ell _j,\ell _m)$
is not realizable. Suppose that this formula is spr-realizable. Thus we have that the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
,
$\neg \neg \mathcal E(k_j,\ell _j)$
,
$\neg \neg \mathcal E(k_m,\ell _m)$
, and
$\neg \neg \mathcal A(\ell _i,\ell _j,\ell _m)$
are spr-realizable. Since the formula
$\widetilde {A_2}$
is spr-realizable, it follows that the formulas
$\neg \neg \mathcal E(\ell _i,k_i)$
,
$\neg \neg \mathcal E(\ell _j,k_j)$
, and
$\neg \neg \mathcal E(\ell _m,k_m)$
are also spr-realizable. Note that the formula
$\widetilde {A_{15}}$
is spr-realizable. It follows that the formula
$$ \begin{align*}\neg\neg\mathcal E(\ell_i,k_i)\,\&\,\neg\neg\mathcal E(\ell_j,k_j)\,\&\,\neg\neg\mathcal E(\ell_m,k_m)\,\&\, \neg\neg\mathcal A(\ell_i,\ell_j,\ell_m)\to\neg\neg\mathcal A(k_i,k_j,k_m)\end{align*} $$
is spr-realizable. Since the premise of this implication is spr-realizable, it follows that its conclusion
$\neg \neg \mathcal A(k_i,k_j,k_m)$
is spr-realizable in contradiction with the assumption that
$\neg \mathcal A(k_i,k_j,k_m)$
is spr-realizable. Thus
$\neg \mathcal A(\ell _i,\ell _j,\ell _m)$
is spr-realizable. By Proposition 3.4, we have
$\mathsf a\Vdash _0\neg \mathcal A(\ell _i,\ell _j,\ell _m)$
and the number
$\mathsf a_{\mathsf a}$
spr-realizes (A.9) at level
$0$
. We have proved that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the number
$\mathsf a_{\mathsf a}$
spr-realizes (A.9) at level
$0$
. Evidently, the number
$\Lambda x_1.\ldots \Lambda x_n.\Lambda y_1.\ldots \Lambda y_n.\mathsf a_{\mathsf a}$
spr-realizes the formula (A.8) at level
$0$
.
5) If
$\Psi (x_1,\dots ,x_n)$
is the formula
$\neg M(x_i,x_j,x_m)$
, where
$1\le i,j,m\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \mathcal M(x_i,x_j,x_m)$
and in this case the formula (7) is
$$ \begin{align} \forall\mathbf x,\mathbf y (\neg\neg\mathcal E(x_1,y_1)\&\cdots\&\neg\neg\mathcal E(x_n,y_n)\&\neg\mathcal M(x_i,x_j,x_m)\to\neg\mathcal M(y_i,y_j,y_m)). \end{align} $$
spr-realizability of the formula (A.10) is proved by the same argument as in the case of the formula (A.8); only one should replace
$\mathcal A$
by
$\mathcal M$
and use the formula
$\widetilde {A_{20}}$
instead of
$\widetilde {A_{15}}$
.
6) If
$\Psi (x_1,\dots ,x_n)$
is
$\neg \Psi _0(x_1,\dots ,x_n)$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \widetilde {\Psi _0}(x_1,\dots ,x_n)$
. By the inductive hypothesis, the formula
$$ \begin{align} \forall\mathbf x,\mathbf y\,(\neg\neg{\mathcal E}(x_1,y_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(x_n,y_n)\,\&\, \widetilde{\Psi_0}(\mathbf x)\to\widetilde{\Psi_0}(\mathbf y)) \end{align} $$
is spr-realizable. We have to prove that the formula
$$ \begin{align} \forall\mathbf x,\mathbf y\,(\neg\neg{\mathcal E}(x_1,y_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(x_n,y_n)\,\&\, \neg\widetilde{\Psi_0}(\mathbf x)\to\neg\widetilde{\Psi_0}(\mathbf y)) \end{align} $$
is spr-realizable.
First we prove that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
the formula
$$ \begin{align} \neg\neg{\mathcal E}(k_1,\ell_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(k_n,\ell_n)\,\&\,\neg\widetilde{\Psi_0}(\mathbf k)\to \neg\widetilde{\Psi_0}(\mathbf l)), \end{align} $$
where
$\mathbf k$
is the list
$k_1,\ldots ,k_n$
and
$\mathbf l$
is the list
$\ell _1,\ldots ,\ell _n$
, is spr-realizable.
If the premise of (A.13) is not spr-realizable, then by Proposition 3.4, the number
$\mathsf a_{\mathsf a}$
spr-realizes the formula (A.13) at level 0. Suppose that the premise of the formula (A.13) is spr-realizable. Then the formulas
$\neg \neg \mathcal E(k_i,\ell _i)(i=1,\ldots ,n)$
and
$\neg \widetilde {\Psi _0}(\mathbf k)$
are spr-realizable. We prove that the conclusion of the formula (A.13), i.e.,
$\neg \widetilde {\Psi _0}(\mathbf l)$
, is spr-realizable as well. By Proposition 3.4, it is enough to prove that the formula
$\widetilde {\Psi _0}(\mathbf l)$
is not spr-realizable. Suppose the opposite. Thus we have that the formulas
$\neg \neg \mathcal E(k_i,\ell _i) (i=1,\ldots ,n)$
and
$\widetilde {\Psi _0}(\mathbf l)$
are spr-realizable. Since
$\widetilde {A_2}$
is spr-realizable, it follows that the formulas
$\neg \neg \mathcal E(\ell _i,k_i) (i=1,\ldots ,n)$
are also spr-realizable. Since the formula (A.11) is spr-realizable, then it follows that the formula
$\neg \neg {\mathcal E}(\ell _1,k_1)\,\&\cdots \&\,\neg \neg {\mathcal E}(\ell _n,k_n)\,\&\,\widetilde {\Psi _0}(\mathbf l)\to \widetilde {\Psi _0}(\mathbf k)$
is spr-realizable. Since the premise of this implication is spr-realizable, it follows that its conclusion
$\widetilde {\Psi _0}(\mathbf k)$
is spr-realizable in contradiction with the assumption that the formula
$\neg \widetilde {\Psi _0}(\mathbf k)$
is spr-realizable. Thus
$\neg \widetilde {\Psi _0}(\mathbf l)$
is spr-realizable. By Proposition 3.4,
$\mathsf a\Vdash _0\neg \widetilde {\Psi _0}(\mathbf l)$
and the number
$\mathsf a_{\mathsf a}$
spr-realizes (A.13) at level
$0$
. We have proved that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the number
$\mathsf a_{\mathsf a}$
spr-realizes (A.13) at level
$0$
. Evidently, the number
$\Lambda x_1.\ldots \Lambda x_n.\Lambda y_1.\ldots \Lambda y_n.\mathsf a$
spr-realizes the formula (A.12) at level
$0$
.
7) If
$\Psi (x_1,\dots ,x_n)$
is
$\Psi _1(x_1,\dots ,x_n)\,\&\,\Psi _2(x_1,\dots ,x_n)$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is the formula
$\widetilde {\Psi _1}(x_1,\dots ,x_n)\,\&\,\widetilde {\Psi _2}(x_1,\dots ,x_n)$
. By the inductive hypothesis, the formulas
$$ \begin{align} \forall\mathbf x,\mathbf y\,(\neg\neg{\mathcal E}(x_1,y_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(x_n,y_n)\,\&\, \widetilde{\Psi_1}(\mathbf x)\to\widetilde{\Psi_1}(\mathbf y)) \end{align} $$
and
$$ \begin{align} \forall\mathbf x,\mathbf y\,(\neg\neg{\mathcal E}(x_1,y_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(x_n,y_n)\,\&\, \widetilde{\Psi_2}(\mathbf x)\to\widetilde{\Psi_2}(\mathbf y)) \end{align} $$
are spr-realizable. We have to prove that the formula
$$ \begin{align} \forall\mathbf x,\mathbf y\,(\neg\neg{\mathcal E}(x_1,y_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(x_n,y_n)\,\&\, \widetilde{\Psi_1}(\mathbf x)\,\&\,\widetilde{\Psi_2}(\mathbf x)\to\widetilde{\Psi_1}(\mathbf y)\,\&\,\widetilde{\Psi_2}(\mathbf y)) \end{align} $$
is spr-realizable.
First we prove that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
the formula
$$ \begin{align} \neg\neg{\mathcal E}(k_1,\ell_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(k_n,\ell_n)\,\&\,\widetilde{\Psi_1}(\mathbf k)\,\&\, \widetilde{\Psi_2}(\mathbf k)\to\widetilde{\Psi_1}(\mathbf l)\,\&\,\widetilde{\Psi_2}(\mathbf l) \end{align} $$
is spr-realizable. Suppose that the premise of (A.17) is spr-realizable. Then the formulas
$\neg \neg \mathcal E(k_i,\ell _i) (i=1,\ldots ,n)$
and
$\widetilde {\Psi _1}(\mathbf k)\,\&\,\widetilde {\Psi _2}(\mathbf k)$
are spr-realizable. By Proposition 3.4, the formulas
$\widetilde {\Psi _1}(\mathbf k)$
and
$\widetilde {\Psi _2}(\mathbf k)$
are spr-realizable. We prove that the conclusion of (A.17), i.e.,
$\widetilde {\Psi _1}(\mathbf l)\,\&\,\widetilde {\Psi _2}(\mathbf l)$
, is spr-realizable. By Proposition 3.4, it is enough to prove that
$\widetilde {\Psi _1}(\mathbf l)$
and
$\widetilde {\Psi _2}(\mathbf l)$
are realizable. But this follows from spr-realizability of (A.14) and (A.15). By Proposition 5.13,
$a_{\Psi _i}\Vdash _0\Psi _i(\ell _1,\ldots ,\ell _n)$
for
$i=1,2$
. It follows that
$\langle a_{\Psi _1},a_{\Psi _2}\rangle \Vdash _0\Psi _1(\ell _1,\ldots ,\ell _n)\,\&\,\Psi _2(\ell _1,\ldots ,\ell _n)$
and
$\mathsf a_{\langle a_{\Psi _1},a_{\Psi _2}\rangle }$
spr-realizes (A.17) at level
$0$
. If the premise of (A.17) is not spr-realizable, then by Proposition 3.4, the number
$\mathsf a_{\langle a_{\Psi _1},a_{\Psi _2}\rangle }$
spr-realizes (A.17) at level
$0$
. We see that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the number
$\mathsf a_{\langle a_{\Psi _1},a_{\Psi _2}\rangle }$
spr-realizes the formula (A.17) at level
$0$
. Evidently, the number
$\Lambda x_1.\ldots \Lambda x_n.\Lambda y_1.\ldots \Lambda y_n.\mathsf a_{\langle a_{\Psi _1},a_{\Psi _2}\rangle }$
spr-realizes the formula (A.16) at level
$0$
.
8) Assume that
$\Psi (x_1,\dots ,x_n)$
is the formula
$\Psi _1(x_1,\dots ,x_n)\to \Psi _2(x_1,\dots ,x_n)$
and the formulas (A.14) and (A.15) are spr-realizable. We have to prove that the formula
$$ \begin{align} \hspace{-0.5pc} \forall\mathbf x,\mathbf y(\neg\neg{\mathcal E}(x_1,y_1)\&\cdots\&\neg\neg{\mathcal E}(x_n,y_n)\& (\widetilde{\Psi_1}(\mathbf x)\to\widetilde{\Psi_2}(\mathbf x))\to(\widetilde{\Psi_1}(\mathbf y)\to\widetilde{\Psi_2}(\mathbf y)) \end{align} $$
is spr-realizable.
First we prove that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the formula
$$ \begin{align} \neg\neg{\mathcal E}(k_1,\ell_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(k_n,l_n)\,\&\,(\widetilde{\Psi_1}(\mathbf k)\to\widetilde{\Psi_2}(\mathbf k))\to (\widetilde{\Psi_1}(\mathbf l)\to\widetilde{\Psi_2}(\mathbf l)) \end{align} $$
is spr-realizable. Suppose that the premise of the formula (A.19) is spr-realizable. This means that the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
$(i=1,\ldots ,n)$
and
$\widetilde {\Psi _1}(\mathbf k)\to \widetilde {\Psi _2}(\mathbf k)$
are spr-realizable. Since
$\widetilde {A_2}$
is spr-realizable, it follows that the formulas
$\neg \neg \mathcal E(\ell _i,k_i) (i=1,\ldots ,n)$
are also spr-realizable. We prove that the conclusion of (A.19), i.e.,
$\widetilde {\Psi _1}(\mathbf l)\to \widetilde {\Psi _2}(\mathbf l)$
, is spr-realizable. If the formula
$\widetilde {\Psi _1}(\mathbf l)$
is spr-realizable, then it follows from spr-realizability of the formula (A.14) that the formula
$\widetilde {\Psi _1}(\mathbf k)$
is spr-realizable. Therefore, the formula
$\widetilde {\Psi _2}(\mathbf k)$
is also spr-realizable. Now spr-realizability of
$\widetilde {\Psi _2}(\mathbf l)$
follows from spr-realizability of the formula (A.15). Since the predicate
$Ar$
-formula
$\Psi _2$
is completely negative, it follows from Proposition 5.13 that
$a_{\Psi _2}\Vdash _0\Psi _2(\mathbf l)$
. Therefore, by Proposition 3.4,
$$ \begin{align} \mathsf a_{a_{\Psi_2}}\Vdash_0\Psi_1(\mathbf l)\to\Psi_2(\mathbf l). \end{align} $$
If the formula
$\widetilde {\Psi _1}(\mathbf l)$
is not spr-realizable, then (A.20) holds by Proposition 3.4. Let
$b=\mathsf a_{a_{\Psi _2}}$
. By Proposition 3.4, the number
$\mathsf a_b$
spr-realizes the formula (A.19) at level 0. If the premise of the formula (A.19) is not realizable, then the number
$\mathsf a_b$
spr-realizes the formula (A.19) at level 0. Thus we have proved that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the number
$\mathsf a_b$
spr-realizes the formula (A.19) at level 0. Now it is evident that the number
$\Lambda x_1.\ldots \Lambda x_n.\Lambda y_1.\ldots \Lambda y_n.\mathsf a_b$
spr-realizes the formula (A.18) at level
$0$
.
9) Assume that
$\Psi (x_1,\dots ,x_n)$
is the formula
$\forall x\,\Psi _0(x,x_1,\dots ,x_n)$
. The inductive hypothesis states that the formula
$$ \begin{align} \forall x\forall\mathbf x\forall y\forall\mathbf y\,(\neg\neg{\mathcal E}(x,y)\,\&\,\neg\neg{\mathcal E}(x_1,y_1)\,\&\, \neg\neg{\mathcal E}(x_n,y_n)\,\&\,\widetilde{\Psi_0}(x,\mathbf x)\to\widetilde{\Psi_0}(y,\mathbf y)) \end{align} $$
is spr-realizable. We have to prove that the formula
$$ \begin{align} \forall\mathbf x,\mathbf y\,(\neg\neg{\mathcal E}(x_1,y_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(x_n,y_n)\,\&\, \forall x\,\widetilde{\Psi_0}(x,\mathbf x)\to\forall x\,\widetilde{\Psi_0}(x,\mathbf y)) \end{align} $$
is spr-realizable. First we prove that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the formula
$$ \begin{align} \neg\neg{\mathcal E}(k_1,\ell_1)\,\&\cdots\&\,\neg\neg{\mathcal E}(k_n,\ell_n)\,\&\,\forall x\,\widetilde{\Psi_0}(x,\mathbf k)\to \forall x\,\widetilde{\Psi_0}(x,\mathbf l) \end{align} $$
is spr-realizable. Assume that the premise of the formula (A.23) is spr-realizable. This means that the formulas
$\neg \neg \mathcal E(k_i,\ell _i)$
(
$i=1,\ldots ,n$
) and
$\forall x\,\widetilde {\Psi }(x,\mathbf k)$
are spr-realizable. We prove that the conclusion of the formula (A.23), i.e.,
$\forall x\,\widetilde {\Psi _0}(x,\mathbf l)$
is spr-realizable. First we prove that for any
$\ell $
, the formula
$\widetilde {\Psi _0}(\ell ,\mathbf l)$
is spr-realizable. Note that the formula
$\widetilde {\Psi _0}(\ell ,\mathbf k)$
is spr-realizable. Since the formula
$\widetilde {A_1}$
is spr-realizable, it follows that the formula
$\neg \neg {\mathcal E}(\ell ,\ell )$
is spr-realizable. Now it follows from spr-realizability of the formula (A.21) that
$\widetilde {\Psi _0}(\ell ,\mathbf l)$
is spr-realizable. Since
$\Psi _0$
is a completely negative formula, it follows from Proposition 5.13 that
$a_{\Psi _0}\Vdash _0\widetilde {\Psi _0}(\ell ,\mathbf l)$
. It is evident that
$\Lambda x.a_{\Psi _0}\Vdash _0\forall x\,\widetilde {\Psi _0}(x,\mathbf l)$
. By Proposition 3.4, the number
$\mathsf a_{\Lambda x.a_{\Psi _0}}$
spr-realizes the formula (A.23) at level 0. If the premise of the formula (A.23) is not spr-realizable, then by Proposition 3.4, the number
$\mathsf a_{\Lambda x.a_{\Psi _0}}$
spr-realizes the formula (A.23) at level 0. Thus we have proved that for any
$k_1,\ldots ,k_n,\ell _1,\ldots ,\ell _n$
, the number
$\mathsf a_{\Lambda x.a_{\Psi _0}}$
spr-realizes the formula (A.23) at level 0. Now it is evident that the number
$\Lambda x_1.\ldots \Lambda x_n.\Lambda y_1.\ldots \Lambda y_n.\mathsf a_{\Lambda x.a_{\Psi }}$
spr-realizes the formula (A.22) at level
$0$
.
B Appendix: Proof of Proposition 6.19
Assume that
$$ \begin{align*}{{\boldsymbol\Phi }}={\mathcal Z}(x_1),{\mathcal S}(x_1,x_2),{\mathcal A}(x_1,x_2,x_3),{\mathcal M}(x_1,x_2,x_3),{\mathcal E}(x_1,x_2)\end{align*} $$
is an interpretation of the formula Q. The formula
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is built from the formulas
$\neg \mathcal Z(x_i)$
,
$\neg {\mathcal S}(x_i,x_j)$
,
$\neg \mathcal A(x_i,x_j,x_k)$
,
$\neg \mathcal M(x_i,x_j,x_k),$
and
$\neg \mathcal E(x_i,x_j)$
, where
$1\le i,j,k\le n$
, using the logical symbols
$\neg $
,
$\&$
, and
$\to $
. We prove the proposition by induction on the complexity of
$\Psi (x_1,\dots ,x_n)$
.
1) If
$\Psi (x_1,\dots ,x_n)$
is
$\neg E(x_i,x_j)$
, where
$1\le i,j\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \mathcal E(x_i,x_j)$
. If
$i=j$
, then the formula
$\neg E(k_i,k_j)$
is not true. On the other hand, since the formula
$\widetilde {A_1}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable and the formula
$\neg \mathcal E(\widetilde {k_i},\widetilde {k_j})$
is not spr-realizable. Thus
$\neg E(k_i,k_j)$
is true iff
$\neg \mathcal E(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable. Now assume that
$i\not =j$
. Suppose that the formula
$\neg E(k_i,k_j)$
is true. This means that
$k_i\not =k_j$
. We prove that the formula
$\neg \mathcal E(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable. By Proposition 3.4, it is enough to prove that the formula
$\neg \neg \mathcal E(\widetilde {k_i},\widetilde {k_j})$
is not spr-realizable. Assume the opposite. By Proposition 6.17, we have that the formula
$\widetilde {[k_i]}(\widetilde {k_i})$
is spr-realizable. Then by Proposition 6.14, the formula
$\widetilde {[k_i]}(\widetilde {k_j})$
is spr-realizable as well. On the other hand, the formula
$\widetilde {[k_j]}(\widetilde {k_j})$
is spr-realizable. By Proposition 6.18,
$k_i=k_j$
in contradiction with the assumption that the formula
$\neg E(k_i,k_j)$
is true. Thus the formula
$\neg \mathcal E(\widetilde {k_i},\widetilde {k_j})$
is realizable. Conversely, assume that the formula
$\neg \mathcal E(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable. We prove that the formula
$\neg E(k_i,k_j)$
is true, i.e.,
$k_i\not =k_j$
. Suppose the opposite. Then
$\widetilde {k_i}=\widetilde {k_j}$
. Since the formula
$\widetilde {A_1}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable in contradiction with the assumption that the formula
$\neg \mathcal E(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable. Thus
$k_i\not =k_j$
and the formula
$\neg E(k_i,k_j)$
is true.
2) If
$\Psi (x_1,\dots ,x_n)$
is
$\neg Z(x_i)$
, where
$1\le i\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \mathcal Z(x_i)$
. Assume that the formula
$\neg Z(k_i)$
is true. This means that
$k_i\not =0$
. We prove that the formula
$\neg \mathcal Z(\widetilde {k_i})$
is spr-realizable. Suppose the opposite. Then the formula
$\neg \neg \mathcal Z(\widetilde {k_i})$
, i.e.,
$\widetilde {[0]}(\widetilde {k_i})$
is spr-realizable. On the other hand, the formula
$\widetilde {[k_i]}(\widetilde {k_i})$
is spr-realizable as well. By Proposition 6.18,
$k_i=0$
in contradiction with the assumption that the formula
$\neg Z(k_i)$
is true. Conversely, assume that the formula
$\neg \mathcal Z(\widetilde {k_i})$
is spr-realizable. Then the formula
$\neg \neg \mathcal Z(\widetilde {k_i})$
, i.e.,
$\widetilde {[0]}(\widetilde {k_i})$
, is not spr-realizable. We prove that the formula
$\neg Z(k_i)$
is true, i.e.,
$k_i\not =0$
. Suppose the opposite. Then the formula
$\widetilde {[0]}(\widetilde {k_i})$
is spr-realizable. This contradiction proves that the formula
$\neg Z(k_i)$
is true.
3) If
$\Psi (x_1,\dots ,x_n)$
is
$\neg S(x_i,x_j)$
, where
$1\le i,j\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is the formula
$\neg \mathcal S(x_i,x_j)$
. Assume that the formula
$\neg S(k_i,k_j)$
is true. This means that
$k_j\not =k_i+1$
. We prove that the formula
$\neg \mathcal S(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable. Suppose the opposite. Then the formula
$\neg \neg \mathcal S(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable. Let us prove that the formula
$\widetilde {[k_i+1]}(\widetilde {k_j})$
, i.e.,
$$ \begin{align} \neg\mathcal Z(\widetilde{k_j})\,\&\,\forall y\,(\neg\neg\mathcal S(y,\widetilde{k_j})\to\widetilde{[k_i]}(y)), \end{align} $$
is spr-realizable. Since the formulas
$\neg \neg \mathcal S(\widetilde {k_i},\widetilde {k_j})$
and
$\widetilde {A_{11}}$
are spr-realizable, it follows that the formula
$\neg \mathcal Z(\widetilde {k_j})$
is spr-realizable. Let
$\ell $
be an arbitrary natural number. We prove that the formula
$$ \begin{align} \neg\neg\mathcal S(\ell,\widetilde{k_j})\to\widetilde{[k_i]}(\ell) \end{align} $$
is spr-realizable. Assume that the premise of the formula (B.2), i.e.,
$\neg \neg \mathcal S(\ell ,\widetilde {k_j})$
, is spr-realizable. Thus we have that the formulas
$\neg \neg \mathcal S(\widetilde {k_i},\widetilde {k_j})$
and
$\neg \neg \mathcal S(\ell ,\widetilde {k_j})$
are spr-realizable. Since the formula
$\widetilde {A_{10}}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(\widetilde {k_i},\ell )$
is spr-realizable. It follows from Proposition 6.14 that the formula
$\widetilde {[k_i]}(\ell )$
is spr-realizable. By Proposition 5.13,
$a_{[k_i](x)}\Vdash _0\widetilde {[k_i]}(\ell )$
and by Proposition 3.4, the number
$\mathsf a_{a_{[k_i](x)}}$
spr-realizes the formula (B.2) at level 0. If the premise of the formula (B.2) is not spr-realizable, then by Proposition 3.4, the number
$\mathsf a_{a_{[k_i](x)}}$
spr-realizes the formula (B.2) at level 0. Thus, for any
$\ell $
, the number
$\mathsf a_{a_{[k_i](x)}}$
spr-realizes (B.2) at level 0. Now it is evident that
$\Lambda y.\mathsf a_{a_{[k_i](x)}}\Vdash _0\forall y\,(\neg \neg \mathcal S(y,\widetilde {k_j})\to \widetilde {[k_i]}(y))$
. Thus it is proved that the formula
$\widetilde {[k_i+1]}(\widetilde {k_j})$
is spr-realizable. Since the formula
$\widetilde {[k_j]}(\widetilde {k_j})$
is also spr-realizable, it follows from Proposition 6.18 that
$k_i+1=k_j$
in contradiction with the assumption that the formula
$\neg S(k_i,k_j)$
is true. Thus the formula
$\neg \mathcal S(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable. Conversely, assume that the formula
$\neg \mathcal S(\widetilde {k_i},\widetilde {k_j})$
is realizable. We prove that the formula
$\neg S(k_i,k_j)$
is true, i.e.,
$k_j\not =k_i+1$
. Suppose the opposite. Then the formula
$\widetilde {[k_i+1]}(\widetilde {k_j})$
, i.e., (B.1), is spr-realizable. It follows that the formula
$\neg \mathcal Z(k_j)$
is spr-realizable. Since the formula
$\widetilde {A_{12}}$
is spr-realizable, it follows that there exists a natural number
$\ell $
such that the formula
$\neg \neg \mathcal S(\ell ,\widetilde {k_j})$
is spr-realizable. On the other hand, since the formula (B.1) is spr-realizable, it follows that
$\neg \neg \mathcal S(\ell ,\widetilde {k_j})\to \widetilde {[k_i]}(\ell )$
is spr-realizable, thus the formula
$\widetilde {[k_i]}(\ell )$
is realizable. Since the formula
$\widetilde {[k_i]}(\widetilde {k_i})$
is also spr-realizable, it follows from Proposition 6.15 that the formula
$\neg \neg \mathcal E(\ell ,\widetilde {k_i})$
is spr-realizable. By Proposition 6.14, the formula
$\neg \neg \mathcal S(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable in contradiction with the assumption that the formula
$\neg \mathcal S(\widetilde {k_i},\widetilde {k_j})$
is spr-realizable. Thus it is proved that the formula
$\neg S(k_i,k_j)$
is true.
4) If
$\Psi (x_1,\dots ,x_n)$
is the formula
$\neg A(x_i,x_j,x_m)$
, where
$1\le i,j,m\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \mathcal A(x_i,x_j,x_m)$
. We prove the proposition by induction on
$k_j$
. Let
$k_j=0$
. Then
$\widetilde {k_j}=\tilde 0$
and the formula
$\widetilde {[0]}(\widetilde {k_j})$
, i.e.,
$\neg \neg \mathcal Z(\widetilde {k_j})$
, is spr-realizable. Assume that the formula
$\neg A(k_i,k_j,k_m)$
is true. This means that
$k_m\not =k_i$
. We prove that the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Suppose the opposite. Then the formula
$\neg \neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Since the formula
$\widetilde {A_{16}}$
is realizable, it follows that the formula
$\neg \neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_i})$
is spr-realizable. Since the formula
$\widetilde {A_{14}}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(\widetilde {k_m},\widetilde {k_i})$
is spr-realizable. As it was proved above in the case 1), the formula
$E(k_m,k_i)$
is true, i.e.,
$k_m=k_i$
in contradiction with the assumption that the formula
$\neg A(k_i,k_j,k_m)$
is true. Thus we have proved that the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Conversely, assume that the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. We prove that the formula
$\neg A(k_i,k_j,k_m)$
is true, i.e.,
$k_m\not =k_i$
. Suppose the opposite. Then
$\widetilde {k_m}=\widetilde {k_i}$
. Since the formula
$\widetilde {A_{16}}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable in contradiction with the assumption that the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Thus we have proved that the formula
$\neg A(k_i,k_j,k_m)$
is true. Now suppose that
$k_j=\ell _j+1$
and for any
$k_i,\ell _m$
, the formula
$\neg A(k_i,\ell _j,\ell _m)$
is true iff the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {\ell _j},\widetilde {\ell _m})$
is spr-realizable. Note that the formula
$\neg S(\ell _j,k_j)$
is not true. As it was proved in the case 3) above, the formula
$\neg \mathcal S(\widetilde {\ell _j},\widetilde {k_j})$
is not spr-realizable. Then the formula
$\neg \neg \mathcal S(\widetilde {\ell _j},\widetilde {k_j})$
is spr-realizable. Assume that the formula
$\neg A(k_i,k_j,k_m)$
is true. This means that
$k_m\not =k_i+k_j$
. We prove that the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Suppose the opposite. Then the formula
$\neg \neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. On the other hand, since the formula
$\neg A(k_i,\ell _j,k_i+\ell _j)$
is not true, then by the inductive hypothesis, the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {\ell _j},\widetilde {k_i+\ell _j})$
is not spr-realizable. Then the formula
$\neg \neg \mathcal A(\widetilde {k_i},\widetilde {\ell _j},\widetilde {k_i+\ell _j})$
is spr-realizable. Let
$\ell _m=k_i+\ell _j+1$
. Then the formula
$S(k_i+\ell _j,\ell _m)$
is true and the formula
$\neg S(k_i+\ell _j,\ell _m)$
is not true. As it was proved above in the case 3), the formula
$\neg \mathcal S(\widetilde {k_i+\ell _j},\widetilde {\ell _m})$
is not spr-realizable. Then the formula
$\neg \neg \mathcal S(\widetilde {k_i+\ell _j},\widetilde {\ell _m})$
is spr-realizable. Since the formula
$\widetilde {A_{17}}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {\ell _m})$
is spr-realizable. Since the formula
$\widetilde {A_{14}}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal E(k_m,\ell _m)$
is spr-realizable. As it was proved above, the formula
$E(k_m,\ell _m)$
is true, i.e.,
$k_m=\ell _m=k_i+\ell _j+1=k_i+k_j$
. This means that the formula
$A(k_i,k_j,k_m)$
is true in contradiction with the assumption that the formula
$\neg A(k_i,k_j,k_m)$
is true. Thus we have proved that the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Conversely, assume that the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. We prove that the formula
$\neg A(k_i,k_j,k_m)$
is true. Suppose the opposite. Then the formula
$A(k_i,k_j,k_m)$
is true. This means that
$k_m=k_i+k_j$
. Let
$\ell _m=k_i+\ell _j$
. Then
$k_m=\ell _m+1$
and the formula
$\neg A(k_i,\ell _j,\ell _m)$
is not true. By the inductive hypothesis, the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {\ell _j},\widetilde {\ell _m})$
is not spr-realizable. Then the formula
$\neg \neg \mathcal A(\widetilde {k_i},\widetilde {\ell _j},\widetilde {\ell _m})$
is spr-realizable. On the other hand, since the formulas
$S(\ell _j,k_j)$
and
$S(\ell _m,k_m)$
are true, it follows that the formulas
$\neg S(\ell _j,k_j)$
and
$\neg S(\ell _m,k_m)$
are not true. It follows from the case 3) above that the formulas
$\neg \mathcal S(\widetilde {\ell _j},\widetilde {k_j})$
and
$\neg \mathcal S(\widetilde {\ell _m},\widetilde {k_m})$
are not spr-realizable. Then the formulas
$\neg \neg \mathcal S(\widetilde {\ell _j},\widetilde {k_j})$
and
$\neg \neg \mathcal S(\widetilde {\ell _m},\widetilde {k_m})$
are spr-realizable. Since the formula
$\widetilde {A_{17}}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable in contradiction with the assumption that the formula
$\neg \mathcal A(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Thus we have proved that the formula
$\neg A(k_i,k_j,k_m)$
is true.
5) If
$\Psi (x_1,\dots ,x_n)$
is the formula
$\neg M(x_i,x_j,x_m)$
, where
$1\le i,j,m\le n$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \mathcal M(x_i,x_j,x_m)$
. We prove the proposition by induction on
$k_j$
. Let
$k_j=0$
. Then the formula
$\widetilde {[0]}(\widetilde {k_j})$
, i.e.,
$\neg \neg \mathcal Z(\widetilde {k_j})$
, is spr-realizable. Assume that the formula
$\neg M(k_i,k_j,k_m)$
is true. We prove that the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Suppose the opposite. Then the formula
$\neg \neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Since the formula
$\widetilde {A_{21}}$
is spr-realizable, it follows that
$\neg \neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_j})$
is spr-realizable. Since the formula
$\widetilde {A_{19}}$
is realizable, it follows that the formula
$\neg \neg \mathcal E(\widetilde {k_m},\widetilde {k_j})$
is spr-realizable. As it was proved above in the case 1), the formula
$E(k_m,k_j)$
is true, i.e.,
$k_m=k_j$
. Then the formula
$M(k_i,k_j,k_m)$
is true in contradiction with the assumption that the formula
$\neg M(k_i,k_j,k_m)$
is true. Thus we have proved that the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Conversely, assume that the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. We prove that the formula
$\neg M(k_i,k_j,k_m)$
is true. Suppose the opposite. Then
$k_m=k_j$
and
$\widetilde {k_m}=\widetilde {k_j}$
. Since the formula
$\widetilde {A_{21}}$
is realizable, it follows that the formula
$\neg \neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable in contradiction with the assumption that the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Thus we have proved that the formula
$\neg M(k_i,k_j,k_m)$
is true. Now suppose that
$k_j=\ell _j+1$
and for any
$k_i,\ell _m$
, the formula
$\neg M(k_i,\ell _j,\ell _m)$
is true iff the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {\ell _j},\widetilde {\ell _m})$
is spr-realizable. As it was shown in the case 3) above, the formula
$\neg \neg \mathcal S(\widetilde {\ell _j},\widetilde {k_j})$
is spr-realizable. Assume that the formula
$\neg M(k_i,k_j,k_m)$
is true. We prove that the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Suppose the opposite. Then the formula
$\neg \neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Since the formula
$M(k_i,\ell _j,k_i\cdot \ell _j)$
is true, then the formula
$\neg M(k_i,\ell _j,k_i\cdot \ell _j)$
is not true. By the inductive hypothesis, the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {\ell _j},\widetilde {k_i\cdot \ell _j})$
is not spr-realizable. Then the formula
$\neg \neg \mathcal M(\widetilde {k_i},\widetilde {\ell _j},\widetilde {k_i\cdot \ell _j})$
is spr-realizable. Let
$\ell _m=k_i\cdot \ell _j+k_i$
. Then the formula
$A(k_i\cdot \ell _j,k_i,\ell _m)$
is true and the formula
$\neg A(k_i\cdot \ell _j,k_i,\ell _m)$
is not true. As it was proved in the case 5) above, the formula
$\neg \mathcal A(\widetilde {k_i\cdot \ell _j},\widetilde {k_i},\widetilde {\ell _m})$
is not spr-realizable. Then the formula
$\neg \neg \mathcal A(\widetilde {k_i\cdot \ell _j},\widetilde {k_i},\widetilde {\ell _m})$
is spr-realizable. Since the formula
$\widetilde {A_{22}}$
is spr-realizable, it follows that the formula
$\neg \neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {\ell _m})$
is realizable. Since the formula
$\widetilde {A_{19}}$
is spr-realizable, it follows that
$\neg \neg \mathcal E(k_m,\ell _m)$
is spr-realizable. As it was proved in the case 1) above,
$E(k_m,\ell _m)$
is true, i.e.,
$k_m=\ell _m=k_i+k_i\cdot \ell _j=k_i\cdot k_j$
. This means that the formula
$M(k_i,k_j,k_m)$
is true in contradiction with the assumption that the formula
$\neg M(k_i,k_j,k_m)$
is true. Thus we have proved that the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Conversely, assume that the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. We prove that the formula
$\neg M(k_i,k_j,k_m)$
is true. Suppose the opposite. Then
$k_m=k_i\cdot k_j$
. Let
$\ell _m=k_i\cdot \ell _j$
. Then the formula
$M(k_i,\ell _j,\ell _m)$
is true and
$k_m=\ell _m+k_i$
. This means that the formula
$A(\ell _m,k_i,k_m)$
is true. Then the formulas
$\neg M(k_i,\ell _j,\ell _m)$
and
$\neg A(\ell _m,k_i,k_m)$
are not true. By the inductive hypothesis, the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {\ell _j},\widetilde {\ell _m})$
is not spr-realizable. Then the formula
$\neg \neg \mathcal M(\widetilde {k_i},\widetilde {\ell _j},\widetilde {\ell _m})$
is spr-realizable. Since the formula
$\neg A(\ell _m,k_i,k_m)$
is not true, it follows from the case 4) above that the formula
$\neg \mathcal A(\widetilde {\ell _m},\widetilde {k_i},\widetilde {k_m})$
is not spr-realizable. Then the formula
$\neg \neg \mathcal A(\widetilde {\ell _m},\widetilde {k_i},\widetilde {k_m})$
is spr-realizable. Since the formula
$\widetilde {A_{22}}$
is realizable, it follows that the formula
$\neg \neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable in contradiction with the assumption that the formula
$\neg \mathcal M(\widetilde {k_i},\widetilde {k_j},\widetilde {k_m})$
is spr-realizable. Thus we have proved that the formula
$\neg M(k_i,k_j,k_m)$
is true.
6) If
$\Psi (x_1,\dots ,x_n)$
is
$\neg \Psi _0(x_1,\dots ,x_n)$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is
$\neg \widetilde {\Psi _0}(x_1,\dots ,x_n)$
. By the inductive hypothesis, for any natural
$k_1,\ldots ,k_m$
, the formula
$\Psi _0(k_1,\ldots ,k_m)$
is true iff the formula
$\widetilde {\Psi _0}(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable. Assume that the formula
$\neg \Psi _0(k_1,\ldots ,k_m)$
is true. Then the formula
$\Psi _0(k_1,\ldots ,k_m)$
is not true. By the inductive hypothesis, the formula
$\widetilde {\Psi _0}(\tilde k_1,\ldots ,\tilde k_m)$
it is not spr-realizable. By Proposition 3.4,
$\neg \widetilde {\Psi _0}(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable. Conversely, if
$\neg \widetilde {\Psi _0}(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable, then the formula
$\widetilde {\Psi _0}(\tilde k_1,\ldots ,\tilde k_m)$
is not spr-realizable. By the inductive hypothesis, the formula
$\Psi _0(k_1,\ldots ,k_m)$
it is not true and
$\neg \Psi _0(k_1,\ldots ,k_m)$
is true.
7) If
$\Psi (x_1,\dots ,x_n)$
is
$\Psi _1(x_1,\dots ,x_n)\,\&\,\Psi _2(x_1,\dots ,x_n)$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is the formula
$\widetilde {\Psi _1}(x_1,\dots ,x_n)\,\&\,\widetilde {\Psi _2}(x_1,\dots ,x_n)$
. By the inductive hypothesis, for
$i=1,2$
and any natural numbers
$k_1,\ldots ,k_m$
, the formula
$\Psi _i(k_1,\ldots ,k_m)$
is true iff the formula
$\widetilde {\Psi _i}(\tilde k_1,\ldots ,\tilde k_m)$
is realizable. The formula
$\Psi (k_1,\ldots ,k_m)$
is true iff the formulas
$\Psi _1(k_1,\ldots ,k_m)$
and
$\Psi _2(k_1,\ldots ,k_m)$
are both true. By the inductive hypothesis, this is possible iff the formulas
$\widetilde {\Psi _1}(\tilde k_1,\ldots ,\tilde k_m)$
and
$\widetilde {\Psi _2}(\tilde k_1,\ldots ,\tilde k_m)$
are both spr-realizable and, by Proposition 3.4, the formula
$\widetilde {\Psi }(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable.
8) If
$\Psi (x_1,\dots ,x_n)$
is
$\Psi _1(x_1,\dots ,x_n)\to \Psi _2(x_1,\dots ,x_n)$
, then
$\widetilde {\Psi }(x_1,\dots ,x_n)$
is the formula
$\widetilde {\Psi _1}(x_1,\dots ,x_n)\to \widetilde {\Psi _2}(x_1,\dots ,x_n)$
. The inductive hypothesis is the same as in the previous case. Assume that the formula
$\Psi (k_1,\ldots ,k_m)$
is true. This means that the formula
$\Psi _1(k_1,\ldots ,k_m)$
is false or the formula
$\Psi _2(k_1,\ldots ,k_m)$
is true. In the first case, by the inductive hypothesis, the formula
$\widetilde {\Psi _1}(\tilde k_1,\ldots ,\tilde k_m)$
is not spr-realizable and, by Proposition 3.4, the formula
$\widetilde {\Psi }(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable. In the second case, by the inductive hypothesis, the formula
$\widetilde {\Psi _2}(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable and, by Proposition 3.4, the formula
$\widetilde {\Psi }(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable. Conversely, assume that the formula
$\widetilde {\Psi }(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable. Then the formula
$\Psi (k_1,\ldots ,k_m)$
should be true because otherwise the formula
$\Psi _1(k_1,\ldots ,k_m)$
is true and the formula
$\Psi _2(k_1,\ldots ,k_m)$
is false. By the inductive hypothesis, the formula
$\widetilde {\Psi _1}(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable and the formula
$\widetilde {\Psi _2}(\tilde k_1,\ldots ,\tilde k_m)$
is not realizable. But this is impossible if the formula
$\widetilde {\Psi }(\tilde k_1,\ldots ,\tilde k_m)$
is spr-realizable.
Acknowledgment
The reported study was funded by RFBR, project number 20-01-00670.
