| Математические заметки |
|
|
|
|
|
Корректность базисной логики предикатов относительно модифицированного варианта строгой примитивно-рекурсивной реализуемости А. Ю. Коновалов Московский государственный университет им. М. В. Ломоносова
Англоязычная версия:
Mathematical Notes, 2023, Volume 114, Issue 6, Pages DOI: https://doi.org/10.1134/S0001434623110585 
Реферативные базы данных:
 1. ВведениеВ 1945 г. Клини [1] ввел понятие рекурсивной реализуемости для уточнения неформальной интуиционистской семантики арифметических формул на основе теории рекурсивных функций. Основная идея рекурсивной реализуемости заключается в использовании частично рекурсивных функций для определения понятия эффективной операции. Однако в математике изучаются и другие классы вычислимых функций. Представляет интерес рассмотреть варианты реализуемости на основе субрекурсивных классов функций. Одним из таких классов может быть класс всех примитивно-рекурсивных функций. Семантика строгой примитивно-рекурсивной реализуемости для языка формальной арифметики введена Дамняновичем [2]. Этот вид реализуемости совмещает идеи рекурсивной реализуемости и моделей Крипке. Особенностью строгой примитивно-рекурсивной реализуемости является отсутствие в ее определении функций, отличных от примитивно-рекурсивных. Именно в этом смысле она называется строгой. Другой вид примитивно-рекурсивной реализуемости – примитивно-рекурсивная реализуемость по Салехи [3] – не обладает таким свойством. В связи с построением конструктивной математики представляет интерес исследование логических законов, приемлемых с конструктивной точки зрения. В математической логике логические законы выражаются посредством предикатных формул. Предикатная логика строгой примитивно-рекурсивной реализуемости изучалась Паком [4]. Им была доказана ее неарифметичность. Из результатов Дамняновича [2] вытекает корректность интуиционистской логики относительно семантики строгой примитивно-рекурсивной реализуемости. Однако в дальнейшем была обнаружена ошибочность этого утверждения [5]. В работе [6] Плиско показал, что базисная логика высказываний $\mathsf{BPC}$ [7], логика более слабая чем интуиционистская, корректна относительно строгой примитивно-рекурсивной реализуемости. Руйтенбург [8] на основе $\mathsf{BPC}$ построил базисную логику предикатов $\mathsf{BQC}$. В работе [9] нами был получен результат о некорректности исчисления базисной логики предикатов $\mathsf{BQC}$ относительно сильного варианта строгой примитивно-рекурсивной реализуемости. Отрицательный результат, полученный нами в работе [9], связан с тем, что оригинальная строгая примитивно-рекурсивная реализуемость Дамняновича не учитывает специфические особенности языка исчисления $\mathsf{BQC}$. В настоящей работе мы приспособим определение строгой примитивно-рекурсивной реализуемости к языку базисной логики предикатов $\mathsf{BQC}$ и докажем корректность исчисления $\mathsf{BQC}$ относительно получившегося варианта строгой примитивно-рекурсивной реализуемости. 2. Иерархия примитивно-рекурсивных функцийВ настоящем пункте мы введем необходимые обозначения для иерархии Гжегорчика [10] примитивно-рекурсивных функций, улучшенной Акстом [11]. Будем использовать следующую общеупотребительную символику для замены слов и словосочетаний естественного языка: $\rightleftharpoons$ – “есть по определению”; $\forall\,$ – “для всех”; $\exists$ – “существует”; $\Longleftrightarrow$ – “тогда и только тогда, когда”; $\Longrightarrow$ – “если $\dots$, то $\dots$”. Посредством $\mathbb N$ обозначаем множество натуральных чисел $\{0, 1, 2, \dots\}$. Примитивно-рекурсивными называют функции натурального аргумента, которые могут быть получены с помощью операций подстановки и рекурсии из следующих исходных функций: функции-константы $O(x)=0$, функции прибавления единицы $S(x)=x+1$ и семейства функций проекции
$$
\begin{equation*}
I^n_i(x_1, \dots, x_n)=x_i, \qquad n=1, 2,\dots, \quad 1 \leqslant i \leqslant n.
\end{equation*}
\notag
$$
Пусть $p_1, p_2, \dots$ – последовательность всех простых чисел. Через $\langle a_1, \dots, a_n \rangle$ обозначаем натуральное число $p_1^{a_1}\dotsb p_n^{a_n}$. Для каждого $i \geqslant 1$ определим “обратную” функцию $\mathsf p_i$: $\mathsf p_i(a)$ есть степень простого числа $p_i$ при разложении натурального числа $a$ на простые множители. Условимся считать, что $\mathsf p_i(0)=0$ для любого $i$. В дальнейшем будем выражения вида $\mathsf p_i(t)$ часто писать без скобок: $\mathsf p_i t$. Будем использовать следующее обозначение для функций-констант:
$$
\begin{equation*}
\mathsf c^n_a(x_1, \dots, x_n)=a, \qquad n \geqslant 1, \quad a \geqslant 0.
\end{equation*}
\notag
$$
Введем обозначения для функций сигнум и усеченной разности:
$$
\begin{equation*}
\mathsf{sg}(x)= \begin{cases} 0, & \text{если } x=0, \\ 1, & \text{если } x > 0, \end{cases} \qquad x \ominus y= \begin{cases} x-y, & \text{если } x > y, \\ 0, & \text{если } x \leqslant y. \end{cases}
\end{equation*}
\notag
$$
Функции $\{f_n\}_{n \geqslant 0}$ определяются в [10; § 4] следующими соотношениями:
$$
\begin{equation*}
\begin{aligned} \, f_0(x, y) =y+1, \qquad f_1(x, y)=x+y, \qquad f_2(x, y)=(x+1) \cdot (y+1), \\ f_n(0, y) =f_{n-1}(y+1, y+1), \quad f_n(x+1, y)=f_n(x, f_n(x, y)) \qquad \text{для}\quad n \geqslant 3. \end{aligned}
\end{equation*}
\notag
$$
Последовательность функций $\{f_n\}_{n \geqslant 0}$ служит в [10] для определения иерархии Гжегорчика классов примитивно-рекурсивных функций $\{\mathcal{E}^n\}_{n \geqslant 0}$. При этом каждая функция $f_n$ принадлежит соответствующему классу $\mathcal{E}^n$, а функция $f_{n+1}(x, x)$ растет быстрее всякой функции из класса $\mathcal{E}^n$ [10; теорема 4.9]. Мы будем использовать альтернативную иерархию классов примитивно-рекурсивных функций $\{\mathbf E_n\}_{n \geqslant 0}$, введенную в работе [11]. При этом в [11; с. 58] было доказано, что имеет место $\mathbf E_n= \mathcal{E}^{n+4}$ для всех $n \geqslant 0$. Будем говорить, что функция $\varphi(z, \overline x)$ получена ограниченной рекурсией (по Аксту) из функций $\psi(\overline x)$, $\chi(z, y, \overline x)$ и $\xi(z, \overline x)$, если имеет место следующее:
$$
\begin{equation*}
\begin{aligned} \, \varphi(0, \overline x) &=\psi(\overline x), \\ \varphi(z+1, \overline x) &=\chi\bigl(z, \varphi(z, \overline x), \overline x\bigr) \cdot \mathsf{sg}(\varphi(z, \overline x))\cdot \mathsf{sg}\bigl(\xi(z, \overline x) \ominus \varphi(z, \overline x)\bigr). \end{aligned}
\end{equation*}
\notag
$$
Пусть $\Theta=\{\theta_1, \dots, \theta_m\}$ – конечное множество функций натурального аргумента. Посредством $\mathbf E^4(\Theta)$ будем обозначать наименьший замкнутый относительно подстановки и ограниченной рекурсии класс функций, который содержит все функции из $\Theta$, а также следующие базовые функции:
$$
\begin{equation*}
S, \quad \mathsf{sg}, \quad \ominus, \quad f_4, \quad I^n_i, \quad \mathsf c^n_a, \qquad n \geqslant 1, \quad 1 \leqslant i \leqslant n, \quad a \geqslant 0.
\end{equation*}
\notag
$$
Определим нумерацию функций из класса $\mathbf E^4(\Theta)$ индукцией по построению функций из этого класса:
$$
\begin{equation*}
\mathsf u^\Theta(e, a) \rightleftharpoons \begin{cases} \varphi^\Theta_e(\mathsf p_1 a, \dots, \mathsf p_{(\mathsf p_2 e)} a), & \text{если } e \in \mathsf I^\Theta, \\ 0 & \text{иначе}. \end{cases}
\end{equation*}
\notag
$$
Таким образом, функция $\mathsf u^\Theta$ является универсальной для класса $\mathbf E^4(\Theta)$ в том смысле, что выполняется соотношение
$$
\begin{equation*}
\varphi^\Theta_e(a_1, \dots, a_n)=\mathsf u^\Theta(e, \langle a_1, \dots, a_n \rangle)
\end{equation*}
\notag
$$
для всех натуральных чисел $a_1, \dots, a_n$ и $e \in \mathsf I^\Theta_n$. Используя диагональный метод (рассмотрев функцию $\mathsf u^\Theta(x, \langle x \rangle)+1$), можно показать, что функция $\mathsf u^\Theta$ не принадлежит классу $\mathbf E^4(\Theta)$. Определим иерархию классов $\mathbf E^4(\Theta_0) \subseteq \mathbf E^4(\Theta_1) \subseteq \dotsb$, задав последовательность множеств $\Theta_0 \subseteq \Theta_1 \subseteq \dotsb$ следующим образом:
$$
\begin{equation*}
\Theta_0 \rightleftharpoons \varnothing,\quad \Theta_1 \rightleftharpoons \{\mathsf u^{\Theta_0}\},\quad \dots,\quad \Theta_{i} \rightleftharpoons \Theta_{i-1} \cup \{\mathsf u^{\Theta_{i-1}}\},\quad\dots\,.
\end{equation*}
\notag
$$
В дальнейшем мы будем использовать следующие сокращения:
$$
\begin{equation*}
\mathbf E_i \rightleftharpoons \mathbf E^4(\Theta_i), \qquad \mathsf I^i \rightleftharpoons \mathsf I^{\Theta_i}, \qquad \mathsf I^i_n \rightleftharpoons \mathsf I^{\Theta_i}_n, \qquad \varphi^i_e \rightleftharpoons \varphi^{\Theta_i}_e.
\end{equation*}
\notag
$$
Предложение 1. Объединение $\bigcup_{i=0}^{\infty} \mathbf E_i$ есть в точности множество всех примитивно-рекурсивных функций. Доказательство см. [10; теорема 4.13], [11; теорема на с. 58]. Введем обозначения для следующих функций:
$$
\begin{equation*}
\mathsf t^n(x_1, \dots, x_n)=\langle x_1, \dots, x_n \rangle; \qquad \mathsf{if}(z, x, y)= \begin{cases} x, & \text{если } z=0, \\ y & \text{иначе}. \end{cases}
\end{equation*}
\notag
$$
Предложение 2. Функции $\mathsf{if}, \mathsf p_n, \mathsf t^n$, $n \geqslant 1$, а также функции сложения, умножения и возведения в степень принадлежат классу $\mathbf E_0$. Доказательство см. [12; предложение 2]. Выше нами для части функций из класса $\mathbf E_0$ или введены обозначения, такие как $\ominus$, $f_4$, $\mathsf c^n_a$, $\mathsf{if}, \mathsf p_n$, или используется более-менее общеупотребительная символика: $+$, $\cdot$, $S$, $I^n_i$, $\mathsf{sg}$ и т.п. Пусть $\mathfrak{E}_0$ – множество всех используемых нами обозначений для функций из класса $\mathbf E_0$, которое мы считаем открытым для возможных добавлений. Подмножество множества $\mathfrak{E}_0$ обозначений для всех $n$-местных функций обозначаем $\mathfrak{E}^n_0$. Для каждого обозначения $g \in \mathfrak{E}_0$ фиксируем некоторый номер $\Lambda[g] \in \mathsf I^0$ соответствующей функции $g$. При этом без ограничения общности будем считать, что для базовых функций класса $\mathbf E_0$ фиксирован именно тот номер, который фигурирует выше в определении нумерации классов вида $\mathbf E^4(\Theta)$. Таким образом, например, $\Lambda[\mathsf{sg}]=\langle 4, 1 \rangle=2^4 \cdot 3^1=48$. 3. $\Lambda$-Выражения для примитивно-рекурсивных функцийПри исследовании семантик реализуемости, базирующихся на иерархии классов $\{\mathbf E_n\}_{n \geqslant 0}$, возникает потребность в упрощении термов, построенных на основании универсальных функций для этих классов. Такие термы мы в дальнейшем называем $\varphi$-термами. Техническую трудность представляет тот факт, что универсальная функция для каждого из классов $\mathbf E_n$ сама не принадлежит этому классу. Тем самым, отсутствует общий метод, который бы позволял сводить $\varphi$-терм, построенный на основании универсальных функций для классов $\mathbf E_1, \dots, \mathbf E_n$, к примитивно-рекурсивной функции из класса $\mathbf E_n$. В работе [12] автором была разработана техника, позволяющая решать эту проблему для $\varphi$-термов специального вида. В настоящем пункте мы сформулируем определения и изложим основные результаты работы [12], видоизменив некоторые обозначения. А именно, при записи $\varphi$-термов будем использовать обозначение $\{z\}^n(x_1, \dots, x_m)$ вместо $\varphi^n_z(x_1, \dots, x_m)$. Назовем $\varphi$-атомами предметные переменные и натуральные числа. Будем говорить, что выражение $t$ есть $\varphi$-терм, если выполняется одно из следующих условий:
$$
\begin{equation*}
\mathsf p_1(x), \qquad +(x, 1), \qquad \mathsf t^3(x, y, z), \qquad \{z\}^y(x), \qquad \{\{z\}^0(y)\}^w(x, 2).
\end{equation*}
\notag
$$
При записи $\varphi$-термов будем допускать некоторые сокращения. Например, первые три $\varphi$-терма из списка выше будем записывать так: $ \mathsf p_1 x,\ x+1,\ \langle x, y, z \rangle. $ Множество всех предметных переменных, входящих в $\varphi$-терм $t$, обозначаем через $\operatorname{Var}(t)$. Будем называть замкнутыми те $\varphi$-термы, которые не содержат предметных переменных. Для каждого замкнутого $\varphi$-терма $t$ определим его значение $\mathsf v(t) \in \mathbb N \cup \{-1\}$. Будем писать $!t$, если $\mathsf v(t) \not=-1$. В этом случае будем говорить, что значение $\varphi$-терма $t$ определено. Итак, положим по определению
$$
\begin{equation*}
\begin{gathered} \, \mathsf v(a) \rightleftharpoons a, \qquad\text{если}\quad a \,-\,\text{натуральное число}, \\ \mathsf v(g(t_1, \dots, t_n)) \rightleftharpoons \begin{cases} g(\mathsf v(t_1), \dots, \mathsf v(t_n)), & \text{если } !t_1, \dots, !t_n, \\ -1 & \text{иначе}, \end{cases} \qquad\text{где}\quad g \in \mathfrak{E}^n_0, \\ \mathsf v(\{s\}^j(t_1, \dots, t_n)) \rightleftharpoons \begin{cases} \varphi^j_{\mathsf v(s)}(\mathsf v(t_1), \dots, \mathsf v(t_n)), &\text{если }!s,!t_1,\dots,!t_n \text{ и } \mathsf v(s)\in\mathsf I^j_n, \\ -1& \text{иначе.} \end{cases} \end{gathered}
\end{equation*}
\notag
$$
Иногда, там, где это не создает путаницы, будем писать просто $t$ вместо $\mathsf v(t)$. Через $t[\overline x \to \overline u]$ обозначаем результат подстановки $\varphi$-атомов $\overline u=u_1, \dots, u_n$ в $\varphi$-терм $t$ вместо всех вхождений переменных $\overline x=x_1, \dots, x_n$ соответственно. Если $\overline t=t_1, \dots, t_n$ – $\varphi$-термы, то посредством $\overline t[\overline x \to \overline u]$ обозначаем список $\varphi$-термов
$$
\begin{equation*}
t_1[\overline x \to \overline u], \quad\dots,\quad t_n[\overline x \to \overline u].
\end{equation*}
\notag
$$
Пусть $t_1,t_2$ – $\varphi$-термы, все переменные которых содержатся среди списка переменных $\overline x=x_1, \dots, x_n$. Будем говорить, что $\varphi$-термы $t_1$ и $t_2$ условно равны, и писать $t_1 \simeq t_2$, если имеет место
$$
\begin{equation}
\mathsf v\bigl(t_1[\overline x \to \overline k]\bigr)=\mathsf v\bigl(t_2[\overline x \to \overline k]\bigr)
\end{equation}
\tag{3.1}
$$
для всех натуральных чисел $\overline k=k_1, \dots, k_n$. Нетрудно показать, что отношение $\simeq$ не зависит от выбора списка переменных $x_1, \dots, x_n$. Для каждого $\varphi$-терма $t$ определим его высоту $h(t)$ следующим образом:
Для каждых $\varphi$-терма $t$ и натурального числа $i$ определим множество $\operatorname{In}^i(t)$ верхних индексов $\varphi$-терма $t$ на уровне $i$:
Для каждых $\varphi$-терма $t$ и натурального числа $i$ определим множество $\operatorname{Arg}^i(t)$ неиндексных переменных $\varphi$-терма $t$ на уровне $i$:
Пусть $t$ – $\varphi$-терм, $\overline x=x_1, \dots, x_m$ – список предметных переменных. Определим $\varphi$-терм $\Lambda \overline x.\,t$ индукцией по построению $\varphi$-терма $t$:
Отметим, что если переменная $y$ не входит в список $\overline x$, то для всех натуральных чисел $a$ имеет место $\mathsf v((\Lambda \overline x.\,y)[y \to a])=\Lambda[\mathsf c^m_a]$. Мы хотим, чтобы значение $\varphi$-терма $\Lambda \overline x.\,t(\overline x)$ было номером примитивно-рекурсивной функции, которая по набору натуральных чисел $\overline a$ выдает значение терма $t(\overline a)$. Ниже мы найдем условия на $t(\overline x)$, при которых значение $\varphi$-терма $\Lambda \overline x. t(\overline x)$ определено и является номером соответствующей примитивно-рекурсивной функции. Пусть $t$ – $\varphi$-терм и $\operatorname{Var}(t) \subseteq \{x_1, \dots, x_n\}$. Будем писать $f(x_1, \dots, x_n) :=t$ всякий раз, когда нам потребуется ввести обозначение для функции $f$ типа $\mathbb N^n \to \mathbb N$, определяемой следующим соотношением:
$$
\begin{equation*}
f(a_1, \dots, a_n)= \begin{cases} \mathsf v(t[x_1, \dots, x_n \to a_1,\dots, a_n]), & \text{если } !t[x_1, \dots, x_n \to a_1,\dots, a_n], \\ \text{не определено} & \text{иначе.} \end{cases}
\end{equation*}
\notag
$$
При этом будем говорить, что $\varphi$-терм $t$ определяет функцию $f$. Следующая теорема дает условия, при которых $\varphi$-терм вида $\Lambda \overline x_n \dots \Lambda \overline x_0.\,t$ определяет функцию из $\mathbf E_0$, которая при этом ведет себя в соответствии с интуитивным смыслом выражения $\Lambda \overline x_n \dots \Lambda \overline x_0.\,t$. Теорема 1. Пусть $t$ – $\varphi$-терм, $u_0, \dots, u_n$ – $\varphi$-атомы, $\overline x_0, \dots, \overline x_n, \overline y$ – списки предметных переменных и выполняются следующие условия: Доказательство см. [12; теорема 1]. 4. Базисная логика предикатов $\mathsf{BQC}$Атомарными предикатными формулами назовем логические константы $\top$ (истина) и $\bot$ (ложь), а также выражения вида $P(v_1,\dots,v_n)$, где $P$ – $n$-местная предикатная переменная, а $v_1,\dots,v_n$ – предметные переменные. Понятие предикатной формулы в базисной логике предикатов $\mathsf{BQC}$ несколько отличается от общепринятого в интуиционистской или классической логиках. А именно, предикатные формулы строятся из атомарных при помощи логических связок $\land,\ \lor,\ \to$ и кванторов $\forall\,,\ \exists$, но при этом все вхождения квантора всеобщности в предикатную формулу должны иметь вид $\forall\, x_1, \dots, \forall\, x_n\,(A \to B)$. Для выражений вида $\forall\, x_1 \dots \forall\, x_n\,A$ будем использовать сокращение $\forall\, x_1 \dots x_n\,A$. Секвенциями языка логики предикатов называются выражения вида $\Phi \Rightarrow \Psi$, где $\Phi$ и $\Psi$ – предикатные формулы. Базисная логика высказываний $\mathsf{BPC}$ введена Виссером [7]. Это подсистема интуиционистского исчисления высказываний, в которой ослаблено правило вывода modus ponens. Руйтенбург [8] на основе $\mathsf{BPC}$ построил базисную логику предикатов $\mathsf{BQC}$. Мы будем рассматривать исчисление $\mathsf{BQC}$ в языке логики предикатов без констант и функциональных символов. Базисная логика предикатов $\mathsf{BQC}$ – это секвенциальное исчисление со следующими схемами аксиом: A1) $A \Rightarrow A$; A2) $A \Rightarrow \top$; A3) $\bot \Rightarrow A$; A4) $A\land \exists\, x\,B \Rightarrow \exists\, x\,(A\land B)$, где переменная $x$ не свободнa в $A$; A5) $A\land (B\lor C) \Rightarrow (A\land B)\lor (A\land C)$; A6) $\forall\, \overline x\,(A\to B)\land \forall\, \overline x\,(B\to C) \Rightarrow \forall\,\overline x\,(A\to C)$; A7) $\forall\, \overline x\,(A\to B)\land \forall\, \overline x\,(A\to C) \Rightarrow \forall\, \overline x\,(A\to B\land C)$; A8) $\forall\, \overline x\,(B\to A)\land \forall\, \overline x\,(C\to A) \Rightarrow \forall\, \overline x\,(B\lor C\to A)$; A9) $\forall\, \overline x\,(A(\overline x) \to B(\overline x)) \Rightarrow \forall\, \overline x\,(A(\overline y) \to B(\overline y))$; A10) $\forall\, \overline x (A \to B) \Rightarrow\forall\, \overline z (A \to B)$, где переменные из списка $\overline z$ не входят свободно в левую часть секвенции; A11) $\forall\, \overline x,y\,(B\to A) \Rightarrow \forall\, \overline x\,(\exists\, y\, B\to A)$, где переменная $y$ не свободнa в $A$. Правилами вывода исчисления $\mathsf{BQC}$ являются: R1) $\dfrac{A\Rightarrow B\; B\Rightarrow C}{A\Rightarrow C}$; R2) $\dfrac{A\Rightarrow B\; A\Rightarrow C}{A\Rightarrow B\land C}$; R3) $\dfrac{A\Rightarrow B\land C}{A\Rightarrow B}$ (а), $\quad$ $\dfrac{A\Rightarrow B\land C}{A\Rightarrow C}$ (б); R4) $\dfrac{B\Rightarrow A\; C\Rightarrow A}{B\lor C\Rightarrow A}$; R5) $\dfrac{B\lor C\Rightarrow A}{B\Rightarrow A}$ (а), $\quad$ $\dfrac{B\lor C\Rightarrow A}{C\Rightarrow A}$ (б); R6) $\dfrac{A(\overline x) \Rightarrow B(\overline y)}{ A(\overline y) \Rightarrow B(\overline y)}$; R7) $\dfrac{B\Rightarrow A}{\exists\, x\, B\Rightarrow A}$, где переменная $x$ не свободнa в $A$; R8) $\dfrac{\exists\, x\,B\Rightarrow A}{B\Rightarrow A}$, где переменная $x$ не свободнa в $A$; R9) $\dfrac{A\land B\Rightarrow C}{A\Rightarrow \forall\, \overline x\ (B\to C)}$, где каждая переменная из списка $\overline x$ не свободнa в $A$. Говорят, что секвенция $S$ языка логики предикатов выводится в исчислении $\mathsf{BQC}$, если секвенция $S$ является аксиомой или может быть получена из аксиом конечным применением правил вывода. Выводимость секвенции $S$ в исчислении $\mathsf{BQC}$ обозначаем так: $\mathsf{BQC} \vdash S$. Будем говорить, что в исчислении $\mathsf{BQC}$ выводится формула $A$, если имеет место $\mathsf{BQC} \vdash \top \Rightarrow A$. 5. Строгая примитивно-рекурсивная реализуемостьПонятие строгой примитивно-рекурсивной реализуемости определяется в [2] для формул языка формальной арифметики. Мы рассматриваем язык арифметики $LA$, содержащий функциональные символы для всех примитивно-рекурсивных функций и константы для обозначения всех натуральных чисел. Атомами языка $LA$ назовем логические константы $\top$ (истина), $\bot$ (ложь), а также выражения вида $t_1=t_2$, где $t_1,t_2$ – термы языка $LA$. Формулы языка $LA$ строятся обычным образом из атомов при помощи логических связок $\land$, $\lor$, $\to$ и кванторов $\exists$, $\forall$. Термы и формулы языка $LA$ называем соответственно арифметическими термами и арифметическими формулами. Выражение $\forall\, \overline x\,A$, где $\overline x=x_1, \dots, x_n$, а $A$ – арифметическая формула, условимся считать сокращением для формулы $\forall\, x_1 \dots \forall\, x_n\,A$. Пусть $\overline x=x_1, \dots, x_n$ – список переменных, $\overline t=t_1, \dots, t_n$ – арифметические термы, $A$ – арифметическая или предикатная формула. Через $[\overline t / \overline x]\,A$ обозначаем результат подстановки термов $t_1, \dots, t_n$ вместо всех свободных вхождений переменных $x_1, \dots, x_n$ в формулу $A$ соответственно. При этом считаем, что предварительно происходит переименование связанных переменных в формуле $A$ таким образом, чтобы каждый терм из списка $\overline t$ был свободен для соответствующей переменной из списка $\overline x$ в формуле $A$ (см. [13; § 34]). Тот факт, что в формуле $A$ отсутствуют свободные переменные, отличные от $x_1, \dots, x_n$, будем отражать, записывая формулу $A$ как $A(x_1, \dots, x_n)$. При этом выражение $A(t_1, \dots, t_n)$ рассматривается нами как альтернативная запись для формулы $[\overline t / \overline x]\,A$. Через $A(P_1,\dots,P_n)$ будем обозначать предикатную формулу, не содержащую предикатных переменных, отличных от $P_1,\dots,P_n$. Пусть $\Phi_1,\dots,\Phi_n$ – некоторый список формул языка $LA$, причем каждая из формул $\Phi_i$, $i=1,\dots,n$, не содержит свободных переменных, отличных от $x_1, \dots, x_m$, если $P_i$ есть $m$-местная предикатная переменная. В этом случае через $A(\Phi_1,\dots,\Phi_n)$ обозначим формулу языка $LA$, полученную заменой в $A(P_1,\dots,P_n)$ каждой атомарной подформулы вида $P_i(t_1, \dots, t_m)$ на формулу $[t_1, \dots ,t_m / x_1,\dots,x_m]\,\Phi_i$. Формулы вида $A(\Phi_1,\dots,\Phi_n)$ будем называть арифметическими примерами предикатной формулы $A(P_1,\dots,P_n)$. Очевидно, что если формула $A(P_1,\dots,P_n)$ замкнута, то всякий ее арифметический пример также является замкнутым. Согласно [9] для натуральных чисел $e,i$ и замкнутой формулы $A$ языка $LA$ определим отношение $e \,\mathbf r^0_i\, A$ индукцией по построению формулы $A$:
Отношение $e \,\mathbf r^0_i\, A$ эквивалентно строгой примитивно-рекурсивной реализуемости Дамняновича [2] в части множества реализуемых формул [9; предложение 4]. Вместо отношения $e \,\mathbf r^0_i\, A$ мы будем рассматривать его модификацию $e \,\mathbf{r}'_i\, A$, рекурсивное определение которой отличается от данного выше для случаев $\Phi \to \Psi$ и $\forall\, x\ \Phi(x)$. При этом будем учитывать особенности, присущие формулам языка базисной логики предикатов $\mathsf{BQC}$, подобно тому, как мы делали это в работах [14]–[21], посвященных другим видам реализуемости. Итак,
Замкнутую формулу $\Phi$ языка $LA$ назовем $\mathsf{spr}'$-реализуемой, если существуют такие натуральные числа $e$ и $i$, что $e \,\mathbf{r}'_i\, \Phi$. Будем говорить, что предикатная формула $A$ является сильно $\mathsf{spr}'$-реализуемой, если найдутся такие натуральные числа $e$ и $i$, что имеет место $e \,\mathbf{r}'_i\, A'$ для любого арифметического примера $A'$ формулы $A$. Предложение 3. Пусть $A$ – замкнутая формула языка $LA$. Тогда верно для всех натуральных чисел $e, i$ и $j \geqslant i$. Секвенциями языка $LA$ называются выражения вида $\Phi \Rightarrow \Psi$, где $\Phi$ и $\Psi$ – формулы языка $LA$. Будем говорить, что список переменных $\overline x$ допустим для секвенции $\Phi \Rightarrow \Psi$, если все свободные переменные формул $\Phi$ и $\Psi$ содержатся среди переменных списка $\overline x$. Распространим отношение $\mathbf{r}'_i$ на секвенции языка $LA$ согласно [6]:
$$
\begin{equation*}
f\,\mathbf{r}'_i\, \Phi(\overline x) \Rightarrow \Psi(\overline x) \rightleftharpoons f \in \mathbf E^{n+1}_i \text{ и } \forall\, k_1, \dots, k_n, e \ \forall\, j \geqslant i\,\bigl( e \,\mathbf{r}'_j\, \Phi(\overline k) \Longrightarrow f(\overline k, e) \,\mathbf{r}'_j\, \Psi(\overline k)\bigr),
\end{equation*}
\notag
$$
где $\overline x$ – допустимый для $\Phi \Rightarrow \Psi$ список переменных длины $n$, $\overline k$ – натуральные числа $k_1, \dots, k_n$, а $f$ – $(n+1)$-местная примитивно-рекурсивная функция. Покажем, что данное определение в некотором смысле не зависит от выбора списка переменных $\overline x$. Лемма 1. Пусть список переменных $\overline x=x_1, \dots, x_n$ допустим для секвенции $A \Rightarrow B$ языка $LA$, а список переменных $\overline z=z_1, \dots, z_m$ не имеет со списком $\overline x$ общих переменных. Тогда для каждой примитивно-рекурсивной функции $f$ найдется такая примитивно-рекурсивная функция $f'$, что для всех натуральных чисел $i$ имеет место тогда и только тогда, когда Доказательство. Определим функцию $f'$ следующей подстановкой: Утверждение леммы вытекает из того факта, что $f'(\overline x, \overline z, y)=f(\overline x, y)$. Лемма 2. В условиях леммы 1 для каждой примитивно-рекурсивной функции $f$ найдется такая примитивно-рекурсивная функция $f'$, что для всех натуральных чисел $i$ имеет место тогда и только тогда, когда верно Доказательство. Определим функцию $f'$ следующей подстановкой: Утверждение леммы следует из того факта, что $f'(\overline x, y)= f(\overline x, 0, \dots, 0, y)$. Лемма 3. Пусть список переменных $\overline x=x_1, \dots, x_n$ допустим для секвенции $A \Rightarrow B$ языка $LA$ и $p$ – перестановка на $\{1, \dots, n\}$. Тогда для каждой примитивно-рекурсивной функции $f$ найдется такая примитивно-рекурсивная функция $f'$, что для всех натуральных чисел $i$ имеет место тогда и только тогда, когда верно Доказательство. Определим функцию $f'$ следующей подстановкой: Утверждение леммы следует из того факта, что $f'(\overline x, y)= f(p(\overline x), y)$. Из лемм 1–3 получаем следующее Предложение 4. Пусть списки переменных $\overline x$ и $\overline y$ допустимы для секвенции $S$ языка $LA$. Тогда для каждой примитивно-рекурсивной функции $f$ найдется такая примитивно-рекурсивная функция $f'$, что для всех натуральных чисел $i$ имеет место тогда и только тогда, когда верно 6. Основной результатТеорема 2. Пусть $\mathsf{BQC} \vdash S$ и список переменных $\overline r=r_1, \dots, r_l$ допустим для секвенции $S$. Тогда найдется такая функция $f \in \mathbf E^{l+1}_0$, что для любого арифметического примера $S'$ секвенции $S$ имеет место $f\,\mathbf{r}'_0\,S'$. Доказательство. Индукция по длине вывода секвенции $S$.
Рассмотрим все случаи, когда секвенция $S$ является аксиомой исчисления $\mathsf{BQC}$. Случай A1. Пусть секвенция $S$ есть $A(\overline r) \Rightarrow A(\overline r)$. Тогда $f(\overline r, z) :=z$. Случай A2. Пусть секвенция $S$ есть $A(\overline r) \Rightarrow \top$. Тогда $f(\overline r, z) :=z$. Случай A3. Пусть секвенция $S$ есть $\bot \Rightarrow A(\overline r)$. Тогда $f(\overline r, z) :=z$. Случай A4. Пусть секвенция $S$ есть
$$
\begin{equation*}
A(\overline r) \land \exists\, x\, B(x, \overline r) \Rightarrow \exists\, x\,\bigl(A(\overline r) \land B(x, \overline r)\bigr).
\end{equation*}
\notag
$$
Тогда
$$
\begin{equation*}
f(\overline r, z) :=\bigl\langle \mathsf p_1\mathsf p_2 z, \langle \mathsf p_1 z, \mathsf p_2 \mathsf p_2 z \rangle\bigr \rangle.
\end{equation*}
\notag
$$
Случай A5. Пусть секвенция $S$ есть
$$
\begin{equation*}
A(\overline r) \land \bigl(B(\overline r) \lor C(\overline r)\bigr) \Rightarrow \bigl(A(\overline r) \land B(\overline r)\bigr) \lor \bigl(A(\overline r) \land C(\overline r)\bigr).
\end{equation*}
\notag
$$
Тогда
$$
\begin{equation*}
f(\overline r, z) :=\bigl\langle \mathsf p_1\mathsf p_2 z, \langle \mathsf p_1 z, \mathsf p_2 \mathsf p_2 z \rangle \bigr\rangle.
\end{equation*}
\notag
$$
Случай A6. Пусть секвенция $S$ есть
$$
\begin{equation*}
\forall\, \overline x\,\bigl(A(\overline x, \overline r)\to B(\overline x, \overline r)\bigr) \land \forall\, \overline x\,\bigl(B(\overline x, \overline r)\to C(\overline x, \overline r)\bigr) \Rightarrow \forall\,\overline x\,\bigl(A(\overline x, \overline r)\to C(\overline x, \overline r)\bigr),
\end{equation*}
\notag
$$
где $\overline x=x_1, \dots, x_n$. Определим функцию $f \in \mathbf E^{l+1}_0$ следующим образом:
$$
\begin{equation}
f(\overline r, z) := \Lambda v.\Lambda \overline x, q.\{\{\mathsf p_2 z\}^w(v)\}^v\bigl(\overline x, \{\{\mathsf p_1 z\}^w(v)\}^v(\overline x, q)\bigr).
\end{equation}
\tag{6.1}
$$
Предположим, что $A', B', C'$ – арифметические примеры формул $A, B, C$ и имеет место
$$
\begin{equation}
d \,\mathbf{r}'_i\, \forall\, \overline x\,\bigl(A'(\overline x, \overline k)\to B'(\overline x, \overline k)\bigr) \land \forall\, \overline x\,\bigl(B'(\overline x, \overline k)\to C'(\overline x, \overline k)\bigr)
\end{equation}
\tag{6.2}
$$
для некоторых натуральных чисел $d$, $i$, $\overline k=k_1, \dots, k_l$. И пусть верно для некоторых натуральных чисел $\overline a, q$ и $j \geqslant i$. Из (6.2), (6.3) следует
$$
\begin{equation}
\{\{\mathsf p_1 d\}^i(j)\}^j(\overline a, q) \,\mathbf{r}'_j\, B'(\overline a, \overline k).
\end{equation}
\tag{6.4}
$$
Из (6.2), (6.4) получаем
$$
\begin{equation}
\{\{\mathsf p_2 d\}^i(j)\}^j\bigl(\overline a, \{\{\mathsf p_1 d\}^i(j)\}^j(\overline a, q)\bigr) \,\mathbf{r}'_j\, C'(\overline a, \overline k).
\end{equation}
\tag{6.5}
$$
Применением теоремы 1 из (6.1), (6.5) получаем
$$
\begin{equation}
\{\{f(\overline k, d)\}^i(j)\}^j(\overline a, q) \,\mathbf{r}'_j\, C'(\overline a, \overline k).
\end{equation}
\tag{6.6}
$$
Таким образом, для всех натуральных чисел $q, \overline a$ и $j \geqslant i$ всякий раз, когда верно (6.3), выполняется и (6.6). Следовательно, имеет место
$$
\begin{equation}
f(\overline k, d) \,\mathbf{r}'_i\, \forall\,\overline x\,\bigl(A'(\overline x, \overline k)\to C'(\overline x, \overline k)\bigr).
\end{equation}
\tag{6.7}
$$
Получаем, что для всех натуральных чисел $\overline k, d, i$ имеет место (6.7) всякий раз, когда верно (6.2). Таким образом, $f\,\mathbf{r}'_0\,S'$ для любого арифметического примера секвенции $S$.
Случай A7. Пусть секвенция $S$ имеет вид
$$
\begin{equation*}
\forall\, \overline x\,\bigl(A(\overline x, \overline r)\to B(\overline x, \overline r)\bigr) \land \forall\, \overline x\,\bigl(A(\overline x, \overline r)\to C(\overline x, \overline r)\bigr) \Rightarrow \forall\, \overline x\,\bigl(A(\overline x, \overline r)\to B(\overline x, \overline r)\land C(\overline x, \overline r)\bigr),
\end{equation*}
\notag
$$
где $\overline x=x_1, \dots, x_n$. Легко показать, что утверждение теоремы выполняется для функции $f \in \mathbf E^{l+1}_0$, определенной следующим образом:
$$
\begin{equation*}
f(\overline r, z) := \Lambda v.\Lambda \overline x, q. \bigl\langle \{\{\mathsf p_1 z\}^w(v)\}^v(\overline x, q),\ \{\{\mathsf p_2 z\}^w(v)\}^v(\overline x, q) \bigr\rangle.
\end{equation*}
\notag
$$
Случай A8. Пусть секвенция $S$ есть
$$
\begin{equation*}
\forall\, \overline x\,\bigl(B(\overline x, \overline r)\to A(\overline x, \overline r)\bigr) \land \forall\, \overline x\,\bigl(C(\overline x, \overline r)\to A(\overline x, \overline r)\bigr) \Rightarrow \forall\, \overline x\,\bigl(B(\overline x, \overline r)\lor C(\overline x, \overline r)\to A(\overline x, \overline r)\bigr),
\end{equation*}
\notag
$$
где $\overline x=x_1, \dots, x_n$. Определим функцию $f \in \mathbf E^{l+1}_0$ следующим образом:
$$
\begin{equation}
f(\overline r, z) :=\Lambda v.\Lambda \overline x, q. \mathsf{if}\bigl(\mathsf p_1 q, \{\{\mathsf p_1 z\}^w(v)\}^v(\overline x, \mathsf p_2 q), \{\{\mathsf p_2 z\}^w(v)\}^v(\overline x, \mathsf p_2 q)\bigr).
\end{equation}
\tag{6.8}
$$
Предположим, что $A', B', C'$ – арифметические примеры формул $A, B, C$ и имеет место
$$
\begin{equation}
d \,\mathbf{r}'_i\, \forall\, \overline x\,\bigl(B'(\overline x, \overline k)\to A'(\overline x, \overline k)\bigr) \land \forall\, \overline x\,\bigl(C'(\overline x, \overline k)\to A'(\overline x, \overline k)\bigr)
\end{equation}
\tag{6.9}
$$
для некоторых натуральных чисел $d, i, \overline k=k_1, \dots, k_l$. И пусть верно
$$
\begin{equation}
q \,\mathbf{r}'_j\, B'(\overline a, \overline k) \lor C'(\overline a, \overline k)
\end{equation}
\tag{6.10}
$$
для некоторых натуральных чисел $\overline a, q$ и $j \geqslant i$. Из (6.10) следует, что либо $\mathsf p_1 q=0$ либо $\mathsf p_1 q=1$. Если $\mathsf p_1 q=0$, то $\mathsf p_2 q \,\mathbf{r}'_j\, B'(\overline a, \overline k)$ и из (6.9) получаем
$$
\begin{equation*}
\{\{\mathsf p_1 d\}^i(j)\}^j(\overline a, \mathsf p_2 q) \,\mathbf{r}'_j\, A'(\overline a, \overline k).
\end{equation*}
\notag
$$
Если $\mathsf p_1 q=1$, то $\mathsf p_2 q \,\mathbf{r}'_j\, C'(\overline a, \overline k)$ и из (6.9) следует
$$
\begin{equation*}
\{\{\mathsf p_2 d\}^i(j)\}^j(\overline a, \mathsf p_2 q) \,\mathbf{r}'_j\, A'(\overline a, \overline k).
\end{equation*}
\notag
$$
Таким образом, в любом из возможных случаев имеет место
$$
\begin{equation}
\mathsf{if}\bigl(\mathsf p_1 q, \{\{\mathsf p_1 d\}^i(j)\}^j(\overline a, \mathsf p_2 q), \{\{\mathsf p_2 d\}^i(j)\}^j(\overline a, \mathsf p_2 q)\bigr) \,\mathbf{r}'_j\, A'(\overline a, \overline k).
\end{equation}
\tag{6.11}
$$
Применением теоремы 1 из (6.8), (6.11) получаем
$$
\begin{equation}
\{\{f(\overline k, d)\}^i(j)\}^j(\overline a, q) \,\mathbf{r}'_j\, A'(\overline a, \overline k).
\end{equation}
\tag{6.12}
$$
Таким образом, для всех натуральных чисел $q, \overline a$ и $j \geqslant i$ всякий раз, когда верно (6.10), выполняется и (6.12). Следовательно, имеет место
$$
\begin{equation}
f(\overline k, d) \,\mathbf{r}'_i\, \forall\,\overline x\,\bigl(A'(\overline x, \overline k)\to C'(\overline x, \overline k)\bigr).
\end{equation}
\tag{6.13}
$$
Получаем, что для всех натуральных чисел $\overline k, d, i$ имеет место (6.13) всякий раз, когда верно (6.9). Таким образом, справедливо $f \,\mathbf{r}'_0\,S'$ для любого арифметического примера секвенции $S$.
Случай A9. Пусть секвенция $S$ есть
$$
\begin{equation*}
\forall\, \overline x\,\bigl(A(\overline x) \to B(\overline x)\bigr) \Rightarrow \forall\, \overline x\,\bigl(A(\overline z) \to B(\overline z)\bigr),
\end{equation*}
\notag
$$
где $\overline x=x_1, \dots, x_n$, $\overline z=z_1, \dots, z_n$. Очевидно, что списки переменных $\overline x$ и $\overline r$ не пересекаются, а каждая переменная из списка $\overline z$ есть или переменная из списка $\overline x$, или переменная из списка $\overline r$. Этот факт будем отражать обозначением списка $\overline z$ через $\overline z(\overline x, \overline r)$. Таким образом $S$ имеет вид
$$
\begin{equation*}
\forall\, \overline x\,\bigl(A(\overline x, \overline r) \to B(\overline x, \overline r)\bigr) \Rightarrow \forall\, \overline x\,\bigl(A(\overline z(\overline x, \overline r), \overline r) \to B(\overline z(\overline x, \overline r), \overline r)\bigr).
\end{equation*}
\notag
$$
Если $\overline k$ – список натуральных чисел $k_1, \dots, k_l$, то через $\overline z(\overline x, \overline k)$ обозначаем список, полученный из списка $\overline z(\overline x, \overline r)$ заменой переменных $r_1, \dots, r_l$ натуральными числами $k_1, \dots, k_l$. Если $\overline m$ – список натуральных чисел $m_1, \dots, m_n$, то через $\overline z(\overline m, \overline k)$ обозначаем список, полученный из списка $\overline z(\overline x, \overline k)$ заменой переменных $x_1, \dots, x_n$ натуральными числами $m_1, \dots, m_n$. Очевидно, $\overline z(\overline m, \overline k)$ есть список натуральных чисел длины $n$. Функцию, которая натуральным числам $\overline m, \overline k$ ставит в соответствие $i$-й элемент списка $\overline z(\overline m, \overline k)$, обозначаем через $\mathsf z_i$, $1 \leqslant i \leqslant n$. Каждая функция $\mathsf z_i$ есть $I^{n+l}_{j_i}$ для некоторого $1 \leqslant j_i \leqslant n+l$, так что $\mathsf z_i \in \mathbf E^{n+l}_0$. Определим функцию $f \in \mathbf E^{l+1}_0$ следующим образом:
$$
\begin{equation}
f(\overline r, z) :=\Lambda v.\Lambda \overline x, q. \{\{z\}^w(v)\}^v\bigl(\mathsf z_1(\overline x, \overline r), \dots, \mathsf z_n(\overline x, \overline r), q\bigr).
\end{equation}
\tag{6.14}
$$
Предположим, что $A', B'$ – арифметические примеры формул $A, B$ и верно
$$
\begin{equation}
d \,\mathbf{r}'_i\, \forall\, \overline x\,\bigl(A'(\overline x, \overline k)\to B'(\overline x, \overline k)\bigr)
\end{equation}
\tag{6.15}
$$
для некоторых натуральных чисел $d, i, \overline k=k_1, \dots, k_l$. И пусть имеет место
$$
\begin{equation}
q \,\mathbf{r}'_j\, A'\bigl(\overline z(\overline a, \overline k), \overline k\bigr)
\end{equation}
\tag{6.16}
$$
для некоторых натуральных чисел $\overline a, q$ и $j \geqslant i$. Из (6.15), (6.16) следует
$$
\begin{equation}
\{\{d\}^i(j)\}^j\bigl(\overline z(\overline a, \overline k), q\bigr) \,\mathbf{r}'_j\, B'\bigl(\overline z(\overline a, \overline k), \overline k\bigr).
\end{equation}
\tag{6.17}
$$
Применением теоремы 1 из (6.14), (6.17) получаем
$$
\begin{equation}
\{\{f(\overline k, d)\}^i(j)\}^j(\overline a, q) \,\mathbf{r}'_j\, B'\bigl(\overline z(\overline a, \overline k), \overline k\bigr).
\end{equation}
\tag{6.18}
$$
Таким образом, для всех натуральных чисел $q, \overline a$ и $j \geqslant i$ всякий раз, когда верно (6.16), выполняется и (6.18). Следовательно, имеет место
$$
\begin{equation}
f(\overline k, d) \,\mathbf{r}'_i\, \forall\,\overline x\,\bigl(A'(\overline z(\overline x, \overline k), \overline k)\to B'(\overline z(\overline x, \overline k), \overline k)\bigr).
\end{equation}
\tag{6.19}
$$
Получаем, что для всех натуральных чисел $\overline k, d, i$ имеет место (6.19) всякий раз, когда верно (6.15). Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай A10. Пусть секвенция $S$ есть
$$
\begin{equation*}
\forall\, \overline x\,(A \to B) \Rightarrow \forall\, \overline y\,(A \to B),
\end{equation*}
\notag
$$
где $\overline x=x_1, \dots, x_n$, $\overline y=y_1, \dots, y_p$ и каждая переменная из списка $\overline y$ не входит свободно в левую часть секвенции. Пусть $\overline v=v_1, \dots, v_s$ – список всех свободных переменных формулы $A \to B$. Рассмотрим $(n+l)$-местную функцию $\mathsf v_i$ и $(p+l)$-местную функцию $\mathsf v'_i$ для каждого $i=1, \dots, s$:
$$
\begin{equation*}
\mathsf v_i(\overline m, \overline k) \rightleftharpoons v_i[\overline x \to \overline m][\overline r \to \overline k], \qquad \mathsf v'_i(\overline m', \overline k) \rightleftharpoons v_i[\overline y \to \overline m'][\overline r \to \overline k].
\end{equation*}
\notag
$$
Для каждого $i=1, \dots, n$ рассмотрим $(p+l)$-местную функцию $\mathsf x_i$:
$$
\begin{equation*}
\mathsf x_i(\overline m', \overline k) \rightleftharpoons x_i[\overline y \to \overline m'][\overline r \to \overline k][\overline x \to \overline{0}],
\end{equation*}
\notag
$$
где $\overline{0}$ – список натуральных чисел $0, \dots, 0$ длины $n$. Каждая функция $\mathsf x_i$ есть или $I^{p+l}_{j_i}$ для некоторого $1 \leqslant j_i \leqslant p+l$ или $\mathsf c^{p+l}_0$, так что $\mathsf x_i \in \mathbf E^{p+l}_0$.
Будем писать $\overline v(\overline m, \overline k)$ вместо последовательности натуральных чисел $\mathsf v_1(\overline m, \overline k), \dots, \mathsf v_s(\overline m, \overline k)$, вместо последовательности $\mathsf v'_1(\overline m', \overline k), \dots, \mathsf v'_s(\overline m', \overline k)$ будем писать $\overline v'(\overline m', \overline k)$, а вместо последовательности $\mathsf x_1(\overline m', \overline k), \dots, \mathsf x_s(\overline m', \overline k)$ будем писать $\overline x(\overline m', \overline k)$. Докажем, что для всех натуральных чисел $\overline m', \overline k$ выполняется соотношение
$$
\begin{equation}
\overline v\bigl(\overline x(\overline m', \overline k), \overline k\bigr)=\overline v'(\overline m', \overline k).
\end{equation}
\tag{6.20}
$$
Для этого достаточно показать, что для каждого $i=1, \dots, s$ верно
$$
\begin{equation}
v_i\bigl[\overline x \to \overline x[\overline y \to \overline m'][\overline r \to \overline k][\overline x \to \overline{0}]\bigr][\overline r \to \overline k]= v_i[\overline y \to \overline m'][\overline r \to \overline k].
\end{equation}
\tag{6.21}
$$
Рассмотрим случай, когда переменная $v_i$ находится в списке $\overline x$. Тогда левая часть равенства (6.21) приобретает вид $v_i[\overline y \to \overline m'][\overline r \to \overline k][\overline x \to \overline{0}]$. В силу того, что все свободные переменные правой части секвенции $S$ содержатся в списке $\overline r$, выражение $v_i[\overline y \to \overline m'][\overline r \to \overline k]$ является натуральным числом. Из этого факта следует равенство (6.21).
Теперь рассмотрим случай, когда переменной $v_i$ нет в списке $\overline x$. Тогда переменная $v_i$ входит свободно в левую часть секвенции $S$ и, следовательно, не может быть переменной из списка $\overline y$. Таким образом, и правая и левая части выражения (6.21) равняются $v_i[\overline r \to \overline k]$. Определим функцию $f \in \mathbf E^{l+1}_0$ следующим образом:
$$
\begin{equation}
f(\overline r, z) :=\Lambda v.\Lambda \overline y, q. \{\{z\}^w(v)\}^v\bigl(\mathsf x_1(\overline y, \overline r), \dots, \mathsf x_n(\overline y, \overline r), q\bigr).
\end{equation}
\tag{6.22}
$$
Предположим, что $A', B'$ – арифметические примеры формул $A, B$ и верно
$$
\begin{equation}
d \,\mathbf{r}'_i\, [\overline k/ \overline r]\,\forall\, \overline x\,\bigl(A'(\overline v) \to B'(\overline v)\bigr)
\end{equation}
\tag{6.23}
$$
для некоторых натуральных чисел $d$, $i$, $\overline k=k_1, \dots, k_l$. И пусть имеет место
$$
\begin{equation}
q \,\mathbf{r}'_j\, A'(\overline v'(\overline m', \overline k))
\end{equation}
\tag{6.24}
$$
для некоторых натуральных чисел $\overline m', q$ и $j \geqslant i$. Из (6.20), (6.24) следует
$$
\begin{equation}
q \,\mathbf{r}'_j\, A'\bigl(\overline v(\overline x(\overline m', \overline k), \overline k)\bigr).
\end{equation}
\tag{6.25}
$$
Из (6.23), (6.25) следует
$$
\begin{equation}
\{\{d\}^i(j)\}^j(\overline x(\overline m', \overline k), q) \,\mathbf{r}'_j\, B' \bigl(\overline v(\overline x(\overline m', \overline k), \overline k)\bigr).
\end{equation}
\tag{6.26}
$$
Применением теоремы 1 из (6.22), (6.26) получаем
$$
\begin{equation}
\bigl\{\{f(\overline k, d)\}^i(j)\bigr\}^j(\overline m', q) \,\mathbf{r}'_j\, B'\bigl(\overline v(\overline x(\overline m', \overline k), \overline k)\bigr).
\end{equation}
\tag{6.27}
$$
Из (6.20), (6.27) следует
$$
\begin{equation}
\bigl\{\{f(\overline k, d)\}^i(j)\bigr\}^j(\overline m', q) \,\mathbf{r}'_j\, B'(\overline v'(\overline m', \overline k)).
\end{equation}
\tag{6.28}
$$
Таким образом, для всех натуральных чисел $q, \overline m'$ и $j \geqslant i$ всякий раз, когда верно (6.24), выполняется и (6.28). Следовательно, имеет место
$$
\begin{equation}
f(\overline k, d) \,\mathbf{r}'_i\, [\overline k/\overline r]\,\forall\,\overline y\,\bigl(A'(\overline v)\to B'(\overline v)\bigr).
\end{equation}
\tag{6.29}
$$
Получаем, что для всех натуральных чисел $\overline k, d, i$ имеет место (6.29) всякий раз, когда верно (6.23). Таким образом, справедливо $f\,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай A11. Пусть секвенция $S$ имеет вид
$$
\begin{equation*}
\forall\, \overline x, y\,\bigl(B(\overline x, y, \overline r) \to A(\overline x, \overline r)\bigr) \Rightarrow \forall\, \overline x\,\bigl(\exists\, y\, B(\overline x, y, \overline r) \to A(\overline x, \overline r)\bigr),
\end{equation*}
\notag
$$
где $\overline x=x_1, \dots, x_n$. Определим функцию $f \in \mathbf E^{l+1}_0$ следующим образом.
$$
\begin{equation}
f(\overline r, z) :=\Lambda v.\Lambda \overline x, q.\{\{z\}^w(v)\}^v(\overline x, \mathsf p_1 q, \mathsf p_2 q).
\end{equation}
\tag{6.30}
$$
Предположим, что $A', B'$ – арифметические примеры формул $A, B$ и имеет место
$$
\begin{equation}
d \,\mathbf{r}'_i\, \forall\, \overline x, y\,\bigl(B'(\overline x, y, \overline k) \to A'(\overline x, \overline k)\bigr)
\end{equation}
\tag{6.31}
$$
для некоторых натуральных чисел $d$, $i$, $\overline k=k_1, \dots, k_l$. И пусть верно
$$
\begin{equation}
q \,\mathbf{r}'_j\, \exists\, y\, B'(\overline a, y, \overline k)
\end{equation}
\tag{6.32}
$$
для некоторых натуральных чисел $\overline a, q$ и $j \geqslant i$. Из (6.32) следует
$$
\begin{equation}
\mathsf p_2 q \,\mathbf{r}'_j\, B'(\overline a, \mathsf p_1 q, \overline k).
\end{equation}
\tag{6.33}
$$
Из (6.31), (6.33) получаем
$$
\begin{equation}
\{\{d\}^i(j)\}^j(\overline a, \mathsf p_1 q, \mathsf p_2 q) \,\mathbf{r}'_j\, A'(\overline a, \overline k).
\end{equation}
\tag{6.34}
$$
Применением теоремы 1 из (6.30), (6.34) получаем
$$
\begin{equation}
\{\{f(\overline k, d)\}^i(j)\}^j(\overline a, q) \,\mathbf{r}'_j\, A'(\overline a, \overline k).
\end{equation}
\tag{6.35}
$$
Таким образом, для всех натуральных чисел $q, \overline a$ и $j \geqslant i$ всякий раз, когда верно (6.32), выполняется и (6.35). Следовательно, имеет место
$$
\begin{equation}
f(\overline k, d) \,\mathbf{r}'_i\, \forall\,\overline x\,\bigl(\exists\, y\, B'(\overline x, y, \overline k)\to A'(\overline x, \overline k)\bigr).
\end{equation}
\tag{6.36}
$$
Получаем, что для всех натуральных чисел $\overline k, d, i$ имеет место (6.36) всякий раз, когда верно (6.31). Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Теперь рассмотрим все случаи, когда секвенция $S$ получена по одному из правил вывода исчисления $\mathsf{BQC}$. Случай R1. Пусть секвенция $S$ получена по правилу
$$
\begin{equation*}
\frac{A\Rightarrow B\;\ B\Rightarrow C}{A\Rightarrow C}
\end{equation*}
\notag
$$
и $\overline u=u_1, \dots, u_p$ – список переменных, допустимый для секвенций $A \Rightarrow B$, $B \Rightarrow C$ и $A \Rightarrow C$. Согласно предположению индукции найдутся такие функции $g, h \in \mathbf E^{p+1}_0$, что для всех арифметических примеров $A', B', C'$ формул $A, B, C$ имеет место
$$
\begin{equation*}
g \,\mathbf{r}'_0\, A'(\overline u) \Rightarrow B'(\overline u) \qquad\text{и}\qquad h \,\mathbf{r}'_0\, B'(\overline u) \Rightarrow C'(\overline u).
\end{equation*}
\notag
$$
Определим функцию $f' \in \mathbf E^{p+1}_0$ следующим образом:
$$
\begin{equation*}
f'(\overline u, z) :=h(\overline u, g(\overline u, z)).
\end{equation*}
\notag
$$
Легко видеть, что $f' \,\mathbf{r}'_0\, A'(\overline u) \Rightarrow C'(\overline u)$. Применяя предложение 4, получаем, что найдется такая функция $f \in \mathbf E^{l+1}_0$, что $f \,\mathbf{r}'_0\, A'(\overline r) \Rightarrow C'(\overline r)$. Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай R2. Пусть секвенция $S$ получена по правилу
$$
\begin{equation*}
\frac{A\Rightarrow B\;\ A\Rightarrow C}{A\Rightarrow B\land C}.
\end{equation*}
\notag
$$
Согласно предположению индукции найдутся такие функции $g, h \in \mathbf E^{l+1}_0$, что для всех арифметических примеров $A', B', C'$ формул $A, B, C$ имеет место
$$
\begin{equation*}
g \,\mathbf{r}'_0\, A'(\overline r) \Rightarrow B'(\overline r) \qquad\text{и}\qquad h \,\mathbf{r}'_0\, A'(\overline r) \Rightarrow C'(\overline r).
\end{equation*}
\notag
$$
Определим функцию $f \in \mathbf E^{l+1}_0$ следующим образом:
$$
\begin{equation*}
f(\overline r, z) :=\langle g(\overline r, z), h(\overline r, z)\rangle.
\end{equation*}
\notag
$$
Легко видеть, что $f \,\mathbf{r}'_0\, A'(\overline r) \Rightarrow B'(\overline r) \land C'(\overline r)$. Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай R3, а). Пусть секвенция $S$ получена по правилу и $\overline u=u_1, \dots, u_p$ – список переменных, допустимый для секвенции $A \Rightarrow B \land C$. Согласно предположению индукции найдется такая функция $g \in \mathbf E^{p+1}_0$, что для всех арифметических примеров $A', B', C'$ формул $A, B, C$ имеет место
$$
\begin{equation*}
g \,\mathbf{r}'_0\, A'(\overline u) \Rightarrow B'(\overline u) \land C'(\overline u).
\end{equation*}
\notag
$$
Определим функцию $f' \in \mathbf E^{p+1}_0$ следующим образом: Легко видеть, что $f' \,\mathbf{r}'_0\, A'(\overline u) \Rightarrow B'(\overline u)$. Применяя предложение 4, получаем, что найдется такая функция $f \in \mathbf E^{l+1}_0$, что $f \,\mathbf{r}'_0\, A'(\overline r) \Rightarrow B'(\overline r)$. Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай R3, б). Случай, когда секвенция $S$ получена по правилу рассматривается аналогично пункту а).Случай R4. Пусть секвенция $S$ получена по правилу
$$
\begin{equation*}
\frac{B\Rightarrow A\;\ C\Rightarrow A}{B\lor C\Rightarrow A}.
\end{equation*}
\notag
$$
Согласно предположению индукции найдутся такие функции $g, h \in \mathbf E^{l+1}_0$, что для всех арифметических примеров $A', B', C'$ формул $A, B, C$ имеет место
$$
\begin{equation*}
g \,\mathbf{r}'_0\, B'(\overline r) \Rightarrow A'(\overline r), \qquad h \,\mathbf{r}'_0\, C'(\overline r) \Rightarrow A'(\overline r).
\end{equation*}
\notag
$$
Определим функцию $f \in \mathbf E^{l+1}_0$ следующим образом:
$$
\begin{equation*}
f(\overline r, z) :=\mathsf{if}\bigl(\mathsf p_1 z, g(\overline r, \mathsf p_2 z), h(\overline r, \mathsf p_2 z)\bigr).
\end{equation*}
\notag
$$
Легко видеть, что $f \,\mathbf{r}'_0\, B'(\overline r) \lor C'(\overline r) \Rightarrow A'(\overline r)$. Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай R5, а). Пусть секвенция $S$ получена по правилу и $\overline u=u_1, \dots, u_p$ – список переменных, допустимый для секвенции $B \lor C \Rightarrow A$. Согласно предположению индукции найдется такая функция $g \in \mathbf E^{p+1}_0$, что для всех арифметических примеров $A', B', C'$ формул $A, B, C$ имеет место
$$
\begin{equation*}
g \,\mathbf{r}'_0\, B'(\overline u) \lor C'(\overline u) \Rightarrow A'(\overline u).
\end{equation*}
\notag
$$
Определим функцию $f' \in \mathbf E^{p+1}_0$ следующим образом:
$$
\begin{equation*}
f'(\overline u, z) :=g(\overline u, \langle 0, z \rangle).
\end{equation*}
\notag
$$
Легко видеть, что $f' \,\mathbf{r}'_0\, B'(\overline u) \Rightarrow A'(\overline u)$. Применяя предложение 4, получаем, что найдется такая функция $f \in \mathbf E^{l+1}_0$, что $f \,\mathbf{r}'_0\, B'(\overline r) \Rightarrow A'(\overline r)$. Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай R5, б). Случай, когда секвенция $S$ получена по правилу рассматривается аналогично пункту а).Случай R6. Пусть секвенция $S$ получена по правилу
$$
\begin{equation*}
\frac{A \Rightarrow B}{[\overline y / \overline x]\,A \Rightarrow [\overline y / \overline x]\,B},
\end{equation*}
\notag
$$
где $\overline x=x_1, \dots, x_n$, $\overline y=y_1, \dots, y_n$. И пусть список переменных $\overline u=u_1, \dots, u_p$ является допустимым для секвенций $A \Rightarrow B$, $[\overline y / \overline x]\,A \Rightarrow [\overline y / \overline x]\,B$. Очевидно, что все переменные из списка $\overline u[\overline x \to \overline y]$ содержатся среди переменных списка $\overline u$. Для каждого $i=1, \dots, p$ рассмотрим $p$-местную функцию $\mathsf z_i$:
$$
\begin{equation*}
\mathsf z_i(\overline k) \rightleftharpoons u_i[\overline x \to \overline y][\overline u \to \overline k].
\end{equation*}
\notag
$$
Каждая функция $\mathsf z_i$ есть $I^p_{j_i}$ для некоторого $1 \leqslant j_i \leqslant p$, так что $\mathsf z_i \in \mathbf E^p_0$. Согласно предположению индукции найдется такая функция $g \in \mathbf E^{p+1}_0$, что для всех арифметических примеров $A', B'$ формул $A, B$ имеет место
$$
\begin{equation*}
g \,\mathbf{r}'_0\, A'(\overline u) \Rightarrow B'(\overline u).
\end{equation*}
\notag
$$
Определим функцию $f' \in \mathbf E^{p+1}_0$ следующим образом:
$$
\begin{equation*}
f'(\overline u, z) :=g(\mathsf z_1(\overline u), \dots, \mathsf z_p(\overline u), z).
\end{equation*}
\notag
$$
Нетрудно показать, что $f' \,\mathbf{r}'_0\, ([\overline y / \overline x]\,A')(\overline u) \Rightarrow ([\overline y / \overline x]\,B')(\overline u)$. Применяя предложение 4, получаем, что найдется такая функция $f \in \mathbf E^{l+1}_0$, что имеет место
$$
\begin{equation*}
f \,\mathbf{r}'_0\, ([\overline y / \overline x]\,A')(\overline r) \Rightarrow ([\overline y / \overline x]\,B')(\overline r).
\end{equation*}
\notag
$$
Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай R7. Пусть секвенция $S$ получена по правилу где переменная $x$ не свободна в формуле $A$. Таким образом, секвенция $S$ имеет вид $\exists\, x\, B(\overline r, x) \Rightarrow A(\overline r)$. Согласно предположению индукции найдется такая функция $g \in \mathbf E^{l+2}_0$, что для всех арифметических примеров $A', B'$ формул $A, B$ имеет место
$$
\begin{equation*}
g \,\mathbf{r}'_0\, B'(\overline r, x) \Rightarrow A'(\overline r).
\end{equation*}
\notag
$$
Определим функцию $f \in \mathbf E^{l+1}_0$ следующим образом:
$$
\begin{equation*}
f(\overline r, z) :=g(\overline r, \mathsf p_1 z, \mathsf p_2 z).
\end{equation*}
\notag
$$
Легко видеть, что $f \,\mathbf{r}'_0\, \exists\, x\, B'(\overline r, x) \Rightarrow A'(\overline r)$. Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай R8. Пусть секвенция $S$ получена по правилу где переменная $x$ не свободна в формуле $A$. Таким образом, секвенция $S$ имеет вид $B(\overline u, x) \Rightarrow A(\overline u)$ для некоторого списка переменных $\overline u=u_1, \dots, u_p$. Согласно предположению индукции найдется такая функция $g \in \mathbf E^{p+1}_0$, что для всех арифметических примеров $A', B'$ формул $A, B$ имеет место
$$
\begin{equation*}
g \,\mathbf{r}'_0\, \exists\, x\,B'(\overline u, x) \Rightarrow A'(\overline u).
\end{equation*}
\notag
$$
Определим функцию $f' \in \mathbf E^{p+2}_0$ следующим образом:
$$
\begin{equation*}
f'(\overline u, x, z) :=g(\overline u, \langle x, z\rangle).
\end{equation*}
\notag
$$
Легко видеть, что $f' \,\mathbf{r}'_0\, B'(\overline u, x) \Rightarrow A'(\overline u)$. Применяя предложение 4, получаем, что найдется такая функция $f \in \mathbf E^{l+1}_0$, что имеет место $f \,\mathbf{r}'_0\, B'(\overline r) \Rightarrow A'(\overline r).$ Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$.
Случай R9. Пусть секвенция $S$ получена по правилу
$$
\begin{equation*}
\frac{A \land B\Rightarrow C}{A \Rightarrow \forall\, \overline x\,(B\to C)},
\end{equation*}
\notag
$$
где каждая переменная из списка $\overline x=x_1, \dots, x_n$ не свободнa в $A$. Таким образом, секвенция $S$ имеет вид
$$
\begin{equation*}
A(\overline r) \Rightarrow \forall\, \overline x\,\bigl(B(\overline x, \overline r) \to C(\overline x, \overline r)\bigr).
\end{equation*}
\notag
$$
Согласно предположению индукции найдется такая функция $g \in \mathbf E^{l+n+1}_0$, что для всех арифметических примеров $A', B'$ формул $A, B$ имеет место
$$
\begin{equation}
g \,\mathbf{r}'_0\, A'(\overline r) \land B'(\overline r, \overline x) \Rightarrow C'(\overline r, \overline x).
\end{equation}
\tag{6.37}
$$
Определим функцию $f \in \mathbf E^{l+1}_0$ следующим образом:
$$
\begin{equation}
f(\overline r, z) :=\Lambda v. \Lambda \overline x, q.\,g(\overline r, \overline x, \langle z, q \rangle).
\end{equation}
\tag{6.38}
$$
Предположим, что $A', B', C'$ – арифметические примеры формул $A, B, C$ и имеет место для некоторых натуральных чисел $d, i, \overline k=k_1, \dots, k_l$. И пусть верно для некоторых натуральных чисел $\overline a, q$ и $j \geqslant i$. Применением предложения 3 из (6.39), (6.40) получаем
$$
\begin{equation}
\langle d, q \rangle \,\mathbf{r}'_j\, A'(\overline k) \land B'(\overline a, \overline k).
\end{equation}
\tag{6.41}
$$
Из (6.37), (6.41) получаем
$$
\begin{equation}
g(\overline k, \overline a, \langle d, q \rangle) \,\mathbf{r}'_j\, C'(\overline a, \overline k).
\end{equation}
\tag{6.42}
$$
Применением теоремы 1 из (6.38), (6.42) получаем
$$
\begin{equation}
\{\{f(\overline k, d)\}^i(j)\}^j(\overline a, q) \,\mathbf{r}'_j\, C'(\overline a, \overline k).
\end{equation}
\tag{6.43}
$$
Таким образом, для всех натуральных чисел $q, \overline a$ и $j \geqslant i$ всякий раз, когда верно (6.40), выполняется и (6.43). Следовательно, имеет место
$$
\begin{equation}
f(\overline k, d) \,\mathbf{r}'_i\, \forall\,\overline x\,\bigl(B'(\overline x, \overline k)\to C'(\overline x, \overline k)\bigr).
\end{equation}
\tag{6.44}
$$
Получаем, что для всех натуральных чисел $\overline k, d, i$ имеет место (6.44) всякий раз, когда верно (6.39). Таким образом, справедливо $f \,\mathbf{r}'_0\, S'$ для любого арифметического примера секвенции $S$. Теорема 3. Всякая замкнутая предикатная формула, выводимая в исчислении базисной логики $\mathsf{BQC}$, является сильно $\mathsf{spr}'$-реализуемой. Доказательство. Пусть замкнутая предикатная формула $A$ выводима в исчислении $\mathsf{BQC}$, т.е. имеет место $\mathsf{BQC} \vdash \top \Rightarrow A$. В силу того, что формула $A$ является замкнутой, пустой список переменных допустим для секвенции $\top \Rightarrow A$. Из теоремы 2 получаем, что найдется такая функция $f \in \mathbf E^1_0$, что верно $f \,\mathbf{r}'_0\, \top \Rightarrow A'$ для любого арифметического примера $A'$ формулы $A$. Следовательно, имеет место $f(0) \,\mathbf{r}'_0\, A'$ для любого арифметического примера $A'$ формулы $A$.
Цитирование в формате AMSBIB
\RBibitem{Kon23} |
|
||||||||||
|
Обратная связь: |
Пользовательское соглашение
|
Регистрация посетителей портала |
Логотипы |
|