| Математические заметки |
|
|
|
|
|
Эта публикация цитируется в 1 научной статье (всего в 1 статье) Замыкающий ординал оператора непосредственной выводимости в инфинитарной логике действий Т. Г. Пшеницын Математический институт им. В. А. Стеклова Российской академии наук, г. Москва
Англоязычная версия:
Mathematical Notes, 2024, Volume 116, Issue 4, Pages DOI: https://doi.org/10.1134/S000143462409030X 
Реферативные базы данных:
  1. ВведениеИнфинитарная логика действий $\mathrm{ACT}_\omega$, введенная Палькой в работе [1] – пропозициональное исчисление, аксиоматизирующее $\ast$-непрерывные решетки Клини с делениями. Примером такой решетки является решетка бинарных отношений на фиксированном множестве $W$ со следующими операциями: если $R,S\subseteq W\times W$ – два бинарных отношения, то
Если интерпретировать элементы $W$ как состояния некоторой системы, пару $(u,v)\in W^2$ – как переход из состояния $u$ в состояние $v$, а отношение $R\subseteq W^2$ – как действие, определяемое тем, куда можно попасть из того или иного состояния после применения $R$, то умножение $R\bullet S$ соответствует последовательному выполнению действий $R$ и $S$; дизъюнкция $R\vee S$ соответствует выполнению одного из действий $R$ или $S$ на выбор; и так далее. Инфинитарная логика действий вводится в [1] в секвенциальном формате. Формулы строятся из счетного множества пропозициональных переменных, а также констант $\mathbf 0$ и $\mathbf 1$ с помощью операций $\bullet$, $\setminus$, $/$, $\wedge$, $\vee$, $^\ast$. Секвенция – строка вида $\Gamma\Rightarrow A$, где $\Gamma$ – последовательность формул, а $A$ – формула. Заглавные греческие буквы далее обозначают последовательности формул; заглавные латинские буквы обозначают формулы; строчные латинские буквы $p,q,r,\dots$ обозначают примитивные формулы. Аксиомы и правила логики $\mathrm{ACT}_\omega$ задаются следующим образом:
$$
\begin{equation*}
\begin{gathered} \, \frac{}{A\Rightarrow A}(ax), \\ \frac{\Gamma,A,\Delta\Rightarrow C\quad \Pi\Rightarrow B} {\Gamma,\Pi,B\setminus A,\Delta\Rightarrow C}(\setminus L), \qquad \frac{B,\Pi\Rightarrow A}{\Pi\Rightarrow B\setminus A}(\setminus R), \\ \frac{\Gamma,A,\Delta\Rightarrow C\quad \Pi\Rightarrow B}{\Gamma, A/B,\Pi,\Delta\Rightarrow C}(/L),\qquad \frac{\Pi,B\Rightarrow A}{\Pi\Rightarrow A/B}(/R), \\ \frac{\Gamma,A,B,\Delta\Rightarrow C}{\Gamma,A\bullet B,\Delta\Rightarrow C}(\bullet L),\qquad \frac{\Gamma\Rightarrow A\quad \Delta\Rightarrow B}{\Gamma,\Delta\Rightarrow A\bullet B}(\bullet R), \\ \frac{\Gamma,A_i,\Delta\Rightarrow C}{\Gamma,A_1\wedge A_2,\Delta\Rightarrow C}(\wedge L_i),\quad i=1,2,\qquad \frac{\Pi\Rightarrow A_1\quad \Pi\Rightarrow A_2}{\Pi\Rightarrow A_1\wedge A_2}(\wedge R), \\ \frac{\Gamma,A_1,\Delta\Rightarrow C\quad \Gamma,A_2,\Delta\Rightarrow C} {\Gamma,A_1\vee A_2,\Delta\Rightarrow C}(\vee L),\qquad \frac{\Pi\Rightarrow A_i}{\Pi\Rightarrow A_1\vee A_2}(\vee R_i),\quad i=1,2, \\ \frac{}{\Gamma,\mathbf 0,\Delta\Rightarrow C}(\mathbf 0L),\qquad \frac{\Gamma,\Delta\Rightarrow C}{\Gamma,\mathbf 1,\Delta\Rightarrow C}(\mathbf 1L),\qquad \frac{}{\Rightarrow\mathbf 1}(\mathbf 1R), \\ \frac{(\Gamma,A^n,\Delta\Rightarrow B)_{n<\omega}}{\Gamma,A^\ast,\Delta\Rightarrow B}(\ast L_\omega), \\ \frac{}{\Rightarrow A^\ast}(\ast R_0),\qquad \frac{\Pi_1\Rightarrow A,\dots,\Pi_n\Rightarrow A}{\Pi_1,\dots,\Pi_n\Rightarrow A^\ast}(\ast R_n),\quad 0<n<\omega. \end{gathered}
\end{equation*}
\notag
$$
Особенностью инфинитарной логики действий является наличие $\omega$-правила $(\ast L_\omega)$ для итерации Клини; оно содержит счетное число посылок. Как следствие, доказательства в данной логике могут быть бесконечными; при этом дерево вывода должно быть фундированным. Чтобы формально определить, какие секвенции выводятся в $\mathrm{ACT}_\omega$, введем оператор непосредственной выводимости $\mathscr D$ следующим образом: если $\mathscr S$ – множество секвенций, то $\mathscr D(\mathscr S)$ есть объединение $\mathscr S$ с множеством секвенций, которые можно получить из элементов $\mathscr S$ применением некоторого правила логики $\mathrm{ACT}_\omega$ или которые являются аксиомами $\mathrm{ACT}_\omega$. Определим по трансфинитной рекурсии множества $\mathscr T_\alpha$, где $\alpha$ – ординал:
Поскольку всего секвенций счетное число, существует счетный ординал $\alpha$, для которого $\mathscr T_\alpha=\mathscr T_{\alpha+1}$. Наименьший ординал с таким свойством назовем замыкающим ординалом оператора $\mathscr D$. Далее вместо замыкающий ординал оператора непосредственной выводимости в логике $\mathscr L$ будем иногда говорить замыкающий ординал для логики $\mathscr L$. Замыкающий ординал, неформально говоря, характеризует максимальную глубину доказательств в логике. Интерес к вычислению замыкающего ординала для той или иной логики связан с анализом алгоритмической сложности задачи выводимости в данной логике. Так, в работе [2] показано, что если замыкающий ординал для некоторой логики (при условии элементарности оператора непосредственной выводимости) предельный и равен $\alpha_0<\omega^{CK}_1$, то данная логика лежит в классе $\Sigma^0_{\alpha_0}$ гиперарифметической иерархии. С помощью этого в [2] была доказана верхняя оценка $\Sigma^0_{\omega^\omega}$ на сложность задачи выводимости в инфинитарной логике действий с субэкспоненциальной модальностью, для которой имеется правило мультиплексирования: было показано, что замыкающий ординал для нее не превосходит $\omega^\omega$. Эта верхняя оценка на ординал верна и для $\mathrm{ACT}_\omega$; при этом известно, что задача выводимости в $\mathrm{ACT}_\omega$ является $\Pi^0_1$-полной [1], так что оценка $\Sigma^0_{\omega^\omega}$ на сложность, полученная путем оценки на замыкающий ординал, для исчисления $\mathrm{ACT}_\omega$ заведомо не точна. Нахождение точного значения замыкающего ординала для инфинитарной логики действий является открытым вопросом [2], [3]. В настоящей работе доказывается следующая теорема. Теорема 1. Замыкающий ординал для инфинитарной логики действий $\mathrm{ACT}_\omega$ равен $\omega^\omega$. Доказательство заключается в явном построении для каждого $\alpha=\omega^{n_1}+\dotsb+ \omega^{n_k}$, где $n_i\in\mathbb N$, секвенции, которая выводится в $\mathrm{ACT}_\omega$, но не принадлежит $\mathscr T_\alpha$. Семейство таких секвенций показывает, что последовательность множеств $\mathscr T_\alpha$ не стабилизируется до ординала $\omega^\omega$. Далее, аналогичный вопрос исследуется для коммутативной инфинитарной логики действий $\mathrm{CommACT}_\omega$, введенной и исследованной в [4]. Она отличается от $\mathrm{ACT}_\omega$ тем, что в ней секвенции имеют вид $\Gamma\Rightarrow A$, где $A$ – формула, а $\Gamma$ – мультимножество формул; иначе говоря, в логику неявным образом добавлено правило перестановки формул в антецеденте:
$$
\begin{equation*}
\frac{\Gamma,A,B,\Delta\Rightarrow C}{\Gamma,B,A,\Delta\Rightarrow C}\,.
\end{equation*}
\notag
$$
Аксиомы и правила в $\mathrm{CommACT}_\omega$ такие же, как в $\mathrm{ACT}_\omega$, с тем отличием, что антецеденты в них представляют собой мультимножества, а запятая понимается как дизъюнктное объединение мультимножеств. В статье [2] доказывается, что замыкающий ординал для $\mathrm{CommACT}_\omega$ не превосходит $\omega^\omega$. В настоящей работе доказывается следующая нижняя оценка. Теорема 2. Замыкающий ординал для коммутативной инфинитарной логики действий $\mathrm{CommACT}_\omega$ равен $\omega^\omega$. Доказательство теоремы устроено так же, как и доказательство теоремы 1, но конструкция секвенций становится более сложной. Нами используются идеи из работы [4], в которой показано, как симулировать работу машин Минского в коммутативной инфинитарной логике действий; а именно, в настоящей работе используется техника, похожая на технику проверки равенства нулю из [4]. Аксиоматизация инфинитарной логики действий, приведенная ранее в данном разделе, не включает правило сечения. Добавление этого правила в $\mathrm{ACT}_\omega$ не изменяет множество выводимых секвенций, однако может привести к уменьшению замыкающего ординала, потому что у секвенций могут появиться доказательства “меньшего размера”. В данной работе показывается, что для каждого $n\in\mathbb N$ секвенция, построенная в доказательстве теоремы 1, которая не принадлежит $\mathscr T_{\omega^n}$, принадлежит множеству $\mathscr T^{\mathrm{cut}}_{\omega\cdot(n+1)+5}$, где $\mathscr T^{\mathrm{cut}}_\alpha$ – множества, построенные по оператору непосредственной выводимости в $\mathrm{ACT}_\omega$ с правилом сечения (теорема 5). Таким образом, использование правила сечения действительно позволяет значительно “сократить” доказательства в $\mathrm{ACT}_\omega$. Вопрос, чему равен замыкающий ординал для инфинитарной логики действий с правилом сечения, остается открытым (как в некоммутативном, так и в коммутативном случае). 2. Доказательства теоремПеред тем как перейти к доказательству теорем 1 и 2, дадим несколько вспомогательных определений. Пусть зафиксирована логика $\mathscr L$ и ее оператор непосредственной выводимости $\mathscr D$; пусть $\mathscr T_0=\varnothing$; $\mathscr T_{\beta+1}=\mathscr D(\mathscr T_\beta)$; $\mathscr T_\alpha=\bigcup_{\beta<\alpha}\mathscr T_\beta$, если $\alpha$ – предельный ординал. Определение 1. Ранг выводимой секвенции $\Pi\Rightarrow C$ (относительно логики $\mathscr L$) – наименьший ординал $\alpha$ такой, что $(\Pi\Rightarrow C)\in\mathscr T_\alpha$. Ранг $\Pi\Rightarrow C$ обозначается как $\mathrm{rk}(\Pi\Rightarrow C)$. Заметим, что ранг секвенции не может быть предельным, поскольку $\mathscr T_\alpha$ для предельных $\alpha$ есть объединение $\mathscr T_\beta$ при $\beta<\alpha$. Если ранг секвенции равен $\beta+1$, то она принадлежит $\mathscr D(\mathscr T_\beta)\setminus\mathscr T_\beta$, т.е. получена из секвенций ранга не более $\beta$ применением правила $\mathscr L$. Общий план доказательства теорем 1 и 2 состоит в том, чтобы построить семейство секвенций, ранги которых стремятся к $\omega^\omega$. Определим ранг вывода секвенции $\Pi\Rightarrow C$ по трансфинитной индукции: если вывод $\mathfrak P$ имеет вид
$$
\begin{equation*}
\frac{(\mathfrak P_n)_{n<\alpha}}{\Pi\Rightarrow C}\,,
\end{equation*}
\notag
$$
где $\mathfrak P_n$ – его подвыводы, то ранг $\mathfrak P$ на единицу больше супремума рангов $\mathfrak P_n$. Ранг вывода аксиомы равен $1$. Определение 2. Вывод секвенции $\Pi\Rightarrow C$ минимальный, если его ранг совпадает с рангом секвенции $\Pi\Rightarrow C$. Вывод секвенции $\Pi\Rightarrow C$ оптимальный, если любой его подвывод минимален. Доказательство ведется трансфинитной индукцией по рангу $\Pi\Rightarrow C$. Если ранг секвенции равен 1, то ее оптимальный вывод тривиален (состоит из нее самой), его ранг равен 1.
Докажем шаг индукции. Пусть $\alpha=\beta+1$ – ранг $\Pi\Rightarrow C$. Тогда секвенция $\Pi\Rightarrow C$ получается из некоторых секвенций $\{\Pi_n\Rightarrow C_n\mid n<N\}$, где $N\leqslant\omega$, супремум рангов которых равен $\beta$, применением одного из правил $\mathrm{ACT}_\omega$: По предположению индукции для каждого $n<N$ секвенция $\Pi_n\Rightarrow C_n$ имеет оптимальный вывод $\mathfrak P_n$. Тогда и следующий вывод секвенции $\Pi\Rightarrow C$ оптимален:Следующая лемма очевидным образом следует из определения ранга секвенции. Лемма 2. Даны выводимые секвенции $\Pi\Rightarrow C$ и $\Gamma\Rightarrow A$. Если известно, что в любом применении правила $\mathrm{ACT}_\omega$, в котором заключение совпадает с $\Pi\Rightarrow C$, одна из посылок равна $\Gamma\Rightarrow A$, то 2.1. Доказательство теоремы 1Определим формулы $A_n$, $n\in\mathbb N$, используемые для доказательства теоремы 1:
Теорема 3. Секвенция где $k,l\geqslant 0$ и $0\leqslant n_1\leqslant\dotsb\leqslant n_k$, имеет единственный вывод; ее ранг не меньше $\omega^{n_k}+\dotsb+\omega^{n_1}$. Пример 2. Пусть $l=3$, $k=2$, $n_1=0$, $n_2=1$. Тогда секвенция (2.1) имеет вид Определим множество
$$
\begin{equation*}
\mathrm{SFm}_1=\bigl\{A_m,(q\bullet A_m^\ast),\,A_m^\ast\mid m\geqslant 0\} \cup\{q,p,(p \bullet q)\bigr\},
\end{equation*}
\notag
$$
состоящее из подформул формул $A_k$. Докажем несколько технических лемм, необходимых для анализа возможных выводов секвенции (2.1). Лемма 3. Пусть $\Phi\Rightarrow q$ выводится, причем $\Phi$ – последовательность формул из $\mathrm{SFm}_1$. Тогда $\Phi=q$. Доказательство. Зафиксируем вывод данной секвенции. Доказательство будет вестись индукцией по его рангу. Для проверки базы индукции достаточно рассмотреть случай, когда секвенция является аксиомой. Поскольку в $\mathrm{SFm}_1$ нет константы $\mathbf 0$, аксиома должна иметь вид $q\Rightarrow q$, что и требовалось доказать.
Если секвенция не является аксиомой, рассмотрим последнее правило в ее выводе. Случай 1. Последнее правило – $(\bullet L)$:
$$
\begin{equation*}
\frac{\Gamma,X,Y,\Delta\Rightarrow q}{\Gamma,X\bullet Y,\Delta\Rightarrow q}(\bullet L)\,.
\end{equation*}
\notag
$$
По предположению индукции $\Gamma,X,Y,\Delta=q$. Однако $\Gamma$, $X$, $Y$, $\Delta$ содержит минимум две формулы, что является противоречием. Случай 1 невозможен.
Случай 2. Последнее правило – $(\setminus L)$:
$$
\begin{equation*}
\frac{\Gamma,X,\Delta\Rightarrow q\quad \Pi\Rightarrow Y} {\Gamma,Y\setminus X,\Pi,\Delta\Rightarrow q}(/L)\,.
\end{equation*}
\notag
$$
По предположению индукции $\Gamma,X,\Delta=q$, так что $X=q$. Как следствие, $Y\setminus X=Y\setminus q\in\mathrm{SFm}_1$. Однако никакая формула из $\mathrm{SFm}_1$ не имеет в числителе деления формулу $q$, что приводит к противоречию. Случай 2 невозможен.
Случай 3. Последнее правило – $(\ast L)$:
$$
\begin{equation*}
\frac{(\Gamma,X^n,\Delta\Rightarrow q)_{n<\omega}}{\Gamma,X^\ast,\Delta\Rightarrow q}(\ast L)\,.
\end{equation*}
\notag
$$
По предположению индукции $\Gamma,X^n,\Delta=q$ для всех $n\in\mathbb N$, что приводит к противоречию. Случай 3 невозможен.
Невозможны и случаи других правил. Действительно, последнее правило в выводе $\Phi\Rightarrow q$ должно быть левым (в сукцеденте стоит примитивная формула $q$), а так как формулы из $\Phi$ составлены только из операций $\bullet$, $\setminus$ и $\ast$, то возможны только три правила, перечисленные выше. Приступим к доказательству теоремы 3. Доказательство теоремы 3. Доказательство будет вестись трансфинитной индукцией по параметру $\rho=\omega^{n_k}+\dotsb+\omega^{n_1}$ (при $k=0$ положим $\rho=0$).
База индукции – случай, когда $\rho=0$, т.е. $k=0$. Секвенция (2.1) в таком случае имеет вид $p^l,q\Rightarrow p^\ast\bullet q$. Она, очевидно, имеет единственный вывод; при $l>0$ он имеет следующий вид:
$$
\begin{equation*}
\frac{\dfrac{p\Rightarrow p\quad \dots\quad p\Rightarrow p} {p^l\Rightarrow p^\ast\quad q\Rightarrow q}(\ast R)} {p^l,q\Rightarrow p^\ast\bullet q}(\bullet R)\,.
\end{equation*}
\notag
$$
При $l=0$ отличие в том, что секвенция $p^l\Rightarrow p^\ast$ – аксиома. Условие на ранг в обоих случаях выполнено тривиальным образом.
Для доказательства шага индукции рассмотрим произвольный вывод секвенции $p^l,q,A_{n_1},\dots,A_{n_k}\Rightarrow p^\ast\bullet q$ (считая, что $k>0$) и в нем – последнее примененное правило. Случай 1. Последнее правило – $(\bullet R)$:
$$
\begin{equation*}
\frac{\Gamma\Rightarrow p^\ast\quad \Delta\Rightarrow q} {\Gamma,\Delta\Rightarrow p^\ast\bullet q}(\bullet R).
\end{equation*}
\notag
$$
Здесь $\Gamma,\Delta=p^l,q,A_{n_1},\dots,A_{n_k}$. Из леммы 3 следует, что $\Delta=q$. Но тогда $k=0$, что неверно. Случай 1 невозможен.
Случай 2. Последнее правило – $(\setminus L)$, его главной формулой является формула $A_{n_i}$ (напомним, что она имеет вид $q\setminus X$):
$$
\begin{equation*}
\frac{\Gamma,X,\Delta\Rightarrow p^\ast\bullet q\quad \Pi\Rightarrow q} {\Gamma,\Pi,q\setminus X,\Delta\Rightarrow p^\ast\bullet q}(\setminus L).
\end{equation*}
\notag
$$
Здесь $\Gamma,\Pi=p^l,q,A_{n_1},\dots,A_{n_{i-1}}$ и $\Delta=A_{n_{i+1}},\dots,A_{n_k}$. Применяя лемму 3, заключаем, что $\Pi=q$; как следствие, $i=1$, и $\Gamma=p^l$.
Случай 2a. Пусть $n_1=0$, т.е. $X=p\bullet q$. Произведем анализ подвывода, заканчивающегося секвенцией $\Gamma,X,\Delta\Rightarrow p^\ast\bullet q$ (заметим, что она имеет вид $p^l,p\bullet q,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q$). По лемме 3 последним правилом, применяемым в ее выводе, не может быть ни $(\setminus L)$, ни $(\bullet R)$, поскольку бы это означало, что в антецеденте данной секвенции есть формула $q$, что неверно. Как следствие, последнее правило – $(\bullet L)$:
$$
\begin{equation*}
\frac{p^{l+1},q,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q} {p^l,p\bullet q,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q}(\bullet L).
\end{equation*}
\notag
$$
По предположению индукции посылка данного правила имеет единственный вывод, а ее ранг не меньше $\omega^{n_k}+\dotsb+\omega^{n_2}$. Таким образом, секвенция (2.1) также имеет единственный вывод, а ее ранг не меньше $\omega^{n_k}+\dotsb+\omega^{n_2}+2\geqslant\omega^{n_k}+\dotsb+\omega^{n_1}$.
Случай 2b. Если $n_k>0$, то $X=(q\bullet A_{n_1-1}^\ast)$. Аналогично предыдущему случаю доказывается, что последним правилом в выводе секвенции
$$
\begin{equation*}
p^l,q\bullet A_{n_1-1}^\ast,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q
\end{equation*}
\notag
$$
должно быть $(\bullet L)$:
$$
\begin{equation*}
\frac{p^l,q,A_{n_1-1}^\ast,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q} {p^l,q\bullet A_{n_1-1}^\ast,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q}(\bullet L).
\end{equation*}
\notag
$$
По лемме 3 последним правилом в выводе посылки правила выше должно быть правило $(\ast L)$:
$$
\begin{equation*}
\frac{(p^l,q,A_{n_1-1}^m,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q)_{m<\omega}} {p^l,q,A_{n_1-1}^\ast,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q}(\ast L).
\end{equation*}
\notag
$$
По предположению индукции каждая из секвенций $p^l,q,A_{n_1-1}^m,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q$ имеет единственный вывод и ранг секвенции с номером $m$ не меньше $\omega^{n_k}+\dotsb+\omega^{n_2}+\omega^{n_{1}-1}\cdot m$. Из этого следует, что ранг секвенции
$$
\begin{equation*}
p^l,q,A_{n_1-1}^\ast,A_{n_2},\dots,A_{n_k}\Rightarrow p^\ast\bullet q
\end{equation*}
\notag
$$
(которая, как следствие, также имеет единственный вывод) не меньше
$$
\begin{equation*}
\sup_{m<\omega}(\omega^{n_k}+\dotsb+\omega^{n_2}+\omega^{n_1-1}\cdot m) =\omega^{n_k}+\dotsb+\omega^{n_1}.
\end{equation*}
\notag
$$
Рассуждения выше показывают, что и у секвенции (2.1) вывод единственный, а ее ранг не меньше $\omega^{n_k}+\dotsb+\omega^{n_1}$, что и требовалось доказать. Теорема 3 доказана. Из теоремы 3 напрямую следует теорема 1. Действительно, секвенция $q,A_n\Rightarrow p^\ast\bullet q$ выводима, но не принадлежит $\mathscr T_\alpha$ при $\alpha<\omega^n$. Замечание 2. В конструкции секвенции (2.1) из теоремы 3 были использованы только операции $\setminus$, $\bullet$ и $\ast$. Таким образом, замыкающий ординал для фрагмента $\mathrm{ACT}_\omega$, в котором формулы определяются только через три данных операции, также равен $\omega^\omega$. Замечание 3. Идея конструкции секвенции (2.1) состоит в том, чтобы примитивная формула $q$ “двигалась слева направо”, постепенно “раскрывая” формулы $A_{n_1},\dots,A_{n_k}$. При этом если $n_1$ равно, скажем, $2$, то в процессе вывода (если смотреть на него снизу вверх) $A_2$ заменится последовательностью $A_1,\dots,A_1$ из $m$ формул, после чего формула $q$ будет “раскрывать” самую левую формулу $A_1$; она в свою очередь будет заменена последовательностью $A_0,\dots,A_0$ из произвольного числа $m'$ формул; и так далее. Именно необходимость каждый раз раскрывать самую левую формулу обеспечивает высокий ранг секвенции. Замечание 4. Наличие формулы $p$ внутри $A_0=q\setminus(p\bullet q)$ требуется, чтобы доказать лемму 3. Если бы $A_0$ равнялась бы $q\setminus q$, а секвенция (2.1) имела вид $q,A_{n_1},\dots,A_{n_k}\Rightarrow q$, то лемму 3 применить было бы нельзя. Более того, анализировать выводы такой секвенции было бы значительно труднее. 2.2. Доказательство теоремы 2Коммутативная инфинитарная логика действий $\mathrm{CommACT}_\omega$ получается из логики $\mathrm{ACT}_\omega$, если изменить определение секвенции, сказав, что она имеет вид $\Gamma\Rightarrow A$, где $A$ – формула, а $\Gamma$ – мультимножество формул. Ясно, что деления $B\setminus A$ и $A/B$ становятся эквивалентными, и достаточно использовать только одно из них. Чтобы отличать умножение и деление в $\mathrm{CommACT}_\omega$ от умножения и делений в $\mathrm{ACT}_\omega$, будем обозначать их как $\otimes$ и $\multimap$ соответственно, следуя традиции линейной логики (это делается также для удобства некоторых дальнейших обозначений). Условимся, что
$$
\begin{equation*}
\bigwedge_{i=M}^NT_i=\bigl((\dots((T_M\wedge T_{M+1})\wedge T_{M+2})\wedge\dots) \wedge T_{N-1}\bigr)\wedge T_N;
\end{equation*}
\notag
$$
аналогичное сокращение будем использовать и для операций $\vee$ и $\otimes$. Заметим, что конструкция секвенции (2.1) из теоремы 3 не подходит для коммутативного случая, поскольку в доказательстве существенно, что формула $q$ “движется” слева направо. Несложно показать, что ранги секвенций вида (2.1) относительно $\mathrm{CommACT}_\omega$ значительно меньше и они не дают в пределе $\omega^\omega$. Как следствие, требуется другая конструкция секвенций, ранги которых стремятся к $\omega^\omega$ и выводы которых легко анализировать в коммутативном случае. Зафиксируем $N\in\mathbb N$; введем примитивные формулы $t$, $t'$, $q_i$, $r_i$, $z_i$, где $i=0,\dots,N$. Определим формулы, используемые в основной конструкции:
Теорема 4. Секвенция где $k\geqslant 0$; $N>n_1\geqslant\dotsb\geqslant n_k\geqslant 0$; $m=n_k$, если $k>0$, и $m=N$ иначе, выводится, и ее ранг не меньше $\omega^{n_1}+\dotsb+\omega^{n_k}$. Для доказательства данной теоремы будут полезны следующие наблюдения о возможности “обратить” некоторые из правил $\mathrm{CommACT}_\omega$ без увеличения ранга секвенции. Лемма 4. Дана секвенция $\Gamma,D\Rightarrow C$, где $D$ не входит положительно в $C$ и не входит отрицательно в формулы из $\Gamma$. Тогда выполнены следующие утверждения: Понятия положительного и отрицательного вхождения формулы в формулу или в последовательность формул определяются стандартным образом:
Доказательство леммы 4. Доказательство всех утверждений леммы следует одной и той же схеме. Во-первых, заметим, что в каждом из утверждений часть “тогда” очевидно следует из вида правил вывода $\mathrm{CommACT}_\omega$. Будем доказывать части “только тогда” каждого из утверждений, т.е. что из выводимости $\Gamma,D\Rightarrow C$ следует выводимость тех или иных секвенций в зависимости от утверждения; одновременно будем доказывать утверждения о рангах. Рассуждения ведутся индукцией по рангу секвенции $\Gamma,D\Rightarrow C$. Обозначим через $\Delta$ последовательность формул, которая равна $A$, $B$ для случая, когда $D=A\otimes B$, равна $A_i$ для случая, когда $D=A_1\vee A_2$ (для $i=1$ или $i=2$), и равна $A^m$ для случая, когда $D=A^\ast$ (для некоторого $m\in\mathbb N$).
База индукции – когда ранг $\Gamma,D\Rightarrow C$ равен 1, т.е. секвенция является аксиомой. Она не может иметь вид $D\Rightarrow D$, поскольку тогда $D$ положительно входит в $C$; значит, $\Gamma$ содержит константу $\mathbf 0$. Но тогда и $\Gamma,\Delta\Rightarrow C$ является аксиомой, а ее ранг также равен 1. Для доказательства шага индукции зафиксируем оптимальный вывод секвенции $\Gamma,D\Rightarrow C$ и рассмотрим последнее правило в этом выводе. Случай 1. Формула $D$ не является главной в последнем примененном правиле. Тогда это правило в общем виде выглядит так:
$$
\begin{equation*}
\frac{(\Gamma_n,D\Rightarrow C_n)_{n<\alpha}\quad \mathscr S}{\Gamma,D\Rightarrow C}\,.
\end{equation*}
\notag
$$
Здесь $\mathscr S$ – некоторое множество посылок. Иначе говоря, некоторые из посылок правила содержат $D$ (эти посылки обозначены как $\Gamma_n,D\Rightarrow C_n$), а некоторые – нет (множество последних было обозначено за $\mathscr S$).
Ранг каждой секвенции $\Gamma_n,D\Rightarrow C_n$ строго меньше, чем $\Gamma,D\Rightarrow C$, что следует из определения оптимального вывода. По предположению индукции секвенция $\Gamma_n,\Delta\Rightarrow C_n$ выводится и
$$
\begin{equation*}
\mathrm{rk}(\Gamma_n,\Delta\Rightarrow C_n)\leqslant\mathrm{rk}(\Gamma_n,D\Rightarrow C_n).
\end{equation*}
\notag
$$
Возьмем оптимальный вывод секвенции $\Gamma_n,\Delta\Rightarrow C_n$ для каждого $n<\alpha$; подставим данные выводы в следующее правило:
$$
\begin{equation*}
\frac{(\Gamma_n,\Delta\Rightarrow C_n)_{n<\alpha}\quad \mathscr S}{\Gamma,\Delta\Rightarrow C}\,.
\end{equation*}
\notag
$$
В результате получится вывод секвенции $\Gamma,\Delta\Rightarrow C$. Ранг $\Gamma,\Delta\Rightarrow C$ не превосходит ранга данного вывода, из чего можно получить следующую цепочку неравенств:
$$
\begin{equation*}
\begin{aligned} \, \mathrm{rk}(\Gamma,\Delta\Rightarrow C) &\leqslant\sup\bigl(\{\mathrm{rk}(\Gamma_n,\Delta\Rightarrow C_n)\mid n<\alpha\} \cup\{\mathrm{rk}(\sigma)\mid\sigma\,{\in}\,\mathscr S\}\bigr)+1 \\ &\leqslant\sup\bigl(\{\mathrm{rk}(\Gamma_n,D\Rightarrow C_n)\mid n<\alpha\} \cup\{\mathrm{rk}(\sigma)\mid\sigma\,{\in}\,\mathscr S\}\bigr)+1 =\mathrm{rk}(\Gamma,D\Rightarrow C). \end{aligned}
\end{equation*}
\notag
$$
Последнее равенство следует из оптимальности зафиксированного вывода секвенции $\Gamma,D\Rightarrow C$.
Случай 2. Формула $D$ является главной. Разберем случай, когда $D=A\otimes B$. Тогда последнее правило в зафиксированном выводе имеет следующий вид: Как следствие, Остальные случаи рассматриваются аналогично.Сформулируем теперь техническую лемму, аналогичную лемме 3 для некоммутативного случая. Пусть $\mathrm{SFm}_2$ – множество подформул формулы $B_N$; оно в том числе содержит формулы $B_i$, $B'_i$, $B''_i$ для всех $i=0,\dots,N$ и примитивные формулы $z_i$, $q_i$, $r_i$, $t$, $t'$. Лемма 5. Если секвенция $\Gamma\Rightarrow T$ выводится, причем $\Gamma$ – мультимножество формул из $\mathrm{SFm}_2$, а $T$ – одна из формул $q_i$, $r_i$, $z_i$, $t$ или $t'$, то $\Gamma=T$. Доказательство леммы 5 аналогично доказательству леммы 3. Важным является факт, что множество $\mathrm{SFm}_2$ не содержит формул вида $Y\multimap T$, $Y\wedge T$, $T\wedge Y$ и $T\vee T$, где $T$ равна $q_i$, $r_i$, $z_i$, $t$ или $t'$. Следствие 1. Пусть $T$ – одна из формул $q_i$, $r_i$, $z_i$, $t$ или $t'$, а $\Gamma$ – мультимножество формул из $\mathrm{SFm}_2$, не содержащее $T$. Тогда выполнены следующие утверждения: Нами в основном будет использоваться данное следствие. Приведем пример его применения. Пример 3. Частным случаем теоремы 4 является утверждение, что секвенция $B_2,B_2,q_2,t\Rightarrow S$ выводима (при $N\geqslant 3$). Проанализируем, каким может быть вывод данной секвенции. Зафиксируем некоторый ее вывод. Главной формулой в последнем правиле в нем может быть либо формула $B_2$, либо формула $S$. Если главная формула – $B_2=t\multimap(C_2\wedge B'_2)$, то последнее правило в выводе имеет вид
$$
\begin{equation*}
\frac{\Gamma,C_2\wedge B'_2\Rightarrow S\quad \Delta\Rightarrow t} {B_2,B_2,q_2,t\Rightarrow S}(\multimap L).
\end{equation*}
\notag
$$
Здесь $\Gamma,\Delta=B_2,q_2,t$. Из леммы 5 следует, что $\Delta=t$, поэтому $\Gamma=B_2,q_2$. Рассмотрим подвывод, являющийся выводом секвенции $B_2,q_2,C_2\wedge B'_2\Rightarrow S$, а в нем – последнее правило. По следствию 1 в нем главной формулой не может быть ни $B_2$, ни $S$. Значит, главной формулой является $C_2\wedge B'_2$. Как следствие, последнее правило в выводе секвенции $B_2,q_2,C_2\wedge B'_2\Rightarrow S$ имеет один из двух видов:
$$
\begin{equation*}
\frac{B_2,q_2,C_2\Rightarrow S}{B_2,q_2,C_2\wedge B'_2\Rightarrow S}(\wedge L_1),\qquad \frac{B_2,q_2,B'_2\Rightarrow S}{B_2,q_2,C_2\wedge B'_2\Rightarrow S}(\wedge L_2).
\end{equation*}
\notag
$$
Заметим однако, что секвенция $B_2,q_2,C_2\Rightarrow S$ не выводима, что следует из следствия 1 (напомним, что $C_2=t'\multimap(t\otimes t'\otimes r_2)$). Значит, последнее правило – $(\wedge L_2)$. Формула $B'_2$ равна $q_2\multimap B''_2$. В последнем правиле вывода секвенции $B_2,q_2,q_2\multimap B''_2\Rightarrow S$ главной формулой опять же не может быть ни $B_2$, ни $S$, поскольку в антецеденте секвенции нет $t$. Значит, главной является формула $q_2\multimap B''_2$, и правило имеет следующий вид (здесь снова применяется лемма 5):
$$
\begin{equation*}
\frac{B_2,B''_2\Rightarrow S\quad q_2\Rightarrow q_2} {B_2,q_2,q_2\multimap B''_2\Rightarrow S}(\multimap L).
\end{equation*}
\notag
$$
Разберем второй вариант: главной формулой в последнем правиле вывода секвенции $B_2,B_2,q_2,t\Rightarrow S$ является $S=t\otimes(q_N\vee S')$. Тогда последнее правило в выводе имеет вид
$$
\begin{equation*}
\frac{\Gamma\Rightarrow t\quad \Delta\Rightarrow q_N\vee S'} {B_2,B_2,q_2,t\Rightarrow t\otimes(q_N\vee S')}(\multimap L).
\end{equation*}
\notag
$$
Из леммы 5 следует, что $\Gamma=t$, а $\Delta=B_2,B_2,q_2$. Рассмотрим подвывод секвенции $B_2,B_2,q_2\Rightarrow q_N\vee S'$; вспомним, что $S'=t'\otimes S''$. По следствию 1 формула $B_2$ не может быть главной в последнем правиле данного подвывода, а значит, главной является $q_N\vee S'$. Значит, в посылке правила, заключением которого является $\Delta\Rightarrow q_N\vee S'$, стоит либо секвенция $\Delta\Rightarrow q_N$, либо секвенция $\Delta\Rightarrow S'$. По лемме 5 первый вариант невозможен, ведь секвенция $\Delta\Rightarrow q_N$ выводится только в случае, когда $\Delta=q_N$, что неверно. Предположим, что выводится секвенция $\Delta\Rightarrow S'$; она имеет вид $B_2,B_2,q_2\Rightarrow t'\otimes S''$. Однако по следствию 1 ни $B_2$, ни $t'\otimes S''$ не могут быть главными формулами в последнем правиле вывода рассматриваемой секвенции, что приводит к противоречию. Секвенция $\Delta\Rightarrow q_N\vee S'$ не может быть выведена. Итак, доказано, что нижняя (завершающая) часть любого вывода секвенции $B_2,B_2,q_2,t\Rightarrow S$ имеет следующий вид:
$$
\begin{equation*}
\frac{\dfrac{\dfrac{B_2,B''_2\Rightarrow S\quad q_2\Rightarrow q_2} {B_2,q_2,q_2\multimap B''_2\Rightarrow S}(\multimap L)} {B_2,q_2,C_2\wedge B'_2\Rightarrow S\quad t\Rightarrow t}(\wedge L_2)} {B_2,B_2,q_2,t\Rightarrow S}(\multimap L).
\end{equation*}
\notag
$$
Часть доказательства теоремы 4 имеет ту же структуру: в ней теми же способами используются лемма 2, лемма 4, лемма 5 и cледствие 1. Обобщением леммы 5 является следующая Лемма 6. Пусть $\Gamma$ – мультимножество формул из $\mathrm{SFm}_2$. Тогда выполнены следующие утверждения: Доказательство. Первое утверждение доказывается индукцией по рангу фиксированного вывода секвенции $\Gamma\Rightarrow r_j^\ast$. Отметим, что аксиомой она быть не может. Рассмотрим последнее правило в ее выводе. Как и в случае леммы 3 и леммы 5, оно не может быть ни одним из левых правил $(\otimes L)$, $(\multimap L)$, $(\vee L)$, $(\wedge L)$, $(\ast L)$. Чтобы это доказать, следует рассмотреть возможный вид каждого из этих правил, применить предположение индукции к посылке с сукцедентом $r_j^\ast$, а далее заметить, что в $\mathrm{SFm}_2$ отсутствуют формулы вида $Y \multimap r_j$, $Y\wedge r_j$, $r_j\wedge Y$, $r_j\vee r_j$, а также $r_j\otimes r_j$. Из этого следует, что последним правилом в выводе может быть только $(\ast R)$, т.е. существует представление $\Gamma$ в виде $\Gamma=\Gamma_1,\dots,\Gamma_l$ такое, что правило имеет вид
$$
\begin{equation*}
\frac{\Gamma_1\Rightarrow r_j,\dots,\Gamma_l\Rightarrow r_j} {\Gamma_1,\dots,\Gamma_l\Rightarrow r_j^\ast}(\ast R).
\end{equation*}
\notag
$$
Применяя лемму 5 к каждой из посылок, заключаем, что $\Gamma_1=\dotsb=\Gamma_l=r_j$, что и требовалось доказать.
Доказательство второго утверждения ведется двойной индукцией: по $N$ и по рангу вывода секвенции $\Gamma\Rightarrow\bigotimes_{j=i}^Nr_j^\ast$. При $i=N$ второе утверждение совпадает с первым. Докажем шаг индукции. Как и для первого утверждения, рассмотрим последнее правило вывода данной секвенции; используя предположение индукции, можно тем же способом показать, что оно не может быть левым. Значит, последнее правило в выводе – это $(\otimes R)$, т.е. оно имеет следующий вид где $\Gamma=\Gamma',\Gamma''$: По первому, уже доказанному, утверждению, $\Gamma''=r_N^{l_N}$ для некоторого $l_N$. По предположению индукции $\Gamma'=r_i^{l_i},\dots,r_{N-1}^{l_{N-1}}$ для некоторых $l_i,\dots,l_{N-1}$. В совокупности это доказывает второе утверждение.Приступим к доказательству теоремы 4. Доказательство теоремы 4. Целью является доказать, что секвенция (2.2) вида выводится и что ее ранг не меньше $\rho=\omega^{n_1}+\dotsb+\omega^{n_k}$. Доказательство будет вестись трансфинитной индукцией по $\rho$. Если $\rho=0$, то $m=N$, а секвенция (2.2) имеет вид $q_N,t\Rightarrow t\otimes(q_N\vee S')$. Она, очевидно, выводится, при этом утверждение о ранге выполнено тривиальным образом.
Перейдем к доказательству шага индукции, предполагая, что $\rho>0$ (эквивалентно, $k>0$). Будем строить вывод секвенции (2.2) снизу вверх, анализируя, каким он может быть. Рассмотрим возможный вид последнего правила в данном выводе. Случай 1. Главной формулой в последнем правиле является $S$. В таком случае по лемме 5 в посылке правила находятся секвенции $B_{n_1},\dots,B_{n_k},q_m\Rightarrow q_N\vee S'$ и $t\Rightarrow t$. В правиле, заключением которого является первая из этих секвенций, по следствию 1 ни одна из формул $B_{n_i}$ не может быть главной, значит, главной является $q_N\vee S'$. Однако ни $B_{n_1},\dots,B_{n_k},q_m\Rightarrow q_N$, ни $B_{n_1},\dots,B_{n_k},q_m\Rightarrow S'$ не выводятся (что следует из леммы 5 и следствия 1 соответственно). Значит, случай 1 невозможен. Случай 2. Главной формулой в последнем правиле является $B_{n_i}$ для некоторого $i\in\{1,\dots,k\}$. Обозначим $n_i$ через $n$, а мультимножество $B_{n_1},\dots,B_{n_k}$ – через $\Theta$; через $\Theta'$ обозначим $\Theta$ без $B_n$. Поскольку $B_n=t\multimap(C_n\wedge B'_n)$, последнее правило в любом выводе (2.2) есть $(\multimap L)$:
$$
\begin{equation*}
\frac{\Theta',C_n\wedge B'_n,q_m\Rightarrow S\quad t\Rightarrow t} {\Theta',t\multimap(C_n\wedge B'_n),q_m,t\Rightarrow S}(\multimap L).
\end{equation*}
\notag
$$
В последнем правиле любого вывода секвенции по следствию 1 главной формулой может быть только $C_n\wedge B'_n$ (поскольку в антецеденте нет $t$). Также по следствию 1 секвенция $\Theta',C_n,q_m\Rightarrow S$ не выводится (никакая формула в ней не может быть главной), а значит, последнее правило в любом выводе (2.3) имеет следующий вид:
$$
\begin{equation*}
\frac{\Theta',B'_n,q_m\Rightarrow S}{\Theta',C_n\wedge B'_n,q_m\Rightarrow S}(\wedge L_2).
\end{equation*}
\notag
$$
В последнем правиле любого вывода секвенции по следствию 1 главной формулой может быть только $B'_n=q_n\multimap B''_n$. Также по следствию 1 в антецеденте (2.4) должна быть формула $q_n$. Как следствие, $m=n$; так как $m=n_k$, можно без ограничения общности считать, что $i=k$. Таким образом, последнее правило в любом выводе (2.4) имеет следующий вид:
$$
\begin{equation*}
\frac{\Theta',B''_n\Rightarrow S,\quad q_n\Rightarrow q_n} {\Theta',B'_n,q_n\Rightarrow S}(\multimap L).
\end{equation*}
\notag
$$
Мультимножество $\Theta'$ равно $B_{n_1},\dots,B_{n_{k-1}}$.
Из всех рассуждений, приведенных выше, следует, что секвенция (2.2) выводится тогда и только тогда, когда выводится Помимо этого по лемме 2 если они обе выводятся, то ранг секвенции (2.2) больше ранга секвенции (2.5).Замечание 5. Из рассуждений выше также следует, что секвенция не выводится, если $k>0$ и $i<n_k\leqslant n_{k-1}\leqslant\dotsb\leqslant n_1$. Случай 2a: $n=n_k>0$. Тогда $B''_n=t\otimes q_{n-1}\otimes B_{n-1}^\ast$. По лемме 4 секвенция (2.5) выводима тогда и только тогда, когда для каждого $l\in\mathbb N$ выводима секвенция $\Theta',B_{n-1}^l,q_{n-1},t\Rightarrow S$, и в случае их выводимости
$$
\begin{equation*}
\mathrm{rk}(\Theta', B''_n\Rightarrow S) \geqslant\mathrm{rk}(\Theta',B_{n-1}^l,q_{n-1},t\Rightarrow S)
\end{equation*}
\notag
$$
для каждого $l\in\mathbb N$. Поскольку $\Theta'=B_{n_1},\dots,B_{n_{k-1}}$ и поскольку $n_{k-1}\geqslant n_k=n>n- 1$, к секвенции $\Theta',B_{n-1}^l,q_{n-1},t\Rightarrow S$ применимо предположение индукции; согласно нему она выводится и ее ранг не меньше $\omega^{n_1}+\dotsb+\omega^{n_{k-1}}+\omega^{n_k-1}\cdot l$ (заметим, что этот ординал меньше $\rho$; это дало возможность применить предположение индукции). Как следствие, секвенция (2.2) выводится, и ее ранг не меньше
$$
\begin{equation*}
\sup_l\mathrm{rk}(\Theta',B_{n-1}^l,q_{n-1},t\Rightarrow S) \geqslant\sup_l (\omega^{n_1}+\dotsb+\omega^{n_{k-1}}+\omega^{n_k-1}\cdot l)=\rho,
\end{equation*}
\notag
$$
что и требовалось доказать. Случай 2b: $n=0$. В этом случае
$$
\begin{equation*}
B''_n=Q=\bigwedge_{i=0}^N\bigl((q_i\vee(z_i\otimes t'))\otimes t\bigr),
\end{equation*}
\notag
$$
и секвенция (2.5) имеет следующий вид:
$$
\begin{equation*}
\Theta',\bigwedge_{i=0}^N\bigl((q_i\vee(z_i\otimes t'))\otimes t\bigr)\Rightarrow S.
\end{equation*}
\notag
$$
По следствию 1 главной формулой в последнем правиле вывода этой секвенции должна быть формула $Q$. Более того, из следствия 1, примененного $N$ раз, следует, что секвенция (2.5) выводится одновременно с одной из секвенций
$$
\begin{equation}
\Theta',(q_i\vee(z_i\otimes t'))\otimes t\Rightarrow S,
\end{equation}
\tag{2.6}
$$
где $i\in\{0,\dots,N\}$; если выводимость имеет место, то ранг (2.5) больше ранга (2.6). По лемме 4 секвенция (2.6) выводится тогда и только тогда, когда выводятся обе следующие секвенции: При этом ранг (2.6) не меньше рангов обеих этих секвенций. Если бы к секвенции (2.7) можно было применить предположение индукции, из него бы следовало, что она выводится и что ее ранг не меньше $\rho'=\omega^{n_1}+\dotsb+\omega^{n_{k-1}}$. Тогда, если (2.8) также выводится, то выводится и (2.2), причем ее ранг больше ранга (2.7) и, как следствие, не меньше $\rho'+1=\rho$. Для применения предположения индукции к (2.7) необходимо доказать, что $i=n_{k-1}$, так как $\Theta'=B_{n_1},\dots,B_{n_{k-1}}$. Для этого сформулируем промежуточное утверждение, которое удобно доказывать по индукции. Лемма 7. Пусть $n_1,\dots,n_k$ и $m_1,\dots,m_l$ – два мультимножества натуральных чисел. Секвенция выводится тогда и только тогда, когда $i$ не больше каждого из чисел $n_1,\dots,n_k,m_1,\dots,m_l$. Завершим доказательство теоремы (доказательство леммы 7 будет представлено после него). Если секвенция (2.2) выводится, то для некоторого $i$ выводятся обе секвенции (2.7) и (2.8). Из замечания 5 следует, что $i\geqslant n_{k-1}$. С другой стороны, из леммы 7, примененной к (2.8), следует, что $i\leqslant n_{k-1}$, т.е. $i=n_{k-1}$. Как следствие, к секвенции (2.7) можно применить предположение индукции, из чего, как было показано выше, следует утверждение о ранге (2.2). С другой стороны, по предположению индукции (2.7) действительно выводится при $i=n_{k-1}$; по лемме 7, выводится также и (2.8). Значит, и (2.2) выводится. Теорема 4 доказана. Теперь докажем лемму 7. Доказательство леммы 7. Индукция по $k$. Если у секвенции (2.9) существует вывод, то зафиксируем его и рассмотрим последнее правило в нем. Обозначим через $\Phi$ мультимножество $B_{n_1},\dots,B_{n_k}$, а через $\Psi$ – мультимножество $r_{m_1},\dots,r_{m_l}$.
Случай i. Главная формула в последнем правиле – $B_{n_j}=t\multimap(C_{n_j}\wedge B'_{n_j})$ для некоторого $j\in\{1,\dots,k\}$. Тогда последнее правило в выводе (2.9) имеет следующий вид:
$$
\begin{equation*}
\frac{\Phi',C_{n_j}\wedge B'_{n_j},\Psi,z_i,t'\Rightarrow S\quad t\Rightarrow t} {\Phi,\Psi,z_i,t',t\Rightarrow S}(\multimap L).
\end{equation*}
\notag
$$
Здесь $\Phi=\Phi',B_{n_j}$. Главной формулой в последнем правиле вывода секвенции
$$
\begin{equation}
\Phi',C_{n_j}\wedge B'_{n_j},\Psi,z_i,t'\Rightarrow S
\end{equation}
\tag{2.10}
$$
может быть только $C_{n_j}\wedge B'_{n_j}$ (по следствию 1). Значит, в посылке правила стоит либо секвенция $\Phi',C_{n_j},\Psi,z_i,t'\Rightarrow S$, либо секвенция $\Phi',B'_{n_j},\Psi,z_i,t'\Rightarrow S$. Второе однако невозможно, так как данная секвенция не является аксиомой, при этом ни одна формула в ней не может быть главной (по следствию 1, так как в антецеденте секвенции нет ни формулы $t$, ни формулы $q_{n_j}$), значит, она не выводится. Итак, последнее правило в выводе (2.10) – это $(\wedge L_1)$, в его посылке стоит секвенция В последнем правиле вывода данной секвенции главной формулой может быть только $C_{n_j}=t'\multimap(t\otimes t'\otimes r_{n_j})$ по тем же причинам. Значит, это правило имеет следующий вид:
$$
\begin{equation*}
\frac{\Phi',t\otimes t'\otimes r_{n_j},\Psi,z_i\Rightarrow S\quad t'\Rightarrow t'} {\Phi',C_{n_j},\Psi,z_i,t'\Rightarrow S}(\multimap L).
\end{equation*}
\notag
$$
Секвенция $\Phi',t\otimes t'\otimes r_{n_j},\Psi,z_i\Rightarrow S$ выводится, если и только если выводится секвенция $\Phi',r_{n_j},\Psi,z_i,t',t\Rightarrow S$. К последней секвенции можно применить предположение индукции и заключить, что она выводима тогда и только тогда, когда $i$ не больше каждого из чисел $n_1,\dots,n_k,m_1,\dots,m_l$.
Случай ii. Главная формула в последнем правиле вывода секвенции (2.9) – $S=t\otimes(q_N\vee S')$. Тогда последнее правило в выводе (2.9) имеет следующий вид:
$$
\begin{equation*}
\frac{\Phi,\Psi,z_i,t'\Rightarrow q_N\vee S',\quad t\Rightarrow t} {\Phi,\Psi,z_i,t',t\Rightarrow S}(\otimes R).
\end{equation*}
\notag
$$
Главной формулой в последнем правиле вывода секвенции может быть только $q_N\vee S'$, причем, поскольку секвенция $\Phi,\Psi,z_i,t'\Rightarrow q_N$ не выводится (лемма 5), выводимость эквивалентна выводимости Главной формулой в последнем правиле вывода данной секвенции может быть только $S'=t'\otimes S''$, т.е. это правило имеет следующий вид:
$$
\begin{equation*}
\frac{t'\Rightarrow t'\quad \Phi,\Psi,z_i\Rightarrow S''} {\Phi,\Psi,z_i,t'\Rightarrow S'}(\otimes R).
\end{equation*}
\notag
$$
Исследуем выводимость секвенции
$$
\begin{equation}
\Phi,\Psi,z_i\Rightarrow\bigvee_{p=0}^N \biggl(\bigotimes_{j=p}^Nr_j^\ast\otimes z_p\biggr),
\end{equation}
\tag{2.11}
$$
стоящей в правой посылке данного правила. Поскольку ни одна формула из $\Phi$ не может быть главной, главной является формула в сукцеденте, причем это будет верно и в случае, когда вместо этой формулы стоит любая другая формула. Как следствие, (2.11) выводима тогда и только тогда, когда выводима одна из формул
$$
\begin{equation*}
\Phi,\Psi,z_i\Rightarrow\bigotimes_{j=p}^Nr_j^\ast\otimes z_p.
\end{equation*}
\notag
$$
Главной формулой в последнем правиле вывода этой секвенции снова может быть только формула в сукцеденте; как следствие, $i=p$ и правило имеет следующий вид:
$$
\begin{equation*}
\frac{\Phi,\Psi\Rightarrow\bigotimes_{j=i}^Nr_j^\ast,\quad z_i\Rightarrow z_i} {\Phi,\Psi,z_i\Rightarrow\bigotimes_{j=i}^Nr_j^\ast\otimes z_i}(\otimes R).
\end{equation*}
\notag
$$
Из леммы 6 следует, что секвенция $\Phi,\Psi\Rightarrow\bigotimes_{j=i}^Nr_j^\ast$ выводится тогда и только тогда, когда $\Phi$, $\Psi$ – мультимножество, состоящее только из формул $r_i,\dots,r_N$ (в частности, $\Phi=\Lambda$, т.е. $k=0$). Поскольку $\Psi=r_{m_1},\dots,r_{m_l}$, это эквивалентно тому, что $i\leqslant\min\{m_1,\dots,m_l\}$.
Итак, в каждом из случаев показано, что выводимость секвенции (2.9) равносильна тому, что $i\leqslant\min\{n_1,\dots,n_k,m_1,\dots,m_l\}$, что и требовалось. 2.3. Об инфинитарной логике действий с правилом сеченияТеоремы 1 и 2 были доказаны для конкретной, “стандартной” аксиоматизации инфинитарной логики действий, представленной в разделе 1. В эту аксиоматизацию однако не включено правило сечения ($\mathrm{cut}$):
$$
\begin{equation*}
\frac{\Pi\Rightarrow A,\quad \Gamma,A,\Delta\Rightarrow C} {\Gamma,\Pi,\Delta\Rightarrow C}(\mathrm{cut}).
\end{equation*}
\notag
$$
В работе [1] доказано, что правило сечения допустимо в $\mathrm{ACT}_\omega$, т.е. добавление его в список правил не увеличивает множество выводимых секвенций; это классический результат для исчисления генценовского типа. Однако замыкающий ординал для $\mathrm{ACT}_\omega+(\mathrm{cut})$ может оказаться меньше, чем замыкающий ординал для $\mathrm{ACT}_\omega$, потому что, неформально говоря, ранги секвенций относительно $\mathrm{ACT}_\omega+(\mathrm{cut})$ могут оказаться значительно меньше их рангов относительно $\mathrm{ACT}_\omega$. Как оказывается, это и происходит. Обозначим через $\mathrm{ACT}_\omega+(\mathrm{cut})$ инфинитарную логику действий с правилом сечения. Докажем следующую теорему. Теорема 5. Ранг секвенции относительно $\mathrm{ACT}_\omega+(\mathrm{cut})$ не больше $\omega\cdot(n+1)+5$, в то время как ее ранг относительно $\mathrm{ACT}_\omega$ не меньше $\omega^n$ (формула $A_n$ была определена в п. 2.1). Напомним определение $A_n$:
$$
\begin{equation*}
A_0=q\setminus(p\bullet q),\qquad A_{k+1}=q\setminus(q\bullet A_k^\ast).
\end{equation*}
\notag
$$
Определим также формулу $B=q\setminus(p^\ast\bullet q)$. Для доказательства теоремы 5 достаточно доказать верхнюю оценку на ранг (2.12) относительно $\mathrm{ACT}_\omega+(\mathrm{cut})$; нижняя оценка на ранг данной секвенции относительно $\mathrm{ACT}_\omega$ следует из теоремы 1 и приводится в качестве напоминания. Обратим внимание читателя на то, что в данном пункте рассматривается некоммутативная логика $\mathrm{ACT}_\omega$. Лемма 8. Ранг секвенции $p^t,q,B^m\Rightarrow p^\ast\bullet q$ относительно $\mathrm{ACT}_\omega+(\mathrm{cut})$ не больше $3m+2$. Доказательство. Индукция по $m$. При $m=0$ секвенция выводится следующим образом:
$$
\begin{equation*}
\frac{\dfrac{p\Rightarrow p,\dots,p\Rightarrow p} {p^t\Rightarrow p^\ast\quad q\Rightarrow q}(\ast R)}{p^t,q\Rightarrow p^\ast\bullet q}(\bullet R).
\end{equation*}
\notag
$$
Как следствие, ее ранг не превосходит 2. Докажем шаг индукции, рассмотрев следующий вывод секвенции $p^t,q,B^{m+1}\Rightarrow p^\ast\bullet q$:
$$
\begin{equation*}
\frac{\dfrac{\dfrac{(p^{t+t'},q,B^m\Rightarrow p^\ast\bullet q)_{t'<\omega}} {p^t,p^\ast,q,B^m\Rightarrow p^\ast\bullet q}(\ast L)} {p^t,p^\ast\bullet q,B^m\Rightarrow p^\ast\bullet q\quad q\Rightarrow q}(\bullet L)} {p^t,q,B^{m+1}\Rightarrow p^\ast\bullet q}(\bullet R).
\end{equation*}
\notag
$$
По предположению индукции ранг каждой из секвенций $p^{t+t'},q,B^m\Rightarrow p^\ast\bullet q$ не превосходит $3m+2$. Как следствие, ранг секвенции $p^t,q,B^{m+1}\Rightarrow p^\ast\bullet q$ не превосходит $3m+2+3=3(m+1)+2$, что и требовалось доказать. Доказательство. Оба утверждения доказываются одновременно индукцией по параметру $\mu=\omega\cdot n+l$ (мы полагаем $l=0$ для утверждения 1)). При $n=0$ утверждение 1), очевидно, верно, поскольку у секвенции $q\setminus(p\bullet q)\Rightarrow q\setminus(p^\ast\bullet q)$ существует конечный вывод. При $l=0$ утверждение 2) следует из леммы 8: $3m+2<\omega<\omega\cdot(n+1)+4$.
Докажем шаг индукции для утверждения 1), рассмотрев следующий вывод секвенции $A_{n+1}\Rightarrow B$:
$$
\begin{equation*}
\frac{\dfrac{\dfrac{(q,A_n^l\Rightarrow p^\ast\bullet q)_{l<\omega}} {q,A_n^\ast\Rightarrow p^\ast\bullet q}(\ast L_\omega)} {q,A_n^\ast\Rightarrow p^\ast\bullet q\quad q\Rightarrow q}(\bullet L)} {\dfrac{q,A_{n+1}\Rightarrow p^\ast\bullet q} {A_{n+1}\Rightarrow B}(\setminus R)}(\setminus L).
\end{equation*}
\notag
$$
По предположению индукции ранг $q,A_n^l\Rightarrow p^\ast\bullet q$ не больше $\omega\cdot(n+1)+l+4$. Как следствие, ранг секвенции $q,A_n^\ast\Rightarrow p^\ast\bullet q$ не превосходит
$$
\begin{equation*}
\sup_{l<\omega}\bigl(\omega\cdot(n+1)+l+4\bigr)+1=\omega\cdot(n+2)+1.
\end{equation*}
\notag
$$
Представленный выше вывод показывает, что тогда ранг секвенции $A_{n+1}\Rightarrow B$ не превосходит $\omega\cdot(n+2)+1+3=\omega\cdot(n+2)+4$, что и требовалось доказать.
Для доказательства второго утверждения рассмотрим следующий вывод секвенции $q,B^m,A_n^l\Rightarrow p^\ast\bullet q$ (в предположении, что $l>0$): К обеим посылкам данного правила можно применить предположение индукции, из чего следует, что ранг левой посылки не больше $\omega\cdot(n+1)+4$, а ранг правой посылки не больше $\omega\cdot(n+1)+(l-1)+4$. Значит, ранг секвенции $q,B^m,A_n^l\Rightarrow p^\ast\bullet q$ не превосходит что и требовалось доказать.Теорема 5 следует из леммы 9, таким образом, она тоже доказана. Из этой теоремы следует, что добавление сечения может значительным образом уменьшать ранги секвенции. Вопрос, чему равен замыкающий ординал для логики $\mathrm{ACT}_\omega+(\mathrm{cut})$, остается открытым. Сложность решения этого вопроса заключается в том, что если замыкающий ординал для $\mathrm{ACT}_\omega+(\mathrm{cut})$ меньше $\omega^\omega$ (скажем, равен $\omega^2$), то необходимо для каждой секвенции инфинитарной логики действий найти ее “короткий” вывод с использованием сечения; однако неясно, как описать общую стратегию применения правила сечения, с помощью которой можно было бы построить “маленький” вывод любой секвенции. С другой стороны, если замыкающий ординал для $\mathrm{ACT}_\omega+(\mathrm{cut})$ равен $\omega^\omega$, необходимо придумать новое семейство секвенций и каким-то образом проанализировать их выводы с сечением – что само по себе является сложной задачей. Возможно, впрочем, что существуют принципиально иные, в частности, неконструктивные подходы к вычислению замыкающего ординала. Автор является победителем Всероссийского конкурса математических работ студентов и аспирантов имени Августа Мебиуса и благодарит жюри и Попечительский совет за высокую оценку его работы. Автор благодарен Степану Львовичу Кузнецову и Станиславу Олеговичу Сперанскому за постановку задачи, обсуждение предложенного автором решения и ценные советы. Автор также благодарит рецензента статьи за полезные замечания. 
Цитирование в формате AMSBIB
\RBibitem{Psh24} |
|
||||||||||
|
Обратная связь: |
Пользовательское соглашение
|
Регистрация посетителей портала |
Логотипы |
|