Метода

x7. zAKON PROTIWORE^IQ W IS^ISLENII WYSKAZYWANIJ

tEOREMA O ZAKONE PROTIWORE^IQ. wERNO, ^TO A; A ` B W iw. dOKAZATELXSTWO TEOREMY SOSTOIT IZ SLEDU@]IH UTWERVDENIJ:

A , NAZYWA@TSQ PROTIWORE^IWYMI POTOMU, ^TO IZ \TIH DWUH FORMUL PO DOKAZANNOJ TEOREME MOVNO WYWESTI WSE, ^TO UGODNO, T.E. L@BU@ FORMULU B .

tEOREMA O NESU]ESTWENNOJ GIPOTEZE. eSLI W IS^ISLENII

x8. iNTERPRETACIQ I NEPROTIWORE^IWOSTX

eSLI POSTAWITX W SOOTWETSTWIE BUKWAM ai IS^ISLENIQ WYSKAZY-

11

WANIJ LOGI^ESKIE PEREMENNYE ai , KOTORYE MOGUT PRINIMATX DWA ZNA^ENIQ 0 I 1, TO L@BAQ FORMULA iw PREWRA]AETSQ W PROPOZICIONALXNU@ FORMULU DWUZNA^NOJ LOGIKI. gOWORQT, ^TO DWUZNA^NAQ LOGIKA QWLQETSQ INTERPRETACIEJ iw.

oPREDELENIE 1. iNTERPRETACIQ M NAZYWAETSQ MODELX@ TEORII T , ESLI WYWODIMYE FORMULY (TEOREMY) TEORII T INTERPRETIRU@TSQ TOVDESTWENNO ISTINNYMI FORMULAMI W M .

` F(a1; a2; : : : ; an) W IS^ISLENII WYSKAZYWANIJ, TO F (a1 ; a2; : : : ; an) 1 , T.E. DWUZNA^NAQ LOGIKA QWLQETSQ MODELX@ IS^ISLENIQ WYSKAZYWANIJ.

dOKAZATELXSTWO. pROWERIM, ^TO AKSIOMAM A10 , A20 , A30 iw SOOTWETSTWU@T TOVDESTWENNO ISTINNYE FORMULY DWUZNA^NOJ LOGIKI.

I A ! B , PRIWODIT K TOVDESTWENNO ISTINNOJ FORMULE B .

eSLI F1; F2; : : : ; Fn { WYWOD FORMULY Fn = F (a1; a2; : : : ; an) ,

TO MY POSLEDOWATELXNO POLU^AEM, ^TO Fi 1 DLQ i = 1;2; : : : ; n . w ITOGE Fn = F (a1 ; a2; : : : ; an) 1 . tEOREMA DOKAZANA.

tEOREMA O NEPROTIWORE^IWOSTI iw. nE SU]ESTWUET FORMU-

LY A TAKOJ, ^TO ODNOWREMENNO ` A I ` A W IS^ISLENII WYSKAZYWANIJ.

dOKAZATELXSTWO. eSLI BY TAKAQ FORMULA A SU]ESTWOWALA, TO PRI EE INTERPRETACII MY POLU^ILI BY, ^TO ODNOWREMENNO A 1 I A 0 , A \TOGO W DWUZNA^NOJ LOGIKE BYTX NE MOVET.

tEOREMA O NEPROTIWORE^IWOSTI IS^ISLENIQ WYSKAZYWANIJ DOKAZANA.

12

x9. pOLNOTA IS^ISLENIQ WYSKAZYWANIJ

tEORIQ T NAZYWAETSQ POLNOJ OTNOSITELXNO MODELI M , ESLI W \TOJ TEORII WYWODIMY WSE TOVDESTWENNO ISTINNYE FORMULY MO-

lEMMA. pUSTX F (a1; a2; : : : ; an) { FORMULA I = F( 1; : : : ; n) ,

TOGDA a11 ; a22 ; : : : ; ann ` F (a1; a2; : : : ; an) .

dOKAZATELXSTWO BUDEM WESTI INDUKCIEJ PO LOGI^ESKOMU POSTROENI@ (LOGI^ESKOJ DLINE) FORMULY F .

1.pUSTX F { PEREMENNAQ, T.E. F (a) = a , TOGDA UTWERVDENIE LEMMY PREWRA]AETSQ W a ` a I QWLQETSQ O^EWIDNYM.

2.pUSTX F (a1; a2; : : : ; an) = G(a1; a2; : : : ; an) I DLQ FORMULY G

LEMMA WERNA. tOGDA a11 ; a22 ; : : : ; ann ` G (a1; a2 ; : : : ; an) . pOSKOLX-

KU G (a1; a2 ; : : : ; an) = G (a1; a2; : : : ; an) = F (a1; a2; : : : ; an) , TO

LEMMA WERNA I DLQ FORMULY F .

3. pUSTX F(a1; a2; : : : ; an) = G(a1; a2; : : : ; an) ! H(a1 ; a2; : : : ; an) I = ! , GDE = G( 1; 2; : : : ; n) , = H( 1; 2; : : : ; n) I

DLQ FORMUL G I H SPRAWEDLIWO UTWERVDENIE LEMMY. dALEE RASSMOTRIM TRI SLU^AQ.

3A. pUSTX = 0 . tOGDA = 1 I LEMMA DOKAZYWAETSQ TAK: 1) a11 ; : : : ; ann ` G { PO INDUKCIONNOMU PREDPOLOVENI@;

2) G; G ` H { PO ZAKONU PROTIWORE^IQ;

3) G ` G ! H { IZ 2 PO TEOREME DEDUKCII;

4) a11 ; : : : ; ann ` F { IZ 1 I 3 PO TRANZITIWNOSTI WYWODA S U^ETOM TOGO, ^TO = 1 I F = F = G ! H .

3B. pUSTX = 1 . tOGDA = 1 I LEMMA DOKAZYWAETSQ TAK: 1) a11 ; : : : ; ann ` H { PO INDUKCIONNOMU PREDPOLOVENI@;

2) ` H ! (G ! H) { AKSIOMA A10 ;

3) H ` G ! H { IZ 2 PO TEOREME DEDUKCII;

4) a11 ; : : : ; ann ` F { IZ 1 I 3 PO TRANZITIWNOSTI WYWODA S U^ETOM TOGO, ^TO = 1 I F = F = G ! H .

3W. pUSTX = 1 I = 0 . tOGDA LEMMA DOKAZYWAETSQ TAK:

1)a11 ; : : : ; ann ` G { PO INDUKCIONNOMU PREDPOLOVENI@;

2)a11 ; : : : ; ann ` H { PO INDUKCIONNOMU PREDPOLOVENI@;

3)G; H ` G ! H { PO TEOREME O WWEDENII KON_@NKCII;

13

` G ! H { IZ 1, 2 I 3 PO TRANZITIWNOSTI WYWODA. oSTALOSX U^ESTX, ^TO = 0 I F = F 0 = G ! H .

lEMMA POLNOSTX@ DOKAZANA.

IME@]IMSQ DIZ_@NKTAM A _ B I A _ C DO POLU^ENIQ ISKL@^A@- ]IH DRUG DRUGA FORMUL WIDA G I G .

pRIMER. dOKAZATX, ^TO (ab ! c)(d ! b)ad ` acd .

rE[ENIE. pRIWEDEM DANNYE FORMULY K KON_@NKTIWNOJ FORME I BUDEM POLU^ATX IH REZOLXWENTY:

F1 = ab ! c = a _ b _ c , F2 = d ! b = d _ b ,

14

w REZULXTATE POLU^ILOSX, ^TO F4 F10 = d d 0 .

x11. nEKLAUZALXNOE PRAWILO REZOL@CIJ

tEOREMA. eSLI A(x) I B(x) { FORMULY, SODERVA]IE LOGI^ES-

KU@ PEREMENNU@ x , TO A(x) B(x) = A(x) B(x) (A(0) _ B(1)) {

NEKLAUZALXNOE PRAWILO REZOL@CIJ.

dLQ DOKAZATELXSTWA RAZBEREM DWA SLU^AQ.

1.eSLI x = 0 , TO NEKLAUZALXNOE PRAWILO REZOL@CIJ SLEDUET IZ

RAWENSTWA A(0)(A(0)_B(1)) = A(0) , KOTOROE POLU^AETSQ PO PRAWILU POGLO]ENIQ.

2.eSLI x = 1 , TO DOSTATO^NO PRIMENITX ANALOGI^NOE RAWENSTWO

B(1)(A(0) _ B(1)) = B(1) .

pRIMER. dOKAZATX, ^TO x _ z; xy z ` y z .

rE[ENIE. bUDEM PRIMENQTX NEKLAUZALXNOE PRAWILO REZOL@CIJ, POSLEDOWATELXNO POLU^AQ SLEDU@]IE FORMULY:

F1 = x _ z ,

F2 = xy z ,

F3 = y z ,

F4 = F2jy=0 _ F3jy=1 = z _ z = z ,

F5 = F1jz=1 _ F4jz=0 = x _ 0 = x ,

F6 = F2jz=1 _ F4jz=0 = xy 1 = xy ,

F7 = F6jx=1 _ F5jx=0 = y _ 0 = y ,

F8 = F3jz=1 _ F4jz=0 = y _ 0 = y .

kON_@NKCIQ F7 F8 = yy 0 , ^TO I DOKAZYWAET ISKOMYJ WYWOD.

15

zAME^ANIE 2. fORMULU F , W KOTOROJ KAVDOE WHOVDENIE PEREMENNOJ x QWLQETSQ SWOBODNYM, BUDEM OBOZNA^ATX ^EREZ F (x) . wYRAVENIE F (xjjt) BUDET OZNA^ATX PRAWILXNU@ PODSTANOWKU TERMA t WMESTO KAVDOGO WHOVDENIQ PEREMENNOJ x W FORMULU F(x) . |TA PODSTANOWKA S^ITAETSQ PRAWILXNOJ, ESLI NI ODNA IZ PEREMENNYH WHODQ]IH W TERM t NE IMEET SWQZANNYH WHOVDENIJ W FORMULU F (x) .

dOKAZATELXSTWO. pUSTX G { L@BAQ DOKAZUEMAQ FORMULA, NE IME- @]AQ SWOBODNYH WHOVDENIJ x , TOGDA WERNY SLEDU@]IE UTWERVDENIQ:

1) ` F (x) { DANO PO USLOWI@;

2) ` F (x) ! (G ! F (x)) { AKSIOMA A10 ;

3) ` G ! F(x) { IZ 1 I 2 PO PRAWILU modus ponens; 4) ` G ! 8x F(x) { IZ 3 PO PRAWILU WWEDENIQ 8 ; 5) ` G { DANO PO USLOWI@;

6) ` 8x F (x) { IZ 5 I 4 PO PRAWILU modus ponens;

7) ` 8x F (x) ! F (xjjt) { AKSIOMA P1 ;

8) ` F (xjjt) { IZ 6 I 7 PO PRAWILU modus ponens. tEOREMA DOKAZANA.

zAME^ANIE 3. pO HODU DOKAZATELXSTWA TEOREMY BYLO POLU^ENO, ^TO IZ ` F (x) WYTEKAET ` 8x F(x) (UTWERVDENIE 6), A OTS@DA SLEDUET, ^TO F(x) ` 8x F(x) { PRAWILO OBOB]ENIQ.

17

tEOREMA O PEREIMENOWANII SWQZANNOJ PEREMENNOJ. eSLI

NIQ.

x13. iNTERPRETACIQ I NEPROTIWORE^IWOSTX

IS^ISLENIQ PREDIKATOW

pRI INTERPRETACII ip UKAZYWAETSQ MNOVESTWO M . kAVDAQ PREDMETNAQ PEREMENNAQ RASSMATRIWAETSQ NA \TOM MNOVESTWE M . kAVDAQ PREDMETNAQ KONSTANTA { \LEMENT IZ M . kAVDOMU FUNKCIONALXNOMU SIMWOLU fk OTWE^AET FUNKCIQ y = fk(x1; x2; : : : ; xk) TAKAQ, ^TO xi; y 2 M , A PREDIKATNOMU SIMWOLU Pk STAWITSQ W SOOTWETSTWIE k -MESTNYJ PREDIKAT y = Pk(x1; x2; : : : ; xk) TAKOJ, ^TO xi 2 M , A y 2 f0; 1g . oTS@DA SLEDUET, ^TO L@BAQ FORMULA ip INTERPRETIRUETSQ PREDIKATOM DWUZNA^NOJ LOGIKI.

` F W ip, TO F 1 PRI L@BOJ INTERPRETACII, T.E. DLQ L@BOJ PREDMETNOJ OBLASTI M .

dOKAZATELXSTWO. pUSTX ZADANA NEKOTORAQ INTERPRETACIQ IS^ISLENIQ PREDIKATOW. rASSMOTRIM AKSIOMU P 1 = 8x F (x) ! F (xjjt) . wOZMOVNY DWA SLU^AQ.

1) 8x F(x) = 1 , TOGDA F (x) 1 PRI L@BOM x 2 M I, W ^ASTNOSTI, F (xjjt) 1 , T.K. L@BOE ZNA^ENIE TERMA t PRINADLEVIT M .

oTS@DA SLEDUET, ^TO P 1 = 8x F (x) ! F (xjjt) 1 ! 1 1 .

2) 8x F (x) = 0 =) P 1 = 8x F(x) ! F(xjjt) = 0 ! F (xjjt) 1 . rASSMOTRIM DALEE AKSIOMU P2 = F(xjjt) ! 9x F (x) I WNOWX

RASSMOTRIM DWA SLU^AQ.

1) 9x F(x) = 0 , TOGDA F (x) 0 PRI L@BOM x 2 M I, W ^ASTNOSTI, F (xjjt) 0 , T.K. L@BOE ZNA^ENIE TERMA t PRINADLEVIT M . oTS@DA SLEDUET, ^TO P 2 = F(xjjt) ! 9x F (x) 0 ! 0 1 .

18

2) 9x F (x) = 1 =) P 2 =0 F(x0jjt) ! 90 x F (x) = F(xjjt) ! 1 1 . iSTINNOSTX AKSIOM A1 , A2 I A3 BYLA PROWERENA W iw.

dALEE DOKAZYWAEM, ^TO PRAWILA WYWODA, PRIMENENNYE K ISTINNYM FORMULAM, TAKVE PRIWODQT K ISTINNYM FORMULAM.

! 8

G ! F(x) 1 W DANNOJ INTERPRETACII. wOZMOVNY DWA SLU^AQ. 1) eSLI G = 0 , TO G ! 8x F (x) = 0 ! 8x F (x) = 1 ;

2) eSLI G = 1 , TO F (x) 1 , T.K. PO USLOWI@ G ! F(x) 1 . oTS@DA SLEDUET, ^TO G ! 8x F (x) = 1 ! 1 = 1 .

pRAWILO WWEDENIQ KWANTORA SU]ESTWOWANIQ RASSMATRIWAETSQ ANALOGI^NO, A PRAWILO modus ponens BYLO RASSMOTRENO W IS^ISLENII WYSKAZYWANIJ.

tEOREMA DOKAZANA.

tEOREMA O NEPROTIWORE^IWOSTI ip. nE SU]ESTWUET FOR-

MULY A TAKOJ, ^TO ODNOWREMENNO ` A I ` A W IS^ISLENII PREDIKATOW.

dOKAZATELXSTWO. eSLI BY TAKAQ FORMULA A SU]ESTWOWALA, TO PRI EE INTERPRETACII MY POLU^ILI BY, ^TO ODNOWREMENNO A 1 I A 0 , A \TOGO W DWUZNA^NOJ LOGIKE BYTX NE MOVET.

CII, TO ` F W IS^ISLENII PREDIKATOW. 1 PRI L@BOJ INTERPRETA- dOKAZATELXSTWO \TOJ TEOREMY MOVNO NAJTI, NAPRIMER, W [7].

x14. mETOD REZOL@CIJ W IS^ISLENII PREDIKATOW

tEOREMA DEDUKCII W ip. eSLI ; ` A ! B , TO ;; A ` B W IS^ISLENII PREDIKATOW.

dOKAZATELXSTWO SOSTOIT IZ SLEDU@]IH UTWERVDENIJ: 1) ; ` A ! B { DANO PO USLOWI@;

2) ;; A ` A ! B { PO PRAWILU OSLABLENIQ;

3) ;; A ` A { WYTEKAET IZ A ` A PO PRAWILU OSLABLENIQ; 4) ;; A ` B { IZ 3 I 2 PO PRAWILU modus ponens.

s NEKOTORYMI OGRANI^ENIQMI MOVNO DOKAZATX TEOREMU DEDUKCII I W OBRATNU@ STORONU. nAPRIMER, ESLI PRI WYWODE FORMULY B

19

IZ GIPOTEZ ;; A NE ISPOLXZU@TSQ PRAWILA WWEDENIQ KWANTOROW, TO ; ` A ! B SOGLASNO TEOREME DEDUKCII DLQ IS^ISLENIQ WYSKAZYWANIJ.

sLEDSTWIE. pUSTX F1; : : : ; Fn; F QWLQ@TSQ FORMULAMI IS^ISLENIQ PREDIKATOW I FORMULA G = F1 F2 : : : Fn F 0 DLQ L@BOJ PREDMETNOJ OBLASTI M , TOGDA F1 ; : : : ; Fn; ` F W IS^ISLENII PREDIKATOW.

F1 F2 : : : FnF 0 =) F1F2 : : : FnF 1 =) F1_F2_: : :_Fn_F 1 =) F1 ! (F2 ! : : : ! (Fn ! F) : : : ) 1 . iZ

TEOREMY O POLNOTE SLEDUET, ^TO ` F1 ! (F2 ! : : : ! (Fn ! F ) : : : ) W IS^ISLENII PREDIKATOW I, PRIMENQQ TEOREMU DEDUKCII, POLU^AEM,

^TO F1; : : : ; Fn ` F .

dOKAZATX, ^TO G = F1 F2 : : : Fn F 0 DLQ L@BOJ PREDMETNOJ OBLASTI M QWLQETSQ ZATRUDNITELXNYM WWIDU PROIZWOLXNOSTI MNOVESTWA M . oDNAKO, OKAZYWAETSQ DOSTATO^NYM PROWESTI \TO DOKAZATELXSTWO TOLXKO DLQ SPECIALXNOGO MNOVESTWA H , NAZYWAEMOGO \RBRANOWOJ OBLASTX@.

aLGORITM POSTROENIQ \RBRANOWOJ OBLASTI H DLQ FORMULY G .

^EREZ a . eSLI W FORMULE P NET PREDMETNYH KONSTANT, TO MNOVESTWO H SODERVIT \LEMENT c .

3. eSLI W FORMULE P IMEETSQ FUNKCIONALXNYJ SIMWOL

IZ h1; h2; : : : ; hn 2 H SLEDUET, ^TO fn(h1; h2; : : : ; hn) 2 H . pRIMER 1. eSLI G = 8x 8y (P (x; y) _ Q(x; y)) , TO H = fcg .

pRIMER 2. eSLI G = 8x 8y (P (a; f(x)) _ Q(x; f(y))) , TO OBLASTX H = fa; f(a); f(f(a)); : : : g { BESKONE^NOE MNOVESTWO.

pRIMER 3. eSLI G = 8x 8y (P(a; f(x)) _ Q(x; y; b)) , TO OBLASTX

H = fa; b; f(a); f(b); f(f(a)); f(f(b)); : : : g { BESKONE^NOE MNOVESTWO.

mETOD REZOL@CIJ W IS^ISLENII PREDIKATOW. dLQ DOKAZA-

TELXSTWA NEWYPOLNIMOSTI FORMULY G = 8x1 : : : 8xn P(x1; : : : ; xn) W

20