Математическая логика и теория алгоритмов. Самохин А.В. - 88 стр.

UptoLike

ВУЗ: 

МГТУ ГА | Москва

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

Рубрика: 

88 çÌÁ×Á IV. éÓÞÉÓÌÅÎÉÅ ×ÙÓËÁÚÙ×ÁÎÉÊ
ÆÏÒÍÕÌÁÍ ÜÔÏÇÏ ×Ù×ÏÄÁ ÓÌÅ×Á ÐÏÓÙÌËÕ A:
(A → C
1
), (A → C
2
), . . . , (A → C
n
).
üÔÁ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÏÓÔØ ÏËÁÎÞÉ×ÁÅÔÓÑ ÎÁ (A → B). óÁÍÁ ÐÏ ÓÅÂÅ ÏÎÁ ÎÅ
ÂÕÄÅÔ ×Ù×ÏÄÏÍ ÉÚ •, ÎÏ ÉÚ Îž ÍÏÖÎÏ ÐÏÌÕÞÉÔØ ÔÁËÏÊ ×Ù×ÏÄ, ÄÏÂÁ×É× ÎÅÄÏ-
ÓÔÁÀÝÉÅ ÆÏÒÍÕÌÙ, É ÔÅÍ ÓÁÍÙÍ ÄÏËÁÚÁÔØ ÌÅÍÍÕ Ï ÄÅÄÕËÃÉÉ.
âÕÄÅÍ ÄÏÂÁ×ÌÑÔØ ÜÔÉ ÆÏÒÍÕÌÙ, Ä×ÉÇÁÑÓØ ÓÌÅ×Á ÎÁÐÒÁ×Ï. ðÕÓÔØ ÍÙ ÐÏÄÏ-
ÛÌÉ Ë ÆÏÒÍÕÌÅ (A → C
i
). ðÏ ÐÒÅÄÐÏÌÏÖÅÎÉÀ ÆÏÒÍÕÌÁ C
i
ÌÉÂÏ ÓÏ×ÐÁÄÁÅÔ Ó
A, ÌÉÂÏ ÐÒÉÎÁÄÌÅÖÉÔ •, ÌÉÂÏ Ñ×ÌÑÅÔÓÑ ÁËÓÉÏÍÏÊ, ÌÉÂÏ ÐÏÌÕÞÁÅÔÓÑ ÉÚ Ä×ÕÈ
ÐÒÅÄÙÄÕÝÉÈ ÐÏ ÐÒÁ×ÉÌÕ MP. òÁÓÓÍÏÔÒÉÍ ×ÓÅ ÜÔÉ ÓÌÕÞÁÉ ÐÏ ÏÞÅÒÅÄÉ.
(1) åÓÌÉ C
i
ÅÓÔØ A, ÔÏ ÏÞÅÒÅÄÎÁÑ ÆÏÒÍÕÌÁ ÉÍÅÅÔ ×ÉÄ (A → A). ðÏ ÌÅÍÍÅ 1
ÏÎÁ ×Ù×ÏÄÉÍÁ, ÔÁË ÞÔÏ ÐÅÒÅÄ ÎÅÊ ÍÙ ÄÏÂÁ×ÌÑÅÍ Å¾ ×Ù×ÏÄ.
(2) ðÕÓÔØ C
i
ÐÒÉÎÁÄÌÅÖÉÔ •. ôÏÇÄÁ ÍÙ ×ÓÔÁ×ÌÑÅÍ ÆÏÒÍÕÌÙ C
i
É C
i
→
(A → C
i
) (ÁËÓÉÏÍÁ 1). ðÒÉÍÅÎÅÎÉÅ ÐÒÁ×ÉÌÁ MP Ë ÜÔÉÍ ÆÏÒÍÕÌÁÍ ÄÁ¾Ô
(A → C
i
), ÞÔÏ É ÔÒÅÂÏ×ÁÌÏÓØ.
(3) ôÅ ÖÅ ÆÏÒÍÕÌÙ ÍÏÖÎÏ ÄÏÂÁ×ÉÔØ, ÅÓÌÉ C
i
Ñ×ÌÑÅÔÓÑ ÁËÓÉÏÍÏÊ ÉÓÞÉÓÌÅ-
ÎÉÑ ×ÙÓËÁÚÙ×ÁÎÉÊ.
(4) ðÕÓÔØ, ÎÁËÏÎÅÃ, ÆÏÒÍÕÌÁ C
i
ÐÏÌÕÞÁÅÔÓÑ ÉÚ Ä×ÕÈ ÐÒÅÄÙÄÕÝÉÈ ÆÏÒÍÕÌ
ÐÏ ÐÒÁ×ÉÌÕ MP. üÔÏ ÚÎÁÞÉÔ, ÞÔÏ × ÉÓÈÏÄÎÏÍ ×Ù×ÏÄÅ ÅÊ ÐÒÅÄÛÅÓÔ×Ï×ÁÌÉ
ÆÏÒÍÕÌÙ C
j
É (C
j
→ C
i
). ôÏÇÄÁ × ÎÏ×ÏÊ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÏÓÔÉ (Ó ÄÏÂÁ×ÌÅÎÎÏÊ
ÐÏÓÙÌËÏÊ A) ÕÖÅ ÂÙÌÉ ÆÏÒÍÕÌÙ (A → C
j
) É (A → (C
j
→ C
i
)). ðÏÜÔÏÍÕ ÍÙ
ÍÏÖÅÍ ÐÒÏÄÏÌÖÉÔØ ÎÁÛ •-×Ù×ÏÄ, ÎÁÐÉÓÁ× ÆÏÒÍÕÌÙ
((A → (C
j
→ C
i
)) → ((A → C
j
) → (A → C
i
)) (ÁËÓÉÏÍÁ 2);
((A → C
j
) → (A → C
i
)) (modus ponens);
(A → C
i
) (modus ponens).
éÔÁË, ×Ï ×ÓÅÈ ÞÅÔÙÒ¾È ÓÌÕÞÁÑÈ ÍÙ ÎÁÕÞÉÌÉÓØ ÄÏÐÏÌÎÑÔØ ÐÏÓÌÅÄÏ×ÁÔÅÌØ-
ÎÏÓÔØ ÄÏ ×Ù×ÏÄÁ ÉÚ •, ÔÁË ÞÔÏ ÌÅÍÍÁ Ï ÄÅÄÕËÃÉÉ ÄÏËÁÚÁÎÁ.
úÁÄÁÞÁ 117. äÏËÁÖÉÔÅ, ÞÔÏ ÄÌÑ ÌÀÂÙÈ ÆÏÒÍÕÌ A, B, C ÆÏÒÍÕÌÁ
(A → B) → ((B → C) → (A → C))
×Ù×ÏÄÉÍÁ × ÉÓÞÉÓÌÅÎÉÉ ×ÙÓËÁÚÙ×ÁÎÉÊ. (õËÁÚÁÎÉÅ: ÉÓÐÏÌØÚÕÊÔÅ ÌÅÍÍÕ Ï ÄÅ-
ÄÕËÃÉÉ É ÔÏÔ ÆÁËÔ, ÞÔÏ A → B, B → C, A ` C.)
úÁÄÁÞÁ 118. äÏËÁÖÉÔÅ, ÞÔÏ ÅÓÌÉ •
1
` A É •
2
, A ` B, ÔÏ •
1
∪ •
2
`
` B. (üÔÏ Ó×ÏÊÓÔ×Ï ÉÎÏÇÄÁ ÎÁÚÙ×ÁÀÔ ¥ÐÒÁ×ÉÌÏÍ ÓÅÞÅÎÉÑ¥ (cut); ÇÏ×ÏÒÑÔ,
ÞÔÏ ÆÏÒÍÕÌÁ A ¥ÏÔÓÅËÁÅÔÓÑ¥ ÉÌÉ ¥×ÙÓÅËÁÅÔÓÑ¥. óÈÏÄÎÙÅ ÐÒÁ×ÉÌÁ ÉÇÒÁ-
ÀÔ ÃÅÎÔÒÁÌØÎÕÀ ÒÏÌØ × ÔÅÏÒÉÉ ÄÏËÁÚÁÔÅÌØÓÔ×, ÇÄÅ ÆÏÒÍÕÌÉÒÕÅÔÓÑ É ÄÏ-
ËÁÚÙ×ÁÅÔÓÑ ¥ÔÅÏÒÅÍÁ Ï ÕÓÔÒÁÎÅÎÉÉ ÓÅÞÅÎÉÑ¥ ÄÌÑ ÒÁÚÌÉÞÎÙÈ ÌÏÇÉÞÅÓËÉÈ
ÓÉÓÔÅÍ.)
88                                    çÌÁ×Á IV. éÓÞÉÓÌÅÎÉÅ ×ÙÓËÁÚÙ×ÁÎÉÊ

ÆÏÒÍÕÌÁÍ ÜÔÏÇÏ ×Ù×ÏÄÁ ÓÌÅ×Á ÐÏÓÙÌËÕ A:
                    (A → C1), (A → C2 ), . . . , (A → Cn).
üÔÁ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÏÓÔØ ÏËÁÎÞÉ×ÁÅÔÓÑ ÎÁ (A → B). óÁÍÁ ÐÏ ÓÅÂÅ ÏÎÁ ÎÅ
ÂÕÄÅÔ ×Ù×ÏÄÏÍ ÉÚ •, ÎÏ ÉÚ Îž ÍÏÖÎÏ ÐÏÌÕÞÉÔØ ÔÁËÏÊ ×Ù×ÏÄ, ÄÏÂÁ×É× ÎÅÄÏ-
ÓÔÁÀÝÉÅ ÆÏÒÍÕÌÙ, É ÔÅÍ ÓÁÍÙÍ ÄÏËÁÚÁÔØ ÌÅÍÍÕ Ï ÄÅÄÕËÃÉÉ.
   âÕÄÅÍ ÄÏÂÁ×ÌÑÔØ ÜÔÉ ÆÏÒÍÕÌÙ, Ä×ÉÇÁÑÓØ ÓÌÅ×Á ÎÁÐÒÁ×Ï. ðÕÓÔØ ÍÙ ÐÏÄÏ-
ÛÌÉ Ë ÆÏÒÍÕÌÅ (A → Ci ). ðÏ ÐÒÅÄÐÏÌÏÖÅÎÉÀ ÆÏÒÍÕÌÁ Ci ÌÉÂÏ ÓÏ×ÐÁÄÁÅÔ Ó
A, ÌÉÂÏ ÐÒÉÎÁÄÌÅÖÉÔ •, ÌÉÂÏ Ñ×ÌÑÅÔÓÑ ÁËÓÉÏÍÏÊ, ÌÉÂÏ ÐÏÌÕÞÁÅÔÓÑ ÉÚ Ä×ÕÈ
ÐÒÅÄÙÄÕÝÉÈ ÐÏ ÐÒÁ×ÉÌÕ MP. òÁÓÓÍÏÔÒÉÍ ×ÓÅ ÜÔÉ ÓÌÕÞÁÉ ÐÏ ÏÞÅÒÅÄÉ.
   (1) åÓÌÉ Ci ÅÓÔØ A, ÔÏ ÏÞÅÒÅÄÎÁÑ ÆÏÒÍÕÌÁ ÉÍÅÅÔ ×ÉÄ (A → A). ðÏ ÌÅÍÍÅ 1
ÏÎÁ ×Ù×ÏÄÉÍÁ, ÔÁË ÞÔÏ ÐÅÒÅÄ ÎÅÊ ÍÙ ÄÏÂÁ×ÌÑÅÍ Å¾ ×Ù×ÏÄ.
   (2) ðÕÓÔØ Ci ÐÒÉÎÁÄÌÅÖÉÔ •. ôÏÇÄÁ ÍÙ ×ÓÔÁ×ÌÑÅÍ ÆÏÒÍÕÌÙ Ci É Ci →
(A → Ci) (ÁËÓÉÏÍÁ 1). ðÒÉÍÅÎÅÎÉÅ ÐÒÁ×ÉÌÁ MP Ë ÜÔÉÍ ÆÏÒÍÕÌÁÍ ÄÁ¾Ô
(A → Ci ), ÞÔÏ É ÔÒÅÂÏ×ÁÌÏÓØ.
   (3) ôÅ ÖÅ ÆÏÒÍÕÌÙ ÍÏÖÎÏ ÄÏÂÁ×ÉÔØ, ÅÓÌÉ Ci Ñ×ÌÑÅÔÓÑ ÁËÓÉÏÍÏÊ ÉÓÞÉÓÌÅ-
ÎÉÑ ×ÙÓËÁÚÙ×ÁÎÉÊ.
   (4) ðÕÓÔØ, ÎÁËÏÎÅÃ, ÆÏÒÍÕÌÁ Ci ÐÏÌÕÞÁÅÔÓÑ ÉÚ Ä×ÕÈ ÐÒÅÄÙÄÕÝÉÈ ÆÏÒÍÕÌ
ÐÏ ÐÒÁ×ÉÌÕ MP. üÔÏ ÚÎÁÞÉÔ, ÞÔÏ × ÉÓÈÏÄÎÏÍ ×Ù×ÏÄÅ ÅÊ ÐÒÅÄÛÅÓÔ×Ï×ÁÌÉ
ÆÏÒÍÕÌÙ Cj É (Cj → Ci). ôÏÇÄÁ × ÎÏ×ÏÊ ÐÏÓÌÅÄÏ×ÁÔÅÌØÎÏÓÔÉ (Ó ÄÏÂÁ×ÌÅÎÎÏÊ
ÐÏÓÙÌËÏÊ A) ÕÖÅ ÂÙÌÉ ÆÏÒÍÕÌÙ (A → Cj ) É (A → (Cj → Ci )). ðÏÜÔÏÍÕ ÍÙ
ÍÏÖÅÍ ÐÒÏÄÏÌÖÉÔØ ÎÁÛ •-×Ù×ÏÄ, ÎÁÐÉÓÁ× ÆÏÒÍÕÌÙ
((A → (Cj → Ci )) → ((A → Cj ) → (A → Ci)) (ÁËÓÉÏÍÁ 2);
((A → Cj ) → (A → Ci )) (modus ponens);
(A → Ci ) (modus ponens).
   éÔÁË, ×Ï ×ÓÅÈ ÞÅÔÙÒ¾È ÓÌÕÞÁÑÈ ÍÙ ÎÁÕÞÉÌÉÓØ ÄÏÐÏÌÎÑÔØ ÐÏÓÌÅÄÏ×ÁÔÅÌØ-
ÎÏÓÔØ ÄÏ ×Ù×ÏÄÁ ÉÚ •, ÔÁË ÞÔÏ ÌÅÍÍÁ Ï ÄÅÄÕËÃÉÉ ÄÏËÁÚÁÎÁ.
     úÁÄÁÞÁ 117. äÏËÁÖÉÔÅ, ÞÔÏ ÄÌÑ ÌÀÂÙÈ ÆÏÒÍÕÌ A, B, C ÆÏÒÍÕÌÁ
                    (A → B) → ((B → C) → (A → C))
×Ù×ÏÄÉÍÁ × ÉÓÞÉÓÌÅÎÉÉ ×ÙÓËÁÚÙ×ÁÎÉÊ. (õËÁÚÁÎÉÅ: ÉÓÐÏÌØÚÕÊÔÅ ÌÅÍÍÕ Ï ÄÅ-
ÄÕËÃÉÉ É ÔÏÔ ÆÁËÔ, ÞÔÏ A → B, B → C, A ` C.)
   úÁÄÁÞÁ 118. äÏËÁÖÉÔÅ, ÞÔÏ ÅÓÌÉ •1 ` A É •2 , A ` B, ÔÏ •1 ∪ •2 `
` B. (üÔÏ Ó×ÏÊÓÔ×Ï ÉÎÏÇÄÁ ÎÁÚÙ×ÁÀÔ ¥ÐÒÁ×ÉÌÏÍ ÓÅÞÅÎÉÑ¥ (cut); ÇÏ×ÏÒÑÔ,
ÞÔÏ ÆÏÒÍÕÌÁ A ¥ÏÔÓÅËÁÅÔÓÑ¥ ÉÌÉ ¥×ÙÓÅËÁÅÔÓÑ¥. óÈÏÄÎÙÅ ÐÒÁ×ÉÌÁ ÉÇÒÁ-
ÀÔ ÃÅÎÔÒÁÌØÎÕÀ ÒÏÌØ × ÔÅÏÒÉÉ ÄÏËÁÚÁÔÅÌØÓÔ×, ÇÄÅ ÆÏÒÍÕÌÉÒÕÅÔÓÑ É ÄÏ-
ËÁÚÙ×ÁÅÔÓÑ ¥ÔÅÏÒÅÍÁ Ï ÕÓÔÒÁÎÅÎÉÉ ÓÅÞÅÎÉÑ¥ ÄÌÑ ÒÁÚÌÉÞÎÙÈ ÌÏÇÉÞÅÓËÉÈ
ÓÉÓÔÅÍ.)

Страницы