| Izvestiya: Mathematics |
|
|
|
|
|
The nonarithmeticity of the predicate logic of primitive recursive realizability V. E. Plisko Lomonosov Moscow State University, Faculty of Mechanics and Mathematics
Russian version:
Izvestiya Rossiiskoi Akademii Nauk. Seriya Matematicheskaya, 2023, Volume 87, Issue 2, DOI: https://doi.org/10.4213/im9288 
Bibliographic databases:
    § 1. IntroductionRecursive realizability introduced by Kleene [1] (see also [2], § 82), can be considered as an interpretation of the informal intuitionistic meaning of arithmetical sentences based on the theory of recursive functions. The main idea of recursive realizability is to replace the vague intuitionistic concept of an effective operation with the exact concept of a partial recursive function. On the other hand, many other more limited 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. The concept of primitive recursive realizability similar to the recursive realizability of Kleene but differing from it in that instead of the class of partial recursive functions only primitive recursive functions are considered was introduced by Salehi [3], [4]. The fundamental difference between these two interpretations is due to the fact that for the class of partial recursive functions there is a universal function in the same class and for primitive recursive functions there is no such function. In particular, therefore, there is no correctness of intuitionistic logic with respect to primitive recursive realizability. It turned out, however, that this interpretation is consistent with the so-called basic logic, the propositional version of which was introduced by Visser [5], and predicate by Ruitenburg [6]. Based on basic predicate logic, the basic arithmetic $\mathsf{BA}$ is constructed. Salehi proved the correctness of $\mathsf{BA}$ with respect to his variant of primitive recursive realizability. Primitive recursive realizability can be considered as a kind of constructive semantics of arithmetic sentences. For any semantics, it is of interest to study the corresponding logic. The author considered the predicate logic of Kleene’s recursive realizability. It has been proved [7], that the set of recursively realizable predicate formulas is not arithmetical. A similar result for the primitive recursive realizability of Salehi was obtained in the dissertation of Viter [8]. His technically quite complex proof is based on results about the arithmetical complexity of predicate logics of constructive arithmetical theories [9] and the translation of intuitionistic predicate logic into basic logic proposed by Ardeshir [10] and has not been published in the general press (there is only a deposited manuscript [11]). The purpose of this paper is to present a somewhat simplified proof of this result by direct application of the methods used in [7] to study the predicate logic of recursive realizability. A little earlier, Damnjanovic [12] has introduced another notion of primitive recursive realizability called strictly primitive recursive realizability combining the ideas of recursive realizability and Kripke models. These two variants of primitive recursive realizability (by Damnjanovic and by Salehi) are significantly different (see [13]): there is an arithmetical formula that is primitive recursively realizable in the sense of [3], but is not strictly primitive recursively realizable in the sense of [12], while its negation is strictly primitive recursively realizable but is not primitive recursively realizable. The dissertation of B. H. Park [14] (see also [15]) provides a proof of the nonarithmeticity of the predicate logic of strictly primitive recursive realizability essentially based on the claim that every formula deducible in the intuitionistic predicate calculus is strictly primitive recursively realizable (see [12], Lemma 4.3, Theorem 5.1). This claim was later refuted (see [16]). Nevertheless, the result is valid. The correct proof of this result is presented in the author’s paper [17]. The idea of that proof is in many ways similar to what is given in this paper in the study of predicate logic of primitive recursive realizability but these proofs differ technically due to the difference between the two variants of realizability. § 2. Indexing of primitive recursive functionsPrimitive recursive functions are obtained using substitution and recursion from the basic functions
$$
\begin{equation*}
O(x)=0, \quad S(x)=x+1, \quad I^m_i(x_1, \dots, x_m)=x_i\quad (m =1, 2, \dots;\ 1\leqslant i\leqslant m).
\end{equation*}
\notag
$$
For convenience, we add constant functions
$$
\begin{equation*}
\varphi(x_1, \dots, x_n)=q\quad (n=1, 2, \dots, \ q=0, 1, \dots)
\end{equation*}
\notag
$$
to the basic ones. If $a_0, \dots, a_n$ are natural numbers, then $\langle a_0, \dots, a_n\rangle$ will denote the number $p_0^{a_0}\cdots p_n^{a_n}$, where $p_0, \dots, p_n$ are consecutive primes ($p_0=2$, $p_1=3$, $p_2 =5$, $\dots$). It is known that $i\mapsto p_i$ and $(x, y)\mapsto\langle x, y\rangle$ are primitive recursive functions. Further, if $a\geqslant1$, $i\geqslant0$, then $[a]_i$ denotes the exponent with which $p_i$ enters in the representation of the number $a$ as a product of the powers of primes. Thus $[a]_i = a_i$, if $a=\langle a_0, \dots, a_n\rangle$. For certainty, put $[0]_i =0$ for all $i$. Note that the function $(x, i)\mapsto[x]_i$ is primitive recursive. One way of indexing primitive recursive functions is described in [18]. The possible schemes for defining a function $\varphi$ are listed below and the index of $\varphi$ is indicated on the right:
$$
\begin{equation*}
\begin{alignedat}{3} &({\rm I}) &\quad &\varphi(x)=x+1 &\quad &\langle1, 1\rangle, \\ &({\rm II}) &\quad &\varphi(\mathbf x)=q &\quad &\langle2, n, q\rangle, \\ &({\rm III}) &\quad &\varphi(\mathbf x)=x_i\quad (\text{where }1\leqslant i\leqslant n) &\quad &\langle3, n, i\rangle, \\ &({\rm IV}) &\quad &\varphi(\mathbf x)= \psi\bigl(\chi_1(\mathbf x), \dots, \chi_k(\mathbf x)\bigr) &\quad &\langle4, n, g, h_1, \dots, h_k\rangle, \\ &({\rm V}) &\quad &\begin{cases} \varphi(0, \mathbf x)=\psi(\mathbf x), \\ \varphi(y+1, \mathbf x)=\chi(y, \varphi(y, \mathbf x), \mathbf x) \end{cases} &\quad &\langle5, n+1, g, h\rangle. \end{alignedat}
\end{equation*}
\notag
$$
Here $\mathbf x$ is $x_1, \dots, x_n$, and $g, h_1, \dots, h_k, h$ are indexes of the functions $\psi, \chi_1, \dots, \chi_k, \chi$, respectively. Let $\operatorname{In}(b)$ mean that $b$ is an index of a primitive recursive function. It is shown in [18] that $\operatorname{In}(b)$ is a primitive recursive predicate. If $\operatorname{In}(b)$ holds, then $\mathsf{pr}_b$ will denote $[b]_1$-ary function with the index $b$. Then we put
$$
\begin{equation*}
\mathsf{pr}(b, a)= \begin{cases} \mathsf{pr}_b([a]_0, \dots, [a]_{[b]_1-1}) &\text{if }\operatorname{In}(b), \\ 0 & \text{otherwise}. \end{cases}
\end{equation*}
\notag
$$
The function $\mathsf{pr}$ is universal for the class of all primitive recursive functions and does not belong to this class. Note that if an index $b$ of a function $\varphi(\mathbf x)$ is given, then, for any $\mathbf m$, the value $\varphi(\mathbf m)$ can be computed. Indeed, computing the value of $\varphi(\mathbf x)$ is reduced to computing the values of a finite number of functions whose indexes are less than $b$. Therefore, the process of computing must be terminated. If $k$ is a natural number, put $\Lambda x.k=\langle 2, 1, k\rangle$. Thus, $\Lambda x.k$ is an index of the one-place function $x\mapsto k$. § 3. Primitive recursively realizable arithmetical formulasWe consider arithmetical statements in a purely predicate version of the language of basic arithmetic. Namely, the language $\mathrm{Ar}$ is an elementary language without function symbols and individual constants, whose signature consists of an one-place predicate symbol $Z$, binary predicate symbols $E$ and $S$, as well as triple 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$, $M(x, y, z)$ means $x\cdot y=z$. Along with the language $\mathrm{Ar}$, we consider the extended arithmetical language $\mathrm{Ar}^*$, obtained by adding the individual constants $0, 1, \dots$ for all natural numbers to the language $\mathrm{Ar}$. For convenience, we introduce the logical constants $\top$ and $\bot$ into these languages. Terms and atomic formulas are defined in the usual way. Note that $\top$ and $\bot$ are considered as atomic formulas. $\mathrm{Ar}$- and $\mathrm{Ar}^*$-formulas are constructed from atomic formulas using connectives $\&$, $\lor$, $\to$ and quantifier symbols $\forall$, $\exists$ according to the following rules:
If the list of individual variables $\mathbf x$ in the formula $\forall\mathbf x\, (\Phi\to\Psi)$ is empty, then we omit the quantifier symbol $\forall$ and write simply $(\Phi\to\Psi)$. The expression $\Phi\equiv\Psi$ is an abbreviation for $(\Phi\to\Psi)\, \&\, (\Psi\to\Phi)$. The formula $\Phi\to\bot$ will be denoted as $\neg\Phi$. If the formula $\Phi$ does not contain free variables other than $x_1, \dots, x_n$, we denote this formula as $\Phi(x_1, \dots, x_n)$. In this case, $\Phi(k_1, \dots, k_n)$ denotes the $\mathrm{Ar}^*$-formula obtained by substituting in $\Phi$ the constants $k_1, \dots, k_n$ for $x_1, \dots, x_n$ respectively. For brevity, sometimes we write $\exists\mathbf x$ instead of $\exists x_1\dots\exists x_n$, where $\mathbf x$ the list of variables $x_1, \dots, x_n$. Wel say that a closed $\mathrm{Ar}^*$-formula $\Phi$ is true, if $\mathfrak N\models\Phi$ in the usual classical sense. In this case, the formula $\forall\mathbf x\, (\Phi\to\Psi)$, where $\mathbf x$ is the list $x_1, \dots, x_n$, has the same meaning as the formula $\forall x_1\dots\forall x_n\, (\Phi\to\Psi)$ of the usual arithmetical language. Note that the atomic formula $\top$ is true and $\bot$ is not true. The notion of primitive recursive realizability for arithmetical formulas is introduced by S. Salehi [3], [4]. The relation “a natural number $e$ primitive recursively realizes the closed $\mathrm{Ar}^*$-formula $\Phi$” ($e\, \mathbf{pr}\, \Phi$) is defined by induction on the number of logical symbols in $\Phi$. 1) If $\Phi$ is an atomic formula, then $e\, \mathbf{pr}\, \Phi$ means that $e=0$ and $\Phi$ is true. 2) If $\Phi$ is $(\Psi_1\, \&\, \Psi_2)$, then $e\, \mathbf{pr}\, \Phi$ means that $[e]_0\, \mathbf{pr}\, \Psi_1$ and $[e]_1\, \mathbf{pr}\, \Psi_2$. 3) If $\Phi$ is $(\Psi_1\lor\Psi_2)$, then $e\, \mathbf{pr}\, \Phi$ means that either $[e]_0=0$ and $[e]_1\, \mathbf{pr}\, \Psi_1$ or $[e]_0\ne 0$ and $[e]_1\, \mathbf{pr}\, \Psi_2$. 4) If $\Phi$ is $\exists x\, \Psi(x)$, then $e\, \mathbf{pr}\, \Phi$ means that $[e]_1\, \mathbf{pr}\, \Psi([e]_0)$. 5) If $\Phi$ is $\forall\mathbf x\, (\Psi_1(\mathbf x)\to\Psi_2(\mathbf x))$, then $e\, \mathbf{pr}\, \Phi$ means that $\operatorname{In}(e)$ holds and, for any $b$, $\mathbf m$, if $b\, \mathbf{pr}\, \Psi_1(\mathbf m)$, then $\mathsf{pr}(e, \langle b, \mathbf m\rangle)\, \mathbf{pr}\, \Psi_2(\mathbf m)$. Here $\mathbf m$ is a list of natural numbers of the same length as the list $\mathbf x$. A closed $\mathrm{Ar}^*$-formula $\Phi$ is called primitive recursively realizable ( pr-realizable), if there exists $e$ such that $e\, \mathbf{pr}\, \Phi$. Since every closed $\mathrm{Ar}$-formula is also a closed $\mathrm{Ar}^*$-formula, the notion of primitive recursive realizability is also defined for closed $\mathrm{Ar}$-formulas. Obviously, a formula of the form $(\Phi\, \&\, \Psi)$ is pr-realizable if and only if both formulas $\Phi$ and $\Psi$ are pr-realizable, and the formula $(\Phi\lor\Psi)$ is pr-realizable if and only if at least one of the formulas $\Phi$ and $\Psi$ is pr-realizable. Let $\mathsf a_k^n$ ($k=0, 1, \dots$, $n=1, 2, \dots$) denote the number $\langle2, n, k\rangle$. Thus $\mathsf a_k^n$ is an index of the $n$-ary function $(x_1, \dots, x_n)\mapsto k$. Put $\mathsf a=\mathsf a_0^1$. The following properties of pr-realizability follow directly from the definition. Proposition 1. For any closed $\mathrm{Ar}^*$-formulas $\Phi$ and $\Psi$: 1) if $\Phi$ is pr-realizable and $\Psi$ is not pr-realizable, then the formula $(\Phi\to\Psi)$ is not pr-realizable; 2) if $k\, \mathbf{pr}\, \Psi$, then $\mathsf a_k^1\, \mathbf{pr}\, (\Phi\to\Psi)$; 3) if $\Phi$ is not pr-realizable, then $\mathsf a_k^1\, \mathbf{pr}\, (\Phi\to\Psi)$ for any $k$; 4) if $\neg\Phi$ is pr-realizable, then $\mathsf a\, \mathbf{pr}\, \neg\Phi$. Proof. Assertion 1) is obvious.
2) Suppose $k\, \mathbf{pr}\, \Psi$. Let us show that $\mathsf a_k^1\, \mathbf{pr}\, (\Phi\to\Psi)$, that is, a) $\operatorname{In}(\mathsf a_k^1)$ and b) for any $a$, if $a\, \mathbf{pr}\, \Phi$, then $\mathsf{pr}(\mathsf a_k^1, \langle a\rangle)\, \mathbf{pr}\, \Psi$. Recall that $\mathsf a_k^1$ is the index of the one-place function $x\mapsto k$, therefore, condition a) is satisfied. Condition b) is also obvious, since, for any $a$, we have $\mathsf{pr}(\mathsf a_k^1, \langle a\rangle)=k$, and $k\, \mathbf{pr}\, \Psi$. 3) Suppose $\Phi$ is not pr-realizable. This means that, for any $a$, the condition $a\, \mathbf{pr}\, \Phi$ does not hold. We have to prove that $\mathsf a_k^1\, \mathbf{pr}\, (\Phi\to\bot)$. It was already noted above that $\operatorname{In}(\mathsf a_k^1)$ holds. Therefore, it is sufficient to check that, for any $a$, $a\, \mathbf{pr}\, \Phi\Rightarrow\mathsf{pr} (\mathsf a_k^1, \langle a\rangle)\, \mathbf{pr}\, \bot$, but this is obvious due to the falsity of the premise. 4) follows from 3), since $\Phi$ is not pr-realizable if the formula $\neg\Phi$ is pr-realizable. This proves Proposition 1. Proposition 2. Let $\Psi(\mathbf x)$ be an $\mathrm{Ar}^*$-formula, where $\mathbf x$ is a (possibly empty) list of distinct individual variables $x_1, \dots, x_n$. Suppose that, for any list of natural numbers $\mathbf l=\ell_1, \dots, \ell_n$, the $\mathrm{Ar}^*$-formula $\Psi(\mathbf l)$ is not pr-realizable. Then the formula $\forall\mathbf x\, \neg\Psi(\mathbf x)$ is pr-realizable. Proof. Let prove that $\mathsf a_0^{n+1}\, \mathbf{pr}\, \forall\mathbf x\, (\Psi(\mathbf x)\to\bot)$. This means that
a) $\operatorname{In}(\mathsf a_0^{n+1})$ holds and b) $a\, \mathbf{pr}\, \Psi(\mathbf l)\Rightarrow \mathsf{pr}(\mathsf a_0^{n+1}, \langle a, \mathbf l\rangle)\, \mathbf{pr}\, \bot$ for any natural number $a$ and any list of natural numbers $\mathbf l=\ell_1, \dots, \ell_n$. Condition a) is obvious. Condition b) is also fulfilled due to the falsity of the premise. This proves Proposition 2. The following construction will be frequently used below. Proposition 3. Let $\forall\mathbf x\, (\Phi(\mathbf x)\to\Psi(\mathbf x))$ be an $\mathrm{Ar}^*$-formula, where $\mathbf x$ is a list (possibly empty) of distinct individual variables $x_1, \dots, x_n$. Suppose that there is a natural number $k$ such that, for any list of natural numbers $\mathbf l=\ell_1, \dots, \ell_n$, if the formula $\Phi(\mathbf l)$ is pr-realizable, then $k\, \mathbf{pr}\, \Psi(\mathbf l)$. Then $\mathsf a_k^{n+1}\, \mathbf{pr}\, \forall\mathbf x\, (\Phi(\mathbf x) \to\Psi(\mathbf x))$. Proof. We need to verify that, for any list of natural numbers $\mathbf l=\ell_1, \dots, \ell_n$ and any $a$, if $a\, \mathbf{pr}\, \Phi(\mathbf l)$, then the number $\mathsf{pr}(\mathsf a_k^{n+1}, \langle a, \mathbf l\rangle)$, that is, $k$, pr-realizes the formula $\Psi(\mathbf l)$, but this is what is stated in the hypothesis. An $\mathrm{Ar}^*$-formula $\Phi$ is called completely negative if it does not contain the logical symbols $\lor$ and $\exists$, and every atomic formula $\Psi$, other than $\top$ and $\bot$, occurs in $\Phi$ only in subformulas of the form $\neg\Psi$. The inductive definition of a completely negative $\mathrm{Ar}^*$-formula is as follows: 1) $\top$ and $\bot$ are completely negative formulas; 2) if $\Phi$ is an atomic $\mathrm{Ar}^*$-formula other than $\top$ and $\bot$, then the formula $\neg\Phi$ is completely negative; 3) if $\Phi$ and $\Psi$ are completely negative $\mathrm{Ar}^*$-formulas, then the formula $(\Phi\, \&\, \Psi)$ is completely negative; 4) if $\Phi$ and $\Psi$ are completely negative $\mathrm{Ar}^*$-formulas and $\mathbf x$ is a list (possibly empty) of individual variables, then the formula $\forall\mathbf x\, (\Phi\to\Psi)$ is completely negative. Note that if $\Phi$ is completely negative, then the formula $\neg\Phi$, that is, $\Phi\to\bot$, is completely negative. From the point of view of classical semantics, any formula is equivalent to a completely negative one. Proposition 4. If $\Phi(x_1, \dots, x_n)$ is a completely negative $\mathrm{Ar}^*$-formula, then there exists a natural number $n_{\Phi}$ such that, for any natural numbers $k_1, \dots, k_n$, the following conditions are equivalent: 1) $\Phi(k_1, \dots, k_n)$ is true; 2) $n_{\Phi}\, \mathbf{pr}\, \Phi(k_1, \dots, k_n)$; 3) $\Phi(k_1, \dots, k_n)$ is pr-realizable. Proof. The number $n_{\Phi}$ is defined inductively. Obviously, it is enough to check the following two conditions:
i) $n_{\Phi}\, \mathbf{pr}\, \Phi(k_1, \dots, k_n)$ if and only if the formula $\Phi(k_1, \dots, k_n)$ is true; ii) if the formula $\Phi(k_1, \dots, k_n)$ is pr-realizable, then $n_{\Phi}\, \mathbf{pr}\, \Phi(k_1, \dots, k_n)$. If $\Phi$ is an atomic formula $\top$ or $\bot$, we can take $n_{\Phi}=0$. Obviously, the conditions i) and ii) are fulfilled. Suppose $\Phi(x_1, \dots, x_n)$ is of the form $\neg P(x_1, \dots, x_n)$, where $P$ is one of the predicate symbols $Z$, $E$, $S$, $A$, $M$, $n\in\{1, 2, 3\}$. Then we can take $n_{\Phi}=\mathsf a$. We prove that condition i) holds. Let $\mathsf a\, \mathbf{pr}\, \neg P(k_1, \dots, k_n)$. Then the formula $P(k_1, \dots, k_n)$ is not pr-realizable. It follows from the definition of pr-realizability for atomic formulas that $P(k_1, \dots, k_n)$ is not true. Then the formula $\neg P(k_1, \dots, k_n)$ is true. Conversely, suppose the formula $\neg P(k_1, \dots, k_n)$ is true. Then $P(k_1, \dots, k_n)$ is not true. It follows from the definition of pr-realizability for atomic formulas that the formula $P(k_1, \dots, k_n)$ is not pr-realizable. By Proposition 1, $\mathsf a\, \mathbf{pr}\, \neg P(k_1, \dots, k_n)$. Condition ii) follows from Proposition 1. Suppose that, for the formulas $\Psi_1(x_1, \dots, x_n)$ and $\Psi_2(x_1, \dots, x_n)$, we have found numbers $n_{\Psi_1}$ and $n_{\Psi_2}$ such that, for any $k_1, \dots, k_n$, the following conditions are fulfilled: i1) $n_{\Psi_1}\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n)$ if and only if the formula $\Psi_1(k_1, \dots, k_n)$ is true; i2) $n_{\Psi_2}\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n)$ if and only if the formula $\Psi_2(k_1, \dots, k_n)$ is true; ii1) if $\Psi_1(k_1, \dots, k_n)$ is pr-realizable, then $n_{\Psi_1}\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n)$; ii2) if $\Psi_2(k_1, \dots, k_n)$ is pr-realizable, then $n_{\Psi_2}\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n)$. If the formula $\Phi(x_1, \dots, x_n)$ is of the form $\Psi_1(x_1, \dots, x_n)\, \&\, \Psi_2(x_1, \dots, x_n)$, then we put $n_{\Phi}=\langle n_{\Psi_1}, n_{\Psi_2}\rangle$, and prove that $n_{\Phi}$ is the required number. Let us verify condition i). Suppose the formula $\Phi(k_1, \dots, k_n)$ is true. Then both formulas $\Psi_1(k_1, \dots, k_n)$ and $\Psi_2(k_1, \dots, k_n)$ are true. By conditions i1) and i2), we have $n_{\Psi_1}\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n)$ and $n_{\Psi_2}\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n)$. Then $n_{\Phi}\, \mathbf{pr}\, \Phi(k_1, \dots, k_n)$ by the definition of pr-realizability since $[n_{\Phi}]_0=n_{\Psi_1}$, $[n_{\Phi}]_1=n_{\Psi_2}$. Conversely, if $n_{\Phi}\, \mathbf{pr}\, \Phi(k_1, \dots, k_n)$, then $n_{\Psi_1}\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n)$ and $n_{\Psi_2}\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n)$ by the definition of pr-realizability for conjunction. In this case, by conditions i1) and i2), both formulas $\Psi_1(k_1, \dots, k_n)$ and $\Psi_2(k_1, \dots, k_n)$ are true, and hence the formula $\Phi(k_1, \dots, k_n)$ is also true. Let us verify condition ii). Suppose the formula $\Phi(k_1, \dots, k_n)$ is pr-realizable. Then so are $\Psi_1(k_1, \dots, k_n)$ and $\Psi_2(k_1, \dots, k_n)$. From conditions ii1) and ii2), we have $n_{\Psi_1}\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n)$ and $n_{\Psi_2}\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n)$. Hence $n_{\Phi}\, \mathbf{pr}\, \Phi(k_1, \dots, k_n)$ by the definition of pr-realizability. Suppose $\Phi(x_1, \dots, x_n)$ is $\forall\mathbf y\, (\Psi_1(x_1, \dots, x_n, \mathbf y)\to \Psi_2(x_1, \dots, x_n, \mathbf y))$, where $\mathbf y$ is a list (possibly empty) of distinct individual variables $y_1, \dots, y_m$, and none of the variables $x_i$ is in $\mathbf y$. Suppose that, for the formulas $\Psi_1$ and $\Psi_2$, we have found numbers $n_{\Psi_1}$ and $n_{\Psi_2}$ such that, for any $k_1, \dots, k_n$, $\ell_1, \dots, \ell_m$, the following conditions are fulfilled, where $\mathbf l$ is the list $\ell_1, \dots, \ell_m$: ia) $n_{\Psi_1}\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n, \mathbf l)$ if and only if $\Psi_1(k_1, \dots, k_n, \mathbf l)$ is true; ib) $n_{\Psi_2}\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n, \mathbf l)$ if and only if $\Psi_2(k_1, \dots, k_n, \mathbf l)$ is true; iia) if $\Psi_1(k_1, \dots, k_n, \mathbf l)$ is pr-realizable, then $n_{\Psi_1}\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n, \mathbf l)$; iib) if $\Psi_2(k_1, \dots, k_n, \mathbf l)$ is pr-realizable, then $n_{\Psi_2}\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n, \mathbf l)$. We put $n_\Phi=\mathsf a_{n_{\Psi_2}}^{m+1}$, and prove that $n_{\Phi}$ is the required number. Let us check condition i). Suppose $\Phi(k_1, \dots, k_n)$ is true. Then, for any $\mathbf l$, $\Psi_1(k_1, \dots, k_n, \mathbf l)\to\Psi_2(k_1, \dots, k_n, \mathbf l)$ is true. We prove that $n_{\Phi}\, \mathbf{pr}\, \Phi(k_1, \dots, k_n)$, that is, $\operatorname{In}(n_{\Phi})$ (this condition is fulfilled) and, for any $a$, $\mathbf l$, if $a\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n, \mathbf l)$, then the number $\mathsf{pr}(n_{\Phi}, \langle a, \mathbf l\rangle)$, that is, $n_{\Psi_2}$, pr-realizes $\Psi_2(k_1, \dots, k_n, \mathbf l)$. Suppose $a\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n, \mathbf l)$. Then, by condition iia), we have $n_{\Psi_1}\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n, \mathbf l)$, and, by condition ia), the formula $\Psi_1(k_1, \dots, k_n, \mathbf l)$ is true. Hence the formula $\Psi_2(k_1, \dots, k_n, \mathbf l)$ is true. By condition ib), $n_{\Psi_2}\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n, \mathbf l)$, as was to be proved. Conversely, suppose $n_{\Phi}\, \mathbf{pr}\, \Phi(k_1, \dots, k_n)$. We prove that $\Phi(k_1, \dots, k_n)$ is true. Let an arbitrary list of natural numbers $\mathbf l$ be given. Let us prove that the formula $\Psi_1(k_1, \dots, k_n, \mathbf l)\, {\to}\, \Psi_2(k_1, \dots, k_n, \mathbf l)$ is true. Let the premise $\Psi_1(k_1, \dots, k_n, \mathbf l)$ be true. Let us verify that the conclusion $\Psi_2(k_1, \dots, k_n, \mathbf l)$ is true. By condition ia), we have $n_{\Psi_1}\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n, \mathbf l)$. Then the number $\mathsf{pr}(n_{\Phi}, \langle n_{\Psi_1}, \mathbf l\rangle)$, that is, $n_{\Psi_2}$, pr-realizes $\Psi_2(k_1, \dots, k_n, \mathbf l)$. By condition ib), $\Psi_2(k_1, \dots, k_n, \mathbf l)$ is true, as was to be proved. Let us check condition ii). Assume that the formula $\Phi(k_1, \dots, k_n)$ is pr-realizable, that is, there exists $e$ such that $\operatorname{In}(e)$ holds, and, for any $a, \mathbf l$, $a\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n, \mathbf l)$ implies $\mathsf{pr}(e, \langle a, \mathbf l\rangle)\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n, \mathbf l)$. We prove that $n_{\Phi}\, \mathbf{pr}\, \Phi(k_1, \dots, k_n)$, that is, for any $a$, $\mathbf l$, if $a\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n, \mathbf l)$, then the number $\mathsf{pr}(n_{\Phi}, \langle a, \mathbf l\rangle)$, that is, $n_{\Psi_2}$, pr-realizes $\Psi_2(k_1, \dots, k_n, \mathbf l)$. Suppose that $a\, \mathbf{pr}\, \Psi_1(k_1, \dots, k_n, \mathbf l)$. Then we have $\mathsf{pr}(e, \langle a, \mathbf l\rangle)\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n, \mathbf l)$, that is, $\Psi_2(k_1, \dots, k_n, \mathbf l)$ is pr-realizable. By condition iib), $n_{\Psi_2}\, \mathbf{pr}\, \Psi_2(k_1, \dots, k_n, \mathbf l)$, as was to be proved. This proves Proposition 4. Proposition 5. Let $\Phi(\mathbf x)$ be an $\mathrm{Ar}^*$-formula of the form $\exists\mathbf y\, \Psi(\mathbf x, \mathbf y)$, where $\mathbf x$ is the list $x_1, \dots, x_n$, $\mathbf y$ is the list $y_1, \dots, y_m$, and $\Psi(\mathbf x, \mathbf y)$ is a completely negative $\mathrm{Ar}^*$-formula. Then, for any list of natural numbers $\mathbf k=k_1, \dots, k_n$, the formula $\Phi(\mathbf k)$ is pr-realizable if and only if it is true. Proof. Assume that $\Phi(\mathbf k)$ is pr-realizable. This means that there is a list of natural numbers $\mathbf l=\ell_1, \dots, \ell_m$ such that the formula $\Psi(\mathbf k, \mathbf l)$ is pr-realizable. By Proposition 4, this formula is true. Hence the formula $\Phi(\mathbf k)$ is also true. Conversely, if the formula $\Phi(\mathbf k)$ is true, then there exists a list of natural numbers $\mathbf l$ such that the formula $\Psi(\mathbf k, \mathbf l)$ is true. By Proposition 4, this formula is pr-realizable. Hence the formula $\Phi(\mathbf k)$ also is pr-realizable. This proves Proposition 5.
§ 4. An arithmetical theory sound with respect to pr-realizabilityConsider the following $\mathrm{Ar}$-formulas: $A_1$. $\forall x\, \neg\neg E(x, x)$; $A_2$. $\forall x, y\, (\neg\neg E(x, y)\to\neg\neg E(y, x))$; $A_3$. $\forall x, y, 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, y\, ((\neg\neg Z(x)\, \&\, \neg\neg Z(y))\to \neg\neg E(x, y))$; $A_6$. $\forall x, y\, ((\neg\neg E(x, y)\, \&\, \neg\neg Z(x))\to\neg\neg Z(y))$; $A_7$. $\forall x\, (\top\to\exists y\, \neg\neg S(x, y))$; $A_8$. $\forall x, y, z\, ((\neg\neg S(x, y)\, \&\, \neg\neg S(x, z)) \to\neg\neg E(y, z))$; $A_9$. $\forall x_1, x_2, y_1, 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, y, z\, ((\neg\neg S(x, z)\, \&\, \neg\neg S(y, z)) \to\neg\neg E(x, y))$; $A_{11}$. $\forall x, y\, (\neg\neg S(x, y)\to\neg Z(y))$; $A_{12}$. $\forall x\, (\top\to(\neg\neg Z(x)\lor\exists y\, \neg\neg S(y, x)))$; $A_{13}$. $\forall x, y\, (\top\to\exists z\, \neg\neg A(x, y, z))$; $A_{14}$. $\forall x, y, z_1, 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, x_2, y_1, y_2, z_1, z_2\, ((\neg\neg E(x_1, x_2)\, \&\, \neg\neg E(y_1, y_2)\, \&\, \neg\neg E(z_1, z_2)\, \&$ $\neg\neg A(x_1, y_1, z_1))\to\neg\neg A(x_2, y_2, z_2))$; $A_{16}$. $\forall x, y\, (\neg\neg Z(y)\to\neg\neg A(x, y, x))$; $A_{17}$. $\forall x, y, z, u, 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, y\, (\top\to\exists z\, \neg\neg M(x, y, z))$; $A_{19}$. $\forall x, y, z_1, 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, x_2, y_1, y_2, z_1, z_2\, ((\neg\neg E(x_1, x_2)\, \&\, \neg\neg E(y_1, y_2)\, \&\, \neg\neg E(z_1, z_2)\, \&$ $\neg\neg M(x_1, y_1, z_1))\to\neg\neg M(x_2, y_2, z_2))$; $A_{21}$. $\forall x, y\, (\neg\neg Z(y)\to\neg\neg M(x, y, y))$; $A_{22}$. $\forall x, y, z, u, 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))$. In [2], § 48, a triple function $\beta$ is defined with the following property: for any list of natural numbers $k_0, \dots, k_n$, there are natural numbers $a$ and $b$ such that, for any $i\leqslant n$, $\beta(a, b, i)=k_i$. The predicate $\beta([x]_0, [x]_1, y)=0$ is recursively enumerable. According to Matiyasevich’s theorem, this predicate is 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 easily follows that the predicate $\beta([x]_0, [x]_1, y)=0$ is defined in $\mathfrak N$ by an $\mathrm{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 $\mathrm{Ar}$-formula. Thus, for any natural numbers $a$ and $i$,
$$
\begin{equation*}
\begin{aligned} \, \beta([a]_0, [a]_1, i)=0\quad&\Longrightarrow\quad\mathfrak N\models B(a, i), \\ \beta([a]_0, [a]_1, i)\ne 0\quad&\Longrightarrow\quad \mathfrak N\models\neg B(a, i). \end{aligned}
\end{equation*}
\notag
$$
Let $a$ be a natural number. Then $\{a\}$ will denote a one-place primitive recursive function $n\mapsto\mathsf{pr}(a, n)$. Thus, if $a$ is an index of some $(k+1)$-ary ($k\geqslant0$) primitive recursive function $f$, then $\{a\}(x)=f([x]_0, \dots, [x]_k)$ for any $x$, and otherwise $\{a\}(x)=0$ for any $x$. Since the predicate $\{x_1\}(x_2)=x_3$ is obviously recursively enumerable, it is defined in $\mathfrak N$ by some $\mathrm{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 $\mathrm{Ar}$-formula. Let $H(x_1, x_2)$ be the formula $\exists z\, (\neg\neg Z(z)\, \&\, G(x_1, x_2, z))$. This formula defines in $\mathfrak N$ the predicate $\{x_1\}(x_2)=0$. By $x\leqslant y$ we denote the formula $\exists z\, \neg\neg A(x, z, y)$. Consider the following formulas: $A_{23}$. $\forall x, y, z_1, z_2\, \bigl(G(x, y, z_1)\, \&\, G(x, y, z_2) \to\neg\neg E(z_1, z_2)\bigr)$; $A_{24}$. $\forall y, z\, \neg\neg\exists v\forall x\, \bigl(x\leqslant z \to(\neg\neg B(v, x)\equiv\neg\neg H(y, x))\bigr)$; $A_{25}$. $\forall x\forall y\, \bigl(\top\to (\neg B(x, y)\lor\neg\neg B(x, y))\bigr)$. Let $Q$ be the conjunction of the formulas $A_1$–$A_{25}$. Proof. We prove that each of the formulas $A_1$–$A_{25}$ is pr-realizable. Obviously, all these formulas are true. All of them, with the exception of $A_4$, $A_7$, $A_{12}$, $A_{13}$, $A_{18}$, $A_{23}$, $A_{24}$ and $A_{25}$, are completely negative, hence pr-realizable by Proposition 4.
Consider the formula $A_4$. Let $a=\langle0, \mathsf a\rangle$. We prove that $a\, \mathbf{pr}\, \exists x\, \neg\neg Z(x)$, that is, $\mathsf a\, \mathbf{pr}\, \neg\neg Z(0)$, but this easily follows from Proposition 1, since the formula $\neg Z(0)$ is not pr-realizable. Consider the formula $A_7$. The function $(x, y)\mapsto\langle y+1, \mathsf a\rangle$ is primitive recursive. Let $a$ be its index. We prove that $a\, \mathbf{pr}\, \forall x\, (\top\to\exists y\, \neg\neg S(x, y))$, that is, $\operatorname{In}(a)$ holds (this condition is obviously fulfilled), and, for any $b, k$, if $b\, \mathbf{pr}\, \top$, then the number $\mathsf{pr}(a, \langle b, k\rangle)$, that is, $\langle k+1, \mathsf a\rangle$, pr-realizes the formula $\exists y\, \neg\neg S(k, y)$. Thus, we have to prove that $\mathsf a\, \mathbf{pr}\, \neg\neg S(k, k+1)$, but this easily follows from Proposition 1. It follows that the formula $A_7$ is pr-realizable. Consider the formula $A_{12}$. The function
$$
\begin{equation*}
f(x, y)= \begin{cases} \langle0, \mathsf a\rangle &\text{if }y=0, \\ \langle1, \langle y-1, {\mathsf a}\rangle\rangle & \text{if }y\ne 0, \end{cases}
\end{equation*}
\notag
$$
is primitive recursive. Let $a$ be its index. Let us prove that
$$
\begin{equation*}
a\, \mathbf{pr}\, \forall x\, \bigl(\top\to (\neg\neg Z(x)\lor\exists y\, \neg\neg S(y, x))\bigr),
\end{equation*}
\notag
$$
that is, for any $b, k$, if $b\, \mathbf{pr}\, \top$, that is, $b=0$, then
$$
\begin{equation*}
\mathsf{pr}(a, \langle b, k\rangle)\, \mathbf{pr}\, \bigl(\neg\neg Z(k) \lor\exists y\, \neg\neg S(y, k)\bigr),
\end{equation*}
\notag
$$
that is,
$$
\begin{equation}
f(0, k)\, \mathbf{pr}\, \bigl(\neg\neg Z(k)\lor\exists y\, \neg\neg S(y, k)\bigr).
\end{equation}
\tag{4.1}
$$
If $k=0$, then $f(0, k)=\langle0, \mathsf a\rangle$. The formula $Z(0)$ is pr-realizable. By Proposition 1 $\mathsf a\, \mathbf{pr}\, \neg\neg Z(k)$. In this case, (4.1) holds. If $k>0$, then $f(0, k)=\langle1, \langle k-1, {\mathsf a}\rangle\rangle$. In this case, $[f(0, k)]_0=1$, $[f(0, k)]_1=\langle k-1, {\mathsf a}\rangle$, and (4.1) means that ${\mathsf a}\, \mathbf{pr}\, \neg\neg S(k-1, k)$, and this easily follows from Proposition 1, because the formula $\neg\neg S(k-1, k)$ is pr-realizable. Thus the formula $A_{12}$ is pr-realizable.
Consider the formula $A_{13}$. The function $(x, y, z)\mapsto\langle y+z, \mathsf a\rangle$ is primitive recursive. Let $a$ be its index. We prove that $a\, \mathbf{pr}\, \forall x, y\, (\top\to\exists z\, \neg\neg A(x, y, z))$, that is, $\operatorname{In}(a)$ holds (this condition is obviously fulfilled) and, for any $b$, $k$, $\ell$, if $b\, \mathbf{pr}\, \top$, then the number $\mathsf{pr}(a, \langle b, k, \ell\rangle)$, that is, $\langle k+\ell, \mathsf a\rangle$, pr-realizes the formula $\exists z\, \neg\neg A(k, \ell, z)$. Thus, we have to prove that $\mathsf a\, \mathbf{pr}\, \neg\neg A(k, \ell, k+\ell)$, but this easily follows from Proposition 1. Hence the formula $A_{13}$ is pr-realizable. The formula $A_{18}$ is considered in the same way using $(x, y, z)\mapsto\langle y\cdot z, \mathsf a\rangle$. Consider the formula $A_{23}$. The function $(x, y, z, u, v)\mapsto\mathsf a$ is primitive recursive. Let $a$ be its index. Let us prove that $a$ pr-realizes $A_{23}$. We have to prove that, for any $b$, $k$, $\ell$, $m_1$, $m_2$, if $b\, \mathbf{pr}\, (G(k, \ell, m_1)\, \&\, G(k, \ell, m_2))$, then $\mathsf{pr}(a, \langle b, k, \ell, m_1, m_2\rangle)$, that is, $\mathsf a$, pr-realizes $\neg\neg E(m_1, m_2)$. Suppose $b\, \mathbf{pr}\, (G(k, \ell, m_1)\, \&\, G(k, \ell, m_2))$. Then the formulas $G(k, \ell, m_1)$ and $G(k, \ell, m_2)$ are pr-realizable, and, by Proposition 5, they are true, that is, $\{k\}(\ell)=m_1$ and $\{k\}(\ell)=m_2$. Then $m_1=m_2$, and, by Proposition 1, $\mathsf a\, \mathbf{pr}\, \neg\neg E(m_1, m_2)$, as was to be proved. Thus the formula $A_{23}$ is pr-realizable. Consider the formula $A_{24}$. By Proposition 2, it is sufficient to prove that, for any fixed natural numbers $m$ and $n$, the formula
$$
\begin{equation*}
\neg\exists v\, \forall x\, \bigl(x\leqslant n\to(\neg\neg B(v, x) \equiv\neg\neg H(m, x))\bigr)
\end{equation*}
\notag
$$
is not pr-realizable. We prove that the formula
$$
\begin{equation}
\exists v\, \forall x\, \bigl(x\leqslant n\to(\neg\neg B(v, x) \equiv\neg\neg H(m, x))\bigr).
\end{equation}
\tag{4.2}
$$
is pr-realizable. Consider a list $k_0, \dots, k_n$, where $k_i=0\Leftrightarrow\{m\}(i)=0$. By the property of the function $\beta$, there is a natural number $a$ such that $\beta([a]_0, [a]_1, i)=k_i$ for any $i\leqslant n$. Suppose $i\leqslant n$. If $k_i=0$, then the formulas $B(a, i)$ and $H(m, i)$ are true. By Proposition 5, they are pr-realizable and by Proposition 1, both formulas $\neg\neg B(a, i)$ and $\neg\neg H(m, i)$ are pr-realizable by the number $\mathsf a$. By Proposition 1,
$$
\begin{equation}
\Lambda x.\mathsf a\, \mathbf{pr}\, \bigl(\neg\neg B(a, i) \to\neg\neg H(m, i)\bigr),
\end{equation}
\tag{4.3}
$$
$$
\begin{equation}
\Lambda x.\mathsf a\, \mathbf{pr}\, \bigl(\neg\neg H(m, i) \to\neg\neg B(a, i)\bigr).
\end{equation}
\tag{4.4}
$$
It follows that
$$
\begin{equation}
\mathsf b\, \mathbf{pr}\, \bigl(\neg\neg B(a, i)\equiv\neg\neg H(m, i)\bigr),
\end{equation}
\tag{4.5}
$$
where $\mathsf b=\langle\Lambda x.\mathsf a, \Lambda x.\mathsf a\rangle$. If $k_i\ne 0$, then $B(a, i)$ and $H(m, i)$ are not true, and, by Proposition 5, are not pr-realizable. By Proposition 1, in this case (4.3) and (4.4) hold. Hence (4.5) also holds. Thus, for any $i\leqslant n$, we have (4.5). Let $c$ be the index of the function $(x, y)\mapsto\mathsf b$. We prove that $c\, \mathbf{pr}\, \forall x\, (x\leqslant n\to (\neg\neg B(a, x)\equiv\neg\neg H(m, x)))$. We have to prove that, for any $d$, $i$, if $d\, \mathbf{pr}\, (i\leqslant n)$, then the number $\mathsf{pr}(c, \langle d, i\rangle)$, that is, $\mathbf b$, pr-realizes the formula $\neg\neg B(a, i)\equiv\neg\neg H(m, i)$. Suppose $d\, \mathbf{pr}\, (i\leqslant n)$. By Proposition 5, the formula $i\leqslant n$ is true. As was proved above, in this case (4.5) holds, as was to be proved. Now it is obvious that the number $\langle a, c\rangle$ pr-realizes formula (4.2). Thus the formula $A_{24}$ is pr-realizable.
Consider the formula $A_{25}$. Let $\phi(u, x, y)=\langle\overline{\mathsf{sg}} (\beta([x]_0, [x]_1, y)), \mathsf a\rangle$, where $\overline{\mathsf{sg}}(x)$ is $1$ if $x=0$ and $0$ otherwise. The function $\phi$ is primitive recursive. Let $a$ be its index. Let us prove that $a$ pr-realizes the formula $A_{25}$. We have to prove that $\operatorname{In}(a)$ holds (this condition is fulfilled), and, for any $b$, $k$, $i$, if $b\, \mathbf{pr}\, \top$, then the number $\mathsf{pr}(a, \langle b, k, i\rangle)$, that is, $\phi(b, k, i)$, pr-realizes the formula $\neg B(k, i)\lor\neg\neg B(k, i)$. There are two cases to consider, $\beta([k]_0, [k]_1, i)=0$ or $\beta([k]_0, [k]_1, i)\ne 0$. In the first case, the formula $B(k, i)$ is true. By Proposition 5, it is pr-realizable. Then the formula $\neg\neg B(k, i)$ is pr-realizable. By Proposition 1, $\mathsf a\, \mathbf{pr}\, \neg\neg B(k, i)$. Note that in this case $\phi(b, k, i)=\langle1, \mathbf a\rangle$. It is obvious that $\phi(b, k, i)\, \mathbf{pr}\, (\neg B(k, i)\lor\neg\neg B(k, i))$, as was to be proved. In the second case, the formula $B(k, i)$ is not true. By Proposition 5, it is not pr-realizable. Then $\neg B(k, i)$ is pr-realizable. By Proposition 1, $\mathsf a\, \mathbf{pr}\, \neg B(k, i)$. Note that in this case $\phi(b, k, i)=\langle0, \mathbf a\rangle$ and $\phi(b, k, i)\, \mathbf{pr}\, (\neg B(k, i)\lor\neg\neg B(k, i))$. Theorem 1 is proved. § 5. Primitive recursively realizable predicate formulasThe alphabet of the language of predicate basic logic consists of individual variables $x_0, x_1, \dots$, predicate symbols $P_i^{n_i}$ ($i, n_i\in\mathbb N$), logical symbols $\&$, $\lor$, $\to$, $\forall$, $\exists$, $\top$, $\bot$ and auxiliary symbols “ , ”, “ ( ” and “ ) ”. In this case, $P_i^{n_i}$ is called $n_i$-ary predicate symbol, and $n_i$ is called its arity. Predicate symbols are also called predicate variables, and individual variables are called terms. Atomic formulas are $\top$, $\bot$, as well as the expressions of the form $P(t_1, \dots, t_n)$, where $P$ is some $n$-ary predicate symbol and $t_1, \dots, t_n$ are terms. Sometimes we will use the notation $\mathbf x$ for the list of individual variables $x_1, \dots, x_n$. Predicate formulas are defined inductively as follows:
If the list of individual variables $\mathbf x$ in the formula $\forall\mathbf x\, (F\to G)$ is empty, then we omit the quantifier $\forall$ and write simply $(F\to G)$. The expression $F\equiv G$ is an abbreviation for the formula $(F\to G)\, \&\, (G\to F)$. The formula $F\to\bot$ will be denoted by $\neg F$. For brevity, sometimes we write $\exists\mathbf x$ instead of $\exists x_1\dots\exists x_n$. A predicate formula $F$ will be denoted as $F(P_1, \dots, P_n, y_1, \dots, y_m)$ if it does not contain predicate variables except $P_1, \dots, P_n$ and free individual variables except $y_1, \dots, y_m$. Let $F(P_1, \dots, P_n)$ be a predicate formula. We say that a list of $\mathrm{Ar}^*$-formulas $\Phi_1, \dots, \Phi_n$ is admissible for substitution in $F$ if, for any $i=1, \dots, n$, the formula $\Phi_i$ does not contain free variables other than $x_1, \dots, x_m$, where $m$ is arity of $P_i$. In this case, $F(\Phi_1, \dots, \Phi_n)$ will denote the result of substituting in $F$ formulas $\Phi_1, \dots, \Phi_n$ for the predicate variables $P_1, \dots, P_n$ (it is assumed that bound individual variables are renamed to avoid collisions). The formula $F(\Phi_1, \dots, \Phi_n)$ is called an arithmetical instance of the predicate formula $F(P_1, \dots, P_n)$. A closed predicate formula $F(P_1, \dots, P_n)$ is called primitive recursively ( pr-) realizable if, for any list of $\mathrm{Ar}^*$-formulas $\Phi_1, \dots, \Phi_k$ admissible for substitution in $F$, the closed $\mathrm{Ar}^*$-formula $F(\Phi_1, \dots, \Phi_k)$ is pr-realizable. A predicate formula $F(P_1, \dots, P_n)$ is called completely negative if it does not contain the logical symbols $\lor$ and $\exists$ and each predicate variable $P_i$ occurs in $F$ only in subformulas of the form $\neg P_i(y_1, \dots, y_k)$. An inductive definition of a completely negative predicate formula is as follows:
Proposition 6. Let $F(P_1, \dots, P_n, y_1, \dots, y_m)$ be a completely negative predicate formula. Then there exists a natural number $a_F$ such that, for any list of $\mathrm{Ar}^*$-formulas $\Phi_1, \dots, \Phi_n$ admissible for substitution in $F$ and any natural numbers $k_1, \dots, k_m$, the following conditions are equivalent: 1) $F(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m)$ is pr-realizable; 2) $a_F\, \mathbf{pr}\, F(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m)$. Proof. Induction on the construction of $F$. If $F$ is $\top$ or $\bot$, we can take $a_F=0$. Suppose $F$ has the form $\neg P(y_1, \dots, y_m)$, where $P$ is an $m$-ary predicate variable, $\Phi(x_1, \dots, x_m)$ is an $\mathrm{Ar}^*$-formula admissible for substitution in $F$, and $k_1, \dots, k_m$ are natural numbers. Then $F(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m)$ is $\neg\Phi(k_1, \dots, k_m)$. By Proposition 1, in this case, we can take $a_F=\mathsf a$.
If $F(P_1, \dots, P_n, y_1, \dots, y_m)$ has the form
$$
\begin{equation*}
G(P_1, \dots, P_n, y_1, \dots, y_m)\, \&\, H(P_1, \dots, P_n, y_1, \dots, y_m),
\end{equation*}
\notag
$$
and for the formulas $G$ and $H$ the corresponding numbers $a_G$ and $a_H$ are defined, then one can take $a_F=\langle a_G, a_H\rangle$.
Suppose $F(P_1, \dots, P_n, y_1, \dots, y_m)$ has the form
$$
\begin{equation*}
\forall\mathbf x\, (G(P_1, \dots, P_n, y_1, \dots, y_m, \mathbf x)\to H(P_1, \dots, P_n, y_1, \dots, y_m, \mathbf x)),
\end{equation*}
\notag
$$
where $\mathbf x$ is the list of individual variables $x_1, \dots, x_p$. Put $a_F=\mathsf a_{a_H}^{p+1}$ and prove that $a_F$ is the required number.
Suppose the formula $F(\Phi_1, \dots, \Phi_n, k_1, \dots, k_n)$ is pr-realizable. Then there exists a number $e$ such that, for any list of natural numbers $\mathbf l=\ell_1, \dots, \ell_p$ and any $b$, if
$$
\begin{equation}
b\, \mathbf{pr}\, G(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m, \mathbf l),
\end{equation}
\tag{5.1}
$$
then $\mathsf{pr}(e, \langle b, \mathbf l\rangle)\, \mathbf{pr}\, H(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m, \mathbf l)$. It follows that, for any $\mathbf l$, if the formula $G(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m, \mathbf l)$ is pr-realizable, then $H(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m, \mathbf l)$ is pr-realizable and by the induction hypothesis
$$
\begin{equation}
a_H\, \mathbf{pr}\, H(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m, \mathbf l).
\end{equation}
\tag{5.2}
$$
Suppose that (5.1) holds for some $b$, $\mathbf l$. According to the above, in this case, we have (5.2). Note that $\mathsf{pr}(a_F, \langle b, \mathbf l\rangle)=a_H$. Thus, for any $b$, $\mathbf l$, if (5.1) is fulfilled, then $\mathsf{pr}(a_F, \langle b, \mathbf l\rangle)\, \mathbf{pr}\, H(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m, \mathbf l)$. Consequent;y, this means that $a_F\, \mathbf{pr}\, F(\Phi_1, \dots, \Phi_n, k_1, \dots, k_m)$, as was to be proved. § 6. Simulating arithmetic in the predicate languageEach $\mathrm{Ar}$-formula $F$ can be considered as a predicate formula if the predicate symbols $S$, $A$, $M$, $Z$, $E$ are treated as predicate variables. In this case, we call $F$ a predicate $\mathrm{Ar}$-formula. Since the predicate $\mathrm{Ar}$-formula $F$ does not contain predicate variables other than $S$, $A$, $M$, $Z$, $E$, we denote it $F(S, A, M, Z, E)$. Let $\mathbf\Phi=\mathcal{S}(x_1, x_2), \mathcal{A}(x_1, x_2, x_3), \mathcal{M}(x_1, x_2, x_3), \mathcal{Z}(x_1), \mathcal{E}(x_1, x_2)$ be a list of $\mathrm{Ar}$-formulas admissible for substitution in a predicate $\mathrm{Ar}$-formula $F(S, A, M, Z, E)$. Then the $\mathrm{Ar}$-formula $F(\mathcal{S}, \mathcal{A}, \mathcal{M}, \mathcal{Z}, \mathcal{E})$ will be denoted by $\widetilde F$. We say that the list $\mathbf{\Phi}$ is an interpretation of the predicate $\mathrm{Ar}$-formula $F$ if the $\mathrm{Ar}$-formula $\widetilde F$ is pr-realizable. Note that the list
$$
\begin{equation*}
\mathbf{\Phi}=S(x_1, x_2), A(x_1, x_2, x_3), M(x_1, x_2, x_3), Z(x_1), E(x_1, x_2)
\end{equation*}
\notag
$$
is an interpretation of the predicate $\mathrm{Ar}$-formula $Q$, defined in § 4, since the formula $\widetilde{Q}$ is exactly $Q$, and the last is pr-realizable by Theorem 1. Proposition 7. If $\mathbf{\Phi}$ is an interpretation of the formula $Q$, then, for any completely negative $\mathrm{Ar}$-formula $\Psi(x_1, \dots, x_n)$, the formula is pr-realizable, where $\mathbf x$ is the list $x_1, \dots, x_n$, and $\mathbf y$ is $y_1, \dots, y_n$ Proof. Suppose a list of $\mathrm{Ar}$-formulas
$$
\begin{equation*}
\mathbf{\Phi}=\mathcal{S}(x_1, x_2), \mathcal{A}(x_1, x_2, x_3), \mathcal{M}(x_1, x_2, x_3), \mathcal{Z}(x_1), \mathcal{E}(x_1, x_2)
\end{equation*}
\notag
$$
is an interpretation of the formula $Q$. The formula $\widetilde{\Psi}(x_1, \dots, x_n)$ is constructed from $\top$, $\bot$, $\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)$, $\neg\mathcal M(x_i, x_j, x_k)$, where $1\leqslant i, j, k\leqslant n$, using the logical symbols $\&$, $\to$ and $\forall$. Note that (6.1) is an arithmetical instance of the completely negative predicate $\mathrm{Ar}$-formula
$$
\begin{equation}
\forall\mathbf x, \mathbf y\, \bigl(\neg\neg E(x_1, y_1)\, \&\cdots\&\, \neg\neg E(x_n, y_n)\, \&\, \Psi(\mathbf x)\to\Psi(\mathbf y)\bigr).
\end{equation}
\tag{6.2}
$$
By Proposition 6, there is a number pr-realizing any pr-realizable arithmetical instance of formula (6.2). Thus it is sufficient to prove that formula (6.1) is pr-realizable without worrying about constructing a concrete pr-realization.
Let us prove the pr-realizability of formula (6.1) by induction on the construction of a completely negative $\mathrm{Ar}$-formula $\Psi(x_1, \dots, x_n)$. 1) If $\Psi(x_1, \dots, x_n)$ is $\top$, then $\widetilde{\Psi }(x_1, \dots, x_n)$ is $\top$, and, in this case, (6.1) is the formula $\forall\mathbf x, \mathbf y\, (\neg\neg\mathcal E(x_1, y_1) \, \&\cdots\&\, \neg\neg\mathcal E(x_n, y_n)\, \&\, \top\to\top)$. Since $0\, \mathbf{pr}\, \top$, it is obvious that this formula is pr-realizable by the number $\mathsf a_0^{2n+1}$. 2) If $\Psi(x_1, \dots, x_n)$ is $\bot$, then $\widetilde{\Psi }(x_1, \dots, x_n)$ is $\bot$, and, in this case, (6.1) is the formula $\forall\mathbf x, \mathbf y\, (\neg\neg\mathcal E(x_1, y_1) \, \&\cdots\&\, \neg\neg\mathcal E(x_n, y_n)\, \&\, \bot\to\bot)$. Since $\bot$ is not pr-realizable, it is obvious that this formula is pr-realizable by the number $\mathsf a_0^{2n+1}$. 3) If $\Psi(x_1, \dots, x_n)$ is $\neg E(x_i, x_j)$, $1\leqslant i, j\leqslant n$, then $\widetilde{\Psi }(x_1, \dots, x_n)$ is $\neg\mathcal E(x_i, x_j)$, and, in this case, (6.1) is the formula
$$
\begin{equation}
\forall\mathbf x, \mathbf y\, \bigl(\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)\bigr).
\end{equation}
\tag{6.3}
$$
First, we prove that, for any $k_1, \dots, k_n$, $\ell_1, \dots, \ell_n$, if the $\mathrm{Ar}^*$-formula
$$
\begin{equation}
\neg\neg\mathcal E(k_1, \ell_1)\, \&\cdots\&\, \neg\neg \mathcal E(k_n, \ell_n)\, \&\, \neg\mathcal E(k_i, k_j)
\end{equation}
\tag{6.4}
$$
is pr-realizable, then
$$
\begin{equation}
\mathsf a\, \mathbf{pr}\, \neg\mathcal E(\ell_i, \ell_j).
\end{equation}
\tag{6.5}
$$
Assume that (6.4) is pr-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 pr-realizable. Let us prove that (6.5) is fulfilled. By Proposition 1, it is sufficient to prove that the formula $\neg\neg\mathcal E(\ell_i, \ell_j)$ is not pr-realizable. Assume the opposite. Then $\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 pr-realizable. Since the formula $\widetilde{A_3}$ is pr-realizable, the formula $\neg\neg\mathcal E(k_i, \ell_j)$ is also pr-realizable. Since the formula $\widetilde{A_2}$ is pr-realizable, the formula $\neg\neg\mathcal E(\ell_j, k_j)$ is pr-realizable. Since the formula $\widetilde{A_3}$ is pr-realizable, the formula $\neg\neg\mathcal E(k_i, k_j)$ is also pr-realizable contrary to the assumption that $\neg\mathcal E(k_i, k_j)$ is pr-realizable. Thus the formula $\neg\mathcal E(\ell_i, \ell_j)$ is pr-realizable, as was to be proved. So, we proved that, for any $k_1, \dots, k_n, \ell_1, \dots, \ell_n$, if formula (6.4) is pr-realizable, then (6.5) holds. By Proposition 3, the number $\mathsf a_{\mathsf a}^{2n+1}$ pr-realizes formula (6.3). 4) If $\Psi(x_1, \dots, x_n)$ is $\neg Z(x_i)$, where $1\leqslant i\leqslant n$, then $\widetilde{\Psi }(x_1, \dots, x_n)$ is $\neg\mathcal Z(x_i)$, and, in this case, (6.1) is the formula
$$
\begin{equation}
\forall\mathbf x, \mathbf y\, \bigl(\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)\bigr).
\end{equation}
\tag{6.6}
$$
First, we prove that, for any $k_1, \dots, k_n$, $\ell_1, \dots, \ell_n$, if the $\mathrm{Ar}^*$-formula
$$
\begin{equation}
\neg\neg\mathcal E(k_1, \ell_1)\, \&\cdots\&\, \neg\neg \mathcal E(k_n, \ell_n)\, \&\, \neg\mathcal Z(k_i)
\end{equation}
\tag{6.7}
$$
is pr-realizable, then
Assume that formula (6.7) is pr-realizable. Then the formulas $\neg\neg\mathcal E(k_i, \ell_i)$ and $\neg\mathcal Z(k_i)$ are pr-realizable. We prove that (6.8) holds. By Proposition 1, it is sufficient to prove that the formula $\neg\neg\mathcal Z(\ell_i)$ is not pr-realizable. Assume the opposite. Then the formulas $\neg\neg\mathcal E(k_i, \ell_i)$ and $\neg\neg\mathcal Z(\ell_i)$ are pr-realizable. Since the formula $\widetilde{A_2}$ is pr-realizable, the formula $\neg\neg\mathcal E(\ell_i, k_i)$ is pr-realizable. Since the formula $\widetilde{A_6}$ is pr-realizable, the formula $\neg\neg\mathcal Z(k_i)$ is also pr-realizable contrary to the assumption that the formula $\neg\mathcal Z(k_i)$ is pr-realizable. Thus the formula $\neg\mathcal Z(\ell_i)$ is pr-realizable, as was to be proved. So, we proved that, for any $k_1, \dots, k_n, \ell_1, \dots, \ell_n$, if formula (6.7) is pr-realizable, then (6.8) is fulfilled. By Proposition 3, the number $\mathsf a_{\mathsf a}^{2n+1}$ pr-realizes formula (6.6). 5) If $\Psi(x_1, \dots, x_n)$ is $\neg S(x_i, x_j)$, $1\leqslant i, j\leqslant n$, then $\widetilde{\Psi }(x_1, \dots, x_n)$ is the formula $\neg\mathcal S(x_i, x_j)$, and, in this case, (6.1) is the formula
$$
\begin{equation}
\forall\mathbf x, \mathbf y\, \bigl(\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)\bigr).
\end{equation}
\tag{6.9}
$$
First, we prove that, for any $k_1, \dots, k_n, \ell_1, \dots, \ell_n$, if the $\mathrm{Ar}^*$-formula
$$
\begin{equation}
\neg\neg\mathcal E(k_1, \ell_1)\, \&\cdots\&\, \neg\neg \mathcal E(k_n, \ell_n)\, \&\, \neg\mathcal S(k_i, k_j)
\end{equation}
\tag{6.10}
$$
is pr-realizable, then
$$
\begin{equation}
\mathsf a\, \mathbf{pr}\, \neg\mathcal S(\ell_i, \ell_j).
\end{equation}
\tag{6.11}
$$
Suppose (6.10) is pr-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 pr-realizable. We prove that (6.11) holds. By Proposition 1, it is sufficient to prove that the formula $\neg\neg\mathcal S(\ell_i, \ell_j)$ is not pr-realizable. Assume the opposite. Then 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 pr-realizable. Since the formula $\widetilde{A_2}$ is pr-realizable, the formulas $\neg\neg\mathcal E(\ell_i, k_i)$ and $\neg\neg\mathcal E(\ell_j, k_j)$ are pr-realizable. Since $\widetilde{A_9}$ is pr-realizable, the formula $\neg\neg\mathcal S(k_i, k_j)$ is also pr-realizable contrary to the assumption that $\neg\mathcal S(k_i, k_j)$ is pr-realizable. Thus the formula $\neg\mathcal S(\ell_i, \ell_j)$ is pr-realizable, as was to be proved. So, we proved that, for any $k_1, \dots, k_n$, $\ell_1, \dots, \ell_n$, if formula (6.10) is pr-realizable, then (6.11) is fulfilled. By Proposition 3, the number $\mathsf a_{\mathsf a}^{2n+1}$ pr-realizes formula (6.9). 6) If $\Psi(x_1, \dots, x_n)$ is the formula $\neg A(x_i, x_j, x_m)$, where $1\leqslant i, j, m\leqslant n$, then $\widetilde{\Psi }(x_1, \dots, x_n)$ is the formula $\neg\mathcal A(x_i, x_j, x_m)$, and, in this case, (6.1) is the formula
$$
\begin{equation}
\forall\mathbf x, \mathbf y\, \bigl(\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)\bigr).
\end{equation}
\tag{6.12}
$$
First, we prove that, for any $k_1, \dots, k_n, \ell_1, \dots, \ell_n$, if the $\mathrm{Ar}^*$-formula
$$
\begin{equation}
\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)
\end{equation}
\tag{6.13}
$$
is pr-realizable, then
$$
\begin{equation}
\mathsf a\, \mathbf{pr}\, \neg\mathcal A(\ell_i, \ell_j, \ell_m).
\end{equation}
\tag{6.14}
$$
Suppose (6.13) is pr-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 pr-realizable. We prove that (6.14) holds. By Proposition 1, it is sufficient to prove that the formula $\neg\neg\mathcal A(\ell_i, \ell_j, \ell_m)$ is not pr-realizable. Assume the opposite. 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\neg\mathcal A(\ell_i, \ell_j, \ell_m)$ are pr-realizable. Since $\widetilde{A_2}$ is pr-realizable, so 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)$. Since the formula $\widetilde{A_{15}}$ is pr-realizable, the formula $\neg\neg\mathcal A(k_i, k_j, k_m)$ is also pr-realizable contrary to the assumption that the formula $\neg\mathcal A(k_i, k_j, k_m)$ is pr-realizable. Thus the formula $\neg\mathcal A(\ell_i, \ell_j, \ell_m)$ is pr-realizable, as was to be proved. So, we proved that, for any $k_1, \dots, k_n$, $\ell_1, \dots, \ell_n$, if formula (6.13) is pr-realizable, then (6.14) is fulfilled. By Proposition 3, the number $\mathsf a_{\mathsf a}^{2n+1}$ pr-realizes formula (6.12). 7) If $\Psi(x_1, \dots, x_n)$ is the formula $\neg M(x_i, x_j, x_m)$, where $1\leqslant i, j, m\leqslant n$, then $\widetilde{\Psi }(x_1, \dots, x_n)$ is the formula $\neg\mathcal M(x_i, x_j, x_m)$, and, in this case, (6.1) is the formula
$$
\begin{equation}
\forall\mathbf x, \mathbf y\bigl(\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)\bigr).
\end{equation}
\tag{6.15}
$$
That formula (6.15) is pr-realizable is proved by the same argument as in the case of formula (6.12), only it is necessary to replace $\mathcal A$ by $\mathcal M$ and use the formula $\widetilde{A_{20}}$ instead of $\widetilde{A_{15}}$.
8) If $\Psi(x_1, \dots, x_n)$ is $\Psi_1(x_1, \dots, x_n)\, \&\, \Psi_2(x_1, \dots, x_n)$, where $\Psi_1(x_1, \dots, x_n)$ and $\Psi_2(x_1, \dots, x_n)$ are completely negative $\mathrm{Ar}$-formulas, and the inductive hypothesis states that the formulas
$$
\begin{equation}
\forall\mathbf x, \mathbf y\bigl(\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)\bigr),
\end{equation}
\tag{6.16}
$$
$$
\begin{equation}
\forall\mathbf x, \mathbf y\bigl(\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)\bigr)
\end{equation}
\tag{6.17}
$$
are pr-realizable, 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)$, and we have to prove that the formula
$$
\begin{equation}
\forall\mathbf x, \mathbf y\bigl(\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)\bigr)
\end{equation}
\tag{6.18}
$$
is pr-realizable.
First, we prove that, for any $k_1, \dots, k_n, \ell_1, \dots, \ell_n$, if the $\mathrm{Ar}^*$-formula
$$
\begin{equation}
\neg\neg\mathcal E(k_1, \ell_1)\, \&\cdots\&\, \neg\neg\mathcal E(k_n, \ell_n) \, \&\, \widetilde{\Psi_1}(k_1, \dots, k_n)\, \&\, \widetilde{\Psi_2}(k_1, \dots, k_n)
\end{equation}
\tag{6.19}
$$
is pr-realizable, then so is the formula
$$
\begin{equation}
\widetilde{\Psi_1}(\ell_1, \dots, \ell_n)\, \&\, \widetilde{\Psi_2}(\ell_1, \dots, \ell_n).
\end{equation}
\tag{6.20}
$$
Suppose that formula (6.19) is pr-realizable. Then so are the formulas $\neg\neg\mathcal E(k_i, \ell_i)$ ($i\, {=}\, 1, \dots, n$), $\widetilde{\Psi_1}(k_1, \dots, k_n)$ and $\widetilde{\Psi_2}(k_1, \dots, k_n)$. We need to prove that (6.20) is pr-realizable, that is, that $\widetilde{\Psi_1}(\ell_1, \dots, \ell_n)$ and $\widetilde{\Psi_2}(\ell_1, \dots, \ell_n)$ are pr-realizable. But this follows from pr-realizability of (6.16) and (6.17). By Proposition 6, we have $a_{\Psi_i}\, \mathbf{pr}\, \Psi_i(\ell_1, \dots, \ell_n)$ for $i=1, 2$. As a result, we have $\langle a_{\Psi_1}, a_{\Psi_2}\rangle\, \mathbf{pr}\, \Psi_1 (\ell_1, \dots, \ell_n) \, \&\, \Psi_2(\ell_1, \dots, \ell_n)$. So, we proved that, for any $k_1, \dots, k_n$, $\ell_1, \dots, \ell_n$, if formula (6.19) is pr-realizable, then the number $\langle a_{\Psi_1}, a_{\Psi_2}\rangle$ pr-realizes formula (6.20). By Proposition 3, the number $\mathsf a_{\langle a_{\Psi_1}, a_{\Psi_2}\rangle}^{2n+1}$ pr-realizes formula (6.18). 9) Suppose $\Psi(x_1, \dots, x_n)$ is $\forall\mathbf z\, (\Psi_1(x_1, \dots, x_n, \mathbf z)\to \Psi_2(x_1, \dots, x_n, \mathbf z))$, where $\mathbf z$ is a list (possibly empty) of distinct individual variables $z_1, \dots, z_m$, the variables $x_i$ are not in $\mathbf z$, and $\Psi_1(x_1, \dots, x_n, \mathbf z)$ and $\Psi_2(x_1, \dots, x_n, \mathbf z)$ are completely negative $\mathrm{Ar}$-formulas, and the induction hypothesis states that the formulas
$$
\begin{equation}
\forall\mathbf x, \mathbf z, \mathbf y, \mathbf w\, (\neg\neg\mathcal{E} (\mathbf x, \mathbf y)\, \ \, \neg\neg\mathcal{E}(\mathbf z, \mathbf w)\, \ \, \widetilde{\Psi_1}(\mathbf x, \mathbf z)\to \widetilde{\Psi_1}(\mathbf y, \mathbf w)),
\end{equation}
\tag{6.21}
$$
$$
\begin{equation}
\forall\mathbf x, \mathbf z, \mathbf y, \mathbf w\, (\neg\neg\mathcal{E} (\mathbf x, \mathbf y)\, \ \, \neg\neg\mathcal{E}(\mathbf z, \mathbf w)\, \ \, \widetilde{\Psi_2}(\mathbf x, \mathbf z)\to \widetilde{\Psi_2}(\mathbf y, \mathbf w))
\end{equation}
\tag{6.22}
$$
are pr-realizable. Here, $\mathbf w$ is a list of distinct individual variables $w_1, \dots, w_m$, and if $\mathbf u=u_1, \dots, u_k$ and $\mathbf v=v_1, \dots, v_k$ are some lists of individual variables, then $\neg\neg\mathcal{E}(\mathbf u, \mathbf v)$ is the formula $\neg\neg\mathcal E(u_1, v_1)\, \&\cdots\&\, \neg\neg\mathcal{E}(u_k, v_k)$. Hence $\widetilde{\Psi}(x_1, \dots, x_n)$ is the formula $\forall\mathbf z\, (\widetilde{\Psi_1} (x_1, \dots, x_n, \mathbf z)\to\widetilde{\Psi_2} (x_1, \dots, x_n, \mathbf z))$, and we have to prove that the formula
$$
\begin{equation}
\forall\mathbf x, \mathbf y\bigl(\neg\neg\mathcal{E}(\mathbf x, \mathbf y) \, \&\, \forall\mathbf z\, (\widetilde{\Psi_1}(\mathbf x, \mathbf z)\to \widetilde{\Psi_2}(\mathbf x, \mathbf z))\to\forall\mathbf z\, (\widetilde{\Psi_1}(\mathbf y, \mathbf z)\to\widetilde{\Psi_2} (\mathbf y, \mathbf z))\bigr)
\end{equation}
\tag{6.23}
$$
is pr-realizable.
First, we prove that, for any $k_1, \dots, k_n, \ell_1, \dots, \ell_n$, if the $\mathrm{Ar}^*$-formula
$$
\begin{equation}
\neg\neg\mathcal E(k_1, \ell_1)\&\dots\, \&\, \neg\neg \mathcal E(k_n, \ell_n)\, \&\, \forall\mathbf z\, (\widetilde{\Psi_1} (k_1, \dots, k_n, \mathbf z)\to\widetilde{\Psi_2}(k_1, \dots, k_n, \mathbf z))
\end{equation}
\tag{6.24}
$$
is pr-realizable, then, for any $p_1, \dots, p_m$, if the formula
$$
\begin{equation}
\widetilde{\Psi_1}(\ell_1, \dots, \ell_n, p_1, \dots, p_m)
\end{equation}
\tag{6.25}
$$
is pr-realizable, then so is the formula
$$
\begin{equation}
\widetilde{\Psi_2}(\ell_1, \dots, \ell_n, p_1, \dots, p_m).
\end{equation}
\tag{6.26}
$$
Let $k_1, \dots, k_n, \ell_1, \dots, \ell_n, p_1, \dots, p_m$ be such that formulas (6.24) and (6.25) are pr-realizable. Then the formulas $\neg\neg\mathcal E(k_i, \ell_i)$ ($i=1, \dots, n$) and
$$
\begin{equation}
\forall\mathbf z\bigl(\widetilde{\Psi_1}(k_1, \dots, k_n, \mathbf z) \to\widetilde{\Psi_2}(k_1, \dots, k_n, \mathbf z)\bigr)
\end{equation}
\tag{6.27}
$$
are pr-realizable. Since the formula $\widetilde{A_2}$ is pr-realizable, the formulas $\neg\neg\mathcal E(\ell_i, k_i)$ ($i=1, \dots, n$) are pr-realizable. Since the formula $\widetilde{A_1}$ is pr-realizable, the formulas $\neg\neg\mathcal E(p_i, p_i)$ ($i=1, \dots, m$) are also pr-realizable. Since formula (6.22) is pr-realizable, the formula $\widetilde{\Psi_1}(k_1, \dots, k_n, p_1, \dots, p_m)$ is pr-realizable. Since formula (6.27) is pr-realizable, so is the formula $\widetilde{\Psi_2}(k_1, \dots, k_n, p_1, \dots, p_m)$. Since formula (6.22) is pr-realizable, formula (6.26) is pr-realizable, as was to be proved. By Proposition 6, the number $a_{\Psi_2}$ pr-realizes formula (6.26). Thus, for fixed $k_1, \dots, k_n, \ell_1, \dots, \ell_n$ such that formula (6.24) is pr-realizable, we proved that, for any $p_1, \dots, p_m$, if formula (6.25) is pr-realizable, then $a_{\Psi_2}$ pr-realizes formula (6.26). By Proposition 3, the number $b=\mathsf a_{a_{\Psi_2}}^{m+1}$ pr-realizes the formula $\forall\mathbf z\, (\widetilde{\Psi_1}(\ell_1, \dots, \ell_n, \mathbf z) \to\widetilde{\Psi_2}(\ell_1, \dots, \ell_n, \mathbf z))$, and the number $\mathsf a_b^{2n+1}$ pr-realizes formula (6.23). This proves Proposition 7. § 7. Standard elements in an interpretationFor a natural $n$, the predicate $\mathrm{Ar}$-formula $[n](x)$ is defined inductively:
Proposition 8. If $\mathbf{\Phi}$ is an interpretation of the formula $Q$, then, for any $n$, the $Ar$-formula is pr-realizable. Proof. We prove the pr-realizability of (7.1) by induction on $n$. If $n=0$, then $[n](x)$ is $\neg\neg Z(x)$. So, we have to prove that $\forall x, y\, (\neg\neg\mathcal Z(x)\, \&\, \neg\neg\mathcal Z(y) \to\neg\neg\mathcal{E}(x, y))$ is pr-realizable, but this is exactly the formula $\widetilde{A_5}$, which is pr-realizable since $\mathbf\Phi$ is an interpretation of the formula $Q$. Now suppose that formula (7.1) is pr-realizable for some given $n$. Let us show that the formula is pr-realizable.
First, we prove that, for any $k$, $\ell$, if the formula is pr-realizable, then
$$
\begin{equation}
\mathsf a\, \mathbf{pr}\, \neg\neg\mathcal{E}(k, \ell).
\end{equation}
\tag{7.4}
$$
Assume that (7.3) is pr-realizable. Then $\neg\mathcal Z(k)$ $\forall y\, (\neg\neg\mathcal S(y, k) \to\widetilde{[n]}(y))$, $\neg\mathcal Z(\ell)$, and $\forall y\, (\neg\neg\mathcal S(y, \ell)\to\widetilde{[n]}(y))$ are pr-realizable. Since the formula $\widetilde{A_{12}}$ is pr-realizable, so is the formula $\exists y\, \neg\neg\mathcal S(y, k)$. This means that for some natural number $p$, the formula $\neg\neg\mathcal S(p, k)$ is pr-realizable. It follows that the formula $\widetilde{[n]}(p)$ is pr-realizable. For the same reasons, there is a natural number $q$, such that the formulas $\neg\neg\mathcal S(q, \ell)$ and $\widetilde{[n]}(q)$ are pr-realizable. By the induction hypothesis, the formula $\neg\neg\mathcal E(p, q)$ is pr-realizable. Since the formulas $\mathcal E(k, k)$ and $\widetilde{A_9}$ are pr-realizable, so is the formula $\neg\neg\mathcal S(q, k)$. Since the formula $\widetilde{A_8}$ is pr-realizable, the formula $\neg\neg\mathcal E(k, \ell)$ is pr-realizable. By Proposition 1, (7.4) holds, as was to be proved. So, we proved that, for any $k, \ell$, if formula (7.3) is pr-realizable, then (7.4) is fulfilled. By Proposition 3, the number $\mathsf a_{\mathsf a}^3$ pr-realizes formula (7.2). This proves Proposition 8. Proposition 9. Let $\mathbf{\Phi}$ be an interpretation of the formula $Q$. Then, for any natural numbers $k$ and $n$, it is possible to effectively determine whether the $\mathrm{Ar}^*$-formula $\widetilde{[n]}(k)$ is pr-realizable. Proof. Suppose $\mathbf{\Phi}$ is an interpretation of $Q$, and $e\, \mathbf{pr}\, \widetilde{Q}$. We argue by induction on $n$. If $n=0$, then $\widetilde{[n]}(k)$ is the formula $\neg\neg\mathcal Z(k)$. Suppose a natural number $k$ is given. We can extract from $e$ a pr-realization of the formula $\widetilde{A_{12}}$. Then we are able to determine which of the formulas $\neg\neg\mathcal Z(k)$ and $\exists y\, \neg\neg\mathcal S(y, k)$ is pr-realizable. If the first one is pr-realizable, then the formula $\widetilde{[0]}(k)$ is pr-realizable. If the formula $\exists y\, \neg\neg\mathcal S(y, k)$ is pr-realizable, then for some natural $\ell$, the formula $\neg\neg\mathcal S(\ell, k)$ is pr-realizable. Since the formula $\widetilde{A_{11}}$ is pr-realizable, the formula $\neg\mathcal Z(k)$ is pr-realizable. This means that the formula $\widetilde{[0]}(k)$ is not pr-realizable. Now suppose that, for some given $n$ and any $\ell$, we can effectively determine whether the formula $\widetilde{[n]}(\ell)$ is pr-realizable. Suppose a natural number $k$ is given, and we want to determine whether the formula $\widetilde{[n+1]}(k)$, that is, $\neg\mathcal Z(k)\, \&\, \forall y\, (\neg\neg\mathcal S(y, k)\to \widetilde{[n]}(y))$, is pr-realizable. Using the pr-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 pr-realizable. If the formula $\neg\neg\mathcal Z(k)$ is pr-realizable, then the formula $\widetilde{[n+1]}(k)$ is not pr-realizable. Assume that the formula $\exists y\, \neg\neg\mathcal S(y, k)$ is pr-realizable. Then there is a natural number $\ell$ such that the formula $\neg\neg\mathcal S(\ell, k)$ is pr-realizable. By the inductive hypothesis, we can determine whether the formula $\widetilde{[n]}(\ell)$ is pr-realizable. If it is not pr-realizable, then the formula $\widetilde{[n+1]}(k)$ obviously is not pr-realizable. Suppose the formula $\widetilde{[n]}(\ell)$ is pr-realizable. Let us show that the formula $\widetilde{[n+1]}(k)$ is pr-realizable. It is enough to prove that the formula $\forall y\, (\neg\neg\mathcal S(y, k)\to\widetilde{[n]}(y))$ is pr-realizable. First, we prove that, for any $p$, if the formula $\neg\neg\mathcal S(p, k)$ is pr-realizable, then the formula $\widetilde{[n]}(p)$ is pr-realizable. Assume that the formula $\neg\neg\mathcal S(p, k)$ is pr-realizable. Recall that the formula $\neg\neg\mathcal S(\ell, k)$ is also pr-realizable. Since the formula $\widetilde{A_{10}}$ is pr-realizable, so is the formula $\neg\neg\mathcal E(\ell, p)$. Recall that the formula $\widetilde{[n]}(\ell)$ is pr-realizable. Since the formula $[n](x)$ is completely negative, Proposition 7 yields that the formula $\widetilde{[n]}(p)$ is pr-realizable, as was to be proved. By Proposition 6, $a_{[n](x)}\, \mathbf{pr}\, \widetilde{[n]}(p)$. So, we proved that, for any $p$, if the formula $\neg\neg\mathcal S(p, k)$ is pr-realizable, then $a_{[n](x)}\, \mathbf{pr}\, \widetilde{[n]}(p)$. Hence $\mathsf a_{a_{[n](x)}}^2\, \mathbf{pr}\, \forall y\, (\neg\neg\mathcal S(y, k) \to\widetilde{[n]}(y))$ by Proposition 3. This means that the formula $\widetilde{[n+1]}(k)$ is pr-realizable. Proposition 9 is proved. Proposition 10. If $\mathbf{\Phi}$ is an interpretation of the formula $Q$, then there exists a primitive recursive function $\mathsf f$ such that, for any natural $n$, the $\mathrm{Ar}^*$-formula $\widetilde{[n]}(\mathsf f(n))$ is pr-realizable. Proof. Let $\mathbf{\Phi}$ is an interpretation of $Q$. Then the formula $\widetilde{A_4}$ is pr-realizable. This means that $a_4\, \mathbf{pr}\, \exists x\, \neg\neg\mathcal{Z}(x)$ for some natural $a_4$. Then $[a_4]_1\, \mathbf{pr}\, \neg\neg\mathcal{Z}([a_4]_0)$. Putting $\mathsf f(0)=[a_4]_0$, we see that the formula $\neg\neg\mathcal{Z}((\mathsf f(0))$, that is, $\widetilde{[0]}(\mathsf f(0))$, is pr-realizable. By Proposition 1,
Suppose the value $\mathsf f(n)$ is defined for some given $n$. Since $\widetilde{A_7}$ is pr-realizable, for some natural number $a_7$ we have $a_7\, \mathbf{pr}\, \forall x\, (\top\to\exists y\, \neg\neg\mathcal{S}(x, y))$. Then $a_7$ is an index of a primitive recursive function $g$ such that, for any $k$, the number $g(0, k)$ pr-realizes the formula $\exists y\, \neg\neg\mathcal{S}(k, y)$. In particular, $g(0, \mathsf f(n))\, \mathbf{pr}\, \exists y\, \neg\neg\mathcal{S}(\mathsf f(n), y)$ and $[g(0, \mathsf f(n))]_1\, \mathbf{pr}\, \neg\neg\mathcal{S} (\mathsf f(n), [g(0, \mathsf f(n))]_0)$. Put $\mathsf f(n+1)=[g(0, \mathsf f(n))]_0$. Note that the formula is pr-realizable. Thus, we have the following definition of the function $\mathsf f$:
$$
\begin{equation*}
\begin{cases} \mathsf f(0)=[a_4]_0, \\ \mathsf f(n+1)=[g(0, \mathsf f(n))]_0, \end{cases}
\end{equation*}
\notag
$$
where the number $a_4$ and the primitive recursive function $g$ depend only on the given pr-realization of the formula $\widetilde{Q}$. Obviously, the function $\mathsf f$ is primitive recursive.
We prove that, for any $n$, the formula $\widetilde{[n]}(\mathsf f(n))$ is pr-realizable. We argue by induction on $n$. If $n=0$, then the required result follows from (7.5) proved above. Now suppose that, for some given $n$, the formula $\widetilde{[n]}(\mathsf f(n))$ is pr-realizable. Hence, by Proposition 6, $a_{[n](x)}\, \mathbf{pr}\, \widetilde{[n]}(\mathsf f(n))$. Let us prove that the formula $\widetilde{[n+1]}(\mathsf f(n+1))$ is pr-realizable, that is, that the formulas and
$$
\begin{equation}
\forall y\, (\neg\neg\mathcal{S}(y, \mathsf f(n+1))\to\widetilde{[n]}(y))
\end{equation}
\tag{7.8}
$$
are pr-realizable. Since the formulas (7.6) and $\widetilde{A_{11}}$ are pr-realizable, formula (7.7) is pr-realizable. Now we prove that formula (7.8) is pr-realizable. First, we prove that, for any $k$, if the formula $\neg\neg\mathcal{S}(k, \mathsf f(n+1))$ is pr-realizable, then the formula $\widetilde{[n]}(k)$ is pr-realizable. Suppose the formula $\neg\neg\mathcal{S}(k, \mathsf f(n+1))$ is pr-realizable. Since the formulas (7.6) and $\widetilde{A_{10}}$ are pr-realizable, the formula $\neg\neg\mathcal{E}(\mathsf f(n), k)$ is pr-realizable. By the inductive hypothesis, the formula $\widetilde{[n]}(\mathsf f(n))$ f is pr-realizable. By Proposition 7, the formula $\widetilde{[n]}(k)$ is pr-realizable, as was to be proved. By Proposition 6, $a_{[n](x)}\, \mathbf{pr}\, \widetilde{[n]}(k)$. So, we proved that, for any $k$, if $\neg\neg{\mathcal S}(k, \mathsf f(n+1))$ is pr-realizable, then $a_{[n](x)}\, \mathbf{pr}\, \widetilde{[n]}(k)$. By Proposition 3, the number $\mathsf a_{a_{[n](x)}}^2$ pr-realizes formula (7.8). This proves Proposition 10. Proposition 11. If $\mathbf{\Phi}$ is an interpretation of the formula $Q$, then, for any natural numbers $n$, $m$ and $a$, if the $\mathrm{Ar}^*$-formulas $\widetilde{[n]}(a)$ and $\widetilde{[m]}(a)$ are pr-realizable, then $m=n$. Proof. Suppose $\widetilde{[n]}(a)$ and $\widetilde{[m]}(a)$ are pr-realizable. By induction on $n$ we prove that $n<m$ is impossible. Let $n=0$, $m=k+1$. Then the formulas $\widetilde{[0]}(a)$, that is, $\neg\neg\mathcal Z(a)$, and $\widetilde{[k+1]}(a)$, that is, $\neg\mathcal Z(a)\, \&\, \forall y\, (\neg\neg\mathcal S(y, a)\to \widetilde{[k]}(y))$, are pr-realizable. Obviously, this is not possible. Now let $m=k+1>n+1$, and assume that $\widetilde{[n+1]}(a)$ and $\widetilde{[k+1]}(a)$, that is, $\neg\mathcal Z(a)\, \&\, \forall y\, (\neg\neg\mathcal S(y, a)\to \widetilde{[n]}(y))$ and $\neg\mathcal Z(a)\, \&\, \forall y\, (\neg\neg\mathcal S(y, a)\to\widetilde{[k]}(y))$, are pr-realizable. Since the formulas $\neg\mathcal Z(a)$ and $\widetilde{A_{12}}$ are pr-realizable, there is a number $b$, such that the formula $\neg\neg\mathcal S(b, a)$ is pr-realizable. Hence the formulas $\widetilde{[n]}(b)$ and $\widetilde{[k]}(b)$ are pr-realizable, and at the same time $n<k$. But this is impossible by the inductive hypothesis. This proves Proposition 11. For any $n$, we let $\overline n$ denote the number $\mathsf f(n)$. Proposition 12. Let $\mathbf\Phi$ be an interpretation of the formula $Q$. Then, for any quantifier-free completely negative $\mathrm{Ar}$-formula $\Psi(x_1, \dots, x_m)$ which does not contain free variables other than $x_1, \dots, x_m$, and any natural numbers $k_1, \dots, k_m$, the $\mathrm{Ar}^*$-formula $\Psi(k_1, \dots, k_m)$ is true if and only if the $\mathrm{Ar}^*$-formula $\widetilde{\Psi}(\overline{k_1}, \dots, \overline{k_m})$ is pr-realizable. Proof. Let a list of $\mathrm{Ar}$-formulas be an interpretation of the formula $Q$. Note that each quantifier-free completely negative formula $\widetilde{\Psi}(x_1, \dots, x_n)$ is constructed from the formulas $\top$, $\bot$, $\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\leqslant i, j, k\leqslant n$, using the logical symbols $\&$ and $\to$. We will argue by induction on the construction of a formula $\Psi(x_1, \dots, x_n)$. We omit the trivial case $\Psi$ is $\top$ or $\bot$, because, in this case, $\widetilde{\Psi} (\overline{k_1}, \dots, \overline{k_m})$ coincides with $\Psi(k_1, \dots, k_m)$.
1) Suppose $\Psi(x_1, \dots, x_n)$ is $\neg E(x_i, x_j)$, where $1\leqslant i, j\leqslant n$. Then $\widetilde{\Phi}(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 pr-realizable, the formula $\neg\neg\mathcal E(\overline{k_i}, \overline{k_j})$ is pr-realizable and the formula $\neg\mathcal E(\overline{k_i}, \overline{k_j})$ is not pr-realizable. Thus the formula $\neg E(k_i, k_j)$ is true if and only if the formula $\neg\mathcal E(\overline{k_i}, \overline{k_j})$ is pr-realizable. Now suppose $i\ne j$. Assume that the formula $\neg E(k_i, k_j)$ is true. This means that $k_i\ne k_j$. We prove that the formula $\neg\mathcal E(\overline{k_i}, \overline{k_j})$ is pr-realizable. By Proposition 1, it is sufficient to prove that the formula $\neg\neg\mathcal E(\overline{k_i}, \overline{k_j})$ is not pr-realizable. Assume the opposite. By the definition of the function $\mathsf f$, the formula $\widetilde{[k_i]}(\overline{k_i})$ is pr-realizable. Hence by Proposition 7, the formula $\widetilde{[k_i]}(\overline{k_j})$ is also pr-realizable. On the other hand, the formula $\widetilde{[k_j]}(\overline{k_j})$ is pr-realizable. By Proposition 11, $k_i=k_j$, contrary to the assumption that the formula $\neg E(k_i, k_j)$ is true. Thus the formula $\neg\mathcal E(\overline{k_i}, \overline{k_j})$ is pr-realizable. Conversely, assume that $\neg\mathcal E(\overline{k_i}, \overline{k_j})$ is pr-realizable. We prove that the formula $\neg E(k_i, k_j)$ is true, that is, $k_i\ne k_j$. Assume the opposite. Then $\overline{k_i}=\overline{k_j}$. Since the formula $\widetilde{A_1}$ is pr-realizable, the formula $\neg\neg\mathcal E(\overline{k_i}, \overline{k_j})$ is pr-realizable, contrary to the assumption that the formula $\neg\mathcal E(\overline{k_i}, \overline{k_j})$ is pr-realizable. Thus $k_i\ne k_j$ and the formula $\neg E(k_i, k_j)$ is true. 2) Let $\Psi(x_1, \dots, x_n)$ be $\neg Z(x_i)$, where $1\leqslant i\leqslant 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\ne 0$. Let us prove that the formula $\neg\mathcal Z(\overline{k_i})$ is pr-realizable. Assume the opposite. Then the formula $\neg\neg\mathcal Z(\overline{k_i})$, that is, $\widetilde{[0]}(\overline{k_i})$, is pr-realizable. On the other hand, the formula $\widetilde{[k_i]}(\overline{k_i})$ is also pr-realizable. By Proposition 11, $k_i=0$, contrary to the assumption that the formula $\neg Z(k_i)$ is true. Conversely, suppose the formula $\neg\mathcal Z(\overline{k_i})$ is pr-realizable. Then the formula $\neg\neg\mathcal Z(\overline{k_i})$, that is, $\widetilde{[0]}(\overline{k_i})$, is not pr-realizable. We prove that the formula $\neg Z(k_i)$ is true, that is, $k_i\ne 0$. Assume the opposite. Then the formula $\widetilde{[0]}(\overline{k_i})$ is pr-realizable. This contradiction proves that the formula $\neg Z(k_i)$ is true. 3) Let $\Psi(x_1, \dots, x_n)$ be the formula $\neg S(x_i, x_j)$, where $1\leqslant i, j\leqslant 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\ne k_i+1$. We prove that the formula $\neg\mathcal S(\overline{k_i}, \overline{k_j})$ is pr-realizable. Assume the opposite. Then the formula $\neg\neg\mathcal S(\overline{k_i}, \overline{k_j})$ is pr-realizable. We prove that the formula $\widetilde{[k_i+1]}(\overline{k_j})$, that is,
$$
\begin{equation}
\neg\mathcal Z(\overline{k_j})\, \&\, \forall y\bigl(\neg\neg \mathcal S(y, \overline{k_j})\to\widetilde{[k_i]}(y)\bigr),
\end{equation}
\tag{7.9}
$$
is pr-realizable. Since $\neg\neg\mathcal S(\overline{k_i}, \overline{k_j})$ and $\widetilde{A_{11}}$ are pr-realizable, so is the formula $\neg\mathcal Z(\overline{k_j})$. Let us prove that the formula $\forall y\, (\neg\neg\mathcal S(y, \overline{k_j})\to\widetilde{[k_i]}(y))$ is pr-realizable. First, we prove that, for any $\ell$, if the formula $\neg\neg\mathcal S(\ell, \overline{k_j})$ is pr-realizable, then so is the formula $\widetilde{[k_i]}(\ell)$. Suppose the formula $\neg\neg\mathcal S(\ell, \overline{k_j})$ is pr-realizable. Then the formulas $\neg\neg\mathcal S(\overline{k_i}, \overline{k_j})$ and $\neg\neg\mathcal S(\ell, \overline{k_j})$ are pr-realizable. Since the formula $\widetilde{A_{10}}$ is pr-realizable, the formula $\neg\neg\mathcal E(\overline{k_i}, \ell)$ is pr-realizable. It follows from Proposition 7 that the formula $\widetilde{[k_i]}(\ell)$ is pr-realizable, as was to be proved. By Proposition 6, we have $a_{[k_i](x)}\, \mathbf{pr}\, \widetilde{[k_i]}(\ell)$. So, we proved that, for any $\ell$, if the formula $\neg\neg\mathcal S(\ell, \overline{k_j})$ is pr-realizable, then $a_{[k_i](x)}\, \mathbf{pr}\, \widetilde{[k_i]}(\ell)$. By Proposition 3, the number $\mathsf a_{a_{[k_i](x)}}^2$ pr-realizes the formula $\forall y\, (\neg\neg\mathcal S(y, \overline{k_j})\to\widetilde{[k_i]}(y))$. Thus, we proved that the formula $\neg\mathcal S(\overline{k_i}, \overline{k_j})$ is pr-realizable if the formula $\neg S(k_i, k_j)$ is true.
Conversely, suppose the formula $\neg\mathcal S(\overline{k_i}, \overline{k_j})$ is pr-realizable. We prove that the formula $\neg S(k_i, k_j)$ is true, that is, $k_j\ne k_i+1$. Assume the opposite. Then the formula $\widetilde{[k_i+1]}(\overline{k_j})$, that is, (7.9), is pr-realizable. It follows that the formula $\neg\mathcal Z(k_j)$ is pr-realizable. Since the formula $\widetilde{A_{12}}$ is pr-realizable, there is some natural $\ell$ such that the formula $\neg\neg\mathcal S(\ell, \overline{k_j})$ is pr-realizable. On the other hand, since formula (7.9) is pr-realizable, the formula $\widetilde{[k_i]}(\ell)$ is pr-realizable. Since the formula $\widetilde{[k_i]}(\overline{k_i})$ is also pr-realizable, it follows from Proposition 8, that the formula $\neg\neg\mathcal E(\ell, \overline{k_i})$ is pr-realizable. By Proposition 7, the formula $\neg\neg\mathcal S(\overline{k_i}, \overline{k_j})$ is pr-realizable, which contradicts the assumption, that the formula $\neg\mathcal S(\overline{k_i}, \overline{k_j})$ is pr-realizable. Thus, the formula $\neg S(k_i, k_j)$ is true. 4) Let $\Psi(x_1, \dots, x_n)$ be the formula $\neg A(x_i, x_j, x_m)$, where $1\leqslant i, j, m\leqslant n$. Then $\widetilde{\Psi }(x_1, \dots, x_n)$ is the formula $\neg\mathcal A(x_i, x_j, x_m)$. We prove the proposition by induction on $k_j$. Let $k_j=0$. Hence $\overline{k_j}=\overline0$ and the formula $\widetilde{[0]}(\overline{k_j})$, that is, $\neg\neg\mathcal Z(\overline{k_j})$, is pr-realizable. Suppose the formula $\neg A(k_i, k_j, k_m)$ is true. This means that $k_m\ne k_i$. We prove that the formula $\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Assume the opposite. Then the formula $\neg\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Since the formula $\widetilde{A_{16}}$ pr-realizable, the formula $\neg\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_i})$ is pr-realizable. Since the formula $\widetilde{A_{14}}$ is pr-realizable, the formula $\neg\neg\mathcal E(\overline{k_m}, \overline{k_i})$ is pr-realizable. As was proved in the case 1), the formula $E(k_m, k_i)$ is true, that is, $k_m=k_i$ contrary to the assumption that the formula $\neg A(k_i, k_j, k_m)$ is true. Thus, we proved that the formula $\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Conversely, suppose the formula $\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. We prove that the formula $\neg A(k_i, k_j, k_m)$ is true, that is, $k_m\ne k_i$. Assume the opposite. Then $\overline{k_m}=\overline{k_i}$. Since the formula $\widetilde{A_{16}}$ is pr-realizable, the formula $\neg\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable contrary to the assumption of pr-realizability of $\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$. Thus, we 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 if and only if the formula $\neg\mathcal A(\overline{k_i}, \overline{\ell_j}, \overline{\ell_m})$ is pr-realizable. Note that the formula $\neg S(\ell_j, k_j)$ is not true. As was proved in case 3), the formula $\neg\mathcal S(\overline{\ell_j}, \overline{k_i})$ is not pr-realizable. Then the formula $\neg\neg\mathcal S(\overline{\ell_j}, \overline{k_i})$ is pr-realizable. Suppose the formula $\neg A(k_i, k_j, k_m)$ is true. This means that $k_m\ne k_i+k_j$. We prove that the formula $\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Assume the opposite. Then the formula $\neg\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. On the other hand, since $\neg A(k_i, \ell_j, k_i+\ell_j)$ is not true, by the induction assumption, the formula $\neg\mathcal A(\overline{k_i}, \overline{\ell_j}, \overline{k_i+\ell_j})$ is not pr-realizable. Then $\neg\neg\mathcal A(\overline{k_i}, \overline{\ell_j}, \overline{k_i+\ell_j})$ is pr-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 was proved in the case 3), the formula $\neg\mathcal S(\overline{k_i+\ell_j}, \overline{\ell_m})$ is not pr-realizable. Then the formula $\neg\neg\mathcal S(\overline{k_i+\ell_j}, \overline{\ell_m})$ is pr-realizable. Since the formula $\widetilde{A_{17}}$ is pr-realizable, the formula $\neg\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{\ell_m})$ is pr-realizable. Since the formula $\widetilde{A_{14}}$ is pr-realizable, the formula $\neg\neg\mathcal E(k_m, \ell_m)$ is pr-realizable. Then the formula $\neg\mathcal E(k_m, \ell_m)$ is not pr-realizable. As was proved in case 1), the formula $\neg E(k_m, \ell_m)$ is not true, and then the formula $E(k_m, \ell_m)$ is true, that is, $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, contrary to the assumption that the formula $\neg A(k_i, k_j, k_m)$ is true. Thus, we proved that the formula $\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Conversely, suppose the formula $\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. We prove that $\neg A(k_i, k_j, k_m)$ is true. Assume the opposite. Then $A(k_i, k_j, k_m)$ is true. This means that $k_m=k_i+k_j$. Put $\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 induction assumption, the formula $\neg\mathcal A(\overline{k_i}, \overline{\ell_j}, \overline{\ell_m})$ is not pr-realizable. Then the formula $\neg\neg\mathcal A(\overline{k_i}, \overline{\ell_j}, \overline{\ell_m})$ is pr-realizable. On the other hand, since the formulas $S(\ell_j, k_j)$ and $S(\ell_m, k_m)$ are true, the formulas $\neg S(\ell_j, k_j)$ and $\neg S(\ell_m, k_m)$ are not true. As was proved in case 3), the formulas $\neg\mathcal S(\overline{\ell_j}, \overline{k_j})$ and $\neg\mathcal S(\overline{\ell_m}, \overline{k_m})$ are not pr-realizable. Hence the formulas $\neg\neg\mathcal S(\overline{\ell_j}, \overline{k_j})$ and $\neg\neg\mathcal S(\overline{\ell_m}, \overline{k_m})$ are pr-realizable. Since the formula $\widetilde{A_{17}}$ is pr-realizable, the formula $\neg\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable contrary to the assumption that the formula $\neg\mathcal A(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Thus, we proved that the formula $\neg A(k_i, k_j, k_m)$ is true. 5) Let $\Psi(x_1, \dots, x_n)$ be the formula $\neg M(x_i, x_j, x_m)$, where $1\leqslant i, j, m\leqslant n$. Then $\widetilde{\Psi}(x_1, \dots, x_n)$ is the formula $\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]}(\overline{k_j})$, that is, $\neg\neg\mathcal Z(\overline{k_j})$, is pr-realizable. Suppose the formula $\neg M(k_i, k_j, k_m)$ is true. We prove that the formula $\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Assume the opposite. Then $\neg\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Since the formula $\widetilde{A_{21}}$ is pr-realizable, the formula $\neg\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_j})$ is pr-realizable. Since the formula $\widetilde{A_{19}}$ is pr-realizable, the formula $\neg\neg\mathcal E(\overline{k_m}, \overline{k_j})$ is pr-realizable. Hence the formula $\neg\mathcal E(\overline{k_m}, \overline{k_j})$ is not pr-realizable. As was proved in case 1), the formula $\neg E(k_m, k_j)$ is not true, that is, $k_m\, {=}\, k_j$. Then the formula $M(k_i, k_j, k_m)$ is true, contrary to the assumption that the formula $\neg M(k_i, k_j, k_m)$ is true. Thus, we proved that the formula $\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Conversely, suppose the formula $\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. We prove that the formula $\neg M(k_i, k_j, k_m)$ is true. Assume the opposite. Then $k_m=k_j$ and $\overline{k_m}=\overline{k_j}$. Since the formula $\widetilde{A_{21}}$ is pr-realizable, the formula $\neg\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable contrary to the assumption that $\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Thus, we proved that the formula $\neg M(k_i, k_j, k_m)$ is true. Now suppose $k_j=\ell_j+1$, and, for any $k_i, \ell_m$, the formula $\neg M(k_i, \ell_j, \ell_m)$ is true if and only if the formula $\neg\mathcal M(\overline{k_i}, \overline{\ell_j}, \overline{\ell_m})$ is pr-realizable. Since the formula $S(\ell_j, k_j)$ is true, the formula $\neg S(\ell_j, k_j)$ is not true. As shown in case 3), the formula $\neg\mathcal S(\overline{\ell_j}, \overline{k_j})$ is not pr-realizable. Hence $\neg\neg\mathcal S(\overline{\ell_j}, \overline{k_j})$ is pr-realizable. Suppose the formula $\neg M(k_i, k_j, k_m)$ is true. We prove that the formula $\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Assume the opposite. Then $\neg\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Since the formula $M(k_i, \ell_j, k_i\cdot\ell_j)$ is true, the formula $\neg M(k_i, \ell_j, k_i\cdot\ell_j)$ is not true. By the inductive assumption, the formula $\neg\mathcal M(\overline{k_i}, \overline{\ell_j}, \overline{k_i\cdot\ell_j})$ is not pr-realizable. Hence $\neg\neg\mathcal M(\overline{k_i}, \overline{\ell_j}, \overline{k_i\cdot\ell_j})$ is pr-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 was proved in case 4), the formula $\neg\mathcal A(\overline{k_i\cdot\ell_j}, \overline{k_i}, \overline{\ell_m})$ is not pr-realizable. Hence the formula $\neg\neg\mathcal A(\overline{k_i\cdot\ell_j}, \overline{k_i}, \overline{\ell_m})$ is pr-realizable. Since the formula $\widetilde{A_{22}}$ is pr-realizable, the formula $\neg\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{\ell_m})$ is pr-realizable. Since the formula $\widetilde{A_{19}}$ is pr-realizable, the formula $\neg\neg\mathcal E(k_m, \ell_m)$ is pr-realizable. Hence $\neg\mathcal E(k_m, \ell_m)$ is not pr-realizable and, as was proved in case 1), the formula $\neg E(k_m, \ell_m)$ is not true. Hence $E(k_m, \ell_m)$ is true, that is, $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, contrary to the assumption that the formula $\neg M(k_i, k_j, k_m)$ is true. Thus, we proved that the formula $\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Conversely, suppose the formula $\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. We prove that the formula $\neg M(k_i, k_j, k_m)$ is true. Assume the opposite. Then $k_m=k_i\cdot k_j$. Let $\ell_m=k_i\cdot\ell_j$. Hence 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. Hence 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 assumption, $\neg\mathcal M(\overline{k_i}, \overline{\ell_j}, \overline{\ell_m})$ is not pr-realizable. Hence the formula $\neg\neg\mathcal M(\overline{k_i}, \overline{\ell_j}, \overline{\ell_m})$ is pr-realizable. Since the formula $\neg A(\ell_m, k_i, k_m)$ is not true, the formula $\neg\mathcal A(\overline{\ell_m}, \overline{k_i}, \overline{k_m})$ is not pr-realizable as shown in case 4). Hence the formula $\neg\neg\mathcal A(\overline{\ell_m}, \overline{k_i}, \overline{k_m})$ is pr-realizable. Since the formula $\widetilde{A_{22}}$ is pr-realizable, the formula $\neg\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable contrary to the assumption that the formula $\neg\mathcal M(\overline{k_i}, \overline{k_j}, \overline{k_m})$ is pr-realizable. Thus, we proved that the formula $\neg M(k_i, k_j, k_m)$ is true. 6) Let $\Psi(x_1, \dots, x_n)$ be $\Psi_1(x_1, \dots, x_n)\, \&\, \Psi_2(x_1, \dots, x_n)$, where $\Psi_1(x_1, \dots, x_n)$ and $\Psi_2(x_1, \dots, x_n)$ are quantifier-free completely negative $\mathrm{Ar}$-formulas. The inductive assumption states that, for any $k_1, \dots, k_m$, the $\mathrm{Ar}^*$-formula $\Psi_i(k_1, \dots, k_m)$ is true if and only if the $\mathrm{Ar}^*$-formula $\widetilde{\Psi_i}(\overline{k_1}, \dots, \overline{k_m})$ is pr-realizable ($i=1, 2$). Then $\widetilde{\Psi }(x_1, \dots, x_n)$ is $\widetilde{\Psi_1}(x_1, \dots, x_n)\, \&\, \widetilde{\Psi_2}(x_1, \dots, x_n)$. The formula $\Psi(k_1, \dots, k_m)$ is true if and only if both formulas $\Psi_1(k_1, \dots, k_m)$ and $\Psi_2(k_1, \dots, k_m)$ are true. By the inductive assumption, this is possible if and only if both formulas $\widetilde{\Psi_1}(\overline{k_1}, \dots, \overline{k_m})$ and $\widetilde{\Psi_2}(\overline{k_1}, \dots, \overline{k_m})$ pr-realizable, that is, the formula $\widetilde{\Phi}(\overline{k_1}, \dots, \overline{k_m})$ is pr-realizable. 7) Suppose $\Psi(x_1, \dots, x_n)$ has the form $\Psi_1(x_1, \dots, x_n)\to\Psi_2(x_1, \dots, x_n)$ under the same conditions as in the previous paragraph. 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)$. Suppose the formula $\Psi(k_1, \dots, k_m)$ is true. This means that the formula $\Psi_1(k_1, \dots, k_m)$ is not true or $\Psi_2(k_1, \dots, k_m)$ is true. In the first case, by the induction assumption, the formula $\widetilde{\Psi_1}(\overline{k_1}, \dots, \overline{k_m})$ is not pr-realizable and by Proposition 1, the formula $\widetilde{\Psi}(\overline{k_1}, \dots, \overline{k_m})$ is pr-realizable. In the second case, by the induction assumption, the formula $\widetilde{\Psi_2}(\overline{k_1}, \dots, \overline{k_m})$ is pr-realizable and by Proposition 1 the formula $\widetilde{\Psi}(\overline{k_1}, \dots, \overline{k_m})$ is pr-realizable. Conversely, if the formula $\widetilde{\Psi}(\overline{k_1}, \dots, \overline{k_m})$ is pr-realizable, then $\Psi(k_1, \dots, k_m)$ must be true, because otherwise the formula $\Psi_1(k_1, \dots, k_m)$ is true, and the formula $\Psi_2(k_1, \dots, k_m)$ is not true, and by the induction assumption, $\widetilde{\Psi_1}(\overline{k_1}, \dots, \overline{k_m})$ is pr-realizable and $\widetilde{\Psi_2}(\overline{k_1}, \dots, \overline{k_m})$ is not pr-realizable, but this is impossible. This proves Proposition 12. Recall that $\{a\}$ is a function $n\mapsto\mathsf{pr}(a, n)$, and the predicate $\{x_1\}(x_2)=x_3$ is defined in $\mathfrak N$ by the $\mathrm{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 $\mathbf y$ is the list $y_1, \dots, y_m$ and $\Psi(\mathbf y, x_1, x_2, x_3)$ is a completely negative quantifier-free $\mathrm{Ar}$-formula. Proposition 13. Let $\mathbf\Phi$ be an interpretation of the formula $Q$. Then, for any natural numbers $e$, $n$, and $k$, the $\mathrm{Ar}^*$-formula $\widetilde{G}(\overline e, \overline n, \overline k)$ is pr-realizable if and only if $\{e\}(n)=k$. Proof. Suppose $\{e\}(n)=k$. Then the formula $G(e, n, k)$ is true. This means that there is a list of natural numbers $\mathbf b=b_1, \dots, b_m$ such that the quantifier-free $\mathrm{Ar}^*$-formula $\Psi(\mathbf b, e, n, k)$ is true. By Proposition 12, the formula $\widetilde{\Psi}(\overline{\mathbf b}, \overline e, \overline n, \overline k)$, where $\overline{\mathbf b}=\overline{b_1}, \dots, \overline{b_m}$, is pr-realizable. Then the formula $\exists\mathbf y\, \widetilde{\Psi}(y, \overline e, \overline n, \overline k)$, that is, $\widetilde{G}(\overline e, \overline n, \overline k)$, is pr-realizable.
Conversely, suppose the formula $\widetilde{G}(\overline e, \overline n, \overline k)$ is pr-realizable. Obviously, there exists a natural number $\ell$ such that $\{e\}(n)=\ell$. Hence the formula $G(e, n, \ell)$ is true. Reasoning as above, we conclude that the formula $\widetilde{G}(\overline e, \overline n, \overline\ell)$ is pr-realizable. Since the formula $\widetilde{A_{23}}$ is pr-realizable, it follows that the formula $\neg\neg\mathcal E(\overline \ell, \overline k)$ is pr-realizable. By the definition of the function $\mathsf f$, the formula $\widetilde{[k]}(\overline k)$ is pr-realizable. It follows from Proposition 7 that $\widetilde{[k]}(\overline\ell)$ is pr-realizable. On the other hand, the formula $\widetilde{[\ell]}(\overline\ell)$ is pr-realizable. Then by Proposition 11, $k=\ell$. Thus, we proved that $\{e\}(n)=k$. This proves Proposition 13. Recall that $H(x_1, x_2)$ is the formula $\exists z\, (\neg\neg Z(z)\, \&\, G(x_1, x_2, z))$. Proposition 14. Let $\mathbf\Phi$ be an interpretation of the formula $Q$. Then, for any natural numbers $e$ and $n$, the $\mathrm{Ar}^*$-formula $\widetilde{H}(\overline e, \overline n)$ is pr-realizable if and only if $\{e\}(n)=0$. Proof. Suppose $\{e\}(n)=0$. By Proposition 13, $\widetilde{G}(\overline e, \overline n, \overline0)$ is pr-realizable. On the other hand, $\neg\neg\mathcal Z(\overline0)$ is also pr-realizable. Hence the formula $\neg\neg\mathcal Z(\overline0)\, \&\, \widetilde{G} (\overline e, \overline n, \overline0)$ is pr-realizable. It follows that the formula $\exists z\, (\neg\neg\mathcal Z(z)\, \&\, \widetilde{G}(\overline e, \overline n, z))$, that is, $\widetilde{H}(\overline e, \overline n)$, is pr-realizable. Conversely, suppose the formula $\widetilde{H}(\overline e, \overline n)$ is pr-realizable. Then there exists a natural number $k$ such that the formulas $\neg\neg\mathcal Z(k)$, that is, $\widetilde{[0]}(k)$, and $\widetilde{G}(\overline e, \overline n, k)$ are pr-realizable. Since the formula $\widetilde{[0]}(\overline0)$ is also pr-realizable, it follows from Proposition 8 that the formula $\neg\neg\mathcal E(k, \overline0)$ is pr-realizable. Now by Proposition 7 the formula $\widetilde{G}(\overline e, \overline n, \overline0)$ is pr-realizable. By Proposition 13, $\{e\}(n)=0$. This proves Proposition 14. Suppose some interpretation $\mathbf{\Phi}$ of the formula $Q$ is fixed. A natural number $a$ is called $\mathbf{\Phi}$-standard if there exists a natural number $n$ such that the formula $\widetilde{[n]}(a)$ is pr-realizable. Note that the numbers $\overline0, \overline1, \dots$ are $\mathbf{\Phi}$-standard. Proposition 15. If a natural number $a$ is $\mathbf{\Phi}$-standard and $b$ is a natural number such that the $\mathrm{Ar}^*$-formula $\neg\neg\mathcal{S}(a, b)$ is pr-realizable, then the number $b$ is $\mathbf{\Phi}$-standard. Proof. Suppose the formula $\widetilde{[n]}(a)$ is pr-realizable. Since the predicate $\mathrm{Ar}$-formula $[n](x)$ is completely negative, it follows from Proposition 6 that there exists a number $d$, namely $a_{[n](x)}$, such that $d\, \mathbf{pr}\, \widetilde{[n]}(a)$. Let $b$ be a natural number such that the formula $\neg\neg\mathcal{S}(a, b)$ is pr-realizable. We prove that the formula $\widetilde{[n+1]}(b)$, that is, $\neg\mathcal Z(b)\, \&\, \forall y\, (\neg\neg\mathcal S(y, b) \to\widetilde{[n]}(y))$, is pr-realizable. Since the formula $\widetilde{A_{11}}$ is pr-realizable, it follows that the formula $\neg\mathcal Z(b)$ is pr-realizable. Let us prove that the formula
$$
\begin{equation}
\forall y\bigl(\neg\neg\mathcal S(y, b)\to\widetilde{[n]}(y)\bigr)
\end{equation}
\tag{7.10}
$$
is pr-realizable. First, we show that, for any $c$, if the formula $\neg\neg\mathcal S(c, b)$ is pr-realizable, then the formula $\widetilde{[n]}(c)$ is pr-realizable. Suppose the formula $\neg\neg\mathcal S(c, b)$ is pr-realizable. Since the formulas $\neg\neg\mathcal{S}(a, b)$, $\neg\neg\mathcal S(c, b)$, and $\widetilde{A_{10}}$ are pr-realizable, it follows that the formula $\neg\neg\mathcal E(a, c)$ is pr-realizable. Since the formula $\widetilde{[n]}(a)$ is pr-realizable, it follows from Proposition 7 that the formula $\widetilde{[n]}(c)$ is pr-realizable, as was to be proved. By Proposition 6, $d\, \mathbf{pr}\, \widetilde{[n]}(c)$. So, we proved that, for any $c$, if the formula $\neg\neg\mathcal S(c, b)$ is pr-realizable, then $d\, \mathbf{pr}\, \widetilde{[n]}(c)$. By Proposition 3, the number $\mathsf a_d^2$ pr-realizes formula (7.10). Thus, we proved that the formula $\widetilde{[n+1]}(b)$ is pr-realizable. This means that the number $b$ is $\mathbf{\Phi}$-standard. This proves Proposition 15. Recall that $x\leqslant y$ denotes the formula $\exists z\, \neg\neg A(z, x, y)$. Proposition 16. Let $\mathbf{\Phi}$ be an interpretation of the formula $Q$. Then, for any natural numbers $n$ and $b$ if $b$ is not $\mathbf{\Phi}$-standard, then the $\mathrm{Ar}^*$-formula $\overline n\mathbin{\widetilde{\leqslant}}b$ is pr-realizable. Proof. Induction on $n$. Let $n=0$. It follows from the pr-realizability of the formula $\widetilde{A_{16}}$ that the formula $\neg\neg\mathcal{Z}(\overline0)\to\neg\neg\mathcal{A}(b, \overline0, b)$ is pr-realizable. Since the formula $\neg\neg\mathcal{Z}(\overline0)$ is pr-realizable, it follows that the formula $\neg\neg\mathcal{A}(b, \overline0, b)$ is pr-realizable. Hence, the formula $\exists z\, \neg\neg\mathcal{A}(z, \overline0, b)$, that is, $\overline0\mathbin{\widetilde{\leqslant}}b$, is pr-realizable.
Now suppose that, for any natural number $b$ that is not $\mathbf{\Phi}$-standard, the formula $\overline n\mathbin{\widetilde{\leqslant}}b$ is pr-realizable. We have to prove that, for any such $b$, the formula $\overline{n+1}\mathbin{\widetilde{\leqslant}}b$ is pr-realizable. Since the number $b$ is not $\mathbf{\Phi}$-standard, it follows that the formula $\neg\neg\mathcal{Z}(b)$ is not pr-realizable. Since the formula $\widetilde{A_{12}}$ is pr-realizable, it follows that the formula $\exists y\, \neg\neg\mathcal{S}(y, b)$ is pr-realizable. This means the existence of a natural number $a$ such that the formula $\neg\neg\mathcal{S}(a, b)$ is pr-realizable. By Proposition 15, the number $a$ cannot be $\mathbf{\Phi}$-standard. By the induction assumption, the formula $\exists z\, \neg\neg\mathcal{A}(z, \overline n, a)$ is pr-realizable. This means the existence of a natural number $c$ such that the formula $\neg\neg\mathcal{A}(c, \overline n, a)$ is pr-realizable. Since the formula $\neg\neg S(n, n+1)$ is true, it follows from Proposition 12 that the formula $\neg\neg\mathcal S(\overline n, \overline{n+1})$ is pr-realizable. Since the formula $\widetilde{A_{17}}$ is pr-realizable, it follows that the formula $\neg\neg{\mathcal A}(c, \overline{n+1}, b)$ is pr-realizable. Hence the formula $\exists z\, \neg\neg\mathcal{A}(z, \overline{n+1}, b)$, that is, $\overline{n+1}\mathbin{\widetilde{\leqslant}}b$, is pr-realizable. This proves Proposition 16. § 8. The main resultTheorem 2. If $\mathbf\Phi$ is an interpretation of the formula $Q$, then every natural number is $\mathbf\Phi$-standard. Proof. Let $\mathbf\Phi$ be an interpretation of the formula $Q$. Then $\widetilde{A_{25}}$ is pr-realizable. This means the existence of a primitive recursive function $g(a, x, y)$ such that, for any $a$, $k$, $\ell$, if $a\, \mathbf{pr}\, \top$, that is, $a=0$, then $g(a, k, \ell)\, \mathbf{pr}\, (\neg\widetilde B(k, \ell)\lor \neg\neg\widetilde B(k, \ell))$, that is, if $[g(0, k, \ell)]_0=0$, then $\neg\neg\widetilde B(k, \ell)$ is pr-realizable, and otherwise $\neg\neg\tilde B(k, \ell)$ is pr-realizable. Consider the one-place function $h(n)=\mathsf{sg}([g(0, n, \mathsf f(n))]_0)$. We prove that the function $h$ has the following property: Suppose the formula $\neg\widetilde B(n, \overline n)$ is pr-realizable. Then $[g(0, k, \overline n)]_0=0$. Recall that $\overline n=\mathsf f(n)$. Thus, we have $h(n)=\mathsf{sg}([g(0, n, \mathsf f(n))]_0)=0$. If the formula $\neg\widetilde B(n, \overline n)$ is not pr-realizable, then $[g(0, k, \overline n)]_0\ne 0$ and $h(n)=\mathsf{sg}([g(0, n, \mathsf f(n))]_0)=1$. Obviously, the function $h$ is primitive recursive. Therefore, there exists a natural number $e$ such that $h(n)=\{e\}(n)$ for all $n$.
Since $\mathbf\Phi$ is an interpretation of the formula $Q$, it follows that the formula $\widetilde{A_{24}}$, that is,
$$
\begin{equation}
\forall y, z\, \neg\neg\exists v\, \forall x\big(x\mathbin{\widetilde{\leqslant}}z \to(\neg\neg\widetilde{B}(v, x)\equiv\neg\neg\widetilde{H}(y, x)) \bigr),
\end{equation}
\tag{8.1}
$$
is pr-realizable. Suppose that there is a natural number $b$ which is not $\mathbf\Phi$-standard. Since formula (8.1) is pr-realizable, it follows that the formula
$$
\begin{equation}
\neg\neg\exists v\, \forall x\bigr(x\mathbin{\widetilde{\leqslant}}b\to (\neg\neg\widetilde{B}(v, x)\equiv \neg\neg\widetilde{H}(\overline e, x))\bigr)
\end{equation}
\tag{8.2}
$$
is pr-realizable. Now suppose that the formula
$$
\begin{equation}
\exists v\, \forall x \bigl(x\mathbin{\widetilde{\leqslant}}b\to (\neg\neg\widetilde{B}(v, x)\equiv \neg\neg\widetilde{H}(\overline e, x))\bigr)
\end{equation}
\tag{8.3}
$$
is pr-realizable. Then there exists a natural number $a$ such that the formula
$$
\begin{equation*}
\forall x \bigl(x\mathbin{\widetilde{\leqslant}}b\to(\neg\neg\widetilde{B}(a, x) \equiv \neg\neg\widetilde{H}(\overline e, x))\bigr)
\end{equation*}
\notag
$$
is pr-realizable. It follows that, for any $n$, the formula
$$
\begin{equation*}
\overline n\mathbin{\widetilde{\leqslant}}b\to \bigl(\neg\neg\widetilde{B}(a, \overline n)\equiv \neg\neg\widetilde{H}(\overline e, \overline n)\bigr)
\end{equation*}
\notag
$$
is pr-realizable. By Proposition 16, the formula $\overline n\mathbin{\widetilde{\leqslant}}b$ is pr-realizable. Then, for any $n$, the formula $\neg\neg\widetilde{B}(a, \overline n)\equiv \neg\neg\widetilde{H}(\overline e, \overline n)$ is pr-realizable. Thus for any $n$, we have:
(a) the formula $\neg\neg\widetilde{B}(a, \overline n)$ is pr-realizable if and only if the formula $\neg\neg\widetilde{H}(\overline e, \overline n)$ is pr-realizable. On the other hand, by Proposition 14, for any $n$, (b) the formula $\neg\neg\widetilde{H}(\overline e, \overline n)$ is pr-realizable if and only if $h(n)=0$. Further, by the property of the function $h$ we have: (c) $h(n)=0$ if and only if the formula $\neg\widetilde{B}(n, \overline n)$ is pr-realizable. It follows from the statements (a), (b), and (c) that for the given number $a$ and any natural number $n$, the following equivalence holds: the formula $\neg\neg\widetilde{B}(a, \overline n)$ is pr-realizable if and only if the formula $\neg\widetilde{B}(n, \overline n)$ is pr-realizable, and we get a contradiction if $n=a$. This contradiction means that formula (8.3) is not pr-realizable. Then its negation is pr-realizable contrary to the pr-realizability of formula (8.2). Thus, we proved that there is no natural number that is not $\mathbf\Phi$-standard. Theorem 2 is proved. Proposition 17. Suppose $\mathbf{\Phi}$ is an interpretation of $Q$, and a pr-realization $e$ of the formula $\widetilde{Q}$ is given. Then, for any natural number $k$, we can effectively find a natural number $n$ such that the formula $\widetilde{[n]}(k)$ is pr-realizable. Proof. Let $\mathbf{\Phi}$ be an interpretation of the formula $Q$, and $e$ be a pr-realization of the formula $\widetilde{Q}$. Suppose a natural number $k$ is given. By Proposition 9, for any natural number $n$ it is possible to effectively check whether the formula $\widetilde{[n]}(k)$ is pr-realizable. Sequentially iterating over the natural numbers starting from $0$, we find $n$ such that the formula $\widetilde{[n]}(k)$ is pr-realizable, since otherwise the number $k$ would not be $\mathbf\Phi$-standard contrary to Theorem 2. This proves Proposition 17. Proposition 18. Let $\mathbf{\Phi}$ be an interpretation of the formula $Q$. Then, for any completely negative $\mathrm{Ar}$-formula $\Phi(x_1, \dots, x_n)$ that does not contain free variables except $x_1, \dots, x_n$, and any natural numbers $k_1, \dots, k_n$, the $\mathrm{Ar}^*$-formula $\Phi(k_1, \dots, k_n)$ is true if and only if the $\mathrm{Ar}^*$-formula $\widetilde{\Phi}(\overline{k_1}, \dots, \overline{k_n})$ is pr-realizable. Proof. Induction on the construction of an $\mathrm{Ar}$-formula $\Phi(x_1, \dots, x_n)$.
The case of an atomic formula $\Phi(x_1, \dots, x_n)$ is considered in Proposition 12. The proof of Proposition 12 also contains an analysis of the case when the formula $\Phi$ has the form $\Psi_1\, \&\, \Psi_2$ and the statement holds for the formulas $\Psi_1$ and $\Psi_2$. Suppose $\Phi(x_1, \dots, x_n)$ is $\forall\mathbf y\, (\Psi_1(\mathbf y, x_1, \dots, x_n)\to \Psi_2(\mathbf y, x_1, \dots, x_n))$, where $\mathbf y$ is the list $y_1, \dots, y_m$, and $\Psi_1(\mathbf y, x_1, \dots, x_n)$ and $\Psi_2(\mathbf y, x_1, \dots, x_n)$ are completely negative $\mathrm{Ar}$-formulas. The induction assumption is that, for any $\mathbf p, k_1, \dots, k_n$, where $\mathbf p=p_1, \dots, p_m$, the formula $\Psi_i(\mathbf p, k_1, \dots, k_n)$ ($i=1, 2$) is true if and only if the formula $\widetilde{\Psi_i}(\overline{\mathbf p}, \overline{k_1}, \dots, \overline{k_n})$, where $\overline{\mathbf p}=\overline{p_1}, \dots, \overline{p_m}$, is pr-realizable. $\widetilde{\Phi}(x_1, \dots, x_n)$ is $\forall\mathbf y\, (\widetilde{\Psi_1}(\mathbf y, x_1, \dots, x_n)\to \widetilde{\Psi_2}(\mathbf y, x_1, \dots, x_n))$. Suppose the formula $\Phi(k_1, \dots, k_n)$ is true. Hence, for any suitable list of natural numbers $\mathbf p$, the formula
$$
\begin{equation}
\Psi_1(\mathbf p, k_1, \dots, k_n)\to\Psi_2(\mathbf p, k_1, \dots, k_n)
\end{equation}
\tag{8.4}
$$
is true. We prove that the formula $\widetilde{\Phi}(\overline{k_1}, \ldots, \overline{k_n})$, that is,
$$
\begin{equation*}
\forall\mathbf y\bigl(\widetilde{\Psi_1} (\mathbf y, \overline{k_1}, \dots, \overline{k_n})\to \widetilde{\Psi_2}(\mathbf y, \overline{k_1}, \dots, \overline{k_n})\bigr),
\end{equation*}
\notag
$$
is pr-realizable. First, we prove that, for any list $\mathbf l=\ell_1, \dots, \ell_m$, if the formula $\widetilde{\Psi_1}(\mathbf l, \overline{k_1}, \dots, \overline{k_n})$ is pr-realizable, then the formula $\widetilde{\Psi_2}(\mathbf l, \overline{k_1}, \dots, \overline{k_n})$ is pr-realizable. Let $\mathbf l$ be a list of natural numbers such that $\widetilde{\Psi_1}(\mathbf l, \overline{k_1}, \dots, \overline{k_n})$ is pr-realizable. By Theorem 2 the numbers in the list $\mathbf l$ are $\mathbf{\Phi}$-standard. This means the existence of natural numbers $p_1, \dots, p_m$ such that the formulas $\widetilde{[p_i]}(\ell_i)$ ($i=1, \dots, m$) are pr-realizable. (Moreover, by Proposition 17, $p_1, \dots, p_m$ can be found effectively.) It follows from Proposition 8, that the formulas $\neg\neg\mathcal{E}(\overline{p_i}, \ell_i)$ are pr-realizable. Since the formula $\widetilde{\Psi_1}(\mathbf l, k_1, \dots, k_n)$ is pr-realizable, it follows from Proposition 7 that the formula $\widetilde{\Psi_1}(\overline{\mathbf p}, \overline{k_1}, \dots, \overline{k_n})$, where $\overline{\mathbf p}$ is the list $\overline{p_1}, \dots, \overline{p_m}$, is pr-realizable. By the induction assumption, the formula $\Psi_1(\mathbf p, k_1, \dots, k_n)$ is true. Since formula (8.4), is true, it follows that the formula $\Psi_2(\mathbf p, k_1, \dots, k_n)$ is true. By the induction assumption, $\widetilde{\Psi_2}(\overline{\mathbf p}, \overline{k_1}, \dots, \overline{k_n})$ pr-realizable. Since the formulas $\neg\neg\mathcal{E}(\overline{p_i}, \ell_i)$ and $\widetilde{A_2}$ are pr-realizable, it follows that the formulas $\neg\neg\mathcal{E}(\ell_i, \overline{p_i})$ are pr-realizable. Now it follows from Proposition 7 that the formula $\widetilde{\Psi_2}(\mathbf l, \overline{k_1}, \dots, \overline{k_n})$ is pr-realizable, as was to be proved. By Proposition 6, $a_{\Psi_2}\, \mathbf{pr}\, \widetilde{\Psi_2} (\mathbf l, \overline{k_1}, \dots, \overline{k_n})$. So, we proved that, for any list of natural numbers $\mathbf l=\ell_1, \dots, \ell_m$, if the formula $\widetilde{\Psi_1}(\mathbf l, \overline{k_1}, \dots, \overline{k_n})$ is pr-realizable, then $a_{\Psi_2}\, \mathbf{pr}\, \widetilde{\Psi_2} (\mathbf l, \overline{k_1}, \dots, \overline{k_n})$. By Proposition 3, the number $\mathsf a_{a_{\Psi_2}}^{m+1}$ pr-realizes the formula $\widetilde{\Phi}(\overline{k_1}, \dots, \overline{k_n})$.
Conversely, suppose the formula $\widetilde{\Phi}(\overline{k_1}, \dots, \overline{k_n})$ is pr-realizable. It follows, in particular, that, for any list of natural numbers $\mathbf l$, if the formula $\widetilde{\Psi_1}(\mathbf l, \overline{k_1}, \dots, \overline{k_n})$ is pr-realizable, then the formula $\widetilde{\Psi_2}(\mathbf l, \overline{k_1}, \dots, \overline{k_n})$ is pr-realizable. We prove that the formula $\Phi(k_1, \dots, k_n)$ is true, that is, for any list of natural numbers $\mathbf p$, if the formula $\Psi_1(\mathbf p, k_1, \dots, k_n)$ is true, then so is the formula $\Psi_2(\mathbf p, k_1, \dots, k_n)$. Let $\mathbf p$ be a list of natural numbers such that the formula $\Psi_1(\mathbf p, k_1, \dots, k_n)$ is true. By the induction assumption, the formula $\widetilde{\Psi_1}(\overline{\mathbf p}, \overline{k_1}, \dots, \overline{k_n})$ is pr-realizable. As noted above, in this case, the formula $\widetilde{\Psi_2}(\overline{\mathbf p}, \overline{k_1}, \dots, \overline{k_n})$ is pr-realizable. By the induction assumption, this formula is true, as was to be proved. This proves Proposition 18. Theorem 3. For any closed completely negative $\mathrm{Ar}$-formula $\Psi$, it is possible to effectively construct a closed predicate formula $\Psi^*$ which is pr-realizable if and only if $\Psi$ is true. Proof. If $\Psi$ is a closed completely negative $\mathrm{Ar}$-formula, then as $\Psi^*$ we take the predicate $\mathrm{Ar}$-formula $Q\to\Psi$. We show that $\Psi^*$ is the required formula.
Lemma 1. If the predicate formula $\Psi^*$ is pr-realizable, then the $\mathrm{Ar}$-formula $\Psi$ is true. Proof. Suppose $\Psi^*$ is pr-realizable. This means that, for any list of $\mathrm{Ar}$-formulas $\mathbf\Phi$ admissible for substitution in $\Psi^*$, the formula $\widetilde{\Psi^*}$ is pr-realizable. In particular, this holds when $\mathbf\Phi$ is the list of formulas $S(x, y)$, $A(x, y, z)$, $M(x, y, z)$, $Z(x)$, $E(x, y)$. In this case, $\widetilde{\Psi^*}$ is exactly the formula $Q\to\Psi$. By Theorem 1, the formula $Q$ is pr-realizable. Then the formula $\Psi$ is also pr-realizable. Since $\Psi$ is a completely negative formula, it follows from Proposition 4 that $\Psi$ is true, as was to be proved. Lemma 1 is proved. Lemma 2. If a closed completely negative $\mathrm{Ar}$-formula $\Psi$ is true, then the predicate formula $\Psi^*$ is pr-realizable. Proof. Suppose a closed completely negative $\mathrm{Ar}$-formula $\Psi$ is true. We prove that the predicate formula $\Psi^*$ is pr-realizable. Let $\mathbf{\Phi}$ be a list of $\mathrm{Ar}$-formulas admissible for substitution in $\Psi^*$. Since $\Psi$ is completely negative, Proposition 6 implies the existence of a number $a_{\Psi}$ such that the formula $\widetilde{\Psi}$ is pr-realizable if and only if $a_{\Psi}\, \mathbf{pr}\, \widetilde{\Psi}$. Let us prove that $\mathsf a_{a_{\Psi}}^1\, \mathbf{pr}\, \widetilde{\Psi^*}$. By the definition of pr-realizability, it is sufficient to prove that, for any $b$, if $b\, \mathbf{pr}\, \widetilde Q$, then $a_{\Psi}\, \mathbf{pr}\, \widetilde{\Psi}$. Suppose $b\, \mathbf{pr}\, \widetilde Q$. This means that $\mathbf\Phi$ is an interpretation of the formula $Q$. By Proposition 18, the formula $\widetilde{\Psi}$ is pr-realizable since the formula $\Psi$ is true. As noted above, in this case $a_{\Psi}\, \mathbf{pr}\, \widetilde{\Psi}$, as was to be proved. Lemma 2 is proved. Now Theorem 3 follows from Lemmas 1 and 2. Proof. It is obvious that the set of all true completely negative closed $\mathrm{Ar}$-formulas is recursively isomorphic to the set of all true closed $\mathrm{Ar}$-formulas, which is not arithmetical by the Tarski theorem. It follows that the set of all true completely negative closed $\mathrm{Ar}$-formulas is also not arithmetical. By Theorem 3 the set of all true completely negative closed $\mathrm{Ar}$-formulas is 1-1-reducible to the set of all pr-predicate formulas. It follows that the set of all pr-realizable predicate formulas is not arithmetical. Theorem 4 is proved.
§ 9. ConclusionsTheorem 4 gives a lower bound on the complexity of the predicate logic of primitive recursive realizability. A natural question arises about the upper bound. In this regard, it is appropriate to recall the solution of this question for the predicate logic of recursive realizability by Kleene. In the author’s paper [19], for a wide class of arithmetical theories $T$, a general theorem was proved that the predicate logic of such a theory is $\Pi_1^T$-complete. It follows from this result that the predicate logic of recursive realizability is in the class $\Pi^0_{\omega+1}$ of the hyperarithmetical hierarchy and is complete in this class. It can be expected that a similar result is true for the predicate logic of primitive recursive realizability. The direct application of this general theorem is impossible because it refers to theories for which intuitionistic logic is correct, and for primitive recursive realizability, the correctness of intuitionistic logic does not hold. However, it seems quite promising to adapt the known methods of dealing with predicate logics of constructive arithmetic theories to the problem of primitive recursive realizability. 
Citation in format AMSBIB
\Bibitem{Pli23} |
|
||||||||||||||||||||||||||
|
Contact us: |
Terms of Use
|
Registration to the website |
Logotypes |
|