Исчисление высказываний. Теорема дедукции

Ãëàâà III. Èñ÷èñëåíèå âûñêàçûâàíèé 1 Ÿ3. Òåîðåìà äåäóêöèè Òåîðåìà äåäóêöèè ÿâëÿåòñÿ îäíèì èç ôóíäàìåíòàëüíûõ ðåçóëüòàòîâ â òåîðèè äîêàçàòåëüñòâ  ðàçäåëå ìàòåìàòè÷åñêîé ëîãèêè, çàíèìàþùåìñÿ èçó÷åíèåì ìàòåìàòè÷åñêèõ äîêàçàòåëüñòâ. Òåîðåìà äåäóêöèè ÿâëÿåòñÿ ïðèìåðîì êëàññè÷åñêîé ñèòóàöèè â ìàòåìàòèêå ðàííèõ ëåò, êîãäà ó÷¼íûå, íå çíàêîìûå äðóã ñ äðóãîì è æèâóùèå â ðàçíûõ ñòðàíàõ, ïî÷òè îäíîâðåìåííî ôîðìóëèðóþò îäíó è òó æå èäåþ. Ýòà òåîðåìà âïåðâûå áûëà ñôîðìóëèðîâàíà è äîêàçàíà â 1930 ãîäó Æàêîì Ýðáðàíîì, ôðàíöóçñêèì ìàòåìàòèêîì.  ýòîì æå ãîäó òåîðåìà äåäóêöèè áûëà ñôîðìóëèðîâàíà Àëüôðåäîì Òàðñêèì, ïîëüñêî-àìåðèêàíñêèì ìàòåìàòèêîì, îñíîâàòåëåì ôîðìàëüíîé òåîðèè èñòèííîñòè. Òåîðåìà 1 (äåäóêöèè). Ïóñòü Γ  ìíîæåñòâî ôîðìóë ÈÂ, Φ, Ψ  ôîðìóëû ÈÂ. Òîãäà Γ, Φ ` Ψ ⇐⇒ Γ ` Φ → Ψ. Ïóñòü Ψ1 , . . . , Ψn  âûâîä Ψ èç Γ ∪ {Φ}. Èíäóêöèåé ïî i ïîêàæåì, ÷òî Γ ` Φ → Ψi . 1. Äëÿ ôîðìóëû Ψ1 âîçìîæíû ñëåäóþùèå ñëó÷àè: à) Ψ1  àêñèîìà; á) Ψ1 ∈ Γ; â) Ψ1 Φ. Ïîñòðîèì âûâîä ôîðìóëû Φ → Ψ1 â ñëó÷àÿõ à) è á): 1. [àêñèîìà èëè ãèïîòåçà] Ψ1 . 2. [A1] ΨΦ1 Ψ Φ Ψ1 → (Φ → Ψ1 ). 3. [MP (1, 2)] Φ → Ψ1 . Åñëè Ψ1 Φ, òî Γ ` Φ → Ψ1 ïî ñâîéñòâó 1. Òàêèì îáðàçîì, óòâåðæäåíèå âåðíî äëÿ i = 1. 2. Ïðåäïîëîæèì, ÷òî Γ ` Φ → Ψj äëÿ âñåõ j < i. Äëÿ ôîðìóëû Ψi âîçìîæíû ñëåäóþùèå ñëó÷àè: Äîêàçàòåëüñòâî. Íåîáõîäèìîñòü. 2 Êîíñïåêò ëåêöèé ïî ìàòåìàòè÷åñêîé ëîãèêå. Åôðåìîâ Å.Ë. à) Ψi  àêñèîìà; á) Ψi ∈ Γ; â) Ψi Φ; ã) Ψi âûâîäèòñÿ èç Ψ1 , . . . , Ψi−1 ïî modus ponens. Î÷åâèäíî, â ñëó÷àÿõ à)â) âûâîä ñòðîèòñÿ àíàëîãè÷íî ï. 1. Ïóñòü Ψi âûâîäèòñÿ èç Ψ1 , . . . , Ψi−1 ïî modus ponens. Òîãäà ñ ïîìîùüþ ïðàâèëà âûâîäà Ψi ïîëó÷àåòñÿ èç ôîðìóë Ψk è Ψl Ψk → Ψi , ãäå k, l < i. Ïî ïðåäïîëîæåíèþ èíäóêöèè Γ ` Φ → Ψk è Γ ` Φ → (Ψk → Ψi ). Ïîñòðîèì êâàçèâûâîä ôîðìóëû Φ → Ψi : 1. [ïî ïðåäï.] Φ → Ψk . 2. [ïî ïðåäï.] Φ → (Ψk → Ψi ). 3. [A2] ΨΨk ΨΘi (Φ → Ψk ) → ((Φ → (Ψk → Ψi )) → (Φ → Ψi ). 4. [MP ((1, 3), 2)] Φ → Ψi . Ñëåäîâàòåëüíî, Γ ` Φ → Ψn , ò.å. Γ ` Φ → Ψ. Äîñòàòî÷íîñòü. Òàê êàê âûâîä  ýòî êîíå÷íàÿ ïîñëåäîâàòåëüíîñòü ôîðìóë, òî âûäåëèì èç ìíîæåñòâà Γ òîëüêî òå ôîðìóëû Φ1 , . . . , Φm , êîòîðûå çàäåéñòâîâàíû â âûâîäå ôîðìóëû Φ → Ψ. Ïîñòðîèì êâàçèâûâîä ôîðìóëû Ψ èç Γ ∪ {Φ}: 1. [ãèï] Φ1 . ... m. [ãèï] Φm . m + 1. [ïî óñë.] Φ → Ψ. m + 2. [ãèï] Φ. m + 3. [MP (m + 2, m + 1)] Ψ.  Ñâîéñòâî 3 (êîíòðàïîçèöèè). Φ → Ψ `qΨ →qΦ. Äîêàçàòåëüñòâî. Äîêàæåì, ÷òî Φ → Ψ, qΨ `qΦ: 1. [ãèï] Φ → Ψ. 2. [ãèï] qΨ. 3. [A9] (Φ → Ψ) → ((Φ →qΨ) →qΦ). 4. [MP (1, 3)] (Φ →qΨ) →qΦ. Φ Ψ qΨ → (Φ →qΨ). 5. [A1] qΨ Φ Ãëàâà III. Èñ÷èñëåíèå âûñêàçûâàíèé 3 6. [MP (2, 5)] Φ →qΨ. 7. [MP (6, 4)] qΦ. Òàêèì îáðàçîì, Φ → Ψ, qΨ `qΦ. Ïðèìåíèâ òåîðåìó äåäóêöèè, ïîëó÷èì Φ → Ψ `qΨ →qΦ.  Ñâîéñòâî 4 (òðàíçèòèâíîñòè). Φ → Ψ, Ψ → Θ ` Φ → Θ. Óïðàæíåíèå 1. Äîêàæèòå ñâîéñòâî 4 ñ èñïîëüçîâàíèåì è áåç èñïîëüçîâàíèÿ òåîðåìû äåäóêöèè. Äîêàæåì åù¼ íåñêîëüêî ñâîéñòâ, êîòîðûìè óäîáíî ïîëüçîâàòüñÿ ïðè ïîñòðîåíèè âûâîäà ôîðìóë. Ñâîéñòâî 5. Φ `qqΦ. Äîêàçàòåëüñòâî. 1. 2. 3. 4. 5. 6. 7. [ãèï] Φ. Φ Ψ (qΦ → Φ) → ((qΦ →qΦ) →qqΦ). [A9] qΦ Φ Ψ [A1] qΦ Φ → (qΦ → Φ). [MP (1, 3)] qΦ → Φ. [MP (4, 2)] (qΦ →qΦ) →qqΦ. Φ qΦ →qΦ. [ñâ. 1] qΦ [MP (6, 5)] qqΦ. Ñâîéñòâî 6. Φ∧qΦ ` Ψ, ãäå Ψ  ëþáàÿ ôîðìóëà ÈÂ.  Äîêàçàòåëüñòâî. 1. [ãèï] Φ∧qΦ. Ψ Φ∧qΦ → Φ. 2. [A3] qΦ 3. [MP (1, 2)] Φ. Ψ Φ∧qΦ →qΦ. 4. [A4] qΦ 5. [MP (3, 4)] qΦ. Ψ Φ → (qΘ → Φ). 6. [A1] qΘ 7. [MP (3, 6)] qΘ → Φ. Φ Ψ qΦ →qqΘ. 8. [ñâ. êîíòð. (7)] qΘ Φ 9. [MP (5, 8)] qqΘ. Φ qqΘ → Θ. 10. [A10] Θ 11. [MP (9, 10)] Θ.