Лекционный курс (1109962), страница 3
Текст из файла (страница 3)
NE IMEET MODELI.2dOKAZATELXSTWO1.2iNTUICIONISTSKAQ LOGIKAzAKON ISKL@^ENNOGO TRETXEGO PRIZNAET DOKAZATELXSTWO DIZ_@NKCIJ WIDA ' _ DAVEW TOM SLU^AE, KOGDA NI ', NI NE DOKAZANY (I DAVE, BYTX MOVET, NE DOKAZUEMY). dOKAZATELXSTWA OT PROTIWNOGO, POZWOLQ@]IE DOKAZYWATX SU]ESTWOWANIE OB_EKTA BEZQWNOGO UKAZANIQ SPOSOBA EGO POSTROENIQ, FORMALIZU@TSQ W Cl PRINQTIEM FORMULY::p ! p. tAKOGO RODA DOKAZATELXSTWA IZWESTNY KAK NEKONSTRUKTIWNYE.
cELX@ INTUICIONISTSKOJ LOGIKI QWLQETSQ WYQWLENIE I OPISANIE ZAKONOW KONSTRUKTIWNYHRASSUVDENIJ.bdOKAVEM, ^TO SU]ESTWU@Tp p2 IRRACIONALXNYE ^ISLApa Ip2b, TAKIE ^TO aRACIONALXNO. rASSMOTRIM ^ISLO 2 . wOZMOVNYppp p2 DWA SLU^AQ. (1) 2 RACIONALXNO.tOGDAp p2 MOVNOp WZQTX a = 2, b = 2. (2) 2 IRRACIONALXNO. tOGDA POLOVIM a =2 , b = 2. iMEETSQp p2, ODNAKO, WESXMA SLOVNOE KONSTRUKTIWNOE DOKAZATELXSTWO,POKAZYWA@]EE, ^TO 2 IRRACIONALXNO.pRIMER 1.22pRINIMAQ FUNDAMENTALXNYE SEMANTI^ESKIE POSTULATY KLASSI^ESKOJ LOGIKI |WSQKOE WYSKAZYWANIE NEPREMENNO LIBO ISTINNO, LIBO LOVNO | MY SOWER[ENNO ABSTRAGIROWALISX OT TOGO FAKTA, ^TO W DEJSTWITELXNOSTI MY MOVEM NE ZNATX a prioriQWLQETSQ LI DANNOE UTWERVDENIE ISTINNYM ILI LOVNYM. mY NE ZNAEM, NAPRIMER,SPRAWEDLIWA LI GIPOTEZA gOLXDBAHA, ESTX LI RAZUMNYE SU]ESTWA W SOZWEZDII sTRELXCA, NO WPOLNE WOZMOVNO, ^TO MY UZNAEM OB \TOM W BUDU]EM, POLU^IW KAKU@-TO NOWU@INFORMACI@ OB OKRUVA@]EM NAS MIRE.iNTUICIONISTSKAQ LOGIKA W OTLI^IE OT KLASSI^ESKOJ BERET W RAS^ET \TOT POZNAWATELXWYJ ASPEKT PONQTIQ ISTINY.
pREDSTAWIM SEBE, ^TO NA[E ZNANIE RAZWIWAETSQDISKRETNO NEDETERMINIROWANNO PEREHODQ IZ ODNOGO SOSTOQNIQ W DRUGOE. nAHODQSX WNEKOTORYJ MOMENT W SOSTOQNII INFORMACII x, MY MOVEM S UWERENNOSTX@ SKAZATX,KAKIE FAKTY NAM IZWESTNY, A KAKIE E]E NET. kROME TOGO, MY MOVEM PREDUGADATX,KAKIE SOSTOQNIQ NA[EGO ZNANIQ WOZMOVNY W BUDU]EM y. (kONE^NO, \TO NE OZNA^AET,^TO MY OBQZATELXNO DOSTIGNEM \TIH UROWNEJ ZNANIQ.) rAZUMNO POLAGATX, ^TO, PRIPEREHODE K NOWOMU SOSTOQNI@ ZNANIQ y, WSE PREVNIE FAKTY x SOHRANQ@TSQ, A KROMETOGO, MY MOVEM POLU^ITX I NOWYE.intuicionistskaq logika15eSTESTWENNO POLAGATX, ^TO WSQKOE ATOMARNOE WYSKAZYWANIE, POLU^ENNOE NA [AGE x,ISTINNO W x; ONO OSTANETSQ ISTINNYM I NA WSEH POSLEDU@]IH [AGAH.
wYSKAZYWANIE,KOTOROE NE ISTINNO W x, NE QWLQETSQ, WOOB]E GOWORQ, LOVNYM W x, POSKOLXKU EGOISTINNOSTX MOVET BYTX OBNARUVENA W POSLEDU@]EM.iSTINNOSTX SOSTAWNYH WYSKAZYWANIJ OPREDELQETSQ SLEDU@]IM OBRAZOM: ' ^ ISTINNA W x, ESLI I ', I ISTINNY W x; ' _ ISTINNA W x, ESLI ' ILI ISTINNA W x; ' ! ISTINNA W x, ESLI WO WSQKIJ WOZMOVNYJ POSLEDU@]IJ MOMENT y, W ^ASTNOSTI I W SAM MOMENT x, ' ISTINNA W y, TOLXKO ESLI W y ISTINNA . ? ISTINNOJ NE QWLQETSQ NIKOGDA.iZ \TOGO OPREDELENIQ SLEDUET, ^TO OTRICANIE :' = ' ! ? ISTINNNO W x, ESLI 'NE QWLQETSQ ISTINNOJ NI W KAKOJ WOZMOVNYJ POSLEDU@]IJ MOMENT.
wYSKAZYWANIE 'MOVET PONIMATXSQ KAK LOVNOE W x, ESLI :' ISTINNO W x.wSE PODSTANOWO^NYE PRIMERY AKSIOM (A1){(A9) OKAZYWA@TSQ ISTINNYMI WO WSEHMYSLIMYH MOMENTAH, ^TO NELXZQ SKAZATX O (A10). w SAMOM DELE, ESLI WYSKAZYWANIE' NE ISTINNO W x, NO STANOWITSQ ISTINNYM W NEKOTORYJ POSLEDU@]IJ MOMENT y, TO:' NE ISTINNO W x, A POTOMU I ' _ :' ISTINNOJ W x NE QWLQETSQ.1.2.1.2.1{KALY I MODELI kRIPKEkAK I W RAZDELE 1.1.1, FIKSIRUEM PROPOZICIONALXNYJ QZYK L SO SWQZKAMI ^, _, ! IKONSTANTOJ ?; ISPOLXZUEM I WSE WWEDENNYE SOKRA]ENIQ. oTPRAWLQQSX OT NEFORMALXNOJ INTERPRETACII IZ PREDYDU]EGO RAZDELA, DADIM TO^NOE OPREDELENIE INTUICIONISTSKOJ MODELI DLQ L.iNTUICIONISTSKAQ [KALA kRIPKE | \TO PARA F = hW; Ri, SOSTOQ]AQ IZ NEPUSTOGO MNOVESTWA W I BINARNOGO OTNO[ENIQ R NA W , UDOWLETWORQ@]EGO SLEDU@]IMUSLOWIQM DLQ WSEH x; y; z 2 W :xRx(REFLEKSIWNOSTX),xRy ^ yRz ! xRz(TRANZITIWNOSTX),xRy ^ yRx ! x = y (ANTISIMMETRI^NOSTX).tAKOE OTNO[ENIE NAZYWAETSQ OTNO[ENIEM ^ASTI^NOGO PORQDKA NA W .
|LEMENTY WNAZYWA@TSQ TO^KAMI [KALY F , A xRy ^ITAETSQ y DOSTIVIMA IZ x ILI x WIDITy.oCENKA QZYKA L W INTUICIONISTSKOJ [KALE F = hW; Ri | \TO OTOBRAVENIE V ,SOPOSTAWLQ@]EE KAVDOJ PEREMENNOJ p 2 VarL NEKOTOROE (WOZMOVNO PUSTOE) PODMNOVESTWO V (p) W , T.^. DLQ L@BYH x 2 V (p) I y 2 W IZ xRy SLEDUET y 2 V (p).glawa logika wyskazywanijpODMNOVESTWA W , UDOWLETWORQ@]IE \TOMU USLOWI@, NAZYWA@TSQ NASLEDSTWENNYMI(ILI WERHNIMI KONUSAMI). mNOVESTWO WSEH NASLEDSTWENNYH PODMNOVESTW W OBOZNA^AEM ^EREZ UpW .
tAKIM OBRAZOM, OCENKA W [KALE hW; Ri | \TO FUNKCIQ V IZ VarLW UpW .iNTUICIONISTSKAQ MODELX kRIPKE QZYKA L | \TO PARA M = hF ; Vi, GDE F |INTUICIONISTSKAQ [KALA, A V | OCENKA NA NEJ.nA SODERVATELXNOM UROWNE TO^KI [KALY F = hW; Ri MODELI M = hF ; Vi PREDSTAWLQ@T SOSTOQNIQ INFORMACII; ESLI MY NAHODIMSQ W SOSTOQNII x I MOVEM W DALXNEJ[EM OKAZATXSQ W SOSTOQNII y, TO \TO FORMALIZUETSQ TEM, ^TO WYPOLNQETSQ xRy.aTOMARNOE WYSKAZYWANIE p S^ITAETSQ ISTINNYM W x, ESLI x 2 V (p). pOSKOLXKU V (p)NASLEDSTWENNO, WSE ATOMARNYE WYSKAZYWANIQ ISTINNYE W NEKOTOROM SOSTOQNII OSTA@TSQ ISTINNYMI I WO WSEH WOZMOVNYH POSLEDU@]IH SOSTOQNIQH.pUSTX M = hF ; Vi NEKOTORAQ INTUICIONISTSKAQ MODELX kRIPKE I x | TO^KA[KALY F = hW; Ri.
iNDUKCIEJ PO POSTROENI@ FORMULY ' OPREDELQEM OTNO[ENIE(M; x) j= ', KOTOROE ^ITAETSQ ' ISTINNA W x MODELI M:(M; x) j= p() x 2 V (p);(M; x) j= ^ () (M; x) j= I (M; x) j= ;(M; x) j= _ () (M; x) j= ILI (M; x) j= ;(M; x) j= ! () DLQ WSEH y 2 W , ESLI xRy I(M; y) j= , TO (M; y) j= ;(M; x) 6j= ?.iZ \TOGO OPREDELENIQ SLEDUET, ^TO(M; x) j= : () DLQ WSEH y 2 W , T.^. xRy, (M; y) 6j= .eSLI PONQTNO, O KAKOJ MODELI M IDET RE^X, PI[EM x j= ' WMESTO (M; x) j= '. mNOVESTWO ISTINNOSTI ' W M = hF ; Vi, T.E. MNOVESTWO fx : x j= 'g, BUDEM OBOZNA^ATXV (').zAMETIM, ^TO INTUICIONISTSKAQ MODELX M = hF ; Vi NA [KALE F , SODERVA]EJODNU-EDINSTWENNU@ TO^KU, SKAVEM x, QWLQETSQ PO SU]ESTWU KLASSI^ESKOJ MODELX@N = fp 2 VarL : x 2 V (p)g;POSKOLXKU (M; x) j= ' TOGDA I TOLXKO TOGDA, KOGDA N j= ' DLQ L@BOJ FORMULY '.pREDLOVENIE 1.23 dLQ WSQKIH INTUICIONISTSKOJ MODELI NA [KALE F = hW; Ri,FORMULY ' I TO^EK x; y 2 W IZ TOGO, ^TO x j= ' I xRy, SLEDUET, ^TO y j= '.dOKAZATELXSTWO rASSUVDENIE INDUKCIEJ PO POSTROENI@ ' OSTAWLQEM ^ITATEL@ WKA^ESTWE UPRAVNENIQ.2161.1.2.intuicionistskaq logika17bpp!?p _ (p ! ?)6pp!?a p _ (p ! ?)rIS.
1.1:pREDLOVENIE 1.23 GOWORIT W TOM, ^TO WSQKOE MNOVESTWO WIDA x 2 V (') QWLQETSQNASLEDSTWENNYM. iZ NEGO MGNOWENNO SLEDUET, ^TO MNOVESTWO TO^EK, W KOTORYH ' NEISTINNO, QWLQETSQ NIVNIM KONUSOM, TO ESTX IZ USLOWIJ x 6j= ' I yRx SLEDUET y 6j= '.gOWORIM, ^TO FORMULA ' WYPOLNQETSQ W MODELI M = hF ; Vi, ESLI x j= ' DLQNEKOTOROJ TO^KI x IZ F .
fORMULA ' ISTINNA W M, ESLI x j= ' DLQ WSQKOJ x IZ F ;PI[EM W \TOM SLU^AE M j= '. eSLI ' NE QWLQETSQ ISTINNOJ W M, TO MY GOWORIM, ^TO 'OPROWERGAETSQ W M ILI M QWLQETSQ KONTRMODELX@ DLQ ', I PI[EM M 6j= '. fORMULA' NAZYWAETSQ OB]EZNA^IMOJ W [KALE F , SIMWOLI^ESKI F j= ', ESLI ' ISTINNA WO WSEHMODELQH, OSNOWANNYH NA F ; W PROTIWNOM SLU^AE GOWORIM, ^TO ' OPROWERGAETSQ W F ,I PI[EM F 6j= '.eSLI WSQKAQ FORMULA I\ MNOVESTWA ISTINNA W TO^KE x MODELI M, TO MY PI[EM(M; x) j= ILI PROSTO x j= . zAPISI M j= I F j= OZNA^A@T, ^TO WSE FORMULYIZ ISTINNY W M I ISTINNY W F , SOOTWETSTWENNO.dOLVNO BYTX QSNO, ^TO ESLI MY HOTIM POSTROITX KONTRMODELX DLQ FORMULY ' NA[KALE F , TO OPREDELQTX OCENKU V , OPROWERGA@]U@ ' NA F , DOSTATO^NO TOLXKO DLQPEREMENNYH '; OCENKA V DLQ DRUGIH PEREMENNYH NE OKAZYWAET NIKAKOGO WLIQNIQ NAISTINNOSTX ' W TO^KAH F .mY BUDEM IZOBRAVATX INTUICIONISTSKIE [KALY W WIDE RISUNKOW, NA KOTORYHTO^KI IZOBRAVA@TSQ KRUVKAMI , A STRELKA IZ TO^KI x W TO^KU y OZNA^AET xRy.dLQ QSNOSTI MY NE BUDEM RISOWATX STRELKI, KOTOROE ODNOZNA^NO WOSSTANAWLIWA@TSQPO SWOJSTWAM REFLEKSIWNOSTI I TRANZITIWNOSTI.
iZOBRAVAQ NA RISUNKAH MODELI,MY BUDEM INOGDA PISATX FORMULY OKOLO TO^EK: SLEWA OT TO^KI x PI[EM FORMULY,KOTORYE W x ISTINNY, A SPRAWA | KOTORYE LOVNY.pOLOVIM, ^TO F = hW; Ri | \TO [KALA, W KOTOROJ W = fa; bg, R =fha; ai ; ha; bi ; hb; big I PUSTX V (p) = fbg I V (q) = fa; bg DLQ WSEH q 2 VarL, OTLI^NYHOT p. tOGDA FORMULA p _ (p ! ?) ISTINNA W b I NE QWLQETSQ ISTINNOJ W a W MODELIM = hF ; Vi.
|TA SITUACIQ IZOBRAVENA GRAFI^ESKI NA RISUNKE 1.1. tAK, p _ (p ! ?) IWYPOLNQETSQ I OPROWERGAETSQ W F . fORMULA ((p ! ?) ! ?) ! p TOVE OPROWERGAETSQW M, POSKOLXKU a j= (p ! ?) ! ? I a 6j= p.pRIMER 1.24glawa logika wyskazywanijpRIMER 1.25 fORMULA p ! ((p ! ?) ! ?) ISTINNA WO WSEH INTUICIONISTSKIH[KALAH, w SAMOM DELE, DOPUSTIM PROTIWNOE.
tOGDA SU]ESTWUET TAKAQ MODELX NA [KALEF = hW; Ri, ^TO x j= p I x 6j= (p ! ?) ! ? DLQ NEKOTOROJ TO^KI x 2 W , I POTOMUSU]ESTWUET y 2 W , T.^. xRy I y j= p ! ?. nO WOPREKI \TOMU PO OPREDELENI@ OCENKIMY DOLVNY IMETX TOGDA y j= p, OTKUDA y 6j= p ! ?.oPREDELIM INTUICIONISTSKU@ PROPOZICIONALXNU@ LOGIKU Int W QZYKE L KAK MNOVESTWO WSEH L-FORMUL, OB]EZNA^IMYH WO WSEH INTUICIONISTSKIH [KALAH, TO ESTXInt = f' 2 ForL : F j= ' DLQ WSEH [KAL Fg:pOSKOLXKU KLASSI^ESKAQ TOVDESTWENNAQ ISTINNOSTX ESTX NE ^TO INOE KAK ISTINNOSTXW ODNOTO^E^NOJ INTUICIONISTSKOJ [KALE, MY POLU^AEM WKL@^ENIEInt Cl:a POSKOLXKU p _:p PRINADLEVIT Cl, NO NE Int, \TO WKL@^ENIE QWLQETSQ SOBSTWENNYM.181.1.2.2sISTEMY hINTIKKImY OPREDELILI I KLASSI^ESKU@, I INTUICIONISTSKU@ LOGIKI KAK MNOVESTWA FORMUL, ISTINNYH W NEKOTORYH [KALAH.
oDNAKO Cl | \TO MNOVESTWO FORMUL, ISTINNYH W ODNOJ KONE^NOJ [KALE, W TO WREMQ KAK Int SOSTOIT IZ FORMUL, ISTINNYH WOWSEH [KALAH, WKL@^AQ I BESKONE^NYE. dRUGIMI SLOWAMI, ^TOBY OTWETITX NA WOPROS' 2 Cl?, DOSTATO^NO WYPOLNITX ZAWEDOMO KONE^NOE WY^ISLENIE (SOSTOQ]EE, NAPRIMER, W WYPISYWANII TABLICY ISTINNOSTI DLQ ', TO ESTX | PEREBORE WSEH MODELEJ STO^NOSTX@ DO PEREMENNYH, NE WHODQ]IH W '), A DLQ POLOVITELXNOGO OTWETA NA WOPROS' 2 Int? MY DOLVNY PREDSTAWITX DOKAZATELXSTWO ISTINNOSTI ' WO WSEH [KALAH.w \TOM RAZDELE MY RAZOWXEM APPARAT SEMANTI^ESKIH TABLIC DLQ INTUICIONISTSKOJ LOGIKI I POKAVEM S EGO POMO]X@, ^TO DLQ KAVDOJ FORMULY ' 62 Int MOVNOPOSTROITX KONE^NU@ KONTRMODELX, SODERVA]U@ NE BOLEE 2jSub'j TO^EK2. tAKIM OBRAZOM, ISTINNOSTX ' WO WSEH [KALAH WPOLNE OPREDELQETSQ EE ISTINNOSTX@ W [KALAHMO]NOSTI 2jSub'j.wNOWX NA^NEM S PRIMEROW.pRIMER 1.26 dOPUSTIM, NAS INTERESUET, PRINADLEVIT LI Int FORMULA' = (p ! q) _ (q ! p):s \TOJ CELX@ POPROBUEM POSTROITX KONTRMODELX \TOJ FORMULY, ISPOLXZUQ TU VEIDE@, KOTORU@ MY PRIMENQLI W RAZDELE 1.1.2 DLQ NAHOVDENIQ KONTRMODELEJ DLQ FORMUL, NE PRINADLEVA]IH Cl.zDESX I NIVE X OBOZNA^AET MO]NOSTX MNOVESTWA X pOD MO]NOSTX@ [KALY MODELI I T PPONIMAEM MO]NOSTX NOSITELQ T E MNOVESTWA TO^EK2jj.,.
..,. .1.2.intuicionistskaq logikat0(p ! q) _ (q ! p)p!qq!pt1p q@@R@(a)t2q p19t1@I@t2t@0(b)rIS. 1.2:pREVDE WSEGO, OBRAZUEM TABLICU t0, ZANESQ ' W EE PRAWU@ ^ASTX, POKAZYWAQ TEMSAMYM, ^TO MY HOTIM, ^TOBY \TA FORMULA BYLA NE ISTINNOJ W TO^KE t0 STROIMOJMODELI. pOSKOLXKU DIZ_@NKCIQ NE ISTINNA W TO^KE x TOGDA I TOLXKO TOGDA, KOGDAW x NE ISTINNY OBA EE DIZ_@NKTIWNYH ^LENA, MY DOLVNY ZANESTI W PRAWU@ ^ASTXt0 E]E DWE FORMULY: p ! q I q ! p. iMPLIKACIQ NE ISTINNA W TO^KE x TOGDA ITOLXKO TOGDA, KOGDA SU]ESTWUET TO^KA y, DOSTIVIMAQ IZ x, W KOTOROJ POSYLKA \TOJIMPLIKACII ISTINNA, A ZAKL@^ENIE | NET (y MOVET, W ^ASTNOSTI, SOWPADATX S x).pO\TOMU OBRAZUEM DWE NOWYH TABLICY t1 I t2, DOSTIVIMYE IZ t0: t1 SODERVIT p WLEWOJ ^ASTI, q | W PRAWOJ, A t2, NAOBOROT, p | W PRAWOJ ^ASTI, q | W LEWOJ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
