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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

H
0
H
1
Γ, (A
¡
¢
B) N (B
¡
¢
A) ` A
¡
¢
B N
Γ ` A
¡
¢
B
Γ, A ` B
Γ, A ` B Γ ` A ≡ B
¤
A ' B ⇔ ` A ≡ B
H
1
H
H H
1
B
1
≡ B
2
` A ≡ A(B
1
| B
2
)
D3 A ≡ B
(A
¡
¢
B) N (B
¡
¢
A)
` A ≡ A ,
A ≡ B ` B ≡ A , A ≡ B ` ¬ A ≡ ¬ B ,
A ≡ B ` (A ∨ C) ≡ (B ∨ C) , A ≡ B ` (C ∨ A) ≡ (C ∨ B ) ,
A ≡ B ` (A N C) ≡ (B N C) , A ≡ B ` (C N A) ≡ (C N B) ,
A ≡ B ` (A
¡
¢
C) ≡ (B
¡
¢
C) , A ≡ B ` (C
¡
¢
A) ≡ (C
¡
¢
B) .
¤
H
1
H
H
1
H
1
∨ N
[H] = [H
1
] H
1
H
1
H
1
H
1
H
T
L
∗
L
∗
[Γ]
Γ
4. ÈÂ H 0 è H1                                                   79

          ¡          ¡         ¡
(2) Γ, (A ¢ B) N (B ¢ A) ` A ¢ B  óäàëåíèå N
            ¡¢
(3) Γ ` A B        ïî Cut èç (1) è (2)
(4) Γ, A ` B     ïî RDT èç ïðåäûäóùåãî
åñòü âûâîä Γ, A ` B èç ïðåäïîëîæåíèÿ Γ ` A ≡ B . Äîêàçóåìîñòü
âòîðîé âûâîäèìîñòè ïîêàçûâàåòñÿ àíàëîãè÷íî.                 ¤


Ñëåäñòâèå. A ' B ⇔ ` A ≡ B .
    Îòìåòèì, ÷òî ðàññìîòðåííûå âûøå âûâîäèìûå ïðàâèëà H1 è òåî-
ðåìû 2.10, 2.11 òàêæå ìîãëè áû áûòü ââåäåíû è â H . Òàêæå, êàê è â
H , â H1 âåðíà
Òåîðåìà 2.12 (Î çàìåíå).      B1 ≡ B2 ` A ≡ A(B1 | B2 ) .
Äîêàçàòåëüñòâî. Ïî     D3 A      ≡   B åñòü ñîêðàùåíèå äëÿ
    ¡         ¡
(A ¢ B) N (B ¢ A). Ñ ó÷¼òîì ýòîãî, ïðèìåíÿÿ ðàññìîòðåííûå âû-
øå ïðàâèëà è DT äîêàçûâàþòñÿ âûâîäèìîñòè
       ` A ≡ A,
   A ≡ B ` B ≡ A,                  A ≡ B ` ¬A ≡ ¬B,
   A ≡ B ` (A ∨ C) ≡ (B ∨ C) ,     A ≡ B ` (C ∨ A) ≡ (C ∨ B) ,
   A ≡ B ` (A N C) ≡ (B N C) ,     A ≡ B ` (C N A) ≡ (C N B) ,
                ¡         ¡                    ¡          ¡
   A ≡ B ` (A ¢ C) ≡ (B ¢ C) ,     A ≡ B ` (C ¢ A) ≡ (C ¢ B) .
Äàëåå èñïîëüçóåì ïðèíöèï èíäóêöèè ïî ïîñòðîåíèþ ôîðìóëû, ïðè-
÷¼ì áàçèñ èíäóêöèè îáåñïå÷èâàåò ïåðâàÿ âûâîäèìîñòü, à èíäóêòèâíûé
øàã  îñòàëüíûå.                                                ¤

    Îñíîâíûå ñâîéñòâà èñ÷èñëåíèÿ H1 àíàëîãè÷íû H . Ýëåìåíòàðíî
ïîêàçûâàåòñÿ êîððåêòíîñòü è íåïðîòèâîðå÷èâîñòü H1 . Àíàëîãè÷íî òî-
ìó, êàê ñäåëàíî â ï. 3 ìîæåò áûòü äîêàçàíà ñåìàíòè÷åñêàÿ ïîëíîòà
H1 : äîêàçûâàåòñÿ àíàëîã òåîðåìû 2.3, ñ òîé ðàçíèöåé, ÷òî øàã èíäóê-
öèè ïðîâîäèòñÿ åù¼ è ïî ïðèìèòèâíûì ñâÿçêàì ∨ è N. Òàêèì îáðà-
çîì, [H] = [H1 ]. Èñ÷èñëåíèå H1 òàêæå ïîëíî ïî Ïîñòó, íå îáëàäàåò
ñâîéñòâîì àáñîëþòíîé ïîëíîòû è ðàçðåøèìî. Ìåòîäàìè, àíàëîãè÷íû-
ìè ðàññìîòðåííûì â ï. 3.4 ìîæíî ïîêàçàòü íåçàâèñèìîñòü äàííîé ñè-
ñòåìû àêñèîì H1 .
    Èññëåäóåì âûâîäèìîñòü èç ãèïîòåç â ÈÂ H1 . Â ñèëó ïîëíîòû â ÈÂ
H1 , êàê è H , âûâîäèìû èñêëþ÷èòåëüíî òàâòîëîãèè àëãåáðû ëîãèêè.
Ýòî îçíà÷àåò, ÷òî òåîðåìàì ýòèõ èñ÷èñëåíèé ñîîòâåòñòâóåò åäèíèöà T
àëãåáðû ËèíäåíáàóìàÒàðñêîãî L∗ . Äàëåå ìû âûÿñíèì, êàêèì ýëåìåí-
òàì L∗ ñîîòâåòñòâóþò ôîðìóëû [Γ], âûâîäèìûå èç íåêîòîðîãî íàáîðà
ãèïîòåç Γ. Äëÿ ýòîãî òðåáóåòñÿ óñòàíîâèòü íåêîòîðûå ôàêòû.

Страницы