| Известия Российской академии наук. Серия математическая |
|
|
|
|
|
Неарифметичность предикатной логики примитивно рекурсивной реализуемости В. Е. Плиско Московский государственный университет имени М. В. Ломоносова, механико-математический факультет
Англоязычная версия:
Izvestiya: Mathematics, 2023, Volume 87, Issue 2, Pages DOI: https://doi.org/10.4213/im9288e 
Реферативные базы данных:
    § 1. ВведениеРекурсивная реализуемость, введенная С. К. Клини [1] (см. также [2; § 82]), может рассматриваться как истолкование неформального интуиционистского смысла арифметических суждений на основе теории рекурсивных функций. Основная идея рекурсивной реализуемости состоит в том, чтобы заменить расплывчатую интуиционистскую концепцию эффективной операции точным понятием частично рекурсивной функции. В математике изучаются многие другие более ограниченные классы вычислимых функций. Представляет интерес рассмотрение вариантов реализуемости на основе субрекурсивных классов функций. Одним из них является класс примитивно рекурсивных функций. Понятие примитивно рекурсивной реализуемости, аналогичное рекурсивной реализуемости Клини, но отличающееся от нее тем, что вместо класса всех частично рекурсивных функций рассматриваются только примитивно рекурсивные функции, было введено С. Салехи [3], [4]. Принципиальное различие этих двух интерпретаций обусловлено тем, что для класса частично рекурсивных функций имеется универсальная функция из этого же класса, а для примитивно рекурсивных функций такой функции нет. В частности поэтому отсутствует корректность интуиционистской логики относительно примитивно рекурсивной реализуемости. Оказалось, однако, что эта интерпретация согласуется с так называемой базисной логикой, пропозициональный вариант которой был введен А. Виссером [5], а предикатный – В. Руйтенбургом [6]. На основе базисной логики предикатов строится базисная арифметика $\mathsf{BA}$. Салехи доказал корректность $\mathsf{BA}$ относительно своего варианта примитивно рекурсивной реализуемости. Примитивно рекурсивную реализуемость можно рассматривать как своего рода конструктивную семантику арифметических суждений. Для любой семантики представляет интерес изучение соответствующей логики. Автором рассматривалась предикатная логика рекурсивной реализуемости Клини. Было доказано [7], что множество рекурсивно реализуемых предикатных формул не является арифметическим. Аналогичный результат для примитивно рекурсивной реализуемости Салехи был получен в диссертации Д. A. Витера [8]. Его технически довольно сложное доказательство, основанное на результатах об арифметической сложности предикатных логик конструктивных арифметических теорий [9] и предложенном М. Ардеширом [10] переводе интуиционистской логики предикатов в базисную, не было опубликовано в широкой печати (имеется только депонированная рукопись [11]). Цель настоящей статьи – представить несколько упрощенное доказательство этого результата посредством прямого применения методов, используемых в [7] для изучения предикатной логики рекурсивной реализуемости. Несколько ранее З. Дамняновичем [12] было введено другое понятие примитивно рекурсивной реализуемости, называемое строго примитивно рекурсивной реализуемостью и сочетающее в себе идеи рекурсивной реализуемости и моделей Крипке. Эти два варианта примитивно рекурсивной реализуемости (по Дамняновичу и по Салехи) существенно различны (см. [13]): существует арифметическая формула, которая является примитивно рекурсивно реализуемой в смысле [3], но не является строго примитивно рекурсивно реализуемой в смысле [12], в то время как ее отрицание строго примитивно рекурсивно реализуемо, но не примитивно рекурсивно реализуемо. В диссертации Б. Х. Пака [14] (см. также [15]) приводится доказательство неарифметичности предикатной логики строго примитивной рекурсивной реализуемости, существенно опирающееся на утверждение, что каждая формула, выводимая в интуиционистском исчислении предикатов, строго примитивно рекурсивно реализуема (см. [12; лемма 4.3, теорема 5.1]). Позже это утверждение было опровергнуто (см. [16]). Тем не менее, результат Пака остается в силе. Правильное доказательство этого результата представлено в работе автора [17]. Доказательство по своей идее во многом аналогично тому, что приводится в настоящей работе при исследовании предикатной логики примитивно рекурсивной реализуемости, но эти доказательства отличаются технически ввиду различия двух вариантов реализуемости. § 2. Нумерация примитивно рекурсивных функцийПримитивно рекурсивные функции получаются с помощью операций подстановки и рекурсии из исходных функций
$$
\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
$$
Для удобства добавим к исходным функциям постоянные функции
$$
\begin{equation*}
\varphi(x_1,\dots, x_n)=q\quad (n=1,2,\dots,\ q=0,1,\dots).
\end{equation*}
\notag
$$
Если $a_0,\dots,a_n$ – натуральные числа, то через $\langle a_0,\dots,a_n\rangle$ будем обозначать число $p_0^{a_0}\cdots p_n^{a_n}$, где $p_0,\dots,p_n$ суть последовательные простые числа ($p_0=2$, $p_1=3$, $p_2 =5$, $\dots$). Известно, что функции $i\mapsto p_i$ и $(x,y)\mapsto\langle x,y\rangle$ являются примитивно рекурсивными. В дальнейшем, если $a\geqslant1$, $i\geqslant0$, то через $[a]_i$ обозначается показатель, с которым $p_i$ входит в представление числа $a$ в виде произведения степеней простых чисел. Таким образом, $[a]_i = a_i$, если $a=\langle a_0,\dots,a_n\rangle$. Для определенности положим $[0]_i =0$ для всех $i$. Заметим, что функция $(x,i)\mapsto[x]_i$ примитивно рекурсивна. Один способ нумерации примитивно рекурсивных функций описан в работе [18]. Ниже перечисляются возможные схемы определения функции $\varphi$ и справа указывается ее номер:
$$
\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{где }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
$$
Здесь $\mathbf x$ – список $x_1,\dots,x_n$, а $g$, $h_1,\dots,h_k$, $h$ – номера функций $\psi$, $\chi_1,\dots,\chi_k$, $\chi$ соответственно. Пусть $\operatorname{In}(b)$ означает, что $b$ является номером примитивно рекурсивной функции. В работе [18] показано, что $\operatorname{In}(b)$ – примитивно рекурсивный предикат. Если имеет место $\operatorname{In}(b)$, то $\mathsf{pr}_b$ будет обозначать $[b]_1$-местную функцию с номером $b$. Затем положим
$$
\begin{equation*}
\mathsf{pr}(b,a)= \begin{cases} \mathsf{pr}_b([a]_0,\dots,[a]_{[b]_1-1}), &\text{если }\operatorname{In}(b), \\ 0 & \text{в противном случае}. \end{cases}
\end{equation*}
\notag
$$
Функция $\mathsf{pr}$ является универсальной для класса всех примитивно рекурсивных функций и не принадлежит этому классу. Заметим, что если дан номер $b$ функции $\varphi(\mathbf x)$, то для любого $\mathbf m$ можно вычислить значение $\varphi(\mathbf m)$. Действительно, вычисление значения $\varphi(\mathbf x)$ сводится к вычислению значений конечного числа функций, номера которых меньше, чем $b$. Поэтому процесс вычисления должен завершиться. Если $k$ – натуральное число, положим $\Lambda x.k=\langle 2,1,k\rangle$. Таким образом, $\Lambda x.k$ есть номер одноместной функции $x\mapsto k$. § 3. Примитивно рекурсивно реализуемые арифметические формулыБудем рассматривать арифметические утверждения в чисто предикатном варианте языка базисной арифметики. А именно, язык $\mathrm{Ar}$ – это элементарный язык без функциональных символов и предметных констант, сигнатура которого состоит из одноместного предикатного символа $Z$, бинарных предикатных символов $E$ и $S$, а также трехместных предикатных символов $A$ и $M$. В стандартной модели арифметики $\mathfrak N$ эти предикатные символы имеют следующий смысл: $Z(x)$ означает $x=0$, $E(x,y)$ означает $x=y$, $S(x,y)$ означает $x+1=y$, $A(x,y,z)$ означает $x+y=z$, $M(x,y,z)$ означает $x\cdot y=z$. Наряду с языком $\mathrm{Ar}$ рассмотрим расширенный язык арифметики $\mathrm{Ar}^*$, полученный добавлением к языку $\mathrm{Ar}$ предметных констант $0,1,\dots$ для всех натуральных чисел. Для удобства введем в эти языки логические константы $\top$ и $\bot$. Термы и атомарные формулы определяются обычным образом. Заметим, что $\top$ и $\bot$ считаются атомарными формулами. $\mathrm{Ar}$- и $\mathrm{Ar}^*$-формулы строятся из атомарных формул с использованием связок $\&$, $\lor$, $\to$ и кванторных символов $\forall$, $\exists$ по следующим правилам:
Если список предметных переменных $\mathbf x$ в формуле $\forall\mathbf x\, (\Phi\to\Psi)$ пуст, то мы будем опускать кванторный символ $\forall$ и писать просто $(\Phi\to\Psi)$. Выражение $\Phi\equiv\Psi$ будет сокращением для формулы $(\Phi\to\Psi)\,\&\,(\Psi\to\Phi)$. Формула $\Phi\to\bot$ будет обозначаться как $\neg\Phi$. Если формула $\Phi$ не содержит свободных переменных, отличных от $x_1,\dots,x_n$, будем обозначать эту формулу как $\Phi(x_1,\dots,x_n)$. В этом случае через $\Phi(k_1,\dots,k_n)$ обозначается $\mathrm{Ar}^*$-формула, полученная подстановкой в $\Phi$ констант $k_1,\dots,k_n$ вместо $x_1,\dots,x_n$ соответственно. Для краткости иногда будем писать $\exists\mathbf x$ вместо $\exists x_1\dots\exists x_n$, где $\mathbf x$ – список переменных $x_1,\dots,x_n$. Будем говорить, что замкнутая $\mathrm{Ar}^*$-формула $\Phi$ истинна, если $\mathfrak N\models\Phi$ в обычном классическом смысле. В этом случае формула $\forall\mathbf x\, (\Phi\to\Psi)$, где $\mathbf x$ есть список $x_1,\dots,x_n$, имеет тот же смысл, что и формула $\forall x_1\dots\forall x_n\, (\Phi\to\Psi)$ обычного языка арифметики. Заметим, что атомарная формула $\top$ истинна, а $\bot$ не истинна. Понятие примитивно рекурсивной реализуемости для арифметических формул введено С. Салехи [3], [4]. Отношение “натуральное число $e$ примитивно рекурсивно реализует замкнутую $\mathrm{Ar}^*$-формулу $\Phi$” ($e\,\mathbf{pr}\,\Phi$) определяется индукцией по числу логических символов в $\Phi$. 1) Если $\Phi$ – атомарная формула, то $e\,\mathbf{pr}\,\Phi$ означает, что $e=0$ и $\Phi$ истинна. 2) Если $\Phi$ есть $(\Psi_1\,\&\,\Psi_2)$, то $e\,\mathbf{pr}\,\Phi$ означает, что $[e]_0\,\mathbf{pr}\,\Psi_1$ и $[e]_1\,\mathbf{pr}\,\Psi_2$. 3) Если $\Phi$ есть $(\Psi_1\lor\Psi_2)$, то $e\,\mathbf{pr}\,\Phi$ означает, что либо $[e]_0=0$ и $[e]_1\,\mathbf{pr}\,\Psi_1$, либо $[e]_0\ne 0$ и $[e]_1\,\mathbf{pr}\,\Psi_2$. 4) Если $\Phi$ есть $\exists x\, \Psi(x)$, то $e\,\mathbf{pr}\,\Phi$ означает, что $[e]_1\,\mathbf{pr}\,\Psi([e]_0)$. 5) Если $\Phi$ есть $\forall\mathbf x\, (\Psi_1(\mathbf x)\to\Psi_2(\mathbf x))$, то $e\,\mathbf{pr}\,\Phi$ означает, что имеет место $\operatorname{In}(e)$ и для любых $b$, $\mathbf m$, если $b\,\mathbf{pr}\,\Psi_1(\mathbf m)$, то $\mathsf{pr}(e,\langle b,\mathbf m\rangle)\,\mathbf{pr}\,\Psi_2(\mathbf m)$. Здесь $\mathbf m$ есть список натуральных чисел той же длины, что и список $\mathbf x$. Замкнутая $\mathrm{Ar}^*$-формула $\Phi$ называется примитивно рекурсивно реализуемой ( pr-реализуемой), если существует такое $e$, что $e\,\mathbf{pr}\,\Phi$. Поскольку всякая замкнутая $\mathrm{Ar}$-формула является также замкнутой $\mathrm{Ar}^*$-формулой, понятие примитивно рекурсивной реализуемости определено и для замкнутых $\mathrm{Ar}$-формул. Очевидно, что формула вида $(\Phi\,\&\,\Psi)$ pr-реализуема тогда и только тогда, когда pr-реализуемы обе формулы $\Phi$ и $\Psi$, а формула $(\Phi\lor\Psi)$ pr-реализуема тогда и только тогда, когда pr-реализуема хотя бы одна из формул $\Phi$ и $\Psi$. Пусть $\mathsf a_k^n$ ($k=0,1,\dots$, $n=1,2,\dots$) обозначает число $\langle2,n,k\rangle$. Таким образом, $\mathsf a_k^n$ – это номер $n$-местной функции $(x_1,\dots,x_n)\mapsto k$. Положим $\mathsf a=\mathsf a_0^1$. Следующие свойства pr-реализуемости вытекают непосредственно из определения. Предложение 1. Каковы бы ни были замкнутые $\mathrm{Ar}^*$-формулы $\Phi$ и $\Psi$: 1) если $\Phi$ pr-реализуема, а $\Psi$ не pr-реализуема, то формула $(\Phi\to\Psi)$ не pr-реализуема; 2) если $k\,\mathbf{pr}\,\Psi$, то $\mathsf a_k^1\,\mathbf{pr}\,(\Phi\to\Psi)$; 3) если $\Phi$ не pr-реализуема, то $\mathsf a_k^1\,\mathbf{pr}\,(\Phi\to\Psi)$, каково бы ни было $k$; 4) если формула $\neg\Phi$ pr-реализуема, то $\mathsf a\,\mathbf{pr}\,\neg\Phi$. Доказательство. Утверждение 1) очевидно.
2) Пусть $k\,\mathbf{pr}\,\Psi$. Докажем, что $\mathsf a_k^1\,\mathbf{pr}\,(\Phi\to\Psi)$, т. е. что a) имеет место $\operatorname{In}(\mathsf a_k^1)$ и b) каково бы ни было $a$, если $a\,\mathbf{pr}\,\Phi$, то $\mathsf{pr}(\mathsf a_k^1,\langle a\rangle)\,\mathbf{pr}\,\Psi$. Напомним, что $\mathsf a_k^1$ – это номер одноместной функции $x\mapsto k$, так что условие a) выполнено. Условие b) также очевидно, поскольку для любого $a$ имеем $\mathsf{pr}(\mathsf a_k^1,\langle a\rangle)=k$, а $k\,\mathbf{pr}\,\Psi$. 3) Пусть $\Phi$ не pr-реализуема. Это означает, что для любого $a$ условие $a\,\mathbf{pr}\,\Phi$ не выполнено. Мы должны доказать, что $\mathsf a_k^1\,\mathbf{pr}\,(\Phi\to\bot)$. Выше уже отмечалось, что имеет место $\operatorname{In}(\mathsf a_k^1)$. Поэтому достаточно проверить, что для любого $a$ выполняется $a\,\mathbf{pr}\,\Phi\Rightarrow\mathsf{pr}(\mathsf a_k^1,\langle a\rangle)\,\mathbf{pr}\,\bot$, но это очевидно ввиду ложности посылки. Утверждение 4) следует из 5), поскольку $\Phi$ не pr-реализуема, если формула $\neg\Phi$ pr-реализуема. Предложение 1 доказано. Предложение 2. Пусть $\Psi(\mathbf x)$ – некоторая $\mathrm{Ar}^*$-формула, где $\mathbf x$ – список (возможно, пустой) различных предметных переменных $x_1,\dots,x_n$. Предположим, что для любого списка натуральных чисел $\mathbf l=\ell_1,\dots,\ell_n$ $\mathrm{Ar}^*$-формула $\Psi(\mathbf l)$ не pr-реализуема. Тогда формула $\forall\mathbf x\, \neg\Psi(\mathbf x)$ pr-реализуема. Доказательство. Докажем, что $\mathsf a_0^{n+1}\,\mathbf{pr}\,\forall\mathbf x\, (\Psi(\mathbf x)\to\bot)$. Последнее означает, что
a) имеет место $\operatorname{In}(\mathsf a_0^{n+1})$ и b) $a\,\mathbf{pr}\,\Psi(\mathbf l)\Rightarrow\mathsf{pr}(\mathsf a_0^{n+1},\langle a,\mathbf l\rangle)\,\mathbf{pr}\,\bot$ для любого натурального числа $a$ и любого списка натуральных чисел $\mathbf l=\ell_1,\dots,\ell_n$. Условие a) очевидно. Условие b) также выполняется ввиду ложности посылки. Предложение 2 доказано. Следующая конструкция будет часто использоваться в дальнейшем. Предложение 3. Пусть $\forall\mathbf x\, (\Phi(\mathbf x)\to\Psi(\mathbf x))$ – некоторая $\mathrm{Ar}^*$-формула, где $\mathbf x$ – список (возможно пустой) различных предметных переменных $x_1,\dots,x_n$. Предположим, что существует такое натуральное число $k$, что каков бы ни был список натуральных чисел $\mathbf l=\ell_1,\dots,\ell_n$, если формула $\Phi(\mathbf l)$ pr-реализуема, то $k\,\mathbf{pr}\,\Psi(\mathbf l)$. Тогда $\mathsf a_k^{n+1}\,\mathbf{pr}\,\forall\mathbf x\, (\Phi(\mathbf x)\to\Psi(\mathbf x))$. Доказательство. Мы должны доказать, что для любого списка натуральных чисел $\mathbf l=\ell_1,\dots,\ell_n$ и любого $a$, если $a\,\mathbf{pr}\,\Phi(\mathbf l)$, то число $\mathsf{pr}(\mathsf a_k^{n+1},\langle a,\mathbf l\rangle)$, т. е. $k$, pr-реализует формулу $\Psi(\mathbf l)$, но именно это утверждается в условии. Предложение 3 доказано. $\mathrm{Ar}^*$-формулу $\Phi$ будем называть вполне негативной, если она не содержит логических символов $\lor$ и $\exists$, а каждая атомарная формула $\Psi$, отличная от $\top$ и $\bot$, встречается в $\Phi$ только в подформулах вида $\neg\Psi$. Индуктивное определение вполне негативной $\mathrm{Ar}^*$-формулы таково: 1) $\top$ и $\bot$ суть вполне негативные формулы; 2) если $\Phi$ – атомарная $\mathrm{Ar}^*$-формула, отличная от $\top$ и $\bot$, то формула $\neg\Phi$ является вполне негативной; 3) если $\Phi$ и $\Psi$ – вполне негативные $\mathrm{Ar}^*$-формулы, то формула $(\Phi\,\&\,\Psi)$ является вполне негативной; 4) если $\Phi$ и $\Psi$ – вполне негативные $\mathrm{Ar}^*$-формулы, а $\mathbf x$ – список (возможно, пустой) предметных переменных, то формула $\forall\mathbf x\, (\Phi\to\Psi)$ является вполне негативной. Отметим, что если $\Phi$ вполне негативна, то формула $\neg\Phi$, т. е. $\Phi\to\bot$, вполне негативна. С точки зрения классической семантики всякая формула эквивалентна вполне негативной. Предложение 4. Если $\Phi(x_1,\dots,x_n)$ – вполне негативная $\mathrm{Ar}^*$-формула, то существует такое натуральное число $n_{\Phi}$, что для любых натуральных чисел $k_1,\dots,k_n$ следующие условия эквивалентны: 1) формула $\Phi(k_1,\dots,k_n)$ истинна; 2) $n_{\Phi}\,\mathbf{pr}\,\Phi(k_1,\dots,k_n)$; 3) формула $\Phi(k_1,\dots,k_n)$ pr-реализуема. Доказательство. Число $n_{\Phi}$ определяется индуктивно. Очевидно, что достаточно проверить два условия:
i) $n_{\Phi}\,\mathbf{pr}\,\Phi(k_1,\dots,k_n)$ тогда и только тогда, когда формула $\Phi(k_1,\dots,k_n)$ истинна; ii) если формула $\Phi(k_1,\dots,k_n)$ pr-реализуема, то $n_{\Phi}\,\mathbf{pr}\,\Phi(k_1,\dots,k_n)$. Если $\Phi$ – атомарная формула $\top$ или $\bot$, можно взять $n_{\Phi}=0$. Очевидно, что условия i) и ii) выполняются. Пусть $\Phi(x_1,\dots,x_n)$ имеет вид $\neg P(x_1,\dots,x_n)$, где $P$ – один из предикатных символов $Z$, $E$, $S$, $A$, $M$, $n\in\{1,2,3\}$. Тогда можно взять $n_{\Phi}=\mathsf a$. Докажем, что выполняется условие i). Пусть $\mathsf a\,\mathbf{pr}\,\neg P(k_1,\dots,k_n)$. Тогда формула $P(k_1,\dots,k_n)$ не pr-реализуема. Из определения pr-реализуемости для атомарных формул следует, что $P(k_1,\dots,k_n)$ не истинна. Тогда формула $\neg P(k_1,\dots,k_n)$ истинна. Обратно, пусть формула $\neg P(k_1,\dots,k_n)$ истинна. Тогда $P(k_1,\dots,k_n)$ не истинна. Из определения pr-реализуемости для атомарных формул следует, что формула $P(k_1,\dots,k_n)$ не pr-реализуема. Тогда в силу предложения 1 имеет место $\mathsf a\,\mathbf{pr}\,\neg P(k_1,\dots,k_n)$. Условие ii) следует из предложения 1. Предположим, что для формул $\Psi_1(x_1,\dots,x_n)$ и $\Psi_2(x_1,\dots,x_n)$ мы нашли такие числа $n_{\Psi_1}$ и $n_{\Psi_2}$, что для любых $k_1,\dots,k_n$ выполняются следующие условия: i1) $n_{\Psi_1}\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n)$, если и только если формула $\Psi_1(k_1,\dots,k_n)$ истинна; i2) $n_{\Psi_2}\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n)$, если и только если формула $\Psi_2(k_1,\dots,k_n)$ истинна; ii1) если формула $\Psi_1(k_1,\dots,k_n)$ pr-реализуема, то $n_{\Psi_1}\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n)$; ii2) если формула $\Psi_2(k_1,\dots,k_n)$ pr-реализуема, то $n_{\Psi_2}\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n)$. Если формула $\Phi(x_1,\dots,x_n)$ имеет вид $\Psi_1(x_1,\dots,x_n)\,\&\,\Psi_2(x_1,\dots,x_n)$, то положим $n_{\Phi}=\langle n_{\Psi_1},n_{\Psi_2}\rangle$ и докажем, что $n_{\Phi}$ – требуемое число. Проверим условие i). Пусть формула $\Phi(k_1,\dots,k_n)$ истинна. Тогда истинны обе формулы $\Psi_1(k_1,\dots,k_n)$ и $\Psi_2(k_1,\dots,k_n)$. В силу условий i1) и i2) имеем, что $n_{\Psi_1}\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n)$ и $n_{\Psi_2}\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n)$. Тогда $n_{\Phi}\,\mathbf{pr}\,\Phi(k_1,\dots,k_n)$ по определению pr-реализуемости, поскольку $[n_{\Phi}]_0=n_{\Psi_1}$, $[n_{\Phi}]_1=n_{\Psi_2}$. Обратно, если $n_{\Phi}\,\mathbf{pr}\,\Phi(k_1,\dots,k_n)$, то $n_{\Psi_1}\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n)$ и $n_{\Psi_2}\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n)$ по определению pr-реализуемости для конъюнкции. В этом случае в силу условий i1) и i2) обе формулы $\Psi_1(k_1,\dots,k_n)$ и $\Psi_2(k_1,\dots,k_n)$ истинны, так что формула $\Phi(k_1,\dots,k_n)$ тоже истинна. Проверим условие ii). Пусть формула $\Phi(k_1,\dots,k_n)$ pr-реализуема. Тогда $\Psi_1(k_1,\dots,k_n)$ и $\Psi_2(k_1,\dots,k_n)$ pr-реализуемы. Из условий ii1) и ii2) следует, что $n_{\Psi_1}\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n)$ и $n_{\Psi_2}\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n)$. Это дает $n_{\Phi}\,\mathbf{pr}\,\Phi(k_1,\dots,k_n)$ по определению pr-реализуемости. Пусть $\Phi(x_1,\dots,x_n)$ есть $\forall\mathbf y\, (\Psi_1(x_1,\dots,x_n,\mathbf y)\to\Psi_2(x_1,\dots,x_n,\mathbf y))$, где $\mathbf y$ – список (возможно, пустой) различных предметных переменных $y_1,\dots,y_m$, причем ни одна из переменных $x_i$ не присутствует в $\mathbf y$. Предположим, что для формул $\Psi_1$ и $\Psi_2$ мы нашли такие числа $n_{\Psi_1}$ и $n_{\Psi_2}$, что для любых $k_1,\dots,k_n$, $\ell_1,\dots,\ell_m$ выполняются следующие условия, где $\mathbf l$ – это список $\ell_1,\dots,\ell_m$: ia) $n_{\Psi_1}\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n,\mathbf l)$, если и только если формула $\Psi_1(k_1,\dots,k_n,\mathbf l)$ истинна; ib) $n_{\Psi_2}\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n,\mathbf l)$, если и только если формула $\Psi_2(k_1,\dots,k_n,\mathbf l)$ истинна; iia) если формула $\Psi_1(k_1,\dots,k_n,\mathbf l)$ pr-реализуема, то $n_{\Psi_1}\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n,\mathbf l)$; iib) если формула $\Psi_2(k_1,\dots,k_n,\mathbf l)$ pr-реализуема, то $n_{\Psi_2}\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n,\mathbf l)$. Положим $n_\Phi=\mathsf a_{n_{\Psi_2}}^{m+1}$ и докажем, что $n_{\Phi}$ – требуемое число. Проверим условие i). Пусть $\Phi(k_1,\dots,k_n)$ истинна. Тогда для любого $\mathbf l$ формула $\Psi_1(k_1,\dots,k_n,\mathbf l)\to\Psi_2(k_1,\dots,k_n,\mathbf l)$ истинна. Докажем, что имеет место $n_{\Phi}\,\mathbf{pr}\,\Phi(k_1,\dots,k_n)$, т. е. $\operatorname{In}(n_{\Phi})$ (это условие выполнено) и для любых $a$, $\mathbf l$, если $a\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n,\mathbf l)$, то число $\mathsf{pr}(n_{\Phi},\langle a,\mathbf l\rangle)$, т. е. $n_{\Psi_2}$, pr-реализует $\Psi_2(k_1,\dots,k_n,\mathbf l)$. Пусть $a\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n,\mathbf l)$. Тогда в силу условия iia) имеем $n_{\Psi_1}\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n,\mathbf l)$, и в силу условия ia) формула $\Psi_1(k_1,\dots,k_n,\mathbf l)$ истинна. Следовательно, формула $\Psi_2(k_1,\dots,k_n,\mathbf l)$ истинна. В силу условия ib) имеем $n_{\Psi_2}\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n,\mathbf l)$, что и требовалось доказать. Обратно, пусть $n_{\Phi}\,\mathbf{pr}\,\Phi(k_1,\dots,k_n)$. Докажем, что формула $\Phi(k_1,\dots,k_n)$ истинна. Пусть дан произвольный список натуральных чисел $\mathbf l$. Докажем, что истинна формула $\Psi_1(k_1,\dots,k_n,\mathbf l)\,{\to}\,\Psi_2(k_1,\dots,k_n,\mathbf l)$. Предположим, что истинна посылка $\Psi_1(k_1,\dots,k_n,\mathbf l)$. Докажем, что истинно заключение $\Psi_2(k_1,\dots,k_n,\mathbf l)$. В силу условия ia) имеем $n_{\Psi_1}\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n,\mathbf l)$. Тогда число $\mathsf{pr}(n_{\Phi},\langle n_{\Psi_1},\mathbf l\rangle)$, т. е. $n_{\Psi_2}$, pr-реализует формулу $\Psi_2(k_1,\dots,k_n,\mathbf l)$. В силу условия ib) формула $\Psi_2(k_1,\dots,k_n,\mathbf l)$ истинна, что и требовалось доказать. Проверим условие ii). Пусть формула $\Phi(k_1,\dots,k_n)$ pr-реализуема, т. е. существует такое $e$, что $\operatorname{In}(e)$ и для любых $a,\mathbf l$ из $a\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n,\mathbf l)$ следует $\mathsf{pr}(e,\langle a,\mathbf l\rangle)\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n,\mathbf l)$. Докажем, что $n_{\Phi}\,\mathbf{pr}\,\Phi(k_1,\dots,k_n)$, т. е. для любых $a$, $\mathbf l$, если $a\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n,\mathbf l)$, то число $\mathsf{pr}(n_{\Phi},\langle a,\mathbf l\rangle)$, т. е. $n_{\Psi_2}$, pr-реализует $\Psi_2(k_1,\dots,k_n,\mathbf l)$. Пусть $a\,\mathbf{pr}\,\Psi_1(k_1,\dots,k_n,\mathbf l)$. Тогда $\mathsf{pr}(e,\langle a,\mathbf l\rangle)\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n,\mathbf l)$, т. е. $\Psi_2(k_1,\dots,k_n,\mathbf l)$ pr-реализуема. В силу условия iib) $n_{\Psi_2}\,\mathbf{pr}\,\Psi_2(k_1,\dots,k_n,\mathbf l)$, что и требовалось доказать. Предложение 4 доказано. Предложение 5. Пусть $\Phi(\mathbf x)$ есть $\mathrm{Ar}^*$-формула вида $\exists\mathbf y\,\Psi(\mathbf x,\mathbf y)$, где $\mathbf x$ – список переменных $x_1,\dots,x_n$, $\mathbf y$ – список переменных $y_1,\dots,y_m$, а $\Psi(\mathbf x,\mathbf y)$ – вполне негативная $\mathrm{Ar}^*$-формула. Тогда, каков бы ни был список натуральных чисел $\mathbf k=k_1,\dots,k_n$, формула $\Phi(\mathbf k)$ pr-реализуема, если и только если она истинна. Доказательство. Пусть $\Phi(\mathbf k)$ pr-реализуема. Это означает, что существует такой список натуральных чисел $\mathbf l=\ell_1,\dots,\ell_m$, что формула $\Psi(\mathbf k,\mathbf l)$ pr-реализуема. В силу предложения 4 эта формула истинна. Отсюда следует, что формула $\Phi(\mathbf k)$ также истинна. Обратно, если формула $\Phi(\mathbf k)$ истинна, то существует такой список натуральных чисел $\mathbf l$, что формула $\Psi(\mathbf k,\mathbf l)$ истинна. В силу предложения 4 эта формула pr-реализуема. Отсюда следует, что формула $\Phi(\mathbf k)$ также pr-реализуема. Предложение 5 доказано.
§ 4. Арифметическая теория, корректная относительно pr-реализуемостиРассмотрим следующие $\mathrm{Ar}$-формулы: $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))$. В [2; § 48] определяется трехместная функция $\beta$ со следующим свойством: для любого списка натуральных чисел $k_0,\dots,k_n$ существуют такие натуральные числа $a$ и $b$, что для любого $i\leqslant n$ имеет место $\beta(a,b,i)=k_i$. Предикат $\beta([x]_0,[x]_1,y)=0$ рекурсивно перечислим. По теореме Матиясевича этот предикат определим в $\mathfrak N$ арифметической формулой $B(x,y)$ вида $\exists\mathbf z\,\Phi(x,y,\mathbf z)$, где $\Phi(x,y,\mathbf z)$ – атомарная арифметическая формула. Отсюда легко следует, что предикат $\beta([x]_0,[x]_1,y)=0$ определим в $\mathfrak N$ $\mathrm{Ar}$-формулой вида $\exists\mathbf z\,\Phi(x,y,\mathbf z)$, где $\Phi(x,y,\mathbf z)$ – вполне негативная бескванторная $\mathrm{Ar}$-формула. Таким образом, для любых натуральных чисел $a$ и $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
$$
Пусть $a$ – некоторое натуральное число. Тогда $\{a\}$ будет обозначать одноместную примитивно рекурсивную функцию $n\mapsto\mathsf{pr}(a,n)$. Таким образом, если $a$ – номер некоторой $(k+1)$-местной ($k\geqslant0$) примитивно рекурсивной функции $f$, то для любого $x$ имеет место $\{a\}(x)=f([x]_0,\dots,[x]_k)$, а в противном случае $\{a\}(x)=0$ для любого $x$. Так как предикат $\{x_1\}(x_2)=x_3$ очевидно рекурсивно перечислим, он определим в $\mathfrak N$ некоторой $\mathrm{Ar}$-формулой $G(x_1,x_2,x_3)$ вида $\exists\mathbf y\,\Psi(\mathbf y,x_1,x_2,x_3)$, где $\Psi(\mathbf y,x_1,x_2,x_3)$ – вполне негативная бескванторная $\mathrm{Ar}$-формула. Пусть $H(x_1,x_2)$ есть формула $\exists z\,(\neg\neg Z(z)\,\&\,G(x_1,x_2,z))$. Эта формула определяет в $\mathfrak N$ предикат $\{x_1\}(x_2)=0$. Через $x\leqslant y$ обозначим формулу $\exists z\,\neg\neg A(x,z,y)$. Рассмотрим следующие формулы: $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)$. Пусть $Q$ – конъюнкция формул $A_1$–$A_{25}$. Доказательство. Докажем, что каждая из формул $A_1$–$A_{25}$ pr-реализуема. Очевидно, что все эти формулы истинны. Все они, за исключением $A_4$, $A_7$, $A_{12}$, $A_{13}$, $A_{18}$, $A_{23}$, $A_{24}$ и $A_{25}$, вполне негативны, так что pr-реализуемы в силу предложения 4.
Рассмотрим формулу $A_4$. Пусть $a=\langle0,\mathsf a\rangle$. Докажем, что $a\,\mathbf{pr}\,\exists x\,\neg\neg Z(x)$, т. е. $\mathsf a\,\mathbf{pr}\,\neg\neg Z(0)$, но это легко следует из предложения 1, поскольку формула $\neg Z(0)$ не pr-реализуема. Рассмотрим формулу $A_7$. Функция $(x,y)\mapsto\langle y+1,\mathsf a\rangle$ примитивно рекурсивна. Пусть $a$ – ее номер. Докажем, что $a\,\mathbf{pr}\,\forall x\,(\top\to\exists y\,\neg\neg S(x,y))$, т. е. имеет место $\operatorname{In}(a)$ (это условие очевидно выполнено) и для любых $b,k$, если $b\,\mathbf{pr}\,\top$, то число $\mathsf{pr}(a,\langle b,k\rangle)$, т. е. $\langle k+1,\mathsf a\rangle$, pr-реализует формулу $\exists y\,\neg\neg S(k,y)$. Таким образом, мы должны доказать, что $\mathsf a\,\mathbf{pr}\,\neg\neg S(k,k+1)$, но это легко следует из предложения 1. Итак, формула $A_7$ pr-реализуема. Рассмотрим формулу $A_{12}$. Функция
$$
\begin{equation*}
f(x,y)= \begin{cases} \langle0,\mathsf a\rangle, &\text{если }y=0, \\ \langle1,\langle y-1,{\mathsf a}\rangle\rangle, & \text{если }y\ne 0, \end{cases}
\end{equation*}
\notag
$$
примитивно рекурсивна. Пусть $a$ – ее номер. Докажем, что
$$
\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
$$
т. е. для любых $b,k$, если $b\,\mathbf{pr}\,\top$, т. е. $b=0$, то
$$
\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
$$
т. е.
$$
\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}
$$
Если $k=0$, то $f(0,k)=\langle0,\mathsf a\rangle$. Формула $Z(0)$ pr-реализуема. В силу предложения 1 $\mathsf a\,\mathbf{pr}\,\neg\neg Z(k)$. В этом случае имеет место (4.1). Если $k>0$, то $f(0,k)=\langle1,\langle k-1,{\mathsf a}\rangle\rangle$. В этом случае $[f(0,k)]_0=1$, $[f(0,k)]_1=\langle k-1,{\mathsf a}\rangle$, и (4.1) означает, что ${\mathsf a}\,\mathbf{pr}\,\neg\neg S(k-1,k)$, а это легко следует из предложения 1, потому что формула $\neg\neg S(k-1,k)$ pr-реализуема. Таким образом, формула $A_{12}$ pr-реализуема.
Рассмотрим формулу $A_{13}$. Функция $(x,y,z)\mapsto\langle y+z,\mathsf a\rangle$ примитивно рекурсивна. Пусть $a$ – ее номер. Докажем, что $a\,\mathbf{pr}\,\forall x,y\,(\top\to\exists z\,\neg\neg A(x,y,z))$, т. е. имеет место $\operatorname{In}(a)$ (это условие очевидно выполнено) и для любых $b$, $k$, $\ell$, если $b\,\mathbf{pr}\,\top$, то число $\mathsf{pr}(a,\langle b,k,\ell\rangle)$, т. е. $\langle k+\ell,\mathsf a\rangle$, pr-реализует формулу $\exists z\,\neg\neg A(k,\ell,z)$. Таким образом, мы должны доказать, что $\mathsf a\,\mathbf{pr}\,\neg\neg A(k,\ell,k+\ell)$, но это легко следует из предложения 1. Итак, формула $A_{13}$ pr-реализуема. Формула $A_{18}$ рассматривается также с функцией $(x,y,z)\mapsto\langle y\cdot z,\mathsf a\rangle$. Рассмотрим формулу $A_{23}$. Функция $(x,y,z,u,v)\mapsto\mathsf a$ примитивно рекурсивна. Пусть $a$ – ее номер. Докажем, что $a$ pr-реализует формулу $A_{23}$. Мы должны доказать, что для любых $b$, $k$, $\ell$, $m_1$, $m_2$, если $b\,\mathbf{pr}\,(G(k,\ell,m_1)\,\&\,G(k,\ell,m_2))$, то число $\mathsf{pr}(a,\langle b,k,\ell,m_1,m_2\rangle)$, т. е. $\mathsf a$, pr-реализует формулу $\neg\neg E(m_1,m_2)$. Пусть $b\,\mathbf{pr}\,(G(k,\ell,m_1)\,\&\,G(k,\ell,m_2))$. Тогда формулы $G(k,\ell,m_1)$ и $G(k,\ell,m_2)$ pr-реализуемы и в силу предложения 5 они истинны, т. е. $\{k\}(\ell)=m_1$ и $\{k\}(\ell)=m_2$. Тогда $m_1=m_2$ и в силу предложения 1 $\mathsf a\,\mathbf{pr}\,\neg\neg E(m_1,m_2)$, что и требовалось доказать. Таким образом, формула $A_{23}$ pr-реализуема. Рассмотрим формулу $A_{24}$. В силу предложения 2 достаточно доказать, что для любых фиксированных натуральных чисел $m$ и $n$ формула
$$
\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
$$
не pr-реализуема. Докажем, что pr-реализуема формула
$$
\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}
$$
Рассмотрим список $k_0,\dots,k_n$, где $k_i=0\Leftrightarrow\{m\}(i)=0$. В силу свойства функции $\beta$ существует такое натуральное число $a$, что $\beta([a]_0,[a]_1,i)=k_i$ для любого $i\leqslant n$. Пусть $i\leqslant n$. Если $k_i=0$, то формулы $B(a,i)$ и $H(m,i)$ истинны. В силу предложения 5 они pr-реализуемы и в силу предложения 1 обе формулы $\neg\neg B(a,i)$ и $\neg\neg H(m,i)$ pr-реализуемы числом $\mathsf a$. В силу предложения 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}
$$
Отсюда следует, что
$$
\begin{equation}
\mathsf b\,\mathbf{pr}\,\bigl(\neg\neg B(a,i)\equiv\neg\neg H(m,i)\bigr),
\end{equation}
\tag{4.5}
$$
где $\mathsf b=\langle\Lambda x.\mathsf a,\Lambda x.\mathsf a\rangle$. Если $k_i\ne 0$, то $B(a,i)$ и $H(m,i)$ не истинны и в силу предложения 5 не pr-реализуемы. В силу предложения 1 в этом случае имеет место (4.3) и (4.4). Тогда имеет место и (4.5). Таким образом, для любого $i\leqslant n$ мы имеем (4.5). Пусть $c$ – номер функции $(x,y)\mapsto\mathsf b$. Докажем, что $c\,\mathbf{pr}\,\forall x\,(x\leqslant n\to(\neg\neg B(a,x)\equiv\neg\neg H(m,x)))$. Мы должны доказать, что для любых $d$, $i$, если $d\,\mathbf{pr}\,(i\leqslant n)$, то число $\mathsf{pr}(c,\langle d,i\rangle)$, т. е. $\mathbf b$, pr-реализует формулу $\neg\neg B(a,i)\equiv\neg\neg H(m,i)$. Пусть $d\,\mathbf{pr}\,(i\leqslant n)$. В силу предложения 5 формула $i\leqslant n$ истинна. Как было доказано выше, в этом случае имеет место (4.5), что и требовалось доказать. Теперь очевидно, что число $\langle a,c\rangle$ pr-реализует формулу (4.2). Таким образом, формула $A_{24}$ pr-реализуема.
Рассмотрим формулу $A_{25}$. Пусть $\phi(u,x,y)=\langle\overline{\mathsf{sg}}(\beta([x]_0,[x]_1,y)),\mathsf a\rangle$, где $\overline{\mathsf{sg}}(x)$ есть $1$, если $x=0$, и $0$ – в противном случае. Функция $\phi$ примитивно рекурсивна. Пусть $a$ – ее номер. Докажем, что $a$ pr-реализует формулу $A_{25}$. Мы должны доказать, что имеет место $\operatorname{In}(a)$ (это условие выполнено) и для любых $b$, $k$, $i$, если $b\,\mathbf{pr}\,\top$, то число $\mathsf{pr}(a,\langle b,k,i\rangle)$, т. е. $\phi(b,k,i)$, pr-реализует формулу $\neg B(k,i)\lor\neg\neg B(k,i)$. Рассмотрим два случая: $\beta([k]_0,[k]_1,i)=0$ и $\beta([k]_0,[k]_1,i)\ne 0$. В первом случае формула $B(k,i)$ истинна. В силу предложения 5 она pr-реализуема. Тогда формула $\neg\neg B(k,i)$ pr-реализуема. В силу предложения 1 имеет место $\mathsf a\,\mathbf{pr}\,\neg\neg B(k,i)$. Заметим, что в этом случае $\phi(b,k,i)=\langle1,\mathbf a\rangle$. Очевидно, что $\phi(b,k,i)\,\mathbf{pr}\,(\neg B(k,i)\lor\neg\neg B(k,i))$, что и требовалось доказать. Во втором случае формула $B(k,i)$ не истинна. В силу предложения 5 она не pr-реализуема. Тогда формула $\neg B(k,i)$ pr-реализуема. В силу предложения 1 имеет место $\mathsf a\,\mathbf{pr}\,\neg B(k,i)$. Заметим, что в этом случае $\phi(b,k,i)=\langle0,\mathbf a\rangle$ и $\phi(b,k,i)\,\mathbf{pr}\,(\neg B(k,i)\lor\neg\neg B(k,i))$. Теорема 1 доказана. § 5. Примитивно рекурсивно реализуемые предикатные формулыАлфавит языка базисной логики предикатов состоит из предметных переменных $x_0,x_1,\dots$, предикатных символов $P_i^{n_i}$ ($i,n_i\in\mathbb N$), логических символов $\&$, $\lor$, $\to$, $\forall$, $\exists$, $\top$, $\bot$ и служебных символов “ , ”, “ ( ” и “ ) ”. При этом $P_i^{n_i}$ называется $n_i$-местным предикатным символом, а $n_i$ – его валентностью. Предикатные символы называются также предикатными переменными, а предметные переменные – термами. Атомарные формулы суть $\top$, $\bot$, а также выражения вида $P(t_1,\dots,t_n)$, где $P$ есть $n$-местный предикатный символ, а $t_1,\dots,t_n$ – термы. Иногда мы будем использовать обозначение $\mathbf x$ для списка предметных переменных $x_1,\dots,x_n$. Предикатные формулы определяются индуктивно следующим образом:
Если список предметных переменных $\mathbf x$ в формуле $\forall\mathbf x\,(F\to G)$ пуст, то мы опускаем квантор $\forall$ и пишем просто $(F\to G)$. Выражение $F\equiv G$ является сокращением для формулы $(F\to G)\,\&\,(G\to F)$. Формула $F\to\bot$ будет обозначаться $\neg F$. Для краткости иногда будем писать $\exists\mathbf x$ вместо $\exists x_1\dots\exists x_n$. Предикатная формула $F$ будет обозначаться как $F(P_1,\dots,P_n,y_1,\dots,y_m)$, если она не содержит предикатных переменных, кроме $P_1,\dots,P_n$, и свободных предметных переменных, кроме $y_1,\dots,y_m$. Пусть $F(P_1,\dots,P_n)$ – предикатная формула. Будем говорить, что список $\mathrm{Ar}^*$-формул $\Phi_1,\dots,\Phi_n$ допустим для подстановки в $F$, если для любого $i=1,\dots,n$ формула $\Phi_i$ не содержит свободных переменных, отличных от $x_1,\dots,x_m$, где $m$ – валентность предикатной переменной $P_i$. В этом случае $F(\Phi_1,\dots,\Phi_n)$ будет обозначать результат подстановки в $F$ формул $\Phi_1,\dots,\Phi_n$ вместо предикатных переменных $P_1,\dots,P_n$ (при этом предполагается, что связанные предметные переменные переименовываются во избежание коллизии). Формулу $F(\Phi_1,\dots,\Phi_n)$ будем называть арифметическим примером предикатной формулы $F(P_1,\dots,P_n)$. Замкнутая предикатная формула $F(P_1,\dots,P_n)$ называется примитивно рекурсивно ( pr-) реализуемой, если для любого списка $\mathrm{Ar}^*$-формул $\Phi_1,\dots,\Phi_k$, допустимого для подстановки в $F$, замкнутая $\mathrm{Ar}^*$-формула $F(\Phi_1,\dots,\Phi_k)$ pr-реализуема. Предикатную формулу $F(P_1,\dots,P_n)$ будем называть вполне негативной, если она не содержит логических символов $\lor$ и $\exists$, а каждая предикатная переменная $P_i$ встречается в $F$ только в подформулах вида $\neg P_i(y_1,\dots,y_k)$. Индуктивное определение вполне негативной предикатной формулы следующее:
Предложение 6. Пусть $F(P_1,\dots,P_n,y_1,\dots,y_m)$ – вполне негативная предикатная формула. Тогда существует такое натуральное число $a_F$, что для любого списка $\mathrm{Ar}^*$-формул $\Phi_1,\dots,\Phi_n$, допустимого для подстановки в $F$, и любых натуральных чисел $k_1,\dots,k_m$ следующие условия эквивалентны: 1) формула $F(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m)$ pr-реализуема; 2) $a_F\,\mathbf{pr}\,F(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m)$. Доказательство. Индукция по построению вполне негативной предикатной формулы $F$. Если $F$ есть $\top$ или $\bot$, мы можем взять $a_F=0$. Пусть $F$ имеет вид $\neg P(y_1,\dots,y_m)$, где $P$ есть $m$-местная предикатная переменная, и пусть $\Phi(x_1,\dots,x_m)$ – некоторая $\mathrm{Ar}^*$-формула, допустимая для подстановки в $F$, а $k_1,\dots,k_m$ – натуральные числа. Тогда $F(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m)$ есть $\neg\Phi(k_1,\dots,k_m)$. В силу предложения 1 в этом случае можно взять $a_F=\mathsf a$.
Пусть $F(P_1,\dots,P_n,y_1,\dots,y_m)$ имеет вид
$$
\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
$$
и для формул $G$ и $H$ соответствующие числа $a_G$ и $a_H$ определены. Тогда можно взять $a_F=\langle a_G,a_H\rangle$.
Пусть $F(P_1,\dots,P_n,y_1,\dots,y_m)$ имеет вид
$$
\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
$$
где $\mathbf x$ – список предметных переменных $x_1,\dots,x_p$. Положим $a_F=\mathsf a_{a_H}^{p+1}$ и докажем, что $a_F$ – требуемое число.
Пусть формула $F(\Phi_1,\dots,\Phi_n,k_1,\dots,k_n)$ pr-реализуема. Тогда существует такое число $e$, что для любого списка натуральных чисел $\mathbf l=\ell_1,\dots,\ell_p$ и любого $b$, если
$$
\begin{equation}
b\,\mathbf{pr}\,G(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m,\mathbf l),
\end{equation}
\tag{5.1}
$$
то $\mathsf{pr}(e,\langle b,\mathbf l\rangle)\,\mathbf{pr}\,H(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m,\mathbf l)$. Отсюда следует, что для любого $\mathbf l$, если формула $G(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m,\mathbf l)$ pr-реализуема, то pr-реализуема формула $H(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m,\mathbf l)$, а тогда по индукционному предположению
$$
\begin{equation}
a_H\,\mathbf{pr}\,H(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m,\mathbf l).
\end{equation}
\tag{5.2}
$$
Пусть для некоторых $b$, $\mathbf l$ выполняется (5.1). Как отмечено выше, в этом случае мы имеем (5.2). Заметим, что $\mathsf{pr}(a_F,\langle b,\mathbf l\rangle)=a_H$. Таким образом, для любых $b$, $\mathbf l$, если выполнено (5.1), то $\mathsf{pr}(a_F,\langle b,\mathbf l\rangle)\,\mathbf{pr}\,H(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m,\mathbf l)$. Это означает, что $a_F\,\mathbf{pr}\,F(\Phi_1,\dots,\Phi_n,k_1,\dots,k_m)$, что и требовалось доказать. § 6. Моделирование арифметики в предикатном языкеКаждая $\mathrm{Ar}$-формула может $F$ рассматриваться как предикатная формула, если трактовать предикатные символы $S$, $A$, $M$, $Z$, $E$ как предикатные переменные. В этом случае будем называть $F$ предикатной $\mathrm{Ar}$-формулой. Поскольку предикатная $\mathrm{Ar}$-формула $F$ не содержит предикатных переменных, отличных от $S$, $A$, $M$, $Z$, $E$, будем обозначать ее $F(S,A,M,Z,E)$. Пусть $\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)$ – некоторый список $\mathrm{Ar}$-формул, допустимый для подстановки в предикатную $\mathrm{Ar}$-формулу $F(S,A,M,Z,E)$. Тогда $\mathrm{Ar}$-формула $F(\mathcal{S},\mathcal{A},\mathcal{M},\mathcal{Z},\mathcal{E})$ будет обозначаться $\widetilde F$. Будем говорить, что список $\mathbf{\Phi}$ является интерпретацией предикатной $\mathrm{Ar}$-формулы $F$, если $\mathrm{Ar}$-формула $\widetilde F$ pr-реализуема. Заметим, что список
$$
\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
$$
является интерпретацией предикатной $\mathrm{Ar}$-формулы $Q$, определенной в § 4, поскольку формула $\widetilde{Q}$ есть в точности $Q$, а последняя pr-реализуема по теореме 1. Предложение 7. Если $\mathbf{\Phi}$ – интерпретация формулы $Q$, то, какова бы ни была вполне негативная $\mathrm{Ar}$-формула $\Psi(x_1,\dots,x_n)$, pr-реализуема формула где $\mathbf x$ есть список $x_1,\dots,x_n$, а $\mathbf y$ есть $y_1,\dots,y_n$. Доказательство. Пусть список $\mathrm{Ar}$-формул
$$
\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
$$
является интерпретацией формулы $Q$. Формула $\widetilde{\Psi}(x_1,\dots,x_n)$ строится из $\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)$, где $1\leqslant i,j,k\leqslant n$, с использованием логических символов $\&$, $\to$ и $\forall$. Заметим, что (6.1) – это арифметический пример вполне негативной предикатной $\mathrm{Ar}$-формулы
$$
\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}
$$
В силу предложения 6 существует число, pr-реализующее любой pr-реализуемый арифметический пример формулы (6.2). Таким образом, достаточно доказать, что формула (6.1) pr-реализуема, не заботясь о построении конкретной pr-реализации.
Докажем pr-реализуемость формулы (6.1) индукцией по построению вполне негативной $\mathrm{Ar}$-формулы $\Psi(x_1,\dots,x_n)$. 1) Пусть $\Psi(x_1,\dots,x_n)$ есть формула $\top$. Тогда $\widetilde{\Psi }(x_1,\dots,x_n)$ есть $\top$, и в этом случае (6.1) есть формула $\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)$. Так как $0\,\mathbf{pr}\,\top$, очевидно, что эта формула pr-реализуема числом $\mathsf a_0^{2n+1}$. 2) Пусть $\Psi(x_1,\dots,x_n)$ есть формула $\bot$. Тогда $\widetilde{\Psi }(x_1,\dots,x_n)$ есть $\bot$, и в этом случае (6.1) есть формула $\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)$. Так как формула $\bot$ не pr-реализуема, очевидно, что эта формула pr-реализуема числом $\mathsf a_0^{2n+1}$. 3) Пусть $\Psi(x_1,\dots,x_n)$ есть $\neg E(x_i,x_j)$, $1\leqslant i,j\leqslant n$. Тогда $\widetilde{\Psi }(x_1,\dots,x_n)$ есть $\neg\mathcal E(x_i,x_j)$, и в этом случае (6.1) – это формула
$$
\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}
$$
Сначала докажем, что для любых $k_1,\dots,k_n$, $\ell_1,\dots,\ell_n$, если $\mathrm{Ar}^*$-формула
$$
\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}
$$
pr-реализуема, то
$$
\begin{equation}
\mathsf a\,\mathbf{pr}\,\neg\mathcal E(\ell_i,\ell_j).
\end{equation}
\tag{6.5}
$$
Пусть формула (6.4) pr-реализуема. Тогда формулы $\neg\neg\mathcal E(k_i,\ell_i)$, $\neg\neg\mathcal E(k_j,\ell_j)$ и $\neg\mathcal E(k_i,k_j)$ pr-реализуемы. Докажем, что выполнено (6.5). В силу предложения 1 достаточно доказать, что формула $\neg\neg\mathcal E(\ell_i,\ell_j)$ не pr-реализуема. Предположим противное. Тогда мы имеем, что формулы $\neg\neg\mathcal E(k_i,\ell_i)$, $\neg\neg\mathcal E(k_j,\ell_j)$ и $\neg\neg\mathcal E(\ell_i,\ell_j)$ pr-реализуемы. Так как формула $\widetilde{A_3}$ pr-реализуема, формула $\neg\neg\mathcal E(k_i,\ell_j)$ также pr-реализуема. Так как pr-реализуема формула $\widetilde{A_2}$, формула $\neg\neg\mathcal E(\ell_j,k_j)$ pr-реализуема. Так как pr-реализуема формула $\widetilde{A_3}$, формула $\neg\neg\mathcal E(k_i,k_j)$ также pr-реализуема вопреки предположению, что формула $\neg\mathcal E(k_i,k_j)$ pr-реализуема. Таким образом, формула $\neg\mathcal E(\ell_i,\ell_j)$ pr-реализуема, что и требовалось доказать. Мы доказали, что для любых $k_1,\dots,k_n,\ell_1,\dots,\ell_n$, если формула (6.4) pr-реализуема, то имеет место (6.5). В силу предложения 3 число $\mathsf a_{\mathsf a}^{2n+1}$ pr-реализует формулу (6.3). 4) Пусть $\Psi(x_1,\dots,x_n)$ есть $\neg Z(x_i)$, где $1\leqslant i\leqslant n$. Тогда $\widetilde{\Psi }(x_1,\dots,x_n)$ есть $\neg\mathcal Z(x_i)$, и в этом случае (6.1) есть формула
$$
\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}
$$
Сначала докажем, что для любых $k_1,\dots,k_n$, $\ell_1,\dots,\ell_n$, если $\mathrm{Ar}^*$-формула
$$
\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}
$$
pr-реализуема, то
Пусть формула (6.7) pr-реализуема. Тогда формулы $\neg\neg\mathcal E(k_i,\ell_i)$ и $\neg\mathcal Z(k_i)$ pr-реализуемы. Докажем, что имеет место (6.8). В силу предложения 1 достаточно доказать, что формула $\neg\neg\mathcal Z(\ell_i)$ не pr-реализуема. Предположим противное. Тогда мы имеем, что формулы $\neg\neg\mathcal E(k_i,\ell_i)$ и $\neg\neg\mathcal Z(\ell_i)$ pr-реализуемы. Так как pr-реализуема формула $\widetilde{A_2}$, формула $\neg\neg\mathcal E(\ell_i,k_i)$ pr-реализуема. Так как pr-реализуема формула $\widetilde{A_6}$, формула $\neg\neg\mathcal Z(k_i)$ также pr-реализуема вопреки предположению, что формула $\neg\mathcal Z(k_i)$ pr-реализуема. Таким образом, формула $\neg\mathcal Z(\ell_i)$ pr-реализуема, что и требовалось доказать. Мы доказали, что для любых $k_1,\dots,k_n,\ell_1,\dots,\ell_n$, если формула (6.7) pr-реализуема, то выполнено (6.8). В силу предложения 3 число $\mathsf a_{\mathsf a}^{2n+1}$ pr-реализует формулу (6.6). 5) Пусть $\Psi(x_1,\dots,x_n)$ есть $\neg S(x_i,x_j)$, $1\leqslant i,j\leqslant n$. Тогда $\widetilde{\Psi }(x_1,\dots,x_n)$ есть формула $\neg\mathcal S(x_i,x_j)$, и в этом случае (6.1) есть формула
$$
\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}
$$
Сначала мы докажем, что для любых $k_1,\dots,k_n,\ell_1,\dots,\ell_n$, если $\mathrm{Ar}^*$-формула
$$
\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}
$$
pr-реализуема, то
$$
\begin{equation}
\mathsf a\,\mathbf{pr}\,\neg\mathcal S(\ell_i,\ell_j).
\end{equation}
\tag{6.11}
$$
Пусть формула (6.10) pr-реализуема. Тогда формулы $\neg\neg\mathcal E(k_i,\ell_i)$, $\neg\neg\mathcal E(k_j,\ell_j)$ и $\neg\mathcal S(k_i,k_j)$ pr-реализуемы. Докажем, что имеет место (6.11). В силу предложения 1 достаточно доказать, что формула $\neg\neg\mathcal S(\ell_i,\ell_j)$ не pr-реализуема. Предположим противное. Тогда мы имеем, что формулы $\neg\neg\mathcal E(k_i,\ell_i)$, $\neg\neg\mathcal E(k_j,\ell_j)$ и $\neg\neg\mathcal S(\ell_i,\ell_j)$ pr-реализуемы. Так как pr-реализуема формула $\widetilde{A_2}$, формулы $\neg\neg\mathcal E(\ell_i,k_i)$ и $\neg\neg\mathcal E(\ell_j,k_j)$ pr-реализуемы. Так как pr-реализуема формула $\widetilde{A_9}$, формула $\neg\neg\mathcal S(k_i,k_j)$ также pr-реализуема вопреки предположению, что pr-реализуема формула $\neg\mathcal S(k_i,k_j)$. Таким образом, формула $\neg\mathcal S(\ell_i,\ell_j)$ pr-реализуема, что и требовалось доказать. Мы доказали, что для любых $k_1,\dots,k_n$, $\ell_1,\dots,\ell_n$, если формула (6.10) pr-реализуема, то выполнено (6.11). В силу предложения 3 число $\mathsf a_{\mathsf a}^{2n+1}$ pr-реализует формулу (6.9). 6) Пусть $\Psi(x_1,\dots,x_n)$ есть формула $\neg A(x_i,x_j,x_m)$, где $1\leqslant i,j,m\leqslant n$. Тогда $\widetilde{\Psi }(x_1,\dots,x_n)$ есть формула $\neg\mathcal A(x_i,x_j,x_m)$, и в этом случае (6.1) есть формула
$$
\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}
$$
Сначала докажем, что для любых $k_1,\dots,k_n,\ell_1,\dots,\ell_n$, если $\mathrm{Ar}^*$-формула
$$
\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}
$$
pr-реализуема, то
$$
\begin{equation}
\mathsf a\,\mathbf{pr}\,\neg\mathcal A(\ell_i,\ell_j,\ell_m).
\end{equation}
\tag{6.14}
$$
Пусть формула (6.13) pr-реализуема. Тогда формулы $\neg\neg\mathcal E(k_i,\ell_i)$, $\neg\neg\mathcal E(k_j,\ell_j)$, $\neg\neg\mathcal E(k_m,\ell_m)$ и $\neg\mathcal A(k_i,k_j,k_m)$ pr-реализуемы. Докажем, что имеет место (6.14). В силу предложения 1 достаточно доказать, что формула $\neg\neg\mathcal A(\ell_i,\ell_j,\ell_m)$ не pr-реализуема. Предположим противное. Тогда мы имеем, что pr-реализуемы формулы $\neg\neg\mathcal E(k_i,\ell_i)$, $\neg\neg\mathcal E(k_j,\ell_j)$, $\neg\neg\mathcal E(k_m,\ell_m)$ и $\neg\neg\mathcal A(\ell_i,\ell_j,\ell_m)$. Так как pr-реализуема формула $\widetilde{A_2}$, формулы $\neg\neg\mathcal E(\ell_i,k_i)$, $\neg\neg\mathcal E(\ell_j,k_j)$ и $\neg\neg\mathcal E(\ell_m,k_m)$ pr-реализуемы. Так как pr-реализуема формула $\widetilde{A_{15}}$, формула $\neg\neg\mathcal A(k_i,k_j,k_m)$ также pr-реализуема вопреки предположению, что pr-реализуема $\neg\mathcal A(k_i,k_j,k_m)$. Таким образом, формула $\neg\mathcal A(\ell_i,\ell_j,\ell_m)$ pr-реализуема, что и требовалось доказать. Мы доказали, что для любых $k_1,\dots,k_n$, $\ell_1,\dots,\ell_n$, если формула (6.13) pr-реализуема, то выполнено (6.14). В силу предложения 3 число $\mathsf a_{\mathsf a}^{2n+1}$ pr-реализует формулу (6.12). 7) Пусть $\Psi(x_1,\dots,x_n)$ есть формула $\neg M(x_i,x_j,x_m)$, где $1\leqslant i,j,m\leqslant n$. Тогда $\widetilde{\Psi }(x_1,\dots,x_n)$ есть формула $\neg\mathcal M(x_i,x_j,x_m)$, и в этом случае (6.1) есть формула
$$
\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}
$$
Тем же рассуждением, что и в случае формулы (6.12), доказывается pr-реализуемость формулы (6.15), только надо заменить $\mathcal A$ на $\mathcal M$ и использовать формулу $\widetilde{A_{20}}$ вместо $\widetilde{A_{15}}$.
8) Пусть $\Psi(x_1,\dots,x_n)$ есть $\Psi_1(x_1,\dots,x_n)\,\&\,\Psi_2(x_1,\dots,x_n)$, где $\Psi_1(x_1,\dots,x_n)$ и $\Psi_2(x_1,\dots,x_n)$ – вполне негативные $\mathrm{Ar}$-формулы, а индукционное предположение утверждает, что pr-реализуемы формулы
$$
\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}
$$
Тогда $\widetilde{\Psi}(x_1,\dots,x_n)$ есть формула $\widetilde{\Psi_1}(x_1,\dots,x_n)\,\&\,\widetilde{\Psi_2}(x_1,\dots,x_n)$, и мы должны доказать, что pr-реализуема формула
$$
\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}
$$
Сначала докажем, что для любых $k_1,\dots,k_n,\ell_1,\dots,\ell_n$, если $\mathrm{Ar}^*$-формула
$$
\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}
$$
pr-реализуема, то pr-реализуема формула
$$
\begin{equation}
\widetilde{\Psi_1}(\ell_1,\dots,\ell_n)\,\&\,\widetilde{\Psi_2}(\ell_1,\dots,\ell_n).
\end{equation}
\tag{6.20}
$$
Пусть pr-реализуема формула (6.19). Тогда формулы $\neg\neg\mathcal E(k_i,\ell_i)$ ($i\,{=}\,1,\dots,n$), $\widetilde{\Psi_1}(k_1,\dots,k_n)$ и $\widetilde{\Psi_2}(k_1,\dots,k_n)$ pr-реализуемы. Мы должны доказать, что формула (6.20) pr-реализуема, т. е. что pr-реализуемы обе формулы $\widetilde{\Psi_1}(\ell_1,\dots,\ell_n)$ и $\widetilde{\Psi_2}(\ell_1,\dots,\ell_n)$, но это легко следует из pr-реализуемости формул (6.16) и (6.17). В силу предложения 6 имеем $a_{\Psi_i}\,\mathbf{pr}\,\Psi_i(\ell_1,\dots,\ell_n)$ для $i=1,2$. Отсюда следует, что $\langle a_{\Psi_1},a_{\Psi_2}\rangle\,\mathbf{pr}\,\Psi_1(\ell_1,\dots,\ell_n) \,\&\,\Psi_2(\ell_1,\dots,\ell_n)$. Мы доказали, что для любых $k_1,\dots,k_n$, $\ell_1,\dots,\ell_n$, если формула (6.19) pr-реализуема, то число $\langle a_{\Psi_1},a_{\Psi_2}\rangle$ pr-реализует формулу (6.20). В силу предложения 3 число $\mathsf a_{\langle a_{\Psi_1},a_{\Psi_2}\rangle}^{2n+1}$ pr-реализует формулу (6.18). 9) Пусть $\Psi(x_1,\dots,x_n)$ есть $\forall\mathbf z\,(\Psi_1(x_1,\dots,x_n,\mathbf z)\to\Psi_2(x_1,\dots,x_n,\mathbf z))$, где $\mathbf z$ – список (возможно, пустой) различных предметных переменных $z_1,\dots,z_m$, причем переменные $x_i$ не содержатся в $\mathbf z$, а $\Psi_1(x_1,\dots,x_n,\mathbf z)$ и $\Psi_2(x_1,\dots,x_n,\mathbf z)$ – вполне негативные $\mathrm{Ar}$-формулы, и индукционное предположение утверждает, что pr-реализуемы формулы
$$
\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}
$$
Здесь $\mathbf w$ есть список различных предметных переменных $w_1,\dots,w_m$, и если $\mathbf u=u_1,\dots,u_k$ и $\mathbf v=v_1,\dots,v_k$ – некоторые списки предметных переменных, то $\neg\neg\mathcal{E}(\mathbf u,\mathbf v)$ есть формула $\neg\neg\mathcal E(u_1,v_1)\,\&\cdots\&\,\neg\neg\mathcal{E}(u_k,v_k)$. Тогда $\widetilde{\Psi}(x_1,\dots,x_n)$ есть формула $\forall\mathbf z\,(\widetilde{\Psi_1}(x_1,\dots,x_n,\mathbf z)\to\widetilde{\Psi_2}(x_1,\dots,x_n,\mathbf z))$, и мы должны доказать, что pr-реализуема формула
$$
\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}
$$
Сначала докажем, что для любых $k_1,\dots,k_n,\ell_1,\dots,\ell_n$, если $\mathrm{Ar}^*$-формула
$$
\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}
$$
pr-реализуема, то для любых $p_1,\dots,p_m$, если формула
$$
\begin{equation}
\widetilde{\Psi_1}(\ell_1,\dots,\ell_n,p_1,\dots,p_m)
\end{equation}
\tag{6.25}
$$
pr-реализуема, то pr-реализуема формула
$$
\begin{equation}
\widetilde{\Psi_2}(\ell_1,\dots,\ell_n,p_1,\dots,p_m).
\end{equation}
\tag{6.26}
$$
Пусть $k_1,\dots,k_n,\ell_1,\dots,\ell_n,p_1,\dots,p_m$ таковы, что формулы (6.24) и (6.25) pr-реализуемы. Тогда pr-реализуемы формулы $\neg\neg\mathcal E(k_i,\ell_i)$ ($i=1,\dots,n$) и
$$
\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}
$$
Так как формула $\widetilde{A_2}$ pr-реализуема, формулы $\neg\neg\mathcal E(\ell_i,k_i)$ ($i=1,\dots,n$) pr-реализуемы. Так как формула $\widetilde{A_1}$ pr-реализуема, pr-реализуемы формулы $\neg\neg\mathcal E(p_i,p_i)$ ($i=1,\dots,m$). Так как pr-реализуема формула (6.22), pr-реализуема формула $\widetilde{\Psi_1}(k_1,\dots,k_n,p_1,\dots,p_m)$. Так как формула (6.27) pr-реализуема, pr-реализуема формула $\widetilde{\Psi_2}(k_1,\dots,k_n,p_1,\dots,p_m)$. Так как pr-реализуема формула (6.22), формула (6.26) pr-реализуема, что и требовалось доказать. В силу предложения 6 число $a_{\Psi_2}$ pr-реализует формулу (6.26). Таким образом, для фиксированных $k_1,\dots,k_n,\ell_1,\dots,\ell_n$ таких, что pr-реализуема формула (6.24), мы доказали, что для любых $p_1,\dots,p_m$, если формула (6.25) pr-реализуема, то $a_{\Psi_2}$ pr-реализует формулу (6.26). В силу предложения 3 число $b=\mathsf a_{a_{\Psi_2}}^{m+1}$ pr-реализует формулу $\forall\mathbf z\,(\widetilde{\Psi_1}(\ell_1,\dots,\ell_n,\mathbf z)\to\widetilde{\Psi_2}(\ell_1,\dots,\ell_n,\mathbf z))$, а число $\mathsf a_b^{2n+1}$ pr-реализует формулу (6.23). Предложение 7 доказано. § 7. Стандартные элементы в интерпретацииДля натурального $n$ предикатная $\mathrm{Ar}$-формула $[n](x)$ определяется индуктивно:
Предложение 8. Если $\mathbf{\Phi}$ – интерпретация формулы $Q$, то для любого $n$ pr-реализуема $\mathrm{Ar}$-формула Доказательство. Доказываем pr-реализуемость формулы (7.1) индукцией по $n$. Если $n=0$, то $[n](x)$ есть $\neg\neg Z(x)$. Таким образом, мы должны доказать, что pr-реализуема формула $\forall x,y\,(\neg\neg\mathcal Z(x)\,\&\,\neg\neg\mathcal Z(y)\to\neg\neg\mathcal{E}(x,y))$, но это есть в точности формула $\widetilde{A_5}$, которая pr-реализуема, поскольку $\mathbf\Phi$ – интерпретация формулы $Q$. Теперь предположим, что формула (7.1) pr-реализуема для некоторого данного $n$. Покажем, что pr-реализуема формула
$$
\begin{equation}
\forall x,y\bigl(\widetilde{[n+1]}(x)\,\&\,\widetilde{[n+1]}(y)\to\neg\neg\mathcal{E}(x,y)\bigr).
\end{equation}
\tag{7.2}
$$
Сначала докажем, что для любых $k$, $\ell$, если формула pr-реализуема, то
$$
\begin{equation}
\mathsf a\,\mathbf{pr}\,\neg\neg\mathcal{E}(k,\ell).
\end{equation}
\tag{7.4}
$$
Пусть формула (7.3) pr-реализуема. Тогда pr-реализуемы формулы $\neg\mathcal Z(k)$, $\forall y\,(\neg\neg\mathcal S(y,k)\to\widetilde{[n]}(y))$, $\neg\mathcal Z(\ell)$ и $\forall y\,(\neg\neg\mathcal S(y,\ell)\to\widetilde{[n]}(y))$. Так как формула $\widetilde{A_{12}}$ pr-реализуема, pr-реализуема формула $\exists y\,\neg\neg\mathcal S(y,k)$. Это означает, что для некоторого натурального числа $p$ pr-реализуема формула $\neg\neg\mathcal S(p,k)$. Отсюда следует, что pr-реализуема формула $\widetilde{[n]}(p)$. По тем же причинам существует такое натуральное число $q$, что pr-реализуемы формулы $\neg\neg\mathcal S(q,\ell)$ и $\widetilde{[n]}(q)$. По индукционному предположению pr-реализуема формула $\neg\neg\mathcal E(p,q)$. Так как pr-реализуемы формулы $\mathcal E(k,k)$ и $\widetilde{A_9}$, формула $\neg\neg\mathcal S(q,k)$ pr-реализуема. Так как pr-реализуема формула $\widetilde{A_8}$, формула $\neg\neg\mathcal E(k,\ell)$ pr-реализуема. В силу предложения 1 имеет место (7.4), что и требовалось доказать. Мы доказали, что для любых $k,\ell$, если формула (7.3) pr-реализуема, то выполнено (7.4). В силу предложения 3 число $\mathsf a_{\mathsf a}^3$ pr-реализует формулу (7.2). Предложение 8 доказано. Предложение 9. Пусть $\mathbf{\Phi}$ – некоторая интерпретация формулы $Q$. Тогда для любых натуральных чисел $k$ и $n$ можно эффективно определить, является ли pr-реализуемой $\mathrm{Ar}^*$-формула $\widetilde{[n]}(k)$. Доказательство. Пусть $\mathbf{\Phi}$ – интерпретация формулы $Q$, причем $e\,\mathbf{pr}\,\widetilde{Q}$. Доказываем утверждение индукцией по $n$. Если $n=0$, то $\widetilde{[n]}(k)$ есть формула $\neg\neg\mathcal Z(k)$. Пусть дано натуральное число $k$. Мы можем извлечь из $e$ pr-реализацию формулы $\widetilde{A_{12}}$. А тогда мы сможем определить, которая из формул $\neg\neg\mathcal Z(k)$ и $\exists y\,\neg\neg\mathcal S(y,k)$ pr-реализуема. Если pr-реализуема первая, то формула $\widetilde{[0]}(k)$ pr-реализуема. Если же pr-реализуема формула $\exists y\,\neg\neg\mathcal S(y,k)$, то для некоторого натурального $\ell$ pr-реализуема формула $\neg\neg\mathcal S(\ell,k)$. Так как формула $\widetilde{A_{11}}$ pr-реализуема, pr-реализуема формула $\neg\mathcal Z(k)$. Это означает, что формула $\widetilde{[0]}(k)$ не pr-реализуема. Теперь предположим, что для некоторого заданного $n$ и любого $\ell$ мы можем эффективно определить, является ли формула $\widetilde{[n]}(\ell)$ pr-реализуемой. Пусть дано число $k$ и мы хотим определить, является ли pr-реализуемой формула $\widetilde{[n+1]}(k)$, т. е. $\neg\mathcal Z(k)\,\&\,\forall y\,(\neg\neg\mathcal S(y,k)\to\widetilde{[n]}(y))$. Используя pr-реализацию формулы $\widetilde{A_{12}}$, определяем, которая из формул $\neg\neg\mathcal Z(k)$ и $\exists y\,\neg\neg\mathcal S(y,k)$ pr-реализуема. Если pr-реализуема формула $\neg\neg\mathcal Z(k)$, то формула $\widetilde{[n+1]}(k)$ не pr-реализуема. Пусть pr-реализуема формула $\exists y\,\neg\neg\mathcal S(y,k)$. Тогда имеется такое натуральное число $\ell$, что формула $\neg\neg\mathcal S(\ell,k)$ pr-реализуема. По индукционному предположению мы можем определить, является ли pr-реализуемой формула $\widetilde{[n]}(\ell)$. Если она не pr-реализуема, то формула $\widetilde{[n+1]}(k)$ очевидно не pr-реализуема. Пусть формула $\widetilde{[n]}(\ell)$ pr-реализуема. Покажем, что pr-реализуема формула $\widetilde{[n+1]}(k)$. Достаточно доказать, что pr-реализуема формула $\forall y\,(\neg\neg\mathcal S(y,k)\to\widetilde{[n]}(y))$. Сначала докажем, что для любого $p$, если формула $\neg\neg\mathcal S(p,k)$ pr-реализуема, то pr-реализуема формула $\widetilde{[n]}(p)$. Пусть формула $\neg\neg\mathcal S(p,k)$ pr-реализуема. Напомним, что формула $\neg\neg\mathcal S(\ell,k)$ также pr-реализуема. Так как pr-реализуема формула $\widetilde{A_{10}}$, формула $\neg\neg\mathcal E(\ell,p)$ pr-реализуема. Напомним, что pr-реализуема формула $\widetilde{[n]}(\ell)$. Так как формула $[n](x)$ вполне негативна, из предложения 7 следует, что формула $\widetilde{[n]}(p)$ pr-реализуема, что и требовалось доказать. В силу предложения 6 имеем $a_{[n](x)}\,\mathbf{pr}\,\widetilde{[n]}(p)$. Мы доказали, что для любого $p$, если формула $\neg\neg\mathcal S(p,k)$ pr-реализуема, то $a_{[n](x)}\,\mathbf{pr}\,\widetilde{[n]}(p)$. Тогда $\mathsf a_{a_{[n](x)}}^2\,\mathbf{pr}\,\forall y\,(\neg\neg\mathcal S(y,k)\to\widetilde{[n]}(y))$ в силу предложения 3. Это означает, что формула $\widetilde{[n+1]}(k)$ pr-реализуема. Предложение 9 доказано. Предложение 10. Если $\mathbf{\Phi}$ – интерпретация формулы $Q$, то существует такая примитивно рекурсивная функция $\mathsf f$, что для любого натурального $n$ pr-реализуема $\mathrm{Ar}^*$-формула $\widetilde{[n]}(\mathsf f(n))$. Доказательство. Пусть $\mathbf{\Phi}$ – некоторая интерпретация формулы $Q$. Тогда pr-реализуема формула $\widetilde{A_4}$. Это означает, что $a_4\,\mathbf{pr}\,\exists x\,\neg\neg\mathcal{Z}(x)$ для некоторого натурального $a_4$. Тогда $[a_4]_1\,\mathbf{pr}\,\neg\neg\mathcal{Z}([a_4]_0)$. Положим $\mathsf f(0)=[a_4]_0$. Таким образом, мы имеем, что формула $\neg\neg\mathcal{Z}((\mathsf f(0))$, т. е. $\widetilde{[0]}(\mathsf f(0))$, pr-реализуема. В силу предложения 1
Предположим, что определено значение $\mathsf f(n)$ для некоторого данного $n$. Так как pr-реализуема формула $\widetilde{A_7}$, для некоторого натурального числа $a_7$ имеем $a_7\,\mathbf{pr}\,\forall x\,(\top\to\exists y\,\neg\neg\mathcal{S}(x,y))$. Тогда $a_7$ – номер такой примитивно рекурсивной функции $g$, что для любого $k$ число $g(0,k)$ pr-реализует формулу $\exists y\,\neg\neg\mathcal{S}(k,y)$. В частности, $g(0,\mathsf f(n))\,\mathbf{pr}\,\exists y\,\neg\neg\mathcal{S}(\mathsf f(n),y)$ и $[g(0,\mathsf f(n))]_1\,\mathbf{pr}\,\neg\neg\mathcal{S}(\mathsf f(n),[g(0,\mathsf f(n))]_0)$. Положим $\mathsf f(n+1)=[g(0,\mathsf f(n))]_0$. Заметим, что pr-реализуема формула Таким образом, мы имеем следующее определение функции $\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
$$
где число $a_4$ и примитивно рекурсивная функция $g$ зависят только от данной pr-реализации формулы $\widetilde{Q}$. Очевидно, что функция $\mathsf f$ примитивно рекурсивна.
Докажем, что для любого $n$ pr-реализуема формула $\widetilde{[n]}(\mathsf f(n))$. Индукция по $n$. Если $n=0$, то это следует из утверждения (7.5), доказанного выше. Теперь предположим, что для некоторого данного $n$ формула $\widetilde{[n]}(\mathsf f(n))$ pr-реализуема. Тогда в силу предложения 6 имеет место $a_{[n](x)}\,\mathbf{pr}\,\widetilde{[n]}(\mathsf f(n))$. Докажем, что pr-реализуема формула $\widetilde{[n+1]}(\mathsf f(n+1))$, т. е. что формулы и
$$
\begin{equation}
\forall y\,(\neg\neg\mathcal{S}(y,\mathsf f(n+1))\to\widetilde{[n]}(y))
\end{equation}
\tag{7.8}
$$
pr-реализуемы. Так как pr-реализуемы формулы (7.6) и $\widetilde{A_{11}}$, формула (7.7) pr-реализуема. Теперь докажем, что pr-реализуема формула (7.8). Сначала докажем, что для любого $k$, если формула $\neg\neg\mathcal{S}(k,\mathsf f(n+1))$ pr-реализуема, то pr-реализуема формула $\widetilde{[n]}(k)$. Пусть формула $\neg\neg\mathcal{S}(k,\mathsf f(n+1))$ pr-реализуема. Так как pr-реализуемы формулы (7.6) и $\widetilde{A_{10}}$, формула $\neg\neg\mathcal{E}(\mathsf f(n),k)$ pr-реализуема. По индукционному предположению pr-реализуема формула $\widetilde{[n]}(\mathsf f(n))$. В силу предложения 7 формула $\widetilde{[n]}(k)$ pr-реализуема, что и требовалось доказать. В силу предложения 6 имеет место $a_{[n](x)}\,\mathbf{pr}\,\widetilde{[n]}(k)$. Мы доказали, что для любого $k$, если pr-реализуема формула $\neg\neg\mathcal{S}(k,\mathsf f(n+1))$, то $a_{[n](x)}\,\mathbf{pr}\,\widetilde{[n]}(k)$. В силу предложения 3 число $\mathsf a_{a_{[n](x)}}^2$ pr-реализует формулу (7.8). Предложение 10 доказано. Предложение 11. Если $\mathbf{\Phi}$ – интерпретация формулы $Q$, то для любых натуральных чисел $n$, $m$ и $a$, если $\mathrm{Ar}^*$-формулы $\widetilde{[n]}(a)$ и $\widetilde{[m]}(a)$ pr-реализуемы, то $m=n$. Доказательство. Пусть формулы $\widetilde{[n]}(a)$ и $\widetilde{[m]}(a)$ pr-реализуемы. Индукцией по $n$ докажем, что невозможно $n<m$. Пусть $n=0$, $m=k+1$. Тогда мы имеем, что pr-реализуемы формулы $\widetilde{[0]}(a)$, т. е. $\neg\neg\mathcal Z(a)$, и $\widetilde{[k+1]}(a)$, т. е. $\neg\mathcal Z(a)\,\&\,\forall y\,(\neg\neg\mathcal S(y,a)\to\widetilde{[k]}(y))$. Очевидно, что это невозможно. Теперь пусть $m=k+1>n+1$, и предположим, что pr-реализуемы $\widetilde{[n+1]}(a)$ и $\widetilde{[k+1]}(a)$, т. е. $\neg\mathcal Z(a)\,\&\,\forall y\,(\neg\neg\mathcal S(y,a)\to\widetilde{[n]}(y))$ и $\neg\mathcal Z(a)\,\&\,\forall y\,(\neg\neg\mathcal S(y,a)\to\widetilde{[k]}(y))$. Так как формулы $\neg\mathcal Z(a)$ и $\widetilde{A_{12}}$ pr-реализуемы, существует такое число $b$, что pr-реализуема формула $\neg\neg\mathcal S(b,a)$. Тогда формулы $\widetilde{[n]}(b)$ и $\widetilde{[k]}(b)$ pr-реализуемы и при этом $n<k$. Но это невозможно по индукционному предположению. Предложение 11 доказано. Для любого $n$ через $\overline n$ обозначим число $\mathsf f(n)$. Предложение 12. Пусть $\mathbf\Phi$ – интерпретация формулы $Q$. Тогда, каковы бы ни были бескванторная вполне негативная $\mathrm{Ar}$-формула $\Psi(x_1,\dots,x_m)$, не содержащая свободных переменных, отличных от $x_1,\dots,x_m$, и натуральные числа $k_1,\dots,k_m$, $\mathrm{Ar}^*$-формула $\Psi(k_1,\dots,k_m)$ истинна тогда и только тогда, когда pr-реализуема $\mathrm{Ar}^*$-формула $\widetilde{\Psi}(\overline{k_1},\dots,\overline{k_m})$. Доказательство. Пусть список $\mathrm{Ar}$-формул является интерпретацией формулы $Q$. Заметим, что бескванторная вполне негативная формула $\widetilde{\Psi}(x_1,\dots,x_n)$ строится из формул $\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),$ где $1\leqslant i,j,k\leqslant n$, с использованием логических символов $\&$ и $\to$. Доказываем утверждение индукцией по построению формулы $\Psi(x_1,\dots,x_n)$. Опустим тривиальный случай, когда $\Psi$ есть $\top$ или $\bot$, ибо тогда $\widetilde{\Psi}(\overline{k_1},\dots,\overline{k_m})$ совпадает с $\Psi(k_1,\dots,k_m)$.
1) Пусть $\Psi(x_1,\dots,x_n)$ есть $\neg E(x_i,x_j)$, где $1\leqslant i,j\leqslant n$. Тогда $\widetilde{\Phi}(x_1,\dots,x_n)$ есть $\neg\mathcal E(x_i,x_j)$. Если $i=j$, то формула $\neg E(k_i,k_j)$ не истинна. С другой стороны, так как формула $\widetilde{A_1}$ pr-реализуема, pr-реализуема формула $\neg\neg\mathcal E(\overline{k_i},\overline{k_j})$, а формула $\neg\mathcal E(\overline{k_i},\overline{k_j})$ не pr-реализуема. Таким образом, формула $\neg E(k_i,k_j)$ истинна, если и только если pr-реализуема формула $\neg\mathcal E(\overline{k_i},\overline{k_j})$. Теперь пусть $i\ne j$. Предположим, что формула $\neg E(k_i,k_j)$ истинна. Это означает, что $k_i\ne k_j$. Докажем, что формула $\neg\mathcal E(\overline{k_i},\overline{k_j})$ pr-реализуема. В силу предложения 1 достаточно доказать, что формула $\neg\neg\mathcal E(\overline{k_i},\overline{k_j})$ не pr-реализуема. Предположим противное. В силу определения функции $\mathsf f$ имеем, что pr-реализуема формула $\widetilde{[k_i]}(\overline{k_i})$. Тогда в силу предложения 7 формула $\widetilde{[k_i]}(\overline{k_j})$ также pr-реализуема. Однако pr-реализуема формула $\widetilde{[k_j]}(\overline{k_j})$. В силу предложения 11 $k_i=k_j$ вопреки предположению, что формула $\neg E(k_i,k_j)$ истинна. Таким образом, формула $\neg\mathcal E(\overline{k_i},\overline{k_j})$ pr-реализуема. Обратно, пусть формула $\neg\mathcal E(\overline{k_i},\overline{k_j})$ pr-реализуема. Докажем, что формула $\neg E(k_i,k_j)$ истинна, т. е. $k_i\ne k_j$. Предположим противное. Тогда $\overline{k_i}=\overline{k_j}$. Так как pr-реализуема формула $\widetilde{A_1}$, формула $\neg\neg\mathcal E(\overline{k_i},\overline{k_j})$ pr-реализуема вопреки предположению, что pr-реализуема формула $\neg\mathcal E(\overline{k_i},\overline{k_j})$. Таким образом, $k_i\ne k_j$ и формула $\neg E(k_i,k_j)$ истинна. 2) Пусть $\Psi(x_1,\dots,x_n)$ есть $\neg Z(x_i)$, где $1\leqslant i\leqslant n$. Тогда $\widetilde{\Psi}(x_1,\dots,x_n)$ есть $\neg\mathcal Z(x_i)$. Пусть формула $\neg Z(k_i)$ истинна. Это означает, что $k_i\ne 0$. Докажем, что формула $\neg\mathcal Z(\overline{k_i})$ pr-реализуема. Предположим противное. Тогда pr-реализуема формула $\neg\neg\mathcal Z(\overline{k_i})$, т. е. $\widetilde{[0]}(\overline{k_i})$. С другой стороны, формула $\widetilde{[k_i]}(\overline{k_i})$ также pr-реализуема. В силу предложения 11 $k_i=0$ вопреки предположению, что истинна формула $\neg Z(k_i)$. Обратно, пусть формула $\neg\mathcal Z(\overline{k_i})$ pr-реализуема. Тогда формула $\neg\neg\mathcal Z(\overline{k_i})$, т. е. $\widetilde{[0]}(\overline{k_i})$, не pr-реализуема. Докажем, что формула $\neg Z(k_i)$ истинна, т. е. $k_i\ne 0$. Предположим противное. Тогда pr-реализуема формула $\widetilde{[0]}(\overline{k_i})$. Это противоречие доказывает, что формула $\neg Z(k_i)$ истинна. 3) Пусть $\Psi(x_1,\dots,x_n)$ есть формула $\neg S(x_i,x_j)$, где $1\leqslant i,j\leqslant n$. Тогда $\widetilde{\Psi}(x_1,\dots,x_n)$ есть формула $\neg\mathcal S(x_i,x_j)$. Пусть формула $\neg S(k_i,k_j)$ истинна. Это означает, что $k_j\ne k_i+1$. Докажем, что формула $\neg\mathcal S(\overline{k_i},\overline{k_j})$ pr-реализуема. Предположим противное. Тогда pr-реализуема формула $\neg\neg\mathcal S(\overline{k_i},\overline{k_j})$. Докажем, что pr-реализуема формула $\widetilde{[k_i+1]}(\overline{k_j})$, т. е.
$$
\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}
$$
Так как формулы $\neg\neg\mathcal S(\overline{k_i},\overline{k_j})$ и $\widetilde{A_{11}}$ pr-реализуемы, pr-реализуема формула $\neg\mathcal Z(\overline{k_j})$. Докажем, что pr-реализуема формула $\forall y\,(\neg\neg\mathcal S(y,\overline{k_j})\to\widetilde{[k_i]}(y))$. Сначала докажем, что для любого $\ell$, если формула $\neg\neg\mathcal S(\ell,\overline{k_j})$ pr-реализуема, то pr-реализуема формула $\widetilde{[k_i]}(\ell)$. Пусть формула $\neg\neg\mathcal S(\ell,\overline{k_j})$ pr-реализуема. Тогда мы имеем, что pr-реализуемы формулы $\neg\neg\mathcal S(\overline{k_i},\overline{k_j})$ и $\neg\neg\mathcal S(\ell,\overline{k_j})$. Так как формула $\widetilde{A_{10}}$ pr-реализуема, pr-реализуема формула $\neg\neg\mathcal E(\overline{k_i},\ell)$. Из предложения 7 следует, что формула $\widetilde{[k_i]}(\ell)$ pr-реализуема, что и требовалось доказать. В силу предложения 6 имеем $a_{[k_i](x)}\,\mathbf{pr}\,\widetilde{[k_i]}(\ell)$. Мы доказали, что для любого $\ell$, если pr-реализуема формула $\neg\neg\mathcal S(\ell,\overline{k_j})$, то $a_{[k_i](x)}\,\mathbf{pr}\,\widetilde{[k_i]}(\ell)$. В силу предложения 3 число $\mathsf a_{a_{[k_i](x)}}^2$ pr-реализует формулу $\forall y\,(\neg\neg\mathcal S(y,\overline{k_j})\to\widetilde{[k_i]}(y))$. Таким образом, мы доказали, что формула $\neg\mathcal S(\overline{k_i},\overline{k_j})$ pr-реализуема, если формула $\neg S(k_i,k_j)$ истинна.
Обратно, пусть формула $\neg\mathcal S(\overline{k_i},\overline{k_j})$ pr-реализуема. Докажем, что формула $\neg S(k_i,k_j)$ истинна, т. е. $k_j\ne k_i+1$. Предположим противное. Тогда формула $\widetilde{[k_i+1]}(\overline{k_j})$, т. е. (7.9), pr-реализуема. Отсюда следует, что pr-реализуема формула $\neg\mathcal Z(k_j)$. Так как формула $\widetilde{A_{12}}$ pr-реализуема, для некоторого натурального $\ell$ формула $\neg\neg\mathcal S(\ell,\overline{k_j})$ pr-реализуема. С другой стороны, так как pr-реализуема формула (7.9), формула $\widetilde{[k_i]}(\ell)$ pr-реализуема. Так как формула $\widetilde{[k_i]}(\overline{k_i})$ также pr-реализуема, из предложения 8 следует, что pr-реализуема формула $\neg\neg\mathcal E(\ell,\overline{k_i})$. В силу предложения 7 формула $\neg\neg\mathcal S(\overline{k_i},\overline{k_j})$ pr-реализуема вопреки предположению, что pr-реализуема формула $\neg\mathcal S(\overline{k_i},\overline{k_j})$. Таким образом, доказано, что формула $\neg S(k_i,k_j)$ истинна. 4) Пусть $\Psi(x_1,\dots,x_n)$ есть формула $\neg A(x_i,x_j,x_m)$, где $1\leqslant i,j,m\leqslant n$. Тогда $\widetilde{\Psi }(x_1,\dots,x_n)$ есть формула $\neg\mathcal A(x_i,x_j,x_m)$. Докажем предложение индукцией по $k_j$. Пусть $k_j=0$. Тогда $\overline{k_j}=\overline0$ и pr-реализуема формула $\widetilde{[0]}(\overline{k_j})$, т. е. $\neg\neg\mathcal Z(\overline{k_j})$. Пусть формула $\neg A(k_i,k_j,k_m)$ истинна. Это означает, что $k_m\ne k_i$. Докажем, что формула $\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Предположим противное. Тогда pr-реализуема формула $\neg\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$. Так как формула $\widetilde{A_{16}}$ pr-реализуема, pr-реализуема формула $\neg\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_i})$. Так как формула $\widetilde{A_{14}}$ pr-реализуема, pr-реализуема формула $\neg\neg\mathcal E(\overline{k_m},\overline{k_i})$. Как было доказано в пункте 1), формула $E(k_m,k_i)$ истинна, т. е. $k_m=k_i$ вопреки предположению, что истинна формула $\neg A(k_i,k_j,k_m)$. Таким образом, мы доказали, что формула $\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Обратно, пусть формула $\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Докажем, что формула $\neg A(k_i,k_j,k_m)$ истинна, т. е. $k_m\ne k_i$. Предположим противное. Тогда $\overline{k_m}=\overline{k_i}$. Так как pr-реализуема формула $\widetilde{A_{16}}$, формула $\neg\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема вопреки предположению о pr-реализуемости $\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$. Таким образом, мы доказали, что формула $\neg A(k_i,k_j,k_m)$ истинна. Теперь предположим, что $k_j=\ell_j+1$ и, каковы бы ни были $k_i,\ell_m$, формула $\neg A(k_i,\ell_j,\ell_m)$ истинна, если и только если формула $\neg\mathcal A(\overline{k_i},\overline{\ell_j},\overline{\ell_m})$ pr-реализуема. Заметим, что формула $\neg S(\ell_j,k_j)$ не истинна. Как было доказано в пункте 3), формула $\neg\mathcal S(\overline{\ell_j},\overline{k_i})$ не pr-реализуема. Тогда pr-реализуема формула $\neg\neg\mathcal S(\overline{\ell_j},\overline{k_i})$. Пусть формула $\neg A(k_i,k_j,k_m)$ истинна. Это означает, что $k_m\ne k_i+k_j$. Докажем, что формула $\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Предположим противное. Тогда pr-реализуема формула $\neg\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$. С другой стороны, так как $\neg A(k_i,\ell_j,k_i+\ell_j)$ не истинна, по индукционному предположению формула $\neg\mathcal A(\overline{k_i},\overline{\ell_j},\overline{k_i+\ell_j})$ не pr-реализуема. Тогда pr-реализуема $\neg\neg\mathcal A(\overline{k_i},\overline{\ell_j},\overline{k_i+\ell_j})$. Положим $\ell_m=k_i+\ell_j+1$. Тогда формула $S(k_i+\ell_j,\ell_m)$ истинна, а формула $\neg S(k_i+\ell_j,\ell_m)$ не истинна. Как было доказано в пункте 3), формула $\neg\mathcal S(\overline{k_i+\ell_j},\overline{\ell_m})$ не pr-реализуема. Тогда pr-реализуема формула $\neg\neg\mathcal S(\overline{k_i+\ell_j},\overline{\ell_m})$. Так как pr-реализуема формула $\widetilde{A_{17}}$, формула $\neg\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{\ell_m})$ pr-реализуема. Так как pr-реализуема формула $\widetilde{A_{14}}$, формула $\neg\neg\mathcal E(k_m,\ell_m)$ pr-реализуема. Тогда формула $\neg\mathcal E(k_m,\ell_m)$ не pr-реализуема. Как было доказано в пункте 1), формула $\neg E(k_m,\ell_m)$ не истинна, а тогда истинна формула $E(k_m,\ell_m)$, т. е. $k_m=\ell_m=k_i+\ell_j+1=k_i+k_j$. Это означает, что формула $A(k_i,k_j,k_m)$ истинна вопреки предположению, что истинна формула $\neg A(k_i,k_j,k_m)$. Таким образом, мы доказали, что формула $\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Обратно, пусть формула $\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Докажем, что формула $\neg A(k_i,k_j,k_m)$ истинна. Предположим противное.Тогда истинна формула $A(k_i,k_j,k_m)$. Это означает, что $k_m=k_i+k_j$. Положим $\ell_m=k_i+\ell_j$. Тогда $k_m=\ell_m+1$ и формула $\neg A(k_i,\ell_j,\ell_m)$ не истинна. По индукционному предположению формула $\neg\mathcal A(\overline{k_i},\overline{\ell_j},\overline{\ell_m})$ не pr-реализуема. Тогда pr-реализуема формула $\neg\neg\mathcal A(\overline{k_i},\overline{\ell_j},\overline{\ell_m})$. С другой стороны, так как формулы $S(\ell_j,k_j)$ и $S(\ell_m,k_m)$ истинны, формулы $\neg S(\ell_j,k_j)$ и $\neg S(\ell_m,k_m)$ не истинны. Как было доказано в пункте 3), в этом случае формулы $\neg\mathcal S(\overline{\ell_j},\overline{k_j})$ и $\neg\mathcal S(\overline{\ell_m},\overline{k_m})$ не pr-реализуемы. Тогда pr-реализуемы формулы $\neg\neg\mathcal S(\overline{\ell_j},\overline{k_j})$ и $\neg\neg\mathcal S(\overline{\ell_m},\overline{k_m})$. Так как формула $\widetilde{A_{17}}$ pr-реализуема, pr-реализуема формула $\neg\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$ вопреки предположению, что pr-реализуема формула $\neg\mathcal A(\overline{k_i},\overline{k_j},\overline{k_m})$. Таким образом, мы доказали, что формула $\neg A(k_i,k_j,k_m)$ истинна. 5) Пусть $\Psi(x_1,\dots,x_n)$ есть формула $\neg M(x_i,x_j,x_m)$, где $1\leqslant i,j,m\leqslant n$. Тогда $\widetilde{\Psi}(x_1,\dots,x_n)$ есть формула $\neg\mathcal M(x_i,x_j,x_m)$. Докажем предложение индукцией по $k_j$. Пусть $k_j=0$. Тогда формула $\widetilde{[0]}(\overline{k_j})$, т. е. $\neg\neg\mathcal Z(\overline{k_j})$, pr-реализуема. Пусть формула $\neg M(k_i,k_j,k_m)$ истинна. Докажем, что формула $\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Предположим противное. Тогда формула $\neg\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Так как формула $\widetilde{A_{21}}$ pr-реализуема, формула $\neg\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_j})$ pr-реализуема. Так как формула $\widetilde{A_{19}}$ pr-реализуема, формула $\neg\neg\mathcal E(\overline{k_m},\overline{k_j})$ pr-реализуема. Тогда формула $\neg\mathcal E(\overline{k_m},\overline{k_j})$ не pr-реализуема. Как было доказано в пункте 1), в этом случае формула $\neg E(k_m,k_j)$ не истинна, т. е. $k_m=k_j$. Тогда формула $M(k_i,k_j,k_m)$ истинна вопреки предположению, что истинна формула $\neg M(k_i,k_j,k_m)$. Таким образом, мы доказали, что формула $\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Обратно, пусть формула $\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Докажем, что формула $\neg M(k_i,k_j,k_m)$ истинна. Предположим противное. Тогда $k_m=k_j$ и $\overline{k_m}=\overline{k_j}$. Так как pr-реализуема формула $\widetilde{A_{21}}$, формула $\neg\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема вопреки предположению, что pr-реализуема $\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$. Таким образом, мы доказали, что формула $\neg M(k_i,k_j,k_m)$ истинна. Теперь предположим, что $k_j=\ell_j+1$ и, каковы бы ни были $k_i,\ell_m$, формула $\neg M(k_i,\ell_j,\ell_m)$ истинна, если и только если формула $\neg\mathcal M(\overline{k_i},\overline{\ell_j},\overline{\ell_m})$ pr-реализуема. Так как формула $S(\ell_j,k_j)$ истинна, формула $\neg S(\ell_j,k_j)$ не истинна. Как было показано в пункте 3), в этом случае формула $\neg\mathcal S(\overline{\ell_j},\overline{k_j})$ не pr-реализуема. Тогда pr-реализуема формула $\neg\neg\mathcal S(\overline{\ell_j},\overline{k_j})$. Пусть формула $\neg M(k_i,k_j,k_m)$ истинна. Докажем, что формула $\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Предположим противное. Тогда pr-реализуема формула $\neg\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$. Так как формула $M(k_i,\ell_j,k_i\cdot\ell_j)$ истинна, формула $\neg M(k_i,\ell_j,k_i\cdot\ell_j)$ не истинна. По индукционному предположению формула $\neg\mathcal M(\overline{k_i},\overline{\ell_j},\overline{k_i\cdot\ell_j})$ не pr-реализуема. Тогда pr-реализуема $\neg\neg\mathcal M(\overline{k_i},\overline{\ell_j},\overline{k_i\cdot\ell_j})$. Положим $\ell_m=k_i\cdot\ell_j+k_i$. Тогда формула $A(k_i\cdot\ell_j,k_i,\ell_m)$ истинна, а формула $\neg A(k_i\cdot\ell_j,k_i,\ell_m)$ не истинна. Как было доказано в пункте 4), формула $\neg\mathcal A(\overline{k_i\cdot\ell_j},\overline{k_i},\overline{\ell_m})$ не pr-реализуема. Тогда pr-реализуема формула $\neg\neg\mathcal A(\overline{k_i\cdot\ell_j},\overline{k_i},\overline{\ell_m})$. Так как формула $\widetilde{A_{22}}$ pr-реализуема, pr-реализуема формула $\neg\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{\ell_m})$. Так как формула $\widetilde{A_{19}}$ pr-реализуема, pr-реализуема формула $\neg\neg\mathcal E(k_m,\ell_m)$. Тогда $\neg\mathcal E(k_m,\ell_m)$ не pr-реализуема и, как было доказано в пункте 1), формула $\neg E(k_m,\ell_m)$ не истинна. Тогда истинна $E(k_m,\ell_m)$, т. е. $k_m=\ell_m=k_i+k_i\cdot\ell_j=k_i\cdot k_j$. Это означает, что формула $M(k_i,k_j,k_m)$ истинна вопреки предположению, что истинна формула $\neg M(k_i,k_j,k_m)$. Таким образом, мы доказали, что формула $\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Обратно, пусть формула $\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Докажем, что формула $\neg M(k_i,k_j,k_m)$ истинна. Предположим противное. Тогда $k_m=k_i\cdot k_j$. Положим $\ell_m=k_i\cdot\ell_j$. Тогда истинна формула $M(k_i,\ell_j,\ell_m)$ и $k_m=\ell_m+k_i$. Это означает, что формула $A(\ell_m,k_i,k_m)$ истинна. Тогда формулы $\neg M(k_i,\ell_j,\ell_m)$ и $\neg A(\ell_m,k_i,k_m)$ не истинны. По индукционному предположению формула $\neg\mathcal M(\overline{k_i},\overline{\ell_j},\overline{\ell_m})$ не pr-реализуема. Тогда pr-реализуема формула $\neg\neg\mathcal M(\overline{k_i},\overline{\ell_j},\overline{\ell_m})$. Так как формула $\neg A(\ell_m,k_i,k_m)$ не истинна, формула $\neg\mathcal A(\overline{\ell_m},\overline{k_i},\overline{k_m})$ не pr-реализуема, как было показано в пункте 4). Тогда формула $\neg\neg\mathcal A(\overline{\ell_m},\overline{k_i},\overline{k_m})$ pr-реализуема. Так как pr-реализуема формула $\widetilde{A_{22}}$, pr-реализуема формула $\neg\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ вопреки предположению, что формула $\neg\mathcal M(\overline{k_i},\overline{k_j},\overline{k_m})$ pr-реализуема. Таким образом, мы доказали, что формула $\neg M(k_i,k_j,k_m)$ истинна. 6) Пусть $\Psi(x_1,\dots,x_n)$ есть $\Psi_1(x_1,\dots,x_n)\,\&\,\Psi_2(x_1,\dots,x_n)$, где $\Psi_1(x_1,\dots,x_n)$ и $\Psi_2(x_1,\dots,x_n)$ – бескванторные вполне негативные $\mathrm{Ar}$-формулы. Индукционное предположение утверждает, что для любых $k_1,\dots,k_m$ $\mathrm{Ar}^*$-формула $\Psi_i(k_1,\dots,k_m)$ истинна, если и только если $\mathrm{Ar}^*$-формула $\widetilde{\Psi_i}(\overline{k_1},\dots,\overline{k_m})$ pr-реализуема ($i=1,2$). Тогда $\widetilde{\Psi }(x_1,\dots,x_n)$ есть $\widetilde{\Psi_1}(x_1,\dots,x_n)\,\&\,\widetilde{\Psi_2}(x_1,\dots,x_n)$. Формула $\Psi(k_1,\dots,k_m)$ истинна, если и только если истинны обе формулы $\Psi_1(k_1,\dots,k_m)$ и $\Psi_2(k_1,\dots,k_m)$. По индукционному предположению это возможно тогда и только тогда, когда обе формулы $\widetilde{\Psi_1}(\overline{k_1},\dots,\overline{k_m})$ и $\widetilde{\Psi_2}(\overline{k_1},\dots,\overline{k_m})$ pr-реализуемы, т. е. pr-реализуема формула $\widetilde{\Phi}(\overline{k_1},\dots,\overline{k_m})$. 7) Пусть $\Psi(x_1,\dots,x_n)$ имеет вид $\Psi_1(x_1,\dots,x_n)\to\Psi_2(x_1,\dots,x_n)$ при тех же условиях, что и в предыдущем пункте. Тогда $\widetilde{\Psi}(x_1,\dots,x_n)$ есть формула $\widetilde{\Psi_1}(x_1,\dots,x_n)\to\widetilde{\Psi_2}(x_1,\dots,x_n)$. Пусть формула $\Psi(k_1,\dots,k_m)$ истинна. Это означает, что формула $\Psi_1(k_1,\dots,k_m)$ не истинна или $\Psi_2(k_1,\dots,k_m)$ истинна. В первом случае по индукционному предположению формула $\widetilde{\Psi_1}(\overline{k_1},\dots,\overline{k_m})$ не pr-реализуема и в силу предложения 1 формула $\widetilde{\Psi}(\overline{k_1},\dots,\overline{k_m})$ pr-реализуема. Во втором случае по индукционному предположению формула $\widetilde{\Psi_2}(\overline{k_1},\dots,\overline{k_m})$ pr-реализуема и в силу предложения 1 pr-реализуема формула $\widetilde{\Psi}(\overline{k_1},\dots,\overline{k_m})$. Обратно, если формула $\widetilde{\Psi}(\overline{k_1},\dots,\overline{k_m})$ pr-реализуема, то $\Psi(k_1,\dots,k_m)$ должна быть истинной, потому что в противном случае формула $\Psi_1(k_1,\dots,k_m)$ истинна, а формула $\Psi_2(k_1,\dots,k_m)$ не истинна, и по индукционному предположению формула $\widetilde{\Psi_1}(\overline{k_1},\dots,\overline{k_m})$ pr-реализуема, а формула $\widetilde{\Psi_2}(\overline{k_1},\dots,\overline{k_m})$ – нет, что невозможно. Предложение 12 доказано. Напомним, что $\{a\}$ есть функция $n\mapsto\mathsf{pr}(a,n)$, а предикат $\{x_1\}(x_2)=x_3$ определяется в $\mathfrak N$ $\mathrm{Ar}$-формулой $G(x_1,x_2,x_3)$ вида $\exists\mathbf y\,\Psi(\mathbf y,x_1,x_2,x_3)$, где $\mathbf y$ – список переменных $y_1,\dots,y_m$, а $\Psi(\mathbf y,x_1,x_2,x_3)$ – вполне негативная бескванторная $\mathrm{Ar}$-формула. Предложение 13. Пусть $\mathbf\Phi$ – интерпретация формулы $Q$. Тогда для любых натуральных чисел $e$, $n$ и $k$ $\mathrm{Ar}^*$-формула $\widetilde{G}(\overline e,\overline n,\overline k)$ pr-реализуема тогда и только тогда, когда $\{e\}(n)=k$. Доказательство. Пусть $\{e\}(n)=k$. Тогда формула $G(e,n,k)$ истинна. Это означает, что существует список натуральных чисел $\mathbf b=b_1,\dots,b_m$ такой, что истинна бескванторная $\mathrm{Ar}^*$-формула $\Psi(\mathbf b,e,n,k)$. В силу предложения 12 pr-реализуема формула $\widetilde{\Psi}(\overline{\mathbf b},\overline e,\overline n,\overline k)$, где $\overline{\mathbf b}=\overline{b_1},\dots,\overline{b_m}$. Тогда pr-реализуема и формула $\exists\mathbf y\,\widetilde{\Psi}(y,\overline e,\overline n,\overline k)$, т. е. $\widetilde{G}(\overline e,\overline n,\overline k)$.
Обратно, пусть формула $\widetilde{G}(\overline e,\overline n,\overline k)$ pr-реализуема. Очевидно, что существует такое натуральное число $\ell$, что $\{e\}(n)=\ell$. Тогда формула $G(e,n,\ell)$ истинна. Рассуждая, как выше, заключаем, что формула $\widetilde{G}(\overline e,\overline n,\overline\ell)$ pr-реализуема. Так как pr-реализуема формула $\widetilde{A_{23}}$, отсюда следует, что pr-реализуема формула $\neg\neg\mathcal E(\overline \ell,\overline k)$. По определению функции $\mathsf f$ формула $\widetilde{[k]}(\overline k)$ pr-реализуема. Из предложения 7 следует, что pr-реализуема $\widetilde{[k]}(\overline\ell)$. С другой стороны, pr-реализуема формула $\widetilde{[\ell]}(\overline\ell)$. Тогда, в силу предложения 11, $k=\ell$. Таким образом, мы доказали, что $\{e\}(n)=k$. Предложение 13 доказано. Напомним, что $H(x_1,x_2)$ – это формула $\exists z\,(\neg\neg Z(z)\,\&\,G(x_1,x_2,z))$. Предложение 14. Пусть $\mathbf\Phi$ – интерпретация формулы $Q$. Тогда для любых натуральных чисел $e$ и $n$ $\mathrm{Ar}^*$-формула $\widetilde{H}(\overline e,\overline n)$ pr-реализуема тогда и только тогда, когда $\{e\}(n)=0$. Доказательство. Пусть $\{e\}(n)=0$. В силу предложения 13 pr-реализуема формула $\widetilde{G}(\overline e,\overline n,\overline0)$. С другой стороны, формула $\neg\neg\mathcal Z(\overline0)$ также pr-реализуема. Тогда pr-реализуема формула $\neg\neg\mathcal Z(\overline0)\,\&\,\widetilde{G}(\overline e,\overline n,\overline0)$. Отсюда следует, что pr-реализуема формула $\exists z\,(\neg\neg\mathcal Z(z)\,\&\,\widetilde{G}(\overline e,\overline n,z))$, т. е. $\widetilde{H}(\overline e,\overline n)$. Обратно, пусть формула $\widetilde{H}(\overline e,\overline n)$ pr-реализуема. Тогда существует такое натуральное число $k$, что pr-реализуемы формулы $\neg\neg\mathcal Z(k)$, т. е. $\widetilde{[0]}(k)$, и $\widetilde{G}(\overline e,\overline n,k)$. Поскольку формула $\widetilde{[0]}(\overline0)$ также pr-реализуема, из предложения 8 следует, что pr-реализуема формула $\neg\neg\mathcal E(k,\overline0)$. Тогда из предложения 7 следует, что формула $\widetilde{G}(\overline e,\overline n,\overline0)$ pr-реализуема. В силу предложения 13 $\{e\}(n)=0$. Предложение 14 доказано. Пусть фиксирована некоторая интерпретация $\mathbf{\Phi}$ формулы $Q$. Натуральное число $a$ будем называть $\mathbf{\Phi}$-стандартным, если существует такое натуральное число $n$, что pr-реализуема формула $\widetilde{[n]}(a)$. Заметим, что числа $\overline0,\overline1,\dots$ являются $\mathbf{\Phi}$-стандартными. Предложение 15. Если натуральное число $a$ является $\mathbf{\Phi}$-стандартным, а $b$ – такое натуральное число, что pr-реализуема $\mathrm{Ar}^*$-формула $\neg\neg\mathcal{S}(a,b)$, то число $b$ является $\mathbf{\Phi}$-стандартным. Доказательство. Пусть pr-реализуема формула $\widetilde{[n]}(a)$. Так как предикатная $\mathrm{Ar}$-формула $[n](x)$ является вполне негативной, из предложения 6 следует, что существует такое число $d$, а именно, $a_{[n](x)}$, что $d\,\mathbf{pr}\,\widetilde{[n]}(a)$. Пусть $b$ – такое натуральное число, что pr-реализуема формула $\neg\neg\mathcal{S}(a,b)$. Докажем, что pr-реализуема формула $\widetilde{[n+1]}(b)$, т. е. $\neg\mathcal Z(b)\,\&\,\forall y\,(\neg\neg\mathcal S(y,b)\to\widetilde{[n]}(y))$. Так как pr-реализуема формула $\widetilde{A_{11}}$, отсюда следует, что pr-реализуема формула $\neg\mathcal Z(b)$. Докажем, что pr-реализуема формула
$$
\begin{equation}
\forall y\bigl(\neg\neg\mathcal S(y,b)\to\widetilde{[n]}(y)\bigr).
\end{equation}
\tag{7.10}
$$
Сначала докажем, что для любого $c$, если pr-реализуема формула $\neg\neg\mathcal S(c,b)$, то pr-реализуема формула $\widetilde{[n]}(c)$. Пусть формула $\neg\neg\mathcal S(c,b)$ pr-реализуема. Так как pr-реализуемы формулы $\neg\neg\mathcal{S}(a,b)$, $\neg\neg\mathcal S(c,b)$ и $\widetilde{A_{10}}$, отсюда следует, что pr-реализуема формула $\neg\neg\mathcal E(a,c)$. Поскольку pr-реализуема формула $\widetilde{[n]}(a)$, из предложения 7 следует pr-реализуемость формулы $\widetilde{[n]}(c)$, что и требовалось. В силу предложения 6 $d\,\mathbf{pr}\,\widetilde{[n]}(c)$. Мы доказали, что для любого $c$, если формула $\neg\neg\mathcal S(c,b)$ pr-реализуема, то $d\,\mathbf{pr}\,\widetilde{[n]}(c)$. В силу предложения 3 число $\mathsf a_d^2$ pr-реализует формулу (7.10). Таким образом, мы доказали, что pr-реализуема формула $\widetilde{[n+1]}(b)$. Это означает, что число $b$ является $\mathbf{\Phi}$-стандартным. Предложение 15 доказано. Напомним, что через $x\leqslant y$ обозначается формула $\exists z\,\neg\neg A(z,x,y)$. Предложение 16. Пусть $\mathbf{\Phi}$ – интерпретация формулы $Q$. Каковы бы ни были натуральные числа $n$ и $b$, если $b$ не является $\mathbf{\Phi}$-стандартным, то pr-реализуема $\mathrm{Ar}^*$-формула $\overline n\mathbin{\widetilde{\leqslant}}b$. Доказательство. Индукция по $n$. Пусть $n=0$. Из pr-реализуемости формулы $\widetilde{A_{16}}$ следует, что pr-реализуема формула $\neg\neg\mathcal{Z}(\overline0)\to\neg\neg\mathcal{A}(b,\overline0,b)$. Так как pr-реализуема формула $\neg\neg\mathcal{Z}(\overline0)$, отсюда следует, что pr-реализуема формула $\neg\neg\mathcal{A}(b,\overline0,b)$. Следовательно, pr-реализуема формула $\exists z\,\neg\neg\mathcal{A}(z,\overline0,b)$, т. е. $\overline0\mathbin{\widetilde{\leqslant}}b$.
Теперь предположим, что для любого натурального числа $b$, которое не является $\mathbf{\Phi}$-стандартным, pr-реализуема формула $\overline n\mathbin{\widetilde{\leqslant}}b$. Мы должны доказать, что для любого такого числа $b$ pr-реализуема формула $\overline{n+1}\mathbin{\widetilde{\leqslant}}b$. Так как число $b$ не является $\mathbf{\Phi}$-стандартным, отсюда следует, что формула $\neg\neg\mathcal{Z}(b)$ не pr-реализуема. Так как pr-реализуема формула $\widetilde{A_{12}}$, отсюда следует, что pr-реализуема формула $\exists y\,\neg\neg\mathcal{S}(y,b)$. Это означает существование такого натурального числа $a$, что pr-реализуема формула $\neg\neg\mathcal{S}(a,b)$. В силу предложения 15 число $a$ не может быть $\mathbf{\Phi}$-стандартным. По индукционному предположению pr-реализуема формула $\exists z\,\neg\neg\mathcal{A}(z,\overline n,a)$. Это означает существование такого натурального числа $c$, что pr-реализуема формула $\neg\neg\mathcal{A}(c,\overline n,a)$. Так как формула $\neg\neg S(n,n+1)$ истинна, из предложения 12 следует, что pr-реализуема формула $\neg\neg\mathcal S(\overline n,\overline{n+1})$. Так как pr-реализуема формула $\widetilde{A_{17}}$, отсюда следует, что pr-реализуема формула $\neg\neg\mathcal{A}(c,\overline{n+1},b)$. Следовательно, pr-реализуема формула $\exists z\,\neg\neg\mathcal{A}(z,\overline{n+1},b)$, т. е. $\overline{n+1}\mathbin{\widetilde{\leqslant}}b$. Предложение 16 доказано. § 8. Основной результатТеорема 2. Если $\mathbf\Phi$ – интерпретация формулы $Q$, то каждое натуральное число является $\mathbf\Phi$-стандартным. Доказательство. Пусть дана интерпретация $\mathbf\Phi$ формулы $Q$. Тогда pr-реализуема формула $\widetilde{A_{25}}$. Это означает существование такой примитивно рекурсивной функции $g(a,x,y)$, что для любых $a$, $k$, $\ell$, если $a\,\mathbf{pr}\,\top$, т. е. $a=0$, то $g(a,k,\ell)\,\mathbf{pr}\,(\neg\widetilde B(k,\ell)\lor\neg\neg\widetilde B(k,\ell))$, т. е. если $[g(0,k,\ell)]_0=0$, то pr-реализуема формула $\neg\widetilde B(k,\ell)$, а в противном случае pr-реализуема формула $\neg\neg\widetilde B(k,\ell)$. Рассмотрим одноместную функцию $h(n)=\mathsf{sg}([g(0,n,\mathsf f(n))]_0)$. Докажем, что функция $h$ обладает следующим свойством:
$h(n)= 0$, если формула $\neg\widetilde B(n,\overline n)$ pr-реализуема, $h(n)= 1$ в противном случае. Пусть формула $\neg\widetilde B(n,\overline n)$ pr-реализуема. Тогда $[g(0,k,\overline n)]_0=0$. Напомним, что $\overline n=\mathsf f(n)$. Таким образом, мы имеем $h(n)=\mathsf{sg}([g(0,n,\mathsf f(n))]_0)=0$. Если формула $\neg\widetilde B(n,\overline n)$ не pr-реализуема, то $[g(0,k,\overline n)]_0\ne 0$ и $h(n)=\mathsf{sg}([g(0,n,\mathsf f(n))]_0)=1$. Очевидно, что функция $h$ примитивно рекурсивна. Следовательно, существует такое натуральное число $e$, что $h(n)=\{e\}(n)$ для всех $n$. Так как $\mathbf\Phi$ – интерпретация формулы $Q$, отсюда следует, что pr-реализуема формула $\widetilde{A_{24}}$, т. е.
$$
\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}
$$
Предположим, что существует натуральное число $b$, которое не является $\mathbf\Phi$-стандартным. Так как pr-реализуема формула (8.1), отсюда следует, что pr-реализуема формула
$$
\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}
$$
Теперь предположим, что pr-реализуема формула
$$
\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}
$$
Тогда существует такое натуральное число $a$, что pr-реализуема формула
$$
\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
$$
Отсюда следует, что для любого $n$ pr-реализуема формула
$$
\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
$$
В силу предложения 16 формула $\overline n\mathbin{\widetilde{\leqslant}}b$ pr-реализуема. Тогда для любого $n$ pr-реализуема формула $\neg\neg\widetilde{B}(a,\overline n)\equiv\neg\neg\widetilde{H}(\overline e,\overline n)$. Таким образом, для любого $n$ мы имеем:
(a) формула $\neg\neg\widetilde{B}(a,\overline n)$ pr-реализуема тогда и только тогда, когда pr-реализуема формула $\neg\neg\widetilde{H}(\overline e,\overline n)$. С другой стороны, в силу предложения 14 для любого $n$ (b) формула $\neg\neg\widetilde{H}(\overline e,\overline n)$ pr-реализуема тогда и только тогда, когда $h(n)=0$. Далее, по свойству функции $h$ имеем (c) $h(n)=0$ тогда и только тогда, когда pr-реализуема формула $\neg\widetilde{B}(n,\overline n)$. Из утверждений (a), (b) и (c) следует, что для данного числа $a$ и всякого натурального числа $n$ выполняется следующая эквивалентность: формула $\neg\neg\widetilde{B}(a,\overline n)$ pr-реализуема тогда и только тогда, когда pr-реализуема формула $\neg\widetilde{B}(n,\overline n)$, и мы получаем противоречие, если $n=a$. Это противоречие означает, что формула (8.3) не pr-реализуема. Тогда pr-реализуемо ее отрицание вопреки pr-реализуемости формулы (8.2). Таким образом, мы доказали, что не существует натурального числа, которое не является $\mathbf\Phi$-стандартным. Теорема 2 доказана. Предложение 17. Пусть $\mathbf{\Phi}$ – интерпретация формулы $Q$, и пусть $e$ pr-реализует формулу $\widetilde{Q}$. Тогда для любого натурального числа $k$ можно эффективно найти такое натуральное число $n$, что pr-реализуема формула $\widetilde{[n]}(k)$. Доказательство. Пусть $\mathbf{\Phi}$ – интерпретация формулы $Q$, и пусть дана pr-реализация $e$ формулы $\widetilde{Q}$. Пусть дано натуральное число $k$. В силу предложения 9 для любого натурального числа $n$ можно эффективно проверить, является ли pr-реализуемой формула $\widetilde{[n]}(k)$. Последовательно перебирая натуральные числа, начиная с $0$, мы найдем такое $n$, что формула $\widetilde{[n]}(k)$ pr-реализуема, так как в противном случае число $k$ не было бы $\mathbf\Phi$-стандартным вопреки теореме 2. Предложение 17 доказано. Предложение 18. Пусть $\mathbf{\Phi}$ – интерпретация формулы $Q$. Тогда, каковы бы ни были вполне негативная $\mathrm{Ar}$-формула $\Phi(x_1,\dots,x_n)$, не содержащая свободных переменных кроме $x_1,\dots,x_n$, и натуральные числа $k_1,\dots,k_n$, $\mathrm{Ar}^*$-формула $\Phi(k_1,\dots,k_n)$ истинна тогда и только тогда, когда pr-реализуема $\mathrm{Ar}^*$-формула $\widetilde{\Phi}(\overline{k_1},\dots,\overline{k_n})$. Доказательство. Индукция по построению $\mathrm{Ar}$-формулы $\Phi(x_1,\dots,x_n)$.
Случай атомарной формулы $\Phi(x_1,\dots,x_n)$ рассмотрен в предложении 12. Доказательство предложения 12 содержит также разбор случая, когда формула $\Phi$ имеет вид $\Psi_1\,\&\,\Psi_2$ и утверждение имеет место для формул $\Psi_1$ и $\Psi_2$. Пусть $\Phi(x_1,\dots,x_n)$ есть $\forall\mathbf y\,(\Psi_1(\mathbf y,x_1,\dots,x_n)\to\Psi_2(\mathbf y,x_1,\dots,x_n))$, где $\mathbf y$ – список переменных $y_1,\dots,y_m$, а $\Psi_1(\mathbf y,x_1,\dots,x_n)$ и $\Psi_2(\mathbf y,x_1,\dots,x_n)$ – вполне негативные $\mathrm{Ar}$-формулы. Индукционное предположение состоит в том, что для любых $\mathbf p,k_1,\dots,k_n$, где $\mathbf p=p_1,\dots,p_m$, формула $\Psi_i(\mathbf p,k_1,\dots,k_n)$ ($i=1,2$) истинна тогда и только тогда, когда pr-реализуема формула $\widetilde{\Psi_i}(\overline{\mathbf p},\overline{k_1},\dots,\overline{k_n})$, где $\overline{\mathbf p}=\overline{p_1},\dots,\overline{p_m}$. $\widetilde{\Phi}(x_1,\dots,x_n)$ есть $\forall\mathbf y\,(\widetilde{\Psi_1}(\mathbf y,x_1,\dots,x_n)\to\widetilde{\Psi_2}(\mathbf y,x_1,\dots,x_n))$. Пусть формула $\Phi(k_1,\dots,k_n)$ истинна. Отсюда следует, что для любого подходящего списка натуральных чисел $\mathbf p$ истинна формула
$$
\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}
$$
Докажем, что pr-реализуема формула $\widetilde{\Phi}(\overline{k_1},\dots,\overline{k_n})$, т. е.
$$
\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
$$
Сначала докажем, что каков бы ни был список $\mathbf l=\ell_1,\dots,\ell_m$, если pr-реализуема формула $\widetilde{\Psi_1}(\mathbf l,\overline{k_1},\dots,\overline{k_n})$, то pr-реализуема формула $\widetilde{\Psi_2}(\mathbf l,\overline{k_1},\dots,\overline{k_n})$. Пусть $\mathbf l$ – такой список натуральных чисел, что формула $\widetilde{\Psi_1}(\mathbf l,\overline{k_1},\dots,\overline{k_n})$ pr-реализуема. По теореме 2 числа в списке $\mathbf l$ $\mathbf{\Phi}$-стандартны. Это означает существование таких натуральных чисел $p_1,\dots,p_m$, что pr-реализуемы формулы $\widetilde{[p_i]}(\ell_i)$ ($i=1,\dots,m$). (Более того, в силу предложения 17 числа $p_1,\dots,p_m$ можно найти эффективно.) Из предложения 8 следует, что pr-реализуемы формулы $\neg\neg\mathcal{E}(\overline{p_i},\ell_i)$. Так как формула $\widetilde{\Psi_1}(\mathbf l,k_1,\dots,k_n)$ pr-реализуема, из предложения 7 следует, что pr-реализуема формула $\widetilde{\Psi_1}(\overline{\mathbf p},\overline{k_1},\dots,\overline{k_n})$, где $\overline{\mathbf p}$ есть список $\overline{p_1},\dots,\overline{p_m}$. По индукционному предположению формула $\Psi_1(\mathbf p,k_1,\dots,k_n)$ истинна. Так как истинна формула (8.4), отсюда следует, что истинна формула $\Psi_2(\mathbf p,k_1,\dots,k_n)$. По индукционному предположению формула $\widetilde{\Psi_2}(\overline{\mathbf p},\overline{k_1},\dots,\overline{k_n})$ pr-реализуема. Так как pr-реализуемы формулы $\neg\neg\mathcal{E}(\overline{p_i},\ell_i)$ и $\widetilde{A_2}$, отсюда следует, что pr-реализуемы формулы $\neg\neg\mathcal{E}(\ell_i,\overline{p_i})$. Тогда из предложения 7 следует pr-реализуемость формулы $\widetilde{\Psi_2}(\mathbf l,\overline{k_1},\dots,\overline{k_n})$, что и требовалось. В силу предложения 6 $a_{\Psi_2}\,\mathbf{pr}\,\widetilde{\Psi_2}(\mathbf l,\overline{k_1},\dots,\overline{k_n})$. Мы доказали, что каков бы ни был список натуральных чисел $\mathbf l=\ell_1,\dots,\ell_m$, если формула $\widetilde{\Psi_1}(\mathbf l,\overline{k_1},\dots,\overline{k_n})$ pr-реализуема, то $a_{\Psi_2}\,\mathbf{pr}\,\widetilde{\Psi_2}(\mathbf l,\overline{k_1},\dots,\overline{k_n})$. В силу предложения 3 число $\mathsf a_{a_{\Psi_2}}^{m+1}$ pr-реализует формулу $\widetilde{\Phi}(\overline{k_1},\dots,\overline{k_n})$.
Обратно, пусть формула $\widetilde{\Phi}(\overline{k_1},\dots,\overline{k_n})$ pr-реализуема. Отсюда, в частности, следует, что каков бы ни был список натуральных чисел $\mathbf l$, если формула $\widetilde{\Psi_1}(\mathbf l,\overline{k_1},\dots,\overline{k_n})$ pr-реализуема, то pr-реализуема формула $\widetilde{\Psi_2}(\mathbf l,\overline{k_1},\dots,\overline{k_n})$. Докажем, что формула $\Phi(k_1,\dots,k_n)$ истинна, т. е. каков бы ни был список натуральных чисел $\mathbf p$, если формула $\Psi_1(\mathbf p,k_1,\dots,k_n)$ истинна, то истинна формула $\Psi_2(\mathbf p,k_1,\dots,k_n)$. Пусть $\mathbf p$ – такой список натуральных чисел, что формула $\Psi_1(\mathbf p,k_1,\dots,k_n)$ истинна. По индукционному предположению формула $\widetilde{\Psi_1}(\overline{\mathbf p},\overline{k_1},\dots,\overline{k_n})$ pr-реализуема. Как выше отмечалось, в этом случае формула $\widetilde{\Psi_2}(\overline{\mathbf p},\overline{k_1},\dots,\overline{k_n})$ pr-реализуема. По индукционному предположению эта формула истинна, что и требовалось доказать. Предложение 18 доказано. Теорема 3. По всякой замкнутой вполне негативной $\mathrm{Ar}$-формуле $\Psi$ можно эффективно построить замкнутую предикатную формулу $\Psi^*$, которая pr-реализуема тогда и только тогда, когда $\Psi$ истинна. Доказательство. Если $\Psi$ – замкнутая вполне негативная $\mathrm{Ar}$-формула, то в качестве $\Psi^*$ возьмем предикатную $\mathrm{Ar}$-формулу $Q\to\Psi$. Покажем, что $\Psi^*$ и есть требуемая формула.
Доказательство. Пусть $\Psi^*$ pr-реализуема. Это означает, что каков бы ни был список $\mathrm{Ar}$-формул $\mathbf\Phi$, допустимый для подстановки в $\Psi^*$, формула $\widetilde{\Psi^*}$ pr-реализуема. В частности, это выполнено, когда $\mathbf\Phi$ есть список формул $S(x,y)$, $A(x,y,z)$, $M(x,y,z)$, $Z(x)$, $E(x,y)$. В этом случае $\widetilde{\Psi^*}$ есть в точности формула $Q\to\Psi$. По теореме 1 формула $Q$ pr-реализуема. Тогда формула $\Psi$ также pr-реализуема. Так как $\Psi$ – вполне негативная формула, из предложения 4 следует ее истинность, что и требовалось доказать. Лемма 1 доказана. Лемма 2. Если замкнутая вполне негативная $\mathrm{Ar}$-формула $\Psi$ истинна, то предикатная формула $\Psi^*$ pr-реализуема. Доказательство. Пусть замкнутая вполне негативная $\mathrm{Ar}$-формула $\Psi$ истинна. Докажем, что предикатная формула $\Psi^*$ pr-реализуема. Пусть $\mathbf{\Phi}$ – список $\mathrm{Ar}$-формул, допустимый для подстановки в $\Psi^*$. Так как $\Psi$ вполне негативна, из предложения 6 следует существование такого числа $a_{\Psi}$, что формула $\widetilde{\Psi}$ pr-реализуема тогда и только тогда, когда $a_{\Psi}\,\mathbf{pr}\,\widetilde{\Psi}$. Докажем, что $\mathsf a_{a_{\Psi}}^1\,\mathbf{pr}\,\widetilde{\Psi^*}$. По определению pr-реализуемости достаточно доказать, что для любого $b$, если $b\,\mathbf{pr}\,\widetilde Q$, то $a_{\Psi}\,\mathbf{pr}\,\widetilde{\Psi}$. Пусть $b\,\mathbf{pr}\,\widetilde Q$. Это означает, что $\mathbf\Phi$ – интерпретация формулы $Q$. В силу предложения 18 формула $\widetilde{\Psi}$ pr-реализуема, поскольку формула $\Psi$ истинна. Как отмечалось выше, в этом случае $a_{\Psi}\,\mathbf{pr}\,\widetilde{\Psi}$, что и требовалось доказать. Лемма 2 доказана. Леммы 1 и 2 дают утверждение теоремы 3. Доказательство. Очевидно, что множество всех истинных вполне негативных замкнутых $\mathrm{Ar}$-формул рекурсивно изоморфно множеству всех истинных замкнутых $\mathrm{Ar}$-формул, которое не является арифметическим по теореме Тарского. Отсюда следует, что множество всех истинных вполне негативных замкнутых $\mathrm{Ar}$-формул также неарифметично. По теореме 3 множество всех истинных вполне негативных замкнутых $\mathrm{Ar}$-формул 1-1-сводимо к множеству всех pr-реализуемых предикатных формул. Отсюда следует, что множество всех pr-реализуемых предикатных формул не является арифметическим. Теорема 4 доказана.
§ 9. ЗаключениеТеорема 4 дает нижнюю оценку сложности предикатной логики примитивно рекурсивной реализуемости. Возникает естественный вопрос о верхней оценке. В связи с этим уместно вспомнить решение этого вопроса для предикатной логики рекурсивной реализуемости по Клини. В работе автора [19] для широкого класса арифметических теорий $T$ доказана общая теорема, что предикатная логика такой теории является $\Pi_1^T$-полной. Из этого результата следует, что предикатная логика рекурсивной реализуемости принадлежит классу $\Pi^0_{\omega+1}$ гиперарифметической иерархии и является полной в этом классе. Можно ожидать, что аналогичное утверждение справедливо и для предикатной логики примитивно рекурсивной реализуемости. Прямое применение указанной общей теоремы невозможно хотя бы потому, что она относится к теориям, для которых корректна интуиционистская логика, а для примитивно рекурсивной реализуемости корректность интуиционистской логики не имеет места. Однако представляется вполне перспективной адаптация известных методов исследования предикатных логик конструктивных арифметических теорий применительно к примитивно рекурсивной реализуемости. 
Цитирование в формате AMSBIB
\RBibitem{Pli23} |
|
||||||||||||||||||||||||||
|
Обратная связь: |
Пользовательское соглашение
|
Регистрация посетителей портала |
Логотипы |
|