Усиление основной теоремы для классической логики предикатов.

2.1 Мы даем следующее усиление основной теоремы:

Пусть имеется LK-вывод со следующими свойствами конечной секвенции: каждая S-формула этой секвенции может содержать знаки всеобщности и существования только в начале, причем областью действия каждого из этих знаков является вся следующая за ними часть формулы.

Тогда этот вывод можно преобразовать в LK-вывод с той же конечной секвенцией, имеющей следующие свойства:

1) она не содержит сечений;

2) в нем имеется некоторая H-секвенция, которую мы назовем «средней секвенцией», такая, что ее вывод (и следовательно, и она сама) не содержит знаков " и $, а в остальной части вывода, включающей и среднюю секвенцию, нет других фигур заключения, кроме AES, AEA, EES, EEA и структурных.       

2.1.1. Средняя секвенция дает вывод на 2-ой части: верхнюю, относящуюся к логике высказываний, и нижнюю, состоящую лишь из введенных знаков " и $.

О форме преобразования вывода можно, очевидно, сказать следующее: нижняя ее часть, от средней секвенции до конечной секвенции, состоит лишь из одной единственной нити выводе, т.к. в нее входят только фигуры заключения с одной верхней секвенцией. S-формулы верхней секвенции имеют следующую особенность: каждая из S-формул, стоящих в антецеденте конечной секвенции, получается из одной из S-формул, стоящих в антецеденте конечной секвенции в результате удаления знаков всеобщности и существования, которыми они начинаются, и замены в оставшейся части формулы связанных предметных переменных некоторыми определенными свободными предметными переменными. То же самое имеет место для сукцедента.

Это следует из такого же рассуждения, как и в III, 2.512.

 

2.2. Доказательство теоремы 2.1.

Преобразование вывода осуществляется в несколько шагов.

2.2.1. Сначала применяется основная теорема (III, 2.5), согласно которой можно преобразовать вывод в вывод без сечения.    

2.2.2. Преобразование основных секвенций, содержащих знак " или $:

Ввиду свойства подформульности (III, 2.513) они могут иметь только вид

"xFx→"xFx, или $xFx→$xFx.

Они преобразуются в

или соответственно

где а – некоторая свободная предметная переменная, не входящая в вывод.

Повторив это преобразование достаточное число раз, можно, очевидно, достичь того, чтобы знаки " и $ не входили не в одну из основных секвенций вывода.  

2.2.3. Теперь мы проведем полную индукцию по «порядку» вывода, который определим следующим образом.

Логические фигуры заключения, относящиеся к знакам &, Ú,, É, «пропозициональными фигурами заключения», а остальные, т.е. AES, AEA, EES и EEA, «предикатными фигурами заключения». Каждый предикат фигуры заключения, входящий в вывод, сопоставим порядковое число следующим образом.

Рассмотрим часть нити вывода от нижней секвенции рассматриваемой фигуры заключения до конечной секвенции вывода (включительно) и подсчитаем входящие в них нижние секвенции пропозициональных фигур заключения. Их число и есть определяемое порядковое число.

Сумма порядковых чисел всех предикатных фигур заключения, входящих в вывод, называется порядком вывода.

Мы хотим уменьшать его шаг за шагом до тех пор, пока он не станет равным 0.

Докажем вначале, что после этого доказательство теоремы (2.1) легко может быть доведено до конца (шаг (2.2.3.2) строится так, что полученные в 2.2.1. и 2.2.2. особенности сохраняются).

 

2.2.3.1. Предположим, что вывод уже имеет порядок, равный 0. Переходим постепенно от конечной секвенции к верхним секвенциям стоящих над ней фигур заключения. Мы останавливаемся, как только встретим нижнюю секвенцию некоторой пропозициональной фигуры заключения или основную секвенцию; эту секвенцию мы обозначим посредством σ . (Она будет служить после указанных ниже преобразований в качестве «средней секвенции»).

Вывод секвенции σ  мы преобразуем так.

Мы просто удалим из него все H-S-формулы, которые еще содержат знак " или $. При этом вывод секвенции σ  остается правильным: основные секвенции не изменяются в силу 2.2.2. Далее, никакие из главных и боковых формул фигур заключения, т.к., если бы какая-нибудь из боковых формул содержала знак " или $, то и главная формула содержала бы этот знак, что невозможно для пропозициональных фигур заключения ввиду свойства подформульности (III, 2.5.1.3) и условия теоремы 2.1, и предикатные фигуры заключения в рассматриваемый вывод не входят (т.к. в противном случае порядковое число этой фигуры заключения было бы больше 0). Но каждая фигура заключения  при удалении из нее любой S-формулы, ни являющейся ни главной, ни боковой формулой, остается то же фигурой заключения; это легко усматривается непосредственно из схем III, 1.2.1, (1.2.2).

(Возможно, однако, появление тождественной фигуры заключения, но она, как и выше, удаляется).

Секвенция σ *, в которую после описанного преобразования превратилась секвенция, может отличаться от σ  лишь тем, что в ней отсутствуют некоторые входящие в σ  S-формулы. Но несколькими уточнениями и перестановками мы можем преобразовать ее снова в секвенцию σ  и присоединить к ней нижнюю часть вывода без изменений.

Следовательно, σ  является средней секвенцией и удовлетворяет, очевидно, всем требованиям теоремы (2.1).

2.2.3.2. Теперь надо провести еще шаг индукции, т.е. допустив, что порядок вывода >0, уменьшить его.

2.2.3.2.1. Мы начнем с переименования свободных предметных переменных способом, описанным в III, 3.10. Этим мы достигаем того, что вывод будет иметь следующее свойство (III, 3.10.1).

Собственная переменная каждой AES (соответственно EEA) входит в вывод только в секвенции, стоящие выше нижней секвенции этой фигуры, и не входит больше ни в какую другую AES и EEA в качестве собственной переменной этой фигуры заключения.

2.2.3.2.2. Теперь мы переходим к самому преобразованию.

Заключим, прежде всего, что в выводе найдется некоторая предикатная фигура заключения (мы будем называть ее σf₁), обладающая следующим свойством: если проследить часть нити вывода от ее нижней секвенции до конечной секвенции, то первая же встретившаяся нижняя секвенция логической фигуры заключения является нижней секвенцией пропозициональной фигуры заключения (эту фигуру заключения мы обозначим посредством σf₂). Действительно, в противном случае порядок вывода был бы равен 0.

Наша цель состоит в том, чтобы переместить фигуру заключения σf₁ на место, расположенной ниже фигуры заключения σf₂.

Это нетрудно выполнить следующим образом:

2.2.3.2.2.1. σf₂ имеет одну верхнюю секвенцию.

2.2.3.2.2.1.1. Пусть σf₁ есть AES. Тогда рассматриваемая часть вывода имеет вид

и возможно, несколько предшествующих ей структурных фигур заключения.

sf2

 

 

Мы преобразуем эту часть вывода так:

возможно несколько перестановок и сокращений

возможно несколько перестановок

фигуры заключения того не видя, что выше, т.е. sf2 с предшествующей ей, возможно, структурными фигурами заключения.

возможно несколько перестановок и уточнений

Удаление в конце этой части вывода "xFx с помощью сокращения возможно потому, что "xFx необходимо входит в Λ в качестве S-формулы.

(Дело в том, что S-формула "xFx в первоначальном выводе не могла быть удалена из сукцедента в результате применения σf₂ и предшествующих ей структурных фигур заключения; эта S-формула не могла быть боковой формулой sf₂ ввиду свойства подформульности III, 2.5.1.3 и условия теоремы 2.1).

Ограничения на применение для перемещенной AES выполнены на основании 2.2.3.2.1.

Порядок вывода, очевидно, понизится на 1.

2.2.3.2.2.1.2. Случай, когда sf₁ есть EES, рассматривается точно так же, надо лишь заменить " на $.

2.2.3.2.2.1.3. Случай, когда sf₁ является фигурой заключения AEA или EEA, могут быть могут быть рассмотрены зеркально-симметрично двум предыдущим.

2.2.3.2.2.2. Случай, когда sf₂ имеет две верхние секвенции, т.е. является VES, OEA или FEA, могут быть рассмотрены совершенно аналогичным образом; во всех случаях могут понадобиться лишь дополнительные применения структурных фигур заключения.

 

2.3. Аналогично теореме 2.1 можно доказать дальнейшие условия основной теоремы в том смысле, что на порядок следствия логических фигур заключения в выводе накладываются те или иные ограничения. Фигуры заключения в выводе можно переставлять различными способами и в довольно широких пределах подобно тому, как делалось выше (2.2.3.2.2).