Исчисления L J и L K (логическое истуиционистское и классическое исчисления).

1.1. Предварительные замечания о строении исчислений LJ и LK.

Мы хотим построить исчисление способов заключений (для логики предикатов), которое, с одной стороны, было бы «логическим», т.е. таким, в котором выводы не содержали бы, в противоположность исчислению NJ, никаких допущений, и которое, с другой стороны, сохраняло бы присущее исчислению NJ деление способов заключений на введения и удаления отдельных логических знаков.

Наиболее непосредственный способ превращения NJ-вывода в логический состоит в том, что Н-формулу В, зависящую от допущений      U₁, …, U_m, заменяют формулой (U₁&…&U_m)ÉВ. Так поступают со всеми Н-формулами.

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

Однако при этом появляются новые логические знаки & и É и тем самым нарушается систематизация фигур заключения на фигуры введения и удаления.

Поэтому мы вводим понятие секвенции (см. I, 2.3) и вместо формулы (U₁& … &U_m) É В пишем секвенцию U₁, …, U_m ® В.

Она отличается от этой формулы не содержательным значением, а лишь формальной структурой (ср. I, 2.4).

Теперь нам нужны еще новые фигуры заключения, которые не укладываются в систематизацию введения-удаления; однако мы имеем при этом то преимущество, что можем предоставить этим новым фигурам особое место, т.к. они относятся уже не к логическим знакам, а к «структурным фигурам заключения», а остальные «логическими фигурами заключения».

В классическом исчислении NK закон исключенного третьего занимает особое место среди способов заключения (см. II, 5.3), т.к. не включается в систематизацию введения-удаления.

В приведенном ниже логическом классическом исчислении NK эта особенность закона исключенного третьего исчезает.

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

Достигаемая при этом симметрия оказывается более подходящей для классической логики. Для интуиционистского исчисления LJ, напротив, остается то ограничение, что сукцеденты секвенций могут состоять не более чем из одной формулы (см. ниже; пустой сукцедент означает то же, что L в сукцеденте).

Мы привели некоторые исходные соображения, положенные в основу построения описываемого ниже исчисления.

По существу, однако, его форма определена с учетом доказываемой ниже «основной теоремы» (§2) и поэтому заранее не может быть обоснована более подробно.

 

1.2. Понятия LK-вывода и LJ-вывода определим следующим образом:

LJ-вывод (соответственно LK-вывод) состоит из секвенций, упорядоченных в виде дерева (см. I, 3.3).

Исходными секвенциями вывода являются основные секвенции вида D®D, где D – произвольная формула.

Каждая фигура заключения, входящая в вывод, получается из приведенных ниже схем в результате следующих подстановок (ср. II, 2.2.1):

U, B, C, D заменяются произвольными формулами,

"xFx и $xFx заменяются произвольными формулами с внешним знаком ", соответственно $;

X обозначает связанную этим знаком предметную переменную;

Fa есть формула, которая получается из Fx при замене связанной предметной переменной х, всюду, где она встречается, свободной предметной переменной а.

G, D, Q, L заменяются (может быть, и пустыми) рядами формул, отделенных друг от друга запятыми.

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

«В сукцеденте каждой Н-секвенции должно быть не более одной S-формулы».

Обозначения отдельных схем логических фигур заключения UES, UEA и т.д. означают следующее:

Фигура заключения, построенная по схеме, является фигурой введения (Е) в сукцедент (S) или в антецедент (А) знака «и» (U), «или» (O), всеобщности (А), существования (Е), отрицания (N), следования (F).

Схема фигур заключения.

1.2.1. Схемы структурных фигур заключения

Утончение

в антецеденте: , в сукцеденте: ;

Сокращение

в антецеденте: , в сукцеденте: ;

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

в антецеденте: , в сукцеденте: ;

сечение:

1.2.2. Схемы логических фигур заключения:

UES:                  OEA:

UEA:     OES:

AES:                              EEA: .

 

Ограничение на переменные: в обеих последних схемах предметная переменная, обозначенная посредством а и называемая собственной переменной AES, соответственно EEA, не должна входить в нижнюю секвенцию фигуры заключения (то есть, ни в Г, ни в Θ, ни в Fx).

АЕА:      EES:

NES:          NEA:

FES:      FEA: .

1.3.   Пример LJ-вывода (ср. II, 4.3):

                       xFх xFх

                                                   NEA

Fа Fа          xFx, xFx

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

Fа xFx      xFx, xFx

                                                                      сечение,

              Fa, xFx

                                          NES

        xFx Fa

                                                                         AES

                          xFx y Fy

                                                             FES

                       ( xFx) ( y Fy)

 

 

1.4. Пример LK-вывода (вывод «закона исключенного третьего»):

 

 A A

              NES

A, A

                       DES

A, A A

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

 A A, A

                                DES

 A A, A A

                                сокращение

 A A.