Описание логического исчисления Гильберта и Гливленко.

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

Основные формулы и фигуры заключения строятся по следующим схемам путем таких же замещений, как в II, 2.21, а именно:

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

2) (соотв. ) – произвольной формулой, внешним знаком которой является (соотв. ), причем x обозначает следующую за ними связанную предметную переменную.

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

Схемы основных формул:

2.1.1.

2.1.2.

2.1.3.

2.1.4.

2.1.5.

2.2.1.

2.2.2.

2.2.3.

2.3.1.

2.3.2.

2.3.3.

2.4.1.

2.4.2.

2.5.1.

2.5.2.

 

 

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

Ограничение на переменные:

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

(Исчисление LHJ, по существу, эквивалентно исчислению Гейтинга). 

Исчисление LHK получается в результате присоединения к исчислению LHJ схемы основных формул .

 

 

§3. Преобразование L HJ –выводы в эквивалентный ему NJ -вывод.

Из LHJ-вывода (V,2) мы получаем NJ-вывод (II,2) с той же конечной формулой в результате следующего преобразования LHJ-вывода (при этом все H-формулы этого вывода становятся Н-формулами NJ-вывода, причем они не будут зависеть ни от каких допущений. Кроме них, в строящийся NJ-вывод будут входить некоторые другие H-формулы, зависящие от тех, или иных допущений).

 

3.1. Все LHJ-основные формулы заменяются теперь выводами этих формул, построенными по следующим схемам:

2.1.1.                                              

2.1.2.

2.1.3.

2.1.4.

2.1.5.

2.2.1.

Совершенно аналогично 2.2.1. выводятся 2.2.2., 2.3.1., 2.3.2., 2.5.1., 2.5.2.

2.2.3.

2.3.3.

2.4.1.

2.4.2.

 

3.2 Все LHJ-фигуры заключения заменяются теперь частями NJ-вывода, построенными по следующим схемам:

    

    

 Как легко видеть, что ограничение на переменные в фигурных заключениях АЕ и ЕВ выполнено вследствие существующего для LHJ-фигур заключения ограничения на переменные.

На этом преобразование LHJ-вывода в эквивалентный ему NJ-вывод заканчивается.

 

 

§4. Преобразование NJ -вывода в эквивалентный ему L J -вывод.

4.1. Это преобразование производится так:

сначала каждая H-формула NJ-вывода заменяется на секвенцию следующего вида (ср.III., 1.1):

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

После этого заменяем знак  всюду, где он входит, формулой A& A. Формулу, полученную при этом из формулы U, мы обозначим посредством U^*).

 

4.2. Таким образом мы уже получили систему секвенций, расположенных в виде дерева. Конечная секвенция имеет пустой антецедент (II., 2.2) и, очевидно, эквивалентна конечной формуле NJ-вывода. Исходные секвенции все имеют вид D^* D^* (II., 2.2), т.е. уже являются основными секвенциями LJ-вывода.

Фигуры, полученные из NJ-фигур заключения, преобразуются в части LJ-вывода по следующим схемам:

4.2.1. Фигуры заключения ОЕ, АЕ, ЕЕ при замещении уже превратились в LJ-фигуры заключения.

(В случае АЕ LJ-ограничение на переменные выполняется в силу выполнения NJ-ограничения на переменные в исходном NJ-выводе).

4.2. 2. Фигура заключения UE приняла вид

             

Ее перестраивают так:

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

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

Г U^*                                                  B^*

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

Г,  U^{* и утончений,}                                              Г, B^{*  утончений}

UES

                                                                                                   

                       Г,  U^*& B^*

4.2.3. Фигура заключения FE приняла вид

              Г₁, U^*, Г₂,…, U^*, Г  B^*

              Г₁, Г₂,…, Г U^* B^*

Ее перестраивают так:

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

Г₁, U^*, Г₂,…, U^*, Г  B^*

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

U^*, Г₁, Г₂,…, Г  B^{*             и, если потребуется, утончений}

                          FES

Г₁, Г₂,…, Г U^* B^*

 

4.2.4. С фигурой заключения NE поступают так же, после чего надо рассмотреть фигуру .

Секвенцию А& A  выводим в исчислении LI следующим образом:

                                А А

                                          NEA

                       A, A

                                          UEA

                       А& A, A

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

                A, А& A

                                     UEA

         А& A, А& A

                                          сокращение

                       А& A

Присоединяя эту секвенцию, перестраиваем рассматриваемую фигуру следующим образом:

4.2.5. NJ-фигура заключения  примет после замещений (4.1) следующий вид:

Делаем следующее ее преобразование:

При этом над секвенцией А& A  пишется ее вывод, приведенный в 4.2.4.

4.2. 6. Фигура заключения АВ принимает вид

Преобразуем ее так:

4.2.7. С фигурой заключения UB поступаем совершенно так же.

4.2.8. Фигура заключения FB принимает вид:

Преобразуем ее так:

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

4.2.9.    Фигура заключения NB принимает вид:

Преобразуем ее так:

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

возможны перестановки и утончения

возможны перестановки и утончения

4.2.10. Фигура заключения OB: сначала применяем как это делалось для FE и NE, к обеим правым верхним секвенциям перестановки, сокращения и утончения (если это необходимо) таким образом, чтобы в результате получать секвенции, в которых формулы, обозначенные посредством U^* и соответственно B^*, стоят в начале антецедента (в то время как из остальной части антецедента упомянутые допущения удалены). После этого следует

ОЕА

                      

сечение

                     U^*  B^* U^*  B^*, Г, С^*

                                  , Г, С^*

4.2.11. С фигурой заключения ЕВ поступаем аналогично; сначала формула Fa в правой верхней секвенции перемещается в начало антецедента (как в 4.2.3), а затем следует

 LJ-ограничение на var для ЕЕА выполнены ввиду выполнения NJ-ограничений на var.

Этим преобразование NJ-вывода в эквивалентный ему LJ-вывод завершено.

 

 

§5. Преобразование L J -вывода в эквивалентный ему L HJ -вывод.

   

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

 

5.1. Прежде всего вводят вместо фигур заключения UEA, OES, AEA, EES, NEA и FEA новые основные секвенции, которые строятся по следующим схемам (правила замещения те же, что и в III, 1.2; это же имеет место всюду в дальнейшем; впрочем, мы будем употреблять для обозначения формулы, кроме букв U, B, D, s(э) также C(цэ), h(ха), I(и)):

(гэ) Gf₁: U&B→U          Gf₂: U&B→B

    Gf₃: U→UÚB           Gf₄: B→UÚB

    Gf₅: "xFx→Fa                  Gf₆: Fa→$xFx  

    Gf₇: ØU, U→           Gf₈: UÉB, U→B

Мы преобразуем соответствующие фигуры заключения в рассмотренном LJ-выводе следующим образом:

UEA преобразуется в:

Соответственно мы преобразуем и другую форму UEA и каждую AEA. Симметрично этому мы поступаем с OES и EES. NEA преобразуется в

      Gf₇

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

FEA преобразуется в

      Gf₈

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

        

5.2. Теперь всем H-секвенциям, имеющим пустой сукцедент, мы напишем в сукцедент формулу A&ØA.

При этом остаются неизменными основные секвенции видов: D→D,     Gf₁ – Gf₆ и Gf₈, а также фигуры заключения UES, AES, FES. Остальные основные секвенции и фигуры заключения переходят в основные секвенции и фигуры заключения по следующим схемам:

Gf₉:

sf₁:                     sf₂:           

sf₃:             sf₄:                   

sf₅:         sf₆:          

sf₇:               sf₈:

(для sf₇ существует ограничение на var: свободная предметная var, обозначается посредством a, не должна входить в нижнюю секвенцию).

 

5.3. Далее фигуру заключения sf₄ можно заменить фигурой следющим образом (такое возможно, по существу, обусловлено общим содержанием схемы sf₉).

                                           sf₂                                sf₉

Подобным образом мы заменяем фигуру заключения sf8 (всюду, где она входит в вывод), но этот раз применяется фигура заключения, построенная по схема

sf₉: .

Замена производится следующим образом: на место sf8 ставится

sf₁                                              s₂

 

5.4 Введем теперь еще две новые схемы фигур заключения:

sf₁₀:  и ее обращение, sf₁₁: эти фигуры вводятся для того, чтобы с их помощью заменить в выводе ряд других фигур заключения их частными случаями (5.4.2, 5.4.3).

5.41 Прежде всего фигуру заключения FES можно удалить из вывода с помощью sf10, преобразовав ее следующим образом:

возможно, несколько sf3 sf10

5.42 После этого преобразуем следующим образом фигуры заключения σf₁ – σf₃, σf₅ – σf₇.

В качестве примера мы возьмем σf₂, которое мы преобразуем в следующую фигуру (считая, что Г имеет вид I₁,…,I_ρ):

несколько раз σƒ11

σƒ13

несколько раз σƒ10

σƒ10

Совершенно аналогично мы поступаем с каждой из остальных перечисленных фигур заключения; в результате, используя σƒ₁₀ и σƒ_11, мы заменяем их фигурами заключения, построенными по следующей схеме:

σƒ₁₂ :                           σƒ₁₃ :                            σƒ₁₃ :                                  

σƒ₁₅ :                           σƒ₁₆ :                            σƒ₁₇ :                         

        

(для σƒ₁₇ имеется ограничение на переменные: свободная предметная переменная, а не должен входить в нижнею секвенцию).

5.43.  сходным образом заменяем далее фигуры замещения σƒ₉, σƒ₁₃, σƒ₁₅ следующим (используя σƒ₁₀ и σƒ₁₁):

σƒ₁₈ :                                              σƒ₁₉ :                          

σƒ₂₀:                                  

 

Таким же образом можно заменить основания основных секвенций σƒ₈ и σƒ₈ на U B→U D; эта формула подпадает под схему D→D, а также σƒ₁₀ на: U→U h.

 

 

     5.5 После этого делаем последний шаг:

     Заменяем каждую H-секвенцию U₁,…,U_m→B формулой (U₁&…&U_m)=B. (Если все U пусты, то этой формулой будет просто B. Сукцедент не может быть пустым, согласно 5.2).

     В результате все основные секвенции (а именно, D→D, sf₁ - sf₆, sf₁₀) становятся основными секвенциями исчисления LHJ.

     Из фигур заключения фигуры AES и sf17 также становятся фигурами заключения исчисления LHJ. (Для первой из них исключение составит не случай, когда Г пуст. В этом случае мы сначала выведем (в исчислении LHJ) формулу (AÉA) ÉFa из Fa с помощью 2.1.2, а затем применяем фигуры заключения LHJ и получаем в конце концов с помощью 2 формулу "xFx).