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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

(∨ →)
A, Γ → ∆ B, Γ → ∆
A ∨ B, Γ → ∆
(→
¡
¢
)
A, Γ → ∆, B
Γ → ∆, A
¡
¢
B
(
¡
¢
→)
Γ → ∆, A B, Γ → ∆
A
¡
¢
B, Γ → ∆
(→ ¬)
A, Γ → ∆
Γ → ∆, ¬ A
(¬ →)
Γ → ∆, A
¬ A, Γ → ∆
→ N
`
S
Γ → ∆ `
S
Γ → ∆
S A S `
S
A
S ((x
¡
¢
y)
¡
¢
x)
¡
¢
x
x → x, y
→ x, x
¡
¢
y
(→
¡
¢
) x → x
((x
¡
¢
y)
¡
¢
x) → x
→ ((x
¡
¢
y)
¡
¢
x)
¡
¢
x
(→
¡
¢
)
(
¡
¢
→)
S ¬ (x N y) → ¬ x ∨ ¬ y
x → x, ¬ y
→ x, ¬ x, ¬ y
(→ ¬)
y → y, ¬ x
→ y, ¬ y, ¬ x
(→ ¬)
→ x N y, ¬ x, ¬ y
(→ N)
→ x N y, ¬ x ∨ ¬ y
¬ (x N y) → ¬ x ∨ ¬ y
(¬ →)
(→ ∨)
114                     Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé

                 A, Γ → ∆      B, Γ → ∆
      (∨ →)                             ;
                      A ∨ B, Γ → ∆

         ¡         A, Γ → ∆, B
      (→ ¢)                  ¡ ;
                  Γ → ∆, A ¢ B

        ¡         Γ → ∆, A     B, Γ → ∆
      ( ¢ →)             ¡              ;
                      A ¢ B, Γ → ∆
                  A, Γ → ∆
      (→ ¬)                 ;
                 Γ → ∆, ¬ A
                  Γ → ∆, A
      (¬ →)                 .
                 ¬ A, Γ → ∆
   Ìû îáõîäèìñÿ áåç ïðàâèë ïåðåñòàíîâêè, ïîñêîëüêó ñîâîêóïíîñòè
ãèïîòåç ðàññìàòðèâàåì êàê ìóëüòèìíîæåñòâà. Îòìåòèì, ÷òî îñíîâíîå
îòëè÷èå ñåêâåíöèàëüíûõ èñ÷èñëåíèé îò ñèñòåì íàòóðàëüíîãî âûâîäà
ÿâëÿåòñÿ òî, ÷òî ïðåîáðàçîâàíèÿ çäåñü ìîãóò ïðîèñõîäèòü íå òîëüêî
ñëåâà, íî è ñïðàâà îò çíàêà âûâîäèìîñòè. Êðîìå òîãî, â ÈÑ íåò îãðà-
íè÷åíèé íà ÷èñëî ôîðìóë ïîñëå → (â È N äîïóñêàåòñÿ, êàê ìû
ïîìíèì, íå áîëåå îäíîé ôîðìóëû ñïðàâà îò `).
   Âûâîäû S áóäåì çàïèñûâàòü â âèäå äåðåâüåâ, èñïîëüçóÿ âñå ïî-
íÿòèÿ, ñâÿçàííûå ñ âûâîäîì â âèäå äåðåâà, ââåä¼ííûå â ï. 1.2. Åñëè
ñåêâåíöèÿ Γ → ∆ âûâîäèìà, áóäåì ïèñàòü `S Γ → ∆ (èíîãäà îïóñêàÿ
èíäåêñ S ). Ôîðìóëà A íàçûâàåòñÿ âûâîäèìîé â ÈÑ S , åñëè `S A.
                                                ¡    ¡   ¡
Ïðèìåð 3.5.     1. Âûâåäåì â S çàêîí Ïèðñà ((x ¢ y) ¢ x) ¢ x:
                   x → x, y         ¡
                            ¡   (→ ¢)        x→x
                   → x, x ¢ y                          ¡
                         ¡    ¡                      ( ¢ →)
                    ((x ¢ y) ¢ x) → x          ¡
                           ¡¢   ¡   ¡       (→ ¢)
                   → ((x y) ¢ x) ¢ x

  2. Ïîêàæåì, ÷òî â S âûâîäèìà ñåêâåíöèÿ ¬ (x N y) → ¬ x ∨ ¬ y :
        x → x, ¬ y                   y → y, ¬ x
                         (→ ¬)                    (→ ¬)
       → x, ¬ x, ¬ y               → y, ¬ y, ¬ x
                                                          (→ N)
                         → x N y, ¬ x, ¬ y
                        → x N y, ¬ x ∨ ¬ y                        (→ ∨)
                                              (¬ →)
                       ¬ (x N y) → ¬ x ∨ ¬ y

Страницы