Некоторые замечания об исчислениях L J и L K . Основная теорема.

(В дальнейшем замечания 2.1, 2.2 и 2.3 не применяются).

2.1. Схемы не являются все независимыми друг от друга, то есть одни из них могут быть заменены другими. Однако при этом «основная теорема» может стать уже неверной.

 

2.2. Вообще, если бы мы не были заинтересованы в основной теореме, исчисление можно было бы упростить во многих отношениях.

Так в LK фигуры заключения:

UES, OEA, UEA, OES, AEA, EES, NES, NEA, FEA

можно было бы заменить основными секвенциями следующих видов:

U; B U&B; U B U,B; U&B U; U&B B; U U B; B U B; Fa, Fa ; U, U (закон исключенного третьего); U, U  (закон противоречия); U B,U B.

Легко показать, что эти основные секвенции эквивалентны соответствующим фигурам заключения.

Для фигур заключения исчисления LJ имеется такая же возможность, за исключением фигур заключения OEA и NES, т.к. Н-секвенции в LJ не могут иметь двух S-формул в сукцеденте (ср. с этим раздел V, §5).

 

2.3. Различие между интуиционистской и классической логиками для исчислений LJ и LK внешне выглядит совершенно иначе, чем для NJ и NK. Там оно состоит в допущении или недопущении закона исключенного третьего, в то время как здесь оно выражается в ограничении, наложенном на сукцеденте секвенций. (То, что оба эти различия являются эквивалентными, будет установлено при доказательстве эквивалентности всех рассматриваемых исчислений в разделе V).

 

2.4. Исчисление LK, если опустить FES и FEA, оказывается зеркально-симметричным в следующем смысле: если в LK-выводе (не содержащем знака ) обратить все секвенции, то есть вместо U₁,…,U_m  B₁,…,B_n написать B_n,…,B₁  U_m,…, U₁, в фигурах с двумя верхними секвенциями поменять местами правую и левую верхние секвенции вместе с их выводами, далее, каждое вхождение & заменить на ,  - на &,  - на ,  - на  (при замене & на  и  на & поменять местами области действия знаков, например B U заменить на U&B), то получим снова LK-вывод. Это явствует непосредственно из схем. (В их распоряжении подчеркнута эта симметрия).

2.4.1. Знак  является для исчисления NK, в известном смысле, вообще излишним, так как U B можно рассматривать как сокращение для ( U) B; легко проверить, что схемы для FES и FEA можно заменить в этом случае схемами для  и .

Для исчисления NJ это не имеет места.

 

2.5. Важнейшим для нас свойством исчислений LJ и LK является следующая

Основная теорема. Каждый LJ-вывод (соответственно LK-вывод) можно перестроить в LJ-вывод (соответственно LK-вывод) с той же конечной секвенцией, в который не входит фигура заключения, называемая «сечением».

2.5.1. Доказательство приведено в §3.

Чтобы предварительно пояснить значение основной теоремы, докажем одну простую дополнительную теорему (см. 2.5.1.3).

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

2.5.1.1 Ту S-формулу, которая в схеме фигуры заключения содержит логический знак, мы называем главной формулой фигуры заключения.

 

 

Таковы S-формулы вида U&B в UES, UEA;

U B в OES, OEA;

 в AES,AEA;

 в EES, EEA;

U в NES, NEA;

U B в FES, FEA.

S-формулы, обозначенные в схемах фигур заключения посредством U, B, Fa, мы называем боковыми формулами соответствующей фигуры заключения. Они всегда являются подформулами главной формулы (в соответствии с определениями подформулы в I, 2.2).

2.5.1.2. Из схем фигур заключения мы можем легко усмотреть следующие факты.

Главная формула всегда стоит в нижней секвенции, боковые формулы всегда стоят в верхних секвенциях логических фигур заключения.

Если некоторая формула входит в верхнюю секвенцию некоторой фигуры заключения в качестве S-формулы и не является там ни боковой формулой, ни формулой D сечения, то эта формула входит и нижнюю секвенцию в качестве S-формулы.

Из этих двух фактов вытекает следующее.

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

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

2.5.1.3. Дополнительная теорема к основной теореме (свойство подформульности):

В LI-выводе (соответственно в LK-выводе), не содержащем сечения, все входящие в него H-S-формулы являются подформулами S-формул, входящих в конечную секвенцию.

2.5.1.4. Образно говоря, описанное свойство вывода без сечения можно выразить так:

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

Пример. Приведенный выше (1.3) вывод секвенции ( xFx) ( y Fy) можно записать без сечения так:

    Fa Fa

                       EES

    Fa xFx

                       NEA

xFx, Fa

                       перестановка

Fa, xFx

и далее, как ранее.