Исчисления высказываний классической логики. Гуров С.И. - 93 стр.

UptoLike

ВУЗ: 

МГУ | Москва

Составители: 

Рубрика: 

N
Σ : Γ, ∆ ` A N B (+ N ) Σ
2
Σ
4
A
¡
¢
B, B
¡
¢
C ` A
¡
¢
C
Σ : A ` A
Σ : A
¡
¢
B ` A
¡
¢
B
Σ : A, A
¡
¢
B ` B −
¡
¢
Σ
1
Σ
2
Σ : B
¡
¢
C ` B
¡
¢
C
Σ : A, A
¡
¢
B, B
¡
¢
C ` C −
¡
¢
Σ
3
Σ
4
Σ : A
¡
¢
B, B
¡
¢
C ` A
¡
¢
C +
¡
¢
Γ ` A ∆, A ` B
Γ, ∆ ` B
(Cut)
N
Σ : Γ ` A
Σ : ∆, A ` B
Σ : ∆ ` A
¡
¢
B +
¡
¢
Σ : Γ, ∆ ` B Σ
1
Σ
3
−
¡
¢
¤
1. Èñ÷èñëåíèå N íàòóðàëüíîãî òèïà                              93


 Σ5 : Γ, ∆ ` A N B  ïî (+ N ) èç Σ2 è Σ4
   Ìû áóäåì ïîëüçîâàòüñÿ îáîáù¼ííûìè àíàëîãàìè ðàññìàòðèâàåìûõ
ïðàâèë áåç ñïåöèàëüíîãî óêàçàíèÿ, ñîõðàíèâ äëÿ íèõ îáîçíà÷åíèÿ èñ-
õîäíûõ ïðàâèë.
Ïðèìåð 3.2.
         ¡      ¡        ¡
  1. A ¢ B, B ¢ C ` A ¢ C
          Σ1   :   A ` A  àêñèîìà
                      ¡          ¡
          Σ2   :   A ¢ B ` A ¢ B  àêñèîìà
                         ¡¢               ¡
          Σ3   :   A, A     B ` B  ïî (− ¢) èç Σ1 è Σ2
                       ¡         ¡
          Σ4   :   B ¢ C ` B ¢ C  àêñèîìà
                          ¡        ¡              ¡
          Σ5   :   A, A ¢ B, B ¢ C ` C  ïî (− ¢) èç Σ3 è Σ4
                      ¡¢      ¡¢     ¡¢             ¡
          Σ6   :   A B, B C ` A C  ïî (+ ¢) èç ïðåäûäóùåãî

Ëåììà 3.1. Ïðàâèëî ñå÷åíèÿ
                          Γ ` A ∆, A ` B
                                           (Cut)
                              Γ, ∆ ` B
ÿâëÿåòñÿ äîïóñòèìûì â N .
Äîêàçàòåëüñòâî.
 Σ1   :   Γ ` A  ïðåäïîëîæåíèå (ïîñûëêà ïðàâèëà)
 Σ2   :   ∆, A ` B  ïðåäïîëîæåíèå (ïîñûëêà ïðàâèëà)
                  ¡           ¡
 Σ3   :   ∆ ` A ¢ B  ïî (+ ¢) èç ïðåäûäóùåãî
                                      ¡
 Σ4   :   Γ, ∆ ` B  èç Σ1 è Σ3 ïî (− ¢)
                                                                ¤

   Âûâîäû ñ èñïîëüçîâàíèåì äîïóñòèìûõ ïðàâèë íàçûâàþòñÿ, êàê ìû
ïîìíèì, êâàçèâûâîäàìè.
   Ñîãëàñíî Ãåíöåíó, îñíîâíàÿ èäåÿ ñîçäàíèÿ íàòóðàëüíîãî èñ÷èñëå-
íèÿ ñâÿçàíà ñ íàìåðåíèåì ¾ïîñòðîèòü òàêîé ôîðìàëèçì, êîòîðûé áûë
áû êàê ìîæíî áëèæå ê ïðèìåíÿþùèìñÿ â äåéñòâèòåëüíîñòè ðàññóæ-
äåíèÿì¿. Ãåíöåí ñ÷èòàë, ÷òî îñíîâíûì ïðèçíàêîì, îòëè÷àþùèì íàòó-
ðàëüíûå èñ÷èñëåíèÿ îò àêñèîìàòè÷åñêèõ, ÿâëÿåòñÿ òî, ÷òî ¾íàòóðàëü-
íûå âûâîäû èñõîäÿò âîîáùå íå èç ëîãè÷åñêèõ àêñèîì, à èç äîïóùåíèé,
èç êîòîðûõ äåëàþòñÿ ëîãè÷åñêèå çàêëþ÷åíèÿ. À çàòåì ïîñðåäñòâîì
íåêîòîðûõ äàëüíåéøèõ çàêëþ÷åíèé ðåçóëüòàò äåëàåòñÿ óæå íåçàâèñè-
ìûì îò äîïóùåíèé¿.

Страницы