Лекционный курс (1109962), страница 2
Текст из файла (страница 2)
w KLASSI^ESKOJ LOGIKE PONQTIE SLEDOWANIQ FORMALIZUETSQTAK.oPREDELENIE 1.7 fORMULA ' NAZYWAETSQ LOGI^ESKIM SLEDSTWIEM MNOVESTWA FORMUL , ESLI WSQKAQ MODELX DLQ QWLQETSQ W TOVE WREMQ MODELX@ DLQ ', T.E. DLQ L@BOJMODELI MM j= =) M j= ':w \TOM SLU^AE MY PI[EM j= '.mY DOKAVEM SEJ^AS DWE PROSTYE, NO WAVNYE TEOREMY OB OTNO[ENII LOGI^ESKOGOSLEDOWANIQ j=. pERWAQ IZ NIH GOWORIT O TOM, ^TO ZADA^I, SWQZANNYE S LOGI^ESKIMSLEDSTWIEM, MOVNO SWESTI K PROBLEME OB]EZNA^IMOSTI.tEOREMA 1.8 (DEDUKCII) dLQ L@BOGO MNOVESTWA FORMUL I L@BYH FORMUL ' I; ' j= () j= ' ! :dOKAZATELXSTWO ()) pUSTX ; ' j= I PUSTX M | MODELX DLQ .
eSLI M j= ', TOM j= I, STALO BYTX, M j= ' ! . a ESLI M 6j= ', TO MY SRAZU IMEEM M j= ' ! .tAKIM OBRAZOM, j= ' ! .(() pUSTX j= ' ! I PUSTX M | MODELX DLQ [ f'g. nO TOGDA M j= , IBOESLI \TO NE TAK, MY BUDEM IMETX 6j= ' ! , ^EGO BYTX NE MOVET.2tEOREMA 1.9 (O ZAMENE) pUSTX '( ) | FORMULA, SODERVA]AQ WHOVDENIE PODFORMULY , A '( ) POLU^ENA IZ '( ) ZAMENOJ \TOGO WHOVDENIQ NA WHOVDENIE FORMULY .
tOGDA j= $ WLE^ET j= '( ) $ '( ).dOKAZATELXSTWO iNDUKCIQ PO POSTROENI@ '. bAZIS INDUKCII: '( ) = p. tOGDA= '( ) = p, = '( ) I POTOMU j= '( ) $ '( ).{AG INDUKCII: PUSTX '( ) = ! . wOZMOVNY TRI SLU^AQ.sLU^AJ 1: = '( ) = ! . tOGDA '( ) = I ZNA^IT j= '( ) $ '( ).sLU^AJ 2: WYDELENNOE WHOVDENIE W ' NAHODITSQ W , T.E. '( ) = ( ) ! ,'( ) = ( ) ! .
pO INDUKCIONNOJ GIPOTEZE j= ( ) $ ( ), T.E. ISTINNOSTNYEZNA^ENIQ ( ) I ( ) ODINAKOWY WO WSEH MODELQH. nO TOGDA ODINAKOWY WO WSEH MODELQHI ISTINNOSTNYE ZNA^ENIQ '( ) I '( ).sLU^AJ 3: '( ) = ! ( ). |TOT SLU^AJ, A TAKVE SLU^AI '( ) = ^ I'( ) = _ RASSMATRIWA@TSQ ANALOGI^NO.2klassi~eskaq logika wyskazywanij9tEOREMA O ZAMENE IMEET MNOGO SLEDSTWIJ.
tAK, POLXZUQSX PRIWEDENNYMI WY[EZAKONAMI Cl I TEOREMOJ O ZAMENE, NETRUDNO DOKAZATX SLEDU@]U@ TEOREMU.oPREDELENIE 1.10 gOWORIM, ^TO FORMULA ' NAHODITSQ W DIZ_@NKTIWNOJ (KON_@NKTIWNOJ) FORMALXNOJ FORME, ESLI ' = 1 _ : : : _ n (' = 1 ^ : : : ^ n), GDE n 1I KAVDAQ i QWLQETSQ KON_@NKCIEJ (SOOTWETSTWENNO, DIZ_@NKCIEJ) PEREMENNYH ILIOTRICANIJ PEREMENNYH.tEOREMA 1.11 pO WSQKOJ FORMULE MOVNO \FFEKTIWNO NAJTI \KWIWALENTNU@ EJFORMULU, NAHODQ]U@SQ W DIZ_@NKTIWNOJ (KON_@NKTIWNOJ) NORMALXNOJ FORME.dOKAZATELXSTWO uPRAVNENIE.21.1.1.1.2sEMANTI^ESKIE TABLICYoPREDELIW KLASSI^ESKU@ ILI KAKU@-LIBO INU@ LOGIKU L, MY STALKIWAEMSQ S PROBLEMOJ RASPOZNAWANIQ PO PROIZWOLXNOJ FORMULE PRINADLEVIT ONA L ILI NET. eSLISU]ESTWUET ALGORITM, RE[A@]IJ \TU PROBLEMU, TO NAZYWAEM LOGIKU RAZRE[IMOJ.rAZRE[IMOSTX KLASSI^ESKOJ LOGIKI SOWER[ENNO O^EWIDNA: TREBUEMYJ ALGORITMMOVET SOSTOQTX, NAPRIMER, W POSTROENII DLQ ISPYTUEMOJ FORMULY '(p1; : : :; pn ) EETABLICY ISTINNOSTI, KOTORAQ ESTX NE ^TO INOE KAK PEREBOR WSEH 2n MODELEJ W QZYKEfp1; : : : ; png.
pOLU^A@]IJSQ ALGORITM SLI[KOM BESHITROSTEN, I ^ASTO PREDPO^TITELXNEE IMETX INYE RAZRE[A@]IE PROCEDURY1 DLQ Cl.iMEETSQ DOBRAQ D@VINA RAZNOOBRAZNYH SPOSOBOW WYQSNENIQ TOVDESTWENNOJ ISTINNOSTI. mY RASSMOTRIM ODIN IZ NIH | METOD SEMANTI^ESKIH TABLIC (ILI TABLIC bETA), KOTORYJ, GRUBO GOWORQ, SOSTOIT W POPYTKE CELENAPRAWLENNOGO POSTROENIQKONTRMODELI DLQ ISPYTUEMOJ FORMULY.nA^NEM S PRIMEROW.pRIMER 1.12 dOPUSTIM, MY HOTIM OPREDELITX, QWLQETSQ LI FORMULA' = ((p ! q) ! p) ! p;IZWESTNAQ KAK ZAKON pIRSA, TOVDESTWENNO ISTINNOJ. s \TOJ CELX@ POPROBUEM POSTROITX KONTRMODELX DLQ '.nA^NEM POSTROENIE S TABLICY, SOSTOQ]EJ IZ DWUH ^ASTEJ: W LEWU@ ^ASTX ZANOSIMTE PODFORMULY ', KOTORYE MY HOTIM SDELATX ISTINNYMI, A W PRAWU@ | LOVNYMI.pOSKOLXKU MY HOTIM OPROWERGNUTX FORMULU ', EE SLEDUET POMESTITX W PRAWU@ ^ASTX.iSTINNOSTNAQ TABLICA DLQ ! ZASTAWLQET NAS POMESTITX (p ! q) ! p SLEWA, A p |SPRAWA:mY ZDESX NE RASSMATRIWAEM WOPROSY SRAWNENIQ RAZRE[A@]IH ALGORITMOW PO IH \FFEKTIWNOSTITO ESTX SKOROSTI RABOTY NAPRIMER oTMETIM ODNAKO ^TO WSE IZWESTNYE RAZRE[A@]IE ALGORITMYDLQ Cl NE BOLEE \FFEKTIWNY ^EM ALGORITM POSTROENIQ ISTINNOSTNYH TABLIC A WOPROS NAHOVDENIQBOLEE \FFEKTIWNOGO ALGORITMA QWLQETSQ ODNOJ IZ SAMYH INTRIGU@]IH PROBLEM TEORII SLOVNOSTIALGORITMOW I WY^ISLENIJ1,,.,.,,,glawa logika wyskazywanij((p ! q) ! p) ! p(p ! q) ! p ptEPERX MY IMEEM DWE WOZMOVNOSTI DLQ TOGO, ^TOBY (p ! q) ! p OKAZALASX ISTINNOJ, A IMENNO: p ISTINNA ILI p ! q LOVNA.
pO\TOMU PRIWEDENNU@ TABLICU MOVNORAS[IRQTX DWUMQ SPOSOBAMI:((p ! q) ! p) ! p(p ! q) ! p pp101.((p ! q) ! p) ! p(p ! q) ! p pp!qp qnO TOGDA MY POLU^AEM PROTIWORE^IE: OBE TABLICY TREBU@T, ^TOBY p BYLA I ISTINNA,I LOVNA. |TO ZNA^IT, ^TO KONTRMODELI DLQ ' NET I, TEM SAMYM,((p ! q) ! p) ! p 2 Cl:pRIMER 1.13 tEPERX ISPOLXZUEM TU VE TEHNIKU DLQ POSTROENIQ KONTRMODELI DLQ' = r ^ (:p _ :q) ! r ^ (p _ :q):pERWYE ^ETYRE STRO^KI TABLICY QSNY:r ^ (:p _ :q) ! r ^ (p _ :q)r ^ (:p _ :q) r ^ (p _ :q)r:p _ :qnO TEPERX IME@TSQ DWA SPOSOBA SDELATX r ^ (p _ :q) LOVNOJ: POMESTITX r W PRAWU@^ASTX ILI POMESTITX TUDA p _ :q.
pO\TOMU MY POLU^AEM DWA RAS[IRENIQ TABLICY:(a)r ^ (:p _ :q) ! r ^ (p _ :q)r ^ (:p _ :q) r ^ (p _ :q)r:p _ :qr1.1.klassi~eskaq logika wyskazywanij11(b)r ^ (:p _ :q) ! r ^ (p _ :q)r ^ (:p _ :q) r ^ (p _ :q)r:p _ :qp _ :qpq :qtREBOWANIQ TABLICY (a) PROTIWORE^IWY. tABLICA (b) WNOWX IMEET DWA RAS[IRENIQ:^TOBY SDELATX :p _ :q ISTINNOJ, MY MOVEM POMESTITX W LEWU@ ^ASTX LIBO :p, LIBO:q. pOSLEDNQQ ALXTERNATIWA SRAZU DAET PROTIWORE^IE, W TO WREMQ KAK PERWAQ DAETNAM TABLICUr ^ (:p _ :q) ! r ^ (p _ :q)r ^ (:p _ :q) r ^ (p _ :q)r:p _ :qp _ :qpq :q:pTREBOWANIQ KOTOROJ MOVNO WYPOLNITX, PRIDAW p ZNA^ENIE l, A q I r | i. pO\TOMU' LOVNA W KAVDOJ MODELI M, TAKOJ ^TO M j= q, M j= r I M 6j= p.tEPERX MY PREDSTAWIM \TU PROCEDURU POSTROENIQ TABLIC W WIDE KONE^NOGO NABORAPRAWIL POROVDENIQ I POKAVEM, ^TO DLQ PROIZWOLXNOJ FORMULY MY ZA KONE^NOE ^ISLO[AGOW LIBO POSTROIM EE KONTRMODELX, LIBO DOKAVEM EE TOVDESTWENNU@ ISTINNNOSTX.bUDEM PREDSTAWLQTX TABLICU KAK PARU MNOVESTW FORMUL: PERWOE SOSTOIT IZ FORMUL LEWOJ ^ASTI TABLICY, WTOROE | IZ FORMUL PRAWOJ ^ASTI.
tAKIM OBRAZOM, SEMANTI^ESKAQ TABLICA W QZYKE L ESTX PROSTO PARA t = ( ; ), GDE ; ForL.oPREDELENIE 1.14FORMUL ; 2 ForL,(S1)(S2)(S3)(S4)(S5)(S6)tABLICA ( ; ) NAZYWAETSQ NASY]ENNOJ W Cl, ESLI DLQ L@BYH^ 2^ 2_ 2_ 2! 2! 2WLE^ETWLE^ETWLE^ETWLE^ETWLE^ETWLE^ET222222IILIILIIILII 2 , 2 , 2 , 2 , 2 , 2 .glawa logika wyskazywanijtABLICA ( ; ) DIZ_@NKTNA, ESLI \ = ; I ? 62 . gOWORIM, ^TO TABLICA t0 =( 0; 0) QWLQETSQ RAS[IRENIEM TABLICY t = ( ; ) (ILI t QWLQETSQ PODTABLICEJ t0) IPI[EM t t0, ESLI 0 I 0.tABLICA t = ( ; ) NAZYWAETSQ REALIZUEMOJ, ESLI SU]ESTWUET MODELX M, TAKAQ^TOM j= DLQ WSEH 2 I M 6j= DLQ WSEH 2 ;W \TOM SLU^AE GOWORIM, ^TO M REALIZUET t.tEOREMA 1.15 tABLICA t = ( ; ) REALIZUEMA TOGDA I TOLXKO TOGDA, KOGDA ONAMOVET BYTX RAS[IRENA DO DIZ_@NKTNOJ NASY]ENNOJ TABLICY t0 = ( 0; 0).dOKAZATELXSTWO ()) pUSTX M | MODELX, REALIZU@]AQ t I PUSTX 0 = f' 2 ForL :M j= 'g I 0 = f' 2 ForL : M 6j= 'g. qSNO, ^TO 0 \ 0 = ;, ? 62 0, 0 I 0.sRAWNIWAQ USLOWIQ (S1) { (S6) S OPREDELENIEM OTNO[ENIQ j= NA STR.
6, LEGKO WIDETX,^TO t0 UDOWLETWORQET \TIM USLOWIQM I POTOMU NASY]ENNA.(() nUVNO POKAZATX, ^TO KAVDAQ DIZ_@NKTNAQ NASY]ENNAQ TABLICA ( 0; 0) REALIZUEMA. oPREDELIM MODELX M, POLAGAQ M = 0 \ VarL. iNDUKCIEJ PO POSTROENI@' LEGKO POLU^ITX, ^TO ' 2 0 WLE^ET M j= ' I ' 2 0 WLE^ET M 6j= '.2pREDLOVENIE 1.15 PREDOSTAWLQET NAM ALGORITM PROWERKI REALIZUEMOSTI KONE^NOJTABLICY. w SAMOM DELE, USLOWIQ (S1){(S6) MOVNO PRO^ITATX KAK PRAWILA NASY]ENIQ:(SR1)ESLI ^ 2 , TO DOBAWITX I K ,(SR2)ESLI ^ 2 , TO DOBAWITX ILI K ,121.etc.i TOGDA MY POLU^AEMtEOREMA 1.16 kONE^NAQ TABLICA t1 REALIZUEMA TOGDA I TOLXKO TOGDA, KOGDA SU]ESTWUET POSLEDOWATELXNOSTX TABLIC t1; : : :; tn, TAKAQ ^TO tn QWLQETSQ DIZ_@NKTNOJ NASY]ENNOJ I KAVDAQ TABLICA ti+1 POLU^AETSQ IZ ti PRIMENENIEM ODNOGOIZ PRAWIL NASY]ENIQ.dOKAZATELXSTWO uPRAVNENIE.21.1.3kLASSI^ESKOE IS^ISLENIE WYSKAZYWANIJkLASSI^ESKAQ LOGIKA WYSKAZYWANIJ MOVET BYTX PREDSTAWLENA W WIDE FORMALXNOJAKSIOMATI^ESKOJ SISTEMY, T.E.
IS^ISLENIEM, RAZLI^NYMI SPOSOBAMI. mY RASSMOTRIMZDESX TOLXKO ODNO IZ NIH. kLASSI^ESKOE IS^ISLENIE WYSKAZYWANIJ cl GILXBERTOWSKOGOTIPA ZADAETSQ SLEDU@]IMI AKSIOMAMI I PRAWILOM WYWODA.aKSIOMAMI: QWLQ@TSQ WSE FORMULY WIDAklassi~eskaq logika wyskazywanij13(A1) '0 ! ('1 ! '0),(A2) ('0 ! ('1 ! '2)) ! (('0 ! '1) ! ('0 ! '2)),(A3) '0 ^ '1 ! '0,(A4) '0 ^ '1 ! '1,(A5) '0 ! ('1 ! '0 ^ '1),(A6) '0 ! '0 _ '1,(A7) '1 ! '0 _ '1,(A8) ('0 ! '2) ! (('1 ! '2) ! ('0 _ '1 ! '2)),(A9) ? ! '0,(A10) '0 _ ('0 ! ?);pRAWILO WYWODA: Modus ponens (MP): '; ' ! = .pUSTX | MNOVESTWO FORMUL. pOSLEDOWATELXNOSTX '1; : : :; 'n NAZYWAEM WYWODOMFORMULY ' IZ MNOVESTWA GIPOTEZ , ESLI 'n = ' I DLQ KAVDOGO i 2 f1; : : : ; ng FORMULA 'i QWLQETSQ LIBO AKSIOMOJ, LIBO GIPOTEZOJ IZ , LIBO POLU^AETSQ IZ KAKIH-TOPRED[ESTWU@]IH DWUH FORMUL POSLEDOWATELXNOSTI PO PRAWILU MP. eSLI SU]ESTWUETWYWOD ' IZ , MY GOWORIM, ^TO ' WYWODIMA IZ I PI[EM `cl ' ILI PROSTO ` ',ESLI \TO NE WYZYWAET DWUSMYSLENNOSTI.
fORMULA ' NAZYWAETSQ WYWODIMOJ W cl, ESLI; `cl '; W \TOM SLU^AE PI[EM `cl ' ILI ` '.1.1.sLEDU@]AQ POSLEDOWATELXNOSTX QWLQETSQ WYWODOM ' ! '(' ! ((' ! ') ! ')) ! ((' ! (' ! ')) ! (' ! '))(A1)' ! ((' ! ') ! ')(A3)(' ! (' ! ')) ! (' ! ')(PO MP IZ (1), (2))' ! (' ! ')(A1)'!'(PO MP IZ (3), (4)).pRIMER 1.17(1)(2)(3)(4)(5)iS^ISLENIE cl NAZYWAEM KORREKTNYM, ESLI ` ' WLE^ET j= ' DLQ WSQKOJ FORMULY', I POLNYM, ESLI WERNO OBRATNOE, TO ESTX j= ' WLE^ET ` '. tEM SAMYM, KORREKTNOSTX I POLNOTA cl WMESTE OZNA^A@T, ^TO MNOVESTWO WYWODIMYH FORMUL SOWPADAET SMNOVESTWOM TOVDESTWENNO ISTINNYH FORMUL.` ' () j= ' DLQ L@BOJ FORMULY '.sLEDSTWIE 1.19 Cl = f' 2 ForL : `cl 'g.tEOREMA 1.18tAKIM OBRAZOM, TOVDESTWENNAQ ISTINNOSTX QWLQETSQ SEMANTI^ESKIM \KWIWALENTOM WYWODIMOSTI W cl.
sLEDU@]EE OBOB]ENIE TEOREMY 1.18 DAET ADEKWATNU@ SEMANTI^ESKU@ HARAKTERISTIKU DLQ PONQTIQ WYWODA IZ GIPOTEZ.tEOREMA 1.20` ' TOGDA I TOLXKO TOGDA, KOGDA j= '.glawa logika wyskazywanijtEOREMA 1.21 mNOVESTWO FORMUL IMEET MODELX TOGDA I TOLXKO TOGDA, KOGDAWSQKOE EGO KONE^NOE PODMNOVESTWO IMEET MODELX.141.dOPUSTIM, MODELI NE IMEET. tOGDA j= ?, I PO PREDYDU]EJTEOREME ` ?, A ZNA^IT IMEETSQ KONE^NOE PODMNOVESTWO MNOVESTWA , TAKOE ^TO ` ?, OTKUDA j= ?, T.E.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
