Лекционный курс (1109962), страница 4
Текст из файла (страница 4)
(sM.RISUNOK 1.2 (a).)tEPERX STROIM [KALU F = hW; Ri I MODELX M = hF ; Vi W SOOTWETSTWII S NA[EJSISTEMOJ TABLIC, T.E. POLAGAQW = ft0; t1; t2g;R = fht0; t1i ; ht0; t2i ; hti; tii : i = 0; 1; 2g;V (p) = ft1g; V (q) = ft2g:(dIAGRAMMA F IZOBRAVENA NA RISUNKE 1.2 (b).) tOGDA MY BUDEM IMETX: t1 j= p, t1 6j= qI POTOMU t0 6j= p ! q; t2 j= q, t2 6j= p I POTOMU t0 6j= q ! p. w ITOGE, (M; t0) 6j= '.pRIMER 1.27 rASSMOTRIM TEPERX FORMULUp2 _ (p2 ! p1 _ :p1):kAK I WY[E, OBRAZUEM TABLICU t0, ZANESQ \TU FORMULU W EE PRAWU@ ^ASTX.
tOGDA TUDAVE MY DOLVNY ZANESTI I p2, I p2 ! p1 _ :p1. ~TOBY SDELATX POSLEDN@@ FORMULU NEISTINNOJ W t0, OBRAZUEM NOWU@ TABLICU t1, DOSTIVIMU@ IZ t0, KOTORAQ SODERVIT p2 WLEWOJ ^ASTI, A p1 _ :p1 I, TEM SAMYM, p1 I :p1 | W PRAWOJ. tEPERX, DLQ TOGO, ^TOBYSDELATX :p1 OPROWERGAEMOJ W t1, OPQTX OBRAZUEM NOWU@ TABLICU t2, DOSTIVIMU@ IZglawa20t0p2 _ (p2 ! p1 _ :p1)p2p2 ! p1 _ :p1-(a)1.t1p2 p1 _ :p1p1:p1logika wyskazywanij-t2p1p26t26t1 t0(b)rIS.
1.3:t1, W KOTOROJ p1 ISTINNA, T.E. NAHODITSQ W LEWOJ ^ASTI \TOJ TABLICY. nAM NUVNO NEZABYTX, ^TO WSE FORMULY, ISTINNYE W t1, DOLVNY BYTX ISTINNYMI I W t2, PO\TOMUZANESEM p2 W LEWU@ ^ASTX t2. (sM. RISUNOK 1.3 (a).)tEPERX OPREDELQEM [KALU F = hW; Ri I OCENKU V W NEJ, POLAGAQ, ^TOW = ft0; t1; t2g;R = fhti; tj i : i; j = 0; 1; 2 I i j g;V (p1) = ft2g; V (p2) = ft1; t2g:(dIAGRAMMA F POKAZANA NA RISUNKE 1.3 (b).) ~ITATELX LEGKO PROWERIT, ^TO WSE FORMULY IZ LEWOJ ^ASTI TABLICY ti ISTINNY W TO^KE ti MODELI M = hF ; Vi, A FORMULY IZPRAWOJ ^ASTI ISTINNYMI NE QWLQ@TSQ. sLEDOWATELXNO, (M; t0) 6j= p2 _ (p2 ! p1 _:p1).nA[A SLEDU@]AQ CELX | POKAZATX, ^TO OPISANNAQ WY[E PROCEDURA OPROWERVENIQWSEGDA SRABATYWAET: ZA KONE^NOE ^ISLO [AGOW MY LIBO POSTROIM KONTRMODELX DLQDANNOJ FORMULY ', LIBO DOKAVEM, ^TO ' 2 Int.kAK I WY[E, TABLICA | \TO PARA t = ( ; ), GDE ; ForL.
tABLICA t NAZYWAETSQ NASY]ENNOJ W Int, ESLI ONA UDOWLETWORQET USLOWIQM (S1){(S5) IZ RAZDELA 1.1.2.tAK, WSQKAQ TABLICA, NASY]ENNAQ W Cl QWLQETSQ NASY]ENNOJ I W Int; OBRATNOE MOVETI NE WYPOLNQTXSQ, KAK \TO WIDNO IZ PRIWEDENNYH WY[E PRIMEROW.sISTEMOJ hINTIKKI W Int NAZYWAETSQ PARA H = hT; S i, SOSTOQ]AQ IZ NEPUSTOGOMNOVESTWA T DIZ_@NKTNYH NASY]ENNYH TABLIC I ^ASTI^NOGO PORQDKA S NA T , DLQKOTOROJ WYPOLNQ@TSQ SLEDU@]IE USLOWIQ:(HSI 1) ESLI t = ( ; ), t0 = ( 0; 0) PRINADLEVAT T I tSt0, TO 0;(HSI 2)ESLI t = ( ; ) NAHODITSQ W T I ! 2 , TO W T SU]ESTWUET t0 = ( 0; 0),T.^.
tSt0, 2 0 I 2 0.gOWORIM, ^TO H = hT; S i QWLQETSQ SISTEMOJ hINTIKKI DLQ TABLICY t, ESLI t t0DLQ NEKOTOROJ t0 2 T . tABLICA t = ( ; ) NAZYWAETSQ REALIZUEMOJ W Int, ESLI IME@TSQINTUICIONISTSKAQ MODELX M I TO^KA x W M, T.^.(M; x) j= DLQ WSQKOJ 2 I (M; x) 6j= DLQ WSQKOJ 2 ;GOWORIM W \TOM SLU^AE TAKVE, ^TO t REALIZUEMA W MODELI M.intuicionistskaq logika21tEOREMA 1.28 tABLICA t REALIZUEMA W Int TOGDA I TOLXKO TOGDA, KOGDA SU]ESTWUET SISTEMA hINTIKKI DLQ t.1.2.()) pREDPOLOVIM, ^TO TABLICA t REALIZUEMA W MODELI M, OPREDELENNOJ NA [KALE F = hW; Ri.
s KAVDOJ x 2 W ASSOCIIRUEM TABLICU tx = ( x ; x),dOKAZATELXSTWOGDE= f' 2 ForL : x j= 'g; x = f' 2 ForL : x 6j= 'g;I OPREDELQEM ^ASTI^NYJ PORQDOK S NA MNOVESTWE T = ftx : x 2 W g, POLAGAQ, ^TOxtxSty () xRy:nEPOSREDSTWENNO IZ OPREDELENIQ INTUICIONISTSKOJ MODELI I UTWERVDENIQ 1.23 SLEDUET, ^TO H = hT; S i QWLQETSQ SISTEMOJ hINTIKKI. kROME TOGO, t tx DLQ NEKOTOROGOx 2 W.(() pUSTX H = hT; S i | SISTEMA hINTIKKI DLQ t. bUDEM PONIMATX H KAK INTUICIONISTSKU@ [KALU. oPREDELQEM NA NEJ MODELX M = hH; Vi, POLAGAQ DLQ KAVDOJPEREMENNOJ p, ^TOV (p) = fu = ( ; ) : u 2 T I p 2 g:uSLOWIE (HSI 1) OBESPE^IWAET, ^TO V (p) 2 UpT . iNDUKCIEJ PO POSTROENI@ FORMULY' POKAZYWAEM, ^TO DLQ WSQKOJ TABLICY u = ( ; ) IZ TIZ ' 2 SLEDUET, ^TO (M; u) j= ';IIZ ' 2 SLEDUET, ^TO (M; u) 6j= ':bAZIS INDUKCII O^EWIDEN, SLU^AI ' = ^ I ' = _ W INDUKCIONNOM [AGERASSMATRIWA@TSQ TO^NO TAKVE, KAK I DLQ Cl.
pUSTX ' = ! , PRI^EM DLQ I DOKAZYWAEMOE WYPOLNQETSQ.dOPUSTIM, ^TO ' 2 , NO u 6j= '. tOGDA SU]ESTWUET TO^KA v = (; ) W T , T.^.uSv, v j= I v 6j= . pO (HSI 1) ' 2 I PO (S5) LIBO 2 , LIBO 2 . tOGDA, POINDUKCIONNOMU PREDPOLOVENI@ MY DOLVNY IMETX LIBO v j= , LIBO v 6j= , NO I TO,I DRUGOE PROTIWORE^IT WYBORU v. zNA^IT u j= '.tEPERX DOPUSTIM, ^TO ' 2 . tOGDA PO USLOWI@ (HSI 2) SU]ESTWUET TAKAQ TABLICAv = (; ), ^TO uSv, 2 I 2 . pO INDUKCIONNOMU PREDPOLOVENI@ POLU^AEMv j= I v 6j= , OTKUDA u 6j= ! .2kAK SLEDUET IZ UTWERVDENIQ 1.28, ' 62 Int TOGDA I TOLXKO TOGDA, KOGDA SU]ESTWUET(BESKONE^NAQ, WOOB]E GOWORQ) SISTEMA hINTIKKI DLQ TABLICY t = (;; f'g). oDNAKO NASAMOM DELE MY MOVEM POLU^ITX NAMNOGO BOLEE SILXNYJ REZULXTAT, ZAMETIW, ^TO PRIPOSTROENII W DOKAZATELXSTWE UTWERVDENIQ 1.28 SISTEMY hINTIKKI DLQ t MY IMELIDELO LI[X S PODFORMULAMI '.
~ISLO RAZLI^NYH TABLIC, SOOTWETSTWU@]IH TO^KAMglawa logika wyskazywanijF , BUDET TOGDA KONE^NYM, TO^NEE GOWORQ | NE PREWOSHODQ]IM 2jSub'j, A OTNO[ENIEDOSTIVIMOSTI MOVET BYTX WSEGDA OPREDELENO TAKIM OBRAZOM, ^TO USLOWIQ (HSI 1) I(HSI 2) WYPOLNQ@TSQ.bOLEE OB]O, IMEET MESTO SLEDU@]AQ221.tABLICA t REALIZUEMA W Int TOGDA I TOLXKO TOGDA, KOGDA SU]ESTWUET SISTEMA hINTIKKI H = hT; S i DLQ t, T.^. jT j 2jj, GDE | \TO MNOVESTWOWSEH PODFORMUL FORMUL IZ t.tEOREMA 1.29dOKAZATELXSTWO ()) mODIFICIRUEM W SOOTWETSTWII S WYSKAZANNOJ IDEEJ DOKAZATELXSTWO ^ASTI TOLXKO ESLI UTWERVDENIQ 1.28. nA \TOT RAZ MY ASSOCIIRUEM SKAVDOJ TO^KOJ x 2 W TABLICU tx = ( x ; x), W KOTOROJx= f' 2 : x j= 'g; x = f' 2 : x 6j= 'g:pOLOVIW T = ftx : x 2 W g, MY O^EWIDNYM OBRAZOM IMEEM jT j 2jj . oPREDELIMOTNO[ENIE S NA T , POLAGAQ DLQ TABLIC tx = ( x; x) I ty = ( y ; y ), ^TO* x y:txSty )dLQ TOGO, ^TOBY PROWERITX, ^TO H = hT; S i QWLQETSQ SISTEMOJ hINTIKKI DLQ t, DOSTATO^NO PROWERITX TOLXKO (HSI 2).
pUSTX tx = ( x ; x) | TABLICA IZ T I ! 2 x.tOGDA x 6j= ! I POTOMU SU]ESTWUET TO^KA y, T.^. xRy, 2 y I 2 y . sOGLASNOPREDLOVENI@ 1.23 WYPOLNQETSQ x y , I ZNA^IT, txSty .dOKAZATELXSTWO (() OSTAETSQ TAKIM VE, KAK DLQ TEOREMY 1.28.2dLQ WSQKOJ FORMULY ' 62 Int SU]ESTWUET [KALA, OPROWERGA@]AQ' I SODERVA]AQ NE BOLEE 2jSub'j TO^EK.sLEDSTWIE 1.30uPRAVNENIE 1.31pOKAVITE, ^TO :p $ :::p 2 Int.tEOREMA 1.29 OZNA^AET, W ^ASTNOSTI, ^TO NA^AW S TABLICY (;; f'g) I ISPOLXZUQPRAWILA NASY]ENIQ (SR1){(SR5) IZ RAZDELA 1.1.2 I PRAWILO(SRI 6) ESLI t = ( ; ) I ! 2 , TO LIBO DOBAWXTE K 0 I K 0 DLQNEKOTOROJ t0 = ( 0; 0), DOSTIVIMOJ IZ t, ILI POSTROJTE NOWU@ TABLICUt0 = ( 0; 0), DOSTIVIMU@ IZ t, POLAGAQ 0 = [ f g, 0 = f g,ZA KONE^NOE ^ISLO [AGOW MY LIBO POSTROIM SISTEMU hINTIKKI DLQ (;; f'g), A POTOMUI KONTRMODELX DLQ ', LIBO POKAVEM, ^TO SISTEMY hINTIKKI DLQ (;; f'g) S 2jSub'jTABLICAMI NE SU]ESTWUET, A POTOMU ' 2 Int.1.2.intuicionistskaq logika1.2.3nEKOTORYE SWOJSTWA Int23iNTUICIONISTSKOE PROPOZICIONALXNOE IS^ISLENIE int W QZYKE L OPREDELQETSQ AKSIOMAMI (A1){(A9) I PRAWILOM WYWODA MP IZ RAZDELA 1.1.3.
pONQTIQ WYWODA I WYWODAIZ GIPOTEZ OPREDELQ@TSQ TO^NO TAK VE KAK DLQ KLASSI^ESKOGO IS^ISLENIQ cl. fAKTWYWODIMOSTI FORMULY ' W Int OBOZNA^AETSQ POSREDSTWOM `int ', A `int ' OZNA^AET,^TO ' WYWODIMA W Int IZ MNOVESTWA GIPOTEZ .`int ' TOGDA I TOLXKO TOGDA, KOGDA (M; x) j= ' DLQ L@BOJ MODELIM I WSQKOJ TO^KI x W M, TAKOJ ^TO (M; x) j= .`int ' () 8F F j= ' () ' 2 Int:tEOREMA 1.32tEOREMA 1.33 (gLIWENKO)dLQ L@BOJ FORMULY '' 2 Cl () ::' 2 Int:()) dOPUSTIM PROTIWNOE, T.E.
' 2 Cl I ::' 62 Int DLQ NEKOTOROJFORMULY '. tOGDA IME@TSQ KONE^NAQ MODELX M I TO^KA x W M, T.^. x 6j= ::'.zNA^IT, ESTX TAKAQ y 2 x", ^TO y j= :'. pUSTX z | NEKOTORAQ MAKSIMALXNAQ TO^KAWO MNOVESTWE y". pO UTWERVDENI@ 1.23 z j= :', A POTOMU I z 6j= ::'. pUSTX M1 |PODMODELX M, POROVDENNAQ, T.E. (M1; z) j= p TOGDA I TOLXKO TOGDA, KOGDA (M; z) j= pDLQ L@BOJ PEREMENNOJ p. pO TEOREME O POROVDENII M1 OPROWERGAET ::', A POSKOLXKUONA SODERVIT WSEGO ODNU TO^KU, \TO DAET ::' 62 Cl, ^TO PO ZAKONU DWOJNOGO OTRICANIQWLE^ET PROTIWORE^IE S PREDPOLOVENIEM.(() iZ ::' 2 Int SLEDUET ::' 2 Cl, OTKUDA, ISPOLXZUQ TOT VE ZAKON DWOJNOGOOTRICANIQ, POLU^AEM ' 2 Cl.2dOKAZATELXSTWOoPREDELENIE 1.34LA F , T.^.lOGIKA L NAZYWAETSQ TABLI^NOJ, ESLI SU]ESTWUET KONE^NAQ [KAL = f' 2 ForL : F j= 'g:pO OPREDELENI@ KLASSI^ESKAQ PROPOZICIONALXNAQ LOGIKA Cl TABLI^NA.tEOREMA 1.35lOGIKA Int NE QWLQETSQ TABLI^NOJ.pREDPOLOVIM PROTIWNOE. pUSTX F | KONE^NAQ [KALA, SODERVA]AQ, SKAVEM, n TO^EK, W KOTOROJ OPROWERGA@TSQ WSE FORMULY, NE PRINADLEVA]IE Int.tOGDA F OPROWERGAET I FORMULUbcm = p0 _ (p0 ! p1 ) _ (p0 ^ p1 ! p2 ) _ : : : _ (p0 ^ : : : ^ pm 1 ! pm )PRI L@BOM m, ^TO NEWOZMOVNO.2dOKAZATELXSTWOglawa24AAF1 AA A1I@@@xA1.logika wyskazywanijF2 A A2xx0rIS.
1.4:tEOREMA 1.36FORMUL ' IlOGIKA Int OBLADAET DIZ_@NKTIWNYM SWOJSTWOM, T.E. DLQ L@BYH' _ 2 Int () ' 2 Int ILI 2 Int:dOPUSTIM, ^TO ' I NE PRINADLEVAT Int, I POKAVEM, ^TO W \TOMSLU^AE ' _ 62 Int.pUSTX M1 = hF1; V1i I M2 = hF2; V2i | KONTRMODELI DLQ ' I , OSNOWYWA@]IESQNA NEPERESEKA@]IHSQ [KALAH F1 = hW1; R1i I F2 = hW2; R2i S KORNQMI x1 I x2,SOOTWETSTWENNO. pOSTROIM NOWU@ [KALU F = hW; Ri, DOBAWIW KORENX x0 K F1 + F2(SM. RISUNOK 1.4). dRUGIMI SLOWAMI, W = fx0g [ W1 [ W2, A xRy WYPOLNQETSQ TOGDAI TOLXKO TOGDA, KOGDA x = x0 ILI xR1y, ILI xR2y DLQ L@BYH x; y 2 W . pOLOVIM,^TO V (p) = V1(p) [ V2(p) DLQ KAVDOJ p 2 VarL, I RASSMOTRIM MODELX M = hF ; Vi.qSNO, ^TO M1 I M2 QWLQ@TSQ POROVDENNYMI PODMODELQMI M.
tOGDA (M; x0) 6j= ',(M; x0) 6j= , A ZNA^IT, (M; x0) 6j= ' _ .oBRATNOE UTWERVDENIE SLEDUET IZ (A6) I (A7).2dOKAZATELXSTWO1.3mODALXNAQ LOGIKAwYRAZITELXNOSTI QZYKA L KLASSI^ESKOJ (ILI INTUICIONISTSKOJ) LOGIKI NEDOSTATO^NO DLQ PREDSTAWLENIQ TAKIH WYSKAZYWANIJ, KAK(A) WOZMOVNO, ^TO WODA ZAKIPAET PRI 70CILI(B) NEOBHODIMO, ^TO WODA ZAKIPAET PRI 70 C,W WIDE KOMBINACII BOLEE PROSTYH WYSKAZYWANIJ. kAK I WYSKAZYWANIE(C) WODA ZAKIPAET PRI 70 C,ONI QWLQ@TSQ \LEMENTARNYMI. pO\TOMU MY NE MOVEM KORREKTNO WYRAZITX W L NIIMPLIKACII ESLI (B), TO (C) I ESLI (C), TO (A), KOTORYE ESTESTWENNO S^ITATXmodalxnaq logika25ISTINNYMI, NI IMPLIKACII ESLI (C), TO (B) I ESLI (A), TO (C), KOTORYE MOVNOPRIZNATX LOVNYMI.pROPOZICIONALXNYJ MODALXNYJ QZYK ML POLU^AETSQ OBOGA]ENIEM QZYKA L NOWOJUNARNOJ SWQZKOJ 2 I DOBAWLENIEM K PRAWILAM POSTROENIQ FORMUL E]E ODNOGO ESLI ' | ML-FORMULA, TO (2') TAKVE QWLQETSQ ML-FORMULOJ.mNOVESTWO WSEH ML-FORMUL OBOZNA^AEM ^EREZ ForML, A MNOVESTWO WSEH PEREMENNYH ML | VarML.
k SOGLA[ENIQM O SOKRA]ENNYH ZAPISQH FORMUL, KOTORYE BYLISFORMULIROWANY W RAZDELE 1.1.1, DOBAWLQEM, ^TO 2 SWQZYWAET FORMULY SILXNEE, ^EM^, _, ! I $. tAK, 2p ! 2q _ 2r QWLQETSQ SOKRA]ENIEM ((2p) ! ((2q) _ (2r))).oPREDELQEM SWQZKU 3 KAK DWOJSTWENNU@ K 2, T.E. POLAGAEM3' = :2:' DLQ WSEH ' 2 ForML;I S^ITAEM, ^TO ONA IMEET TAKU@ VE SWQZYWA@]U@ SILU KAK 2 ILI :.sWQZKI 2 I 3 OBY^NO ^ITA@TSQ NEOBHODIMO, ^TO . .
. I WOZMOVNO, ^TO . . . INAZYWA@TSQ OPERATORAMI NEOBHODIMOSTI I WOZMOVNOSTI, SOOTWETSTWENNO. pO\TOMUWYSKAZYWANIQ (A) I (B) MOVNO ZAPISATX TEPERX KAK 3(C) I 2(C). oDNAKO PODRAZUMEWAEMYJ SMYSL \TIH SWQZOK MOVET BYTX WESXMA RAZLI^NYM. pRIWEDEM ZDESX TOLXKONESKOLXKO WOZMOVNYH SODERVATELXNYH ISTOLKOWANIJ 2 I 3.(i) 2 PONIMAETSQ KAK LOGI^ESKAQ NEOBHODIMOSTX, T.E. KAK NEOBHODIMO S TO^KI ZRENIQ LOGI^ESKIH ZAKONOW, A 3 | KAK LOGI^ESKAQ WOZMOVNOSTX, T.E. NE PROTIWORE^ITLOGI^ESKIM ZAKONAM.(ii) 2 MOVET PONIMATXSQ KAK \PISTEMI^ESKAQ NEOBHODIMOSTX, T.E.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
