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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

¤
F, A, B N A F
A ' B ⇒ F ' F (A|B) .
F
F = A
F = ¬ G F = G◦H ◦
¡
¢
N
∨ F ' F (A|B)
¤
N
N
T Σ
T Σ
Σ
Rl(N)
(+ N )
Γ ` A ∆ ` B
Γ, ∆ ` A N B
.
ϕ
M
= ϕ
M
T
Γ
T
∆
Γ ∆
T
Γ ⊆ |A|
ϕ
T
∆ ⊆ |B|
ϕ
T
Γ ∩
T
∆ =
T
{Γ ∪ ∆} ⊆ |A|
ϕ
∩ |B|
ϕ
ϕ
Γ, ∆ ` A N B
(−
¡
¢
)
Γ ` A
¡
¢
B ∆ ` A
Γ, ∆ ` B
.
106                 Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé


Âñå òðåáóåìûå âûâîäèìîñòè óñòàíîâëåíû.                               ¤


Òåîðåìà 3.4 (Î çàìåíå äåäóêòèâíî ýêâèâàëåíòíûõ). Ïóñòü
F, A, B  ôîðìóëû ÈC N , ïðè÷¼ì A  ïîäôîðìóëà F . Òîãäà

                      A ' B ⇒ F ' F (A|B) .

Äîêàçàòåëüñòâî. Ïóñòü õîòÿ áû îäíà ïîäñòàíîâêà ôàêòè÷åñêè ïðîèç-
âîäèòñÿ, èíà÷å äîêàçûâàòü íå÷åãî. Ïðèìåíÿåì èíäóêöèþ ïî ñëîæíîñòè
ôîðìóëû F .
   Åñëè F = A, òî óòâåðæäåíèå òåîðåìû òðèâèàëüíî. Èíà÷å, ðàññìàò-
                                                             ¡
ðèâàåì ñëó÷àè F = ¬ G è F = G◦H , ãäå ◦  îäèí èç ñèìâîëîâ ¢, N,
∨. Òðåáóåìàÿ ýêâèâàëåíòíîñòü F ' F (A|B) ñëåäóåò èç èíäóêòèâíîãî
ïðåäïîëîæåíèÿ è ëåììû 3.4.                                      ¤



1.4 Ìåòàòåîðèÿ ÈÑ N

Êîððåêòíîñòü è íåïðîòèâîðå÷èâîñòü.
Òåîðåìà 3.5 (Î êîððåêòíîñòè ÈÑ N ). Âñå âûâîäèìûå â N ñåêâåí-
öèè òîæäåñòâåííî èñòèííû.
Äîêàçàòåëüñòâî. Ïóñòü T  äåðåâî âûâîäà ñåêâåíöèè Σ. Èñïîëüçóåì
ïðèíöèï èíäóêöèè ïî âûñîòå äåðåâà T äîêàçàòåëüñòâà Σ.
   Åñëè Σ  àêñèîìà, òî óòâåðæäåíèå òåîðåìû òðèâèàëüíî. Òåïåðü
íàäî óáåäèòüñÿ, ÷òî âñå ïðàâèëà èç Rl(N ) ñîõðàíÿþò òîæäåñòâåííóþ
èñòèííîñòü ïðè òîæäåñòâåííîé èñòèííîñòè ãèïîòåç. Ïóñòü, íàïðèìåð,
ïðèìåíÿåòñÿ ïðàâèëî (+ N ):

                         Γ ` A    ∆ ` B
                                        .
                           Γ, ∆ ` A N B
Ðàññìîòðèì íåêîòîðóþ èíòåðïðåòàöèþ T    ϕM = Tϕ äëÿ äàííîãî íåïó-
ñòîãî ìíîæåñòâà M . Îáîçíà÷èì ÷åðåç        Γ è    ∆ ïåðåñå÷åíèå âñåõ
ìíîæåñòâ-îöåíîê ôîðìóë èç íàáîðîâ
                              T       Γ  è  ∆  ñîîòâåòñòâåííî.
                                               T                 Ïî èí-
äóêòèâíîìó
T     T     ïðåäïîëîæåíèþ,
              T                 Γ  ⊆  |A|ϕ  è    ∆  ⊆  |B| ϕ . Íî òîãäà
  Γ ∩ ∆ = {Γ ∪ ∆} ⊆ |A|ϕ ∩ |B|ϕ , ò.å. ϕ  ìîäåëü äëÿ ñåêâåíöèè
Γ, ∆ ` A N B . Â ñèëó ïðîèçâîëüíîñòè èíòåðïðåòàöèè ðàññìàòðèâàåìàÿ
ñåêâåíöèÿ òîæäåñòâåííî èñòèííà.
                                    ¡
   Ïóñòü ïðèìåíÿåòñÿ ïðàâèëî (− ¢):
                              ¡
                       Γ ` A ¢B     ∆ ` A
                                          .
                            Γ, ∆ ` B

Страницы