Документ взят из кэша поисковой машины. Адрес оригинального документа : http://www.intsys.msu.ru/staff/mironov/godel.pdf Дата изменения: Wed Dec 5 00:14:17 2007 Дата индексирования: Mon Oct 1 21:09:24 2012 Кодировка:

dOKAZATELXSTWO TEOREMY gEDELQ O NEPOLNOTE, OSNOWANNOE NA PONQTIQH FUNKCIONALXNOGO PROGRAMMIROWANIQ

a m mIRONOW
. .

aNNOTACIQ w STATXE IZLAGAETSQ NOWOE DOKAZATELXSTWO TEOREMY gEDELQ O NEPOLNOTE FORMALXNYH LOGI^ESKIH SISTEM, OSNOWANNOE NA PONQTIQH FUNKCIONALXNOGO PROGRAMMIROWANIQ. wWEDENIE tEOREMA gEDELQ O NEPOLNOTE FORMALXNYH LOGIKO-MATEMATI^ESKIH SISTEM (NAZYWAEMAQNIVE PROSTOTEOREMOJgEDELQ) ZANIMAET CENTRALXNOE POLOVENIE NETOLXKO W MATEMATI^ESKOJ LOGIKE, NO I WO WSEM SOWREMENNOM ESTESTWOZNANII. w SWOEJ ISHODNOJ FORMULIROWKE (SM. 1]) TEOREMA gEDELQ OTNOSITSQ K FORMALXNYM SISTEMAM, WKOTORYH DOPUSKAETSQ WOZMOVNOSTX INTERPRETACII ARIFMETIKI pEANO (SM. 2], 3]), I UTWERVDAET, ^TO ESLI FORMALXNAQ SISTEMA QWLQETSQ NEPROTIWORE^IWOJ, I OBLADAET WOZMOVNOSTQMI DLQ ADEKWATNOGO WYRAVENIQ W NEJ UTWERVDENIJ ARIFMETIKI pEANO TO \TA TEORIQ NE QWLQETSQ POLNOJ, T.E. NE POZWOLQET POSTROITX WYWOD WSEH ISTINNYH UTWERVDENIJ. w \TOJ FORMULIROWKE EE DOKAZATELXSTWO OSNOWANO NA NUMERACII FORMUL I DOKAZATELXSTW NATURALXNYMI ^ISLAMI, IIMEET WYSOKU@ SLOVNOSTX. oDNAKO, ESLI RAS IRITX SINTAKSIS FORMALXNOJARIFMETIKI, I RASSMATRIWATX TAKIE FORMALXNYE SISTEMY, WKOTORYH MOVNO WYRAVATX SWOJSTWA SIMWOLXNYH STROK, TO DOKAZATELXSTWO NEPOLNOTY TAKIH FORMALXNYH SISTEM MOVET BYTX SU]ESTWENNO UPRO]ENO. oSNOWNAQIDEQ IZLAGAEMOGO W NASTOQ]EM TEKSTE DOKAZATELXSTWA NEPOLNOTY TAKIH SISTEM ZAKL@^AETSQ W MODELIROWANII WY^ISLITELXNYH PROCESSOW, SWQZANNYH S PONQTIEM LOGI^ESKOGO WYWODA, FUNKCIONALXNYMI PROGRAMMAMI, I ESTESTWENNOM PREDSTAWLENII OPISANIJ I SWOJSTW FUNKCIONALXNYH PROGRAMM LOGI^ESKIMI FORMULAMI.

1

2

aKSIOMATI^ESKIJ METOD sOGLASNO OB]EPRINQTOMU MNENI@, NAIBOLEE PRAWILXNYJ SPOSOB ORGANIZACII NAU^NYH ZNANIJ ZAKL@^AETSQ
1

WPREDSTAWLENII IH W WIDELOGI^ESKIH SLEDSTWIJ, WYWEDENNYH NA OSNOWE FORMALXNYH PRAWIL WYWODA IZ NEKOTORYH ISHODNYH UTWERVDENIJ, ISTINNOSTX KOTORYH NE PODWERGAETSQ SOMNENI@. dANNYJ SPOSOB ORGANIZACII ZNANIJ NAIBOLEE PREDPO^TITELEN POSLEDU@]IM PRI^INAM. 1. nALI^IE U NEKOTOROJ SOWOKUPNOSTI ZNANIJ HOROEJ LOGI^ESKOJ STRUKTURY SU]ESTWENNO UPRO]AET OWLADENIE \TIMI ZNANIQMI. 2. lOGI^ESKAQ STRUKTURIZACIQ ZNANIJ OBLEG^AET IH OBRABOTKUI SU]ESTWENNOPOWY AET EE OB_EKTIWNOSTX I NADEVNOSTX, POSKOLXKU TAKAQ OBRABOTKA MOVET BYTX PROWEDENA TOLXKO POSREDSTWOM FORMALXNYH OPERACIJ NAD SIMWOLXNYMI STROKAMI, BEZ PRIWLE^ENIQ RASPLYW^ATO{NEFORMALXNOJI SUB_EKTIWNOJ INTERPRETACII PONQTIJ, WYRAVAEMYH \TIMI STROKAMI. kROMETOGO, SWEDENIE ZADA^I OBRABOTKI ZNANIJ K ZADA^E WYPOLNENIQ OPERACIJ NAD STROKAMI OBESPE^IWAET WOZMOVNOSTX AWTOMATIZACII OBRABOTKI ZNANIJ. 3. pOSKOLXKU KRITERIEM ISTINNOSTI LOGI^ESKI STRUKTURIROWANNYH ZNANIJ QWLQETSQ IH SOOTWETSTWIE NEKOTORYM SINTAKSI^ESKIM PRAWILAM, TOLOGI^ESKAQ STRUKTURIZACIQ ZNANIJ OBLEG^AET PROWERKU O IBO^NOSTI W RASSUVDENIQH, WKOTORYH ISPOLXZU@TSQ \TI ZNANIQ, POSKOLXKUONA POZWOLQET SWESTI ZADA^U NAHOVDENIQ O IBOK W RASSUVDENIQH K ZADA^E PROWERKI PRAWILXNOSTI ISPOLXZOWANIQ SINTAKSI^ESKIH PRAWIL PRI FORMALXNYH OPERACIQH NAD SIMWOLXNYMI STROKAMI. 4. pREDSTAWLENIE SOWOKUPNOSTI ZNANIJ W WIDELOGI^ESKIH SLEDSTWIJ IZ NEKOTORYH ISHODNYH PRINCIPOW QWLQETSQ INSTRUMENTOMSINTEZA NOWYH ZNANIJ, POSKOLXKU PROCESS POLU^ENIQ NOWYH ZNANIJ MOVET IMETX WID FORMALXNOJKOMBINACII UVEUSTANOWLENNYH UTWERVDENIJ S ISPOLXZOWANIEM PODHODQ]IH PRAWIL LOGI^ESKOGO WYWODA. nAIBOLEE PLODOTWORNYE REZULXTATY REALIZACIQ DANNOJ TO^KI ZRENIQ PRINESLA W MATEMATIKE, GDEUDALOSX PREDSTAWITX WSE POLU^ENNNYE REZULXTATY W WIDE LOGI^ESKIH SLEDSTWIJ IZ NE BOLX OGO ^ISLA ISHODNYH PROSTYH UTWERVDENIJ, NAZYWAEMYH AKSIOMAMI. mETODORGANIZACII ZNANIJ W WIDE LOGI^ESKIH SLEDSTWIJ IZ AKSIOM POLU^IL NAZWANIE AKSIOMATI^ESKOGOMETODA.


aKSIOMATI^ESKIJ METOD STAL ISTO^NIKOM BURNOGO RAZWITIQ MNOGIH OBLASTEJ MATEMATIKI, I OBOGATIL IH NOWYMI PLODOTWORNYMI PODHODAMI I GLUBOKIMI REZULXTATAMI. nAIBOLEE QRKO\TO PROQWILOSX W ALGEBRE, KOTORAQ, BLAGODARQ ISPOLXZOWANI@ W NEJ AKSIOMATI^ESKOGO METODA, ZANQLA CENTRALXNOE POLOVENIE W MATEMATIKE. nEKOTOROE WREMQ SU]ESTWOWALO UBEVDENIE, ^TO NA BAZE AKSIOMATI^ESKOGO METODA MOVNO POSTROITX WS@ MATEMATIKU, TO ESTX WS@ SOWOKUPNOSTX ISTINNYH MATEMATI^ESKIH UTWERVDENIJ MOVNOPREDSTAWITX W WIDE LOGI^ESKIH SLEDSTWIJ NEKOTORYH AKSIOM, ^TOPOZWOLIT SWESTI ZADA^U POLU^ENIQ NOWYH MATEMATI^ESKIH ZNANIJ K WYPOLNENI@ FORMALXNYH OPERACIJ NAD SIMWOLXNYMI STROKAMI PO ZARANEE ZADANNYM PRAWILAM. oDNAKO, KAK BYLO USTANOWLENOW 1931 GODU gEDELEM, NIKAKAQFORMALXNAQSISTEMA (T.E. SOWOKUPNOSTX AKSIOM I PRAWIL WYWODA) NE QWLQETSQ POLNOJ, T.E. NEMOVET POZWOLITX POLU^ITX TAKIM MEHANI^ESKIM SPOSOBOMWS@ SOWOKUPNOSTX ISTINNYH MATEMATI^ESKIH UTWERVDENIJ. w ^ASTNOSTI, UTWERVDENIE O TOM, ^TODANNAQFORMALXNAQ SISTEMA NEPROTIWORE^IWA (T.E. WNEJ NEWOZMOVNOWYWESTI DWUH WZAIMOISKL@^A@]IH PREDLOVENIJ) NEWOZMOVNO OBOSNOWATX METODAMI DANNOJFORMALXNOJ SISTEMY. tEOREMA gEDELQ QWLQETSQ UBEDITELXNYM PODTWERVDENIEM TEZISA O TOM, ^TO GLAWNYJ ISTO^NIK RAZWITIQ MATEMATIKI NAHODITSQ ZA EE PREDELAMI. nAIBOLEE SU]ESTWENNYE IZMENENIQ W MATEMATIKE, PRIWODQ]IE K WOZNIKNOWENI@ NOWYH, BOLEE SILXNYH KONCEPCIJ I SWQZANNYH S NIMI FORMALXNYH SISTEM, NEWOZMOVNY W RAMKAH FIKSIROWANNOJ SISTEMY PONQTIJ, ONI MOGUT PROIZOJTI TOLXKO W REZULXTATE WZAIMOPRONIKNOWENIQ I WZAIMOWLIQNIQ SAMYH RAZNYH OBLASTEJ NAU^NOJ, KULXTURNOJI PRAKTI^ESKOJDEQTELXNOSTI. wSQKAQ PRINCIPIALXNONOWAQ I BOLEE SILXNAQ FORMALXNAQ SISTEMA MOVET BYTX TOLXKO IZOBRETENIEM: SOGLASNO TEOREME gEDELQ, NIKAKIM DRUGIM OBRAZOMEEPOLU^ITX NEWOZMOVNO.

BYTX NEOPREDELENY DLQ NEKOTORYH ZNA^ENIJ SWOIH ARGUMENTOW. |TI FUNKCII DELQTSQ NA DWA KLASSA: BAZOWYE FUNKCII, I FUNKCII, OPREDELQEMYE PRI POMO]I FUNKCIONALXNYH PROGRAMM.
3.2 bAZOWYE FUNKCII

sOWOKUPNOSTX BAZOWYH FUNKCIJ IMEET SLEDU@]IJ WID.
1.

dLQ KAVDOJTROJKI (u v w)
if then else

if then else S3 ! S

:

8 v ESLI u SOSTOIT IZ < (u v w) def : = ODNOGO SIMWOLA 1 w INA^E
u?v:w

2 S3

nIVE ZNAKOSO^ETANIE if then else(u v w) BUDET SOKRA]ENNO ZAPISYWATXSQ W WIDE
2.
head S ! S

|TA FUNKCIQ OPREDELENA TOLXKONA NEPUSTYH STROKAH, ONA SOPOSTAWLQET KAVDOJ NEPUSTOJ STROKE u STROKU, SOSTOQ]U@ IZ PERWOGO SIMWOLA STROKI u.
tail S ! S

:

3.

|TA FUNKCIQ TOVE OPREDELENA TOLXKO NA NEPUSTYH STROKAH. oNA SOPOSTAWLQET KAVDOJNEPUSTOJ STROKE u STROKU, POLU^AEMU@ IZ u UDALENIEM PERWOGO SIMWOLA.
conc S2 ! S

:

4.

3

sTROKI I FUNKCII NA NIH
5.

wSE OB_EKTY, RASSMATRIWAEMYE W MATEMATIKE, MOVNO IZOBRAZITX SIMWOLXNYMI STROKAMI (KOTORYEMYNIVE BUDEM NAZYWATX PROSTO STROKAMI), IOPERACII NA OB_EKTAH MOVNO PREDSTAWITX W WIDE FUNKCIJ NA STROKAH, IZOBRAVA@]IH \TI OB_EKTY. mY PREDPOLAGAEM, ^TO ZADANO NEKOTOROE KONE^NOE MNOVESTWO C, \LEMENTY KOTOROGO NAZYWA@TSQ SIMWOLAMI. w C WHODQT BUKWY, CIFRY, SKOBKI, INEKOTORYE DRUGIE SIMWOLY. sTROKOJ NAZYWAETSQ PROIZWOLXNAQKONE^NAQPOSLEDOWATELXNOSTX SIMWOLOWIZ C. sOWOKUPNOSTX WSEHSTROK OBOZNA^AETSQ SIMWOLOM S. sU]ESTWUET PUSTAQ STROKA, ONA NESODERVIT NI ODNOGO SIMWOLA. wSE FUNKCII NA STROKAH, RASSMATRIWAEMYE W NASTOQ]EJ STATXE, QWLQ@TSQ ^ASTI^NYMI, T.E. ONI MOGUT
2

3.1 sIMWOLXNYE STROKI

dLQ KAVDOJ PARY (u v) 2 S2 STROKA conc(u v) PREDSTAWLQET SOBOJ KONKATENACI@ STROK u I v, T.E. STROKU a1 ::: an b1 ::: bm , ESLI u I v IME@T WID SOOTWETSTWENNO a1 ::: an I b1 ::: bm , GDE m n > 0, I STROKU v, ESLI STROKA u PUSTA, STROKU u, ESLI STROKA v PUSTA.
eq S2 ! S

:

dLQ KAVDOJ PARY (u v)
eq

:

2 S2

(u v) def =

1 ESLI u = v 0 INA^E

3.3 sTRUKTURIROWANNYE STROKI

nEKOTORYE STROKI MY BUDEM NAZYWATX STRUKTURIROWANNYMI. pONQTIE STRUKTURIROWANNOJ STROKI (ss) OPREDELQETSQ INDUKTIWNO. pRI OPREDELENII PONQTIQ ss ISPOLXZUETSQ WSPOMOGATELXNOE PONQTIE ATOMA. aTOMOM NAZYWAETSQ PROIZWOLXNAQ STROKA, NESODERVA]AQFIGURNYH SKOBOK (T.E. SIMWOLOW f I g). kAVDYJ ATOM QWLQETSQ ss.


x1 ::: xn { SPISOKRAZLI^NYHPEREMENNYH, I e1 ::: en { SPISOKWYRAVENIJ. fu1 ::: ung (POLU^AEMAQ PRIPISYWANIEM K KONKATENACII STROK dLQ KAVDOJPODSTANOWKI WIDA (2) I KAVDOGO WYRAu1 ::: un SKOBKI f SLEWA I SKOBKI g SPRAWA) QWLQ- VENIQ e ZNAKOSO^ETANIE e OBOZNA^AET WYRAVENIE, POLU^AEMOE IZ e ZAMENOJ DLQ KAVDOGO i 2 f1 ::: ng KAVETSQ ss. DOGOWHOVDENIQ PEREMENNOJ xi W e NA WYRAVENIE ei . wCELQH UDOBSTWA ^TENIQ, WYRAVENIE WIDA 3.4 pEREMENNYE, KONSTANTY, WYRAVENIQ I PODSTANOWKI ffsubstgfx1 ::: xn gfe1 ::: engge ss WIDA ffvargug (GDE var { STROKA IZ TR
eSLI STROKI u1 ::: un (GDE n 1) QWLQ@TSQ ss, TO STROKA

n

ss

1

n

QWLQETSQ WYRAVENIEM. fp (4) QWLQETSQ OPREDELENIEM FUNKCIJ, SOOTWETSTWU@]IH fs f1 ::: fn. mY BUDEM PREDPOLAGATX, ^TO w CELQH UDOBSTWA ^TENIQ, WYRAVENIE WIDA (1) MY ARGUMENTAMI I ZNA^ENIQMI WSEH RASSMATRIWAEMYH FUNKBUDEM ZAPISYWATX ZNAKOSO^ETANIEM CIJ QWLQ@TSQ ss. dLQ KAVDOGO i =1 ::: n MY BUDEM OBOZNA^ATX FUNKCI@, SOOTWETSTWU@]U@ fs fi , TEM VE f (e1 ::: en) SIMWOLOM fi . fUNKCII f1 ::: fn , WY^ISLQ@TSQ STANDARTNOJ REKURSIEJ: ESLI TRE BUETSQ WY^ISLITX ZNA^EpODSTANOWKA { \TOss WIDA NIE FUNKCII fi NA KORTEVE ARGUMENTOW (u1 ::: uk ), TO ffsubstgfx1 ::: xn gfe1 ::: en gg (2) DLQ \TOGO WY^ISLQETSQ ZNA^ENIE WYRAVENIQ ei ( u1 =xi1 ::: uk =xik ) (6) GDE
i i i

ffexprgfe1

::: en

g

(1)

f1 ::: fn

(5)

3


IISKOMOE ZNA^ENI@ fi (u1 ::: uk ) PO OPREDELENI@ POLAGAETSQ RAWNYM ZNA^ENI@ WYRAVENIQ (6). wY^ISLENIE ZNA^ENIQ WYRAVENIQ (6) PROISHODIT PO SLEDU@]EMU REKURSIWNOMU PRAWILU. eSLI (6) IMEET WID u, TOEGO ZNA^ENIEM QWLQETSQ
i

1. fp, OPREDELQ@]AQ FUNKCI@ rev, KOTORAQ PREOBRAZUET KAVDU@ STROKU W STROKU, ZAPISANNU@ W OBRATNOMPORQDKE (T.E. rev(a1 ::: an )= an ::: a1 ): rev(x)= eq(x ") ? " : conc(rev(tail(x)) head(x)) 2. wSLEDU@]EM PRIMERE MY PREDPOLAGAEM, ^TOMNOVESTWO SIMWOLOW C LINEJNO UPORQDO^ENO, I IMEETSQ DOPOLNITELXNAQ BAZOWAQ FUNKCIQ leq OT DWUH ARGUMENTOW, KOTORAQ OPREDELENA TOLXKONA STROKAH IZ ODNOGO SIMWOLA, I PRINIMAET NA PARE SWOIH ARGUMENTOW ZNA^E1, ESLI PERWYJ ARGUMENT NE PREWOSHODIT WTOROGO, I { 0- WPROTIWNOMSLU^AE. nIVE PREDSTAWLENA fp, OPREDELQ@]AQ FUNKCI@ sort. dANNAQ FUNKCIQ PREOBRAZUET KAVDU@ STROKU x WSTROKU sort(x), OBLADA@]U@ SLEDU@]IMI SWOJSTWAMI: KOMPONENTY STROKI sort(x) OBRAZU@T NEUBYWA@]U@ POSLEDOWATELXNOSTX, I KAVDYJ SIMWOL WHODIT W STROKU sort(x) STOLXKOVE RAZ, SKOLXKORAZ ONWHODIT W x T.E. FUNKCIQ sort OSU]ESTWLQET SORTIROWKU SWOEGO ARGUMENTA.
{

u.

eSLI WYRAVENIE (6) IMEET WID
f (e1 ::: em ) GDE f { BAZOWYJ fs, OTLI^NYJ OT
0 0

TO WY^ISLQ@TSQ ZNA^ENIQ WYRAVENIJ e1 ::: em , I ZNA^ENIE WYRAVENIQ (6) POLAGAETSQ RAWNYM ZNA^ENI@ FUNKCII f NA SPISKEZNA^ENIJ WYRAVENIJ
0 0

if_then_else

,

e1 ::: em .
0 0

NIE

eSLI WYRAVENIE (6) IMEET WID
e1 ? e2 : e
0 0 0

3
0

TO SNA^ALA WY^ISLQETSQ ZNA^ENIE WYRAVENIQ e1 , I { ESLI ONO RAWNO STROKE IZ ODNOGO SIMWOLA 1, TO WY^ISLQETSQ ZNA^ENIE WYRAVENIQ e2 , { INA^E - WY^ISLQETSQ ZNA^ENIE WYRAVENIQ e3 I ZNA^ENIE WYRAVENIQ (6) POLAGAETSQ RAWNYM ZNA^ENI@ e2 ILI e3 SOOTWETSTWENNO. eSLI WYRAVENIE (6) IMEET WID
0 0 0 0

fj (e1 ::: ek )
0 0

j

GDE fs fj PRINADLEVIT SPISKU (5), TO ZNA^ENIE WYRAVENIQ (6) PO OPREDELENI@ RAWNO ZNA^ENI@ WYRAVENIQ
ej (e1 =xj 1 ::: ek =xjk )
0 0

j

j

KOTOROE WY^ISLQETSQ POTOMU VE PRAWILU, POKOTOROMU WY^ISLQETSQ ZNA^ENIE WYRAVENIQ (6). eSLI OPISANNYJ WY E PROCESS NE ZAWER AETSQ, TOMY BUDEM S^ITATX, ^TO ZNA^ENIE FUNKCII fi NA KORTEVE ARGUMENTOW (u1 ::: uk ) NEOPREDELENO.
i

8 " > > sort(x)= eq(x ")?head(x) sort(tail(x))) : insert( < a "a > insert(leqy)= eq(yy)))? conc(a y) (a head( ? >: : : conc(head(y) insert(a tail(y))
3. pOISK ZADANNOJPODSTROKI x W STROKE y: FUNKCIQ substring WOZWRA]AET 1, ESLI EEPERWYJ ARGUMENT QWLQETSQ PODSTROKOJWTOROGO ARGUMENTA, I 0, INA^E. 8 substring(x y)= (pref ix(x y)) ? 1 > > > : eq(y ")? 0 > : ing tail > < pref ix(x substreq(x(x")? 1(y)) y)= y > : eq(0 ")? 0 1 > (head(x)= head(y)) ? > > : @ pref ix(tail(x) tail(y)) A > : :0

3.6 pRIMERY fp

pRIWEDEM TRI PRIMERA fp. nIVE SIMWOL " OBOZNA^AET KONSTANTU ffcongg (T.E. INTERPRETACIEJ KONSTANTY " QWLQETSQ PUSTAQSTROKA), I ZNAKOSO^ETANIQ eq, conc, head I tail OBOZNA^A@T SOOTWETSTWU@]IE BAZOWYE fs.

4


3.7 sWOJSTWO ALGORITMI^ESKOJ POLNOTY fp

KAVDAQ ^ASTI^NAQ FUNKCIQ NA STROKAH, WY^ISLIMAQW NEKOTOROM INTUITIWNOM SMYSLE, MOVET BYTX OPREDELEeSLI q { ZAKL@^ITELXNOE SOSTOQNIE, TO SOOTWETNA PRI POMO]I NEKOTOROJ fp. |TO SWOJSTWO DOKAZYSTWU@]EE EMU URAWNENIE IMEET WID WAETSQ POSREDSTWOM MODELIROWANIQ FUNKCIONALXNYMI PROGRAMMAMI MA IN tX@RINGA. dOKAZATELXSTWO OSNOq(x y)= remove blanks(y) WANO NA PREDPOLOVENII, ^TO MNOVESTWO MA IN tX@RINGA OBLADAET SWOJSTWOMALGORITMI^ESKOJPOLNOTY. GDE FUNKCIQ, SOOTWETSTWU@]AQfs remove blanks, pUSTX IMEETSQ NEKOTORAQ MA INA tX@RINGA S MNODEJSTWUET NA SWOJ ARGUMENT PUTEM UDALENIQ PROVESTWOM SOSTOQNIJ Q I ALFAWITOM A SIMWOLOW, KOTOBELXNYH SIMWOLOWW EGO PRAWOJ ^ASTI, T.E. RYE MOGUT BYTX NAPISANY W Q^EJKAH LENTY. mY BU8 remove blanks(x)= eq(x ")? " > DEM PREDPOLAGATX, ^TO A NESODERVIT FIGURNYH SKOBOK > : eq(last(x) )? remove blanks(rem last(x)) > (ESLI TAKIE SKOBKI PRISUTSTWU@T W A, TO MY IH KAK> :x < NIBUDX PEREOBOZNA^IM). tAKVEMYBUDEM PREDPOLAGATX, last(x)= eq(tail(x) ")? head(x) ^TO > : last(tail(x)) > > rem last(x)= eq(tail(x) ")? " WWEDENNOE WY EMNOVESTWO SIMWOLOW C SODERVIT > : : conc(head(x) rem last(tail(x))) KAVDYJ SIMWOL, WHODQ]IJ W A, I A SODERVIT PROBELXNYJ SIMWOL, KOTORYJ MY 3.8 iNTERPRETIRUEMYE fs BUDEM OBOZNA^ATX ^EREZ . pUSTX u { fpWIDA (4). tOGDA DLQ KAVDOGO i =1 ::: n pUSTX RABOTA \TOJ MA INY OPISYWAETSQ OTOBRAVE- fs WIDA NIEM tOGDA fp, SOOTWETSTWU@]AQ \TOJ MA INE, OPREDELQETSQ SLEDU@]IM OBRAZOM. sOPOSTAWIM KAVDOMU SOSTOQNI@ q 2 Q NEKOTORYJ NE BAZOWYJ fs ARNOSTI 2, KOTORYJ MY BUDEM OBOZNA^ATX TAK VE, KAK I \TO SOSTOQNIE, T.E. ^EREZ q. iSKOMAQfp SOSTOIT IZ SLEDU@]IH URAWNENIJ: URAWNENIE, SOOTWETSTWU@]EE FUNKCII f , KOTORU@ WY^ISLQEET \TA MA INA, IMEET WID
f (x)= q0(" x) :Q A
!

mNOVESTWO WSEH fp OBLADAET SWOJSTWOM ALGORITMI^ESKOJPOLNOTY, KOTOROE ZAKL@^AETSQWSLEDU@]EM:

TOURAWNENIE, SOOTWETSTWU@]EE SOSTOQNI@ q, IMEET WID
q(x y)= eq(y ")? q(x ) : eq(head(y) a1 )? qi (conc(aj x) tail(y)) : eq(head(y) a2 )? :::

QA

fleft rightg

NAZYWAETSQ INTERPRETIRUEMYM STWUET TA VE SAMAQ FUNKCIQ
i

fffungfkigfinterpretedgufigg

(7) fs, I EMU SOOTWET-

fi : Sk ! S KOTORAQ SOOTWETSTWUET fs fi Wfp (4). wCELQH UDOBSTWA ^TENIQ, MY BUDEM OBOZNA^ATX fs WIDA (7) ZNAKOSO^ETANIEM fiu .

4

fORMULY

GDE q0 { NA^ALXNOE SOSTOQNIE MA INY DLQ KAVDOGO q 2 Q fpSODERVIT URAWNENIE WIDA q(x y)= :::, GDE { PEREMENNAQ x SOOTWETSTWUET ZAPISI NA LENTE MA INY SLEWA OT GOLOWKI, PRO^ITANNOJ SPRAWA NALEWO, I { PEREMENNAQ y SOOTWETSTWUET ZAPISI NA LENTE PODGOLOWKOJ I SPRAWA OT NEE. eSLI { MNOVESTWO A IMEET WID fa1 :::g, { q { NEKOTOROE NEZAKL@^ITELXNOE SOSTOQNIE, I { (q a1 ) IMEET WID, NAPRIMER,(qi aj right)
5

wYRAVENIE e NAZYWAETSQ INTERPRETIRUEMYM, ESLI \TOLIBO PEREMENNAQ, LIBO KONSTANTA, LIBO IMEET WID GDE f { BAZOWYJ ILI INTERPRETIRUEMYJ fs. dLQ KAVDOJPARY e1 e2 INTERPRETIRUEMYH WYRAVENIJ ss
ffelem fmg e1

4.1 pONQTIE FORMULY

f (e1 ::: en)

= e2 g (8) QWLQETSQ FORMULOJ. fORMULY WIDA (8) NAZYWA@TSQ \LEMENTARNYMI FORMULAMI. wCELQH UDOBSTWA ^TENIQ, FORMULU WIDA (8) MY BUDEM ZAPISYWATX ZNAKOSO^ETANI-

EM

oSTALXNYE FORMULY STROQTSQ STANDARTNYM OBRAZOM IZ \LEMENTARNYH FORMUL PRI POMO]I BULEWSKIH SWQZOK I KWANTOROW:

e1 = e

2


ESLI A I B - FORMULY, TOss
ff ff ff ff ff
fm fm fm fm fm

5
(9)

fORMALXNYE SISTEMY
-

g A ^ Bg g A _ Bg g A ! Bg g A $ Bg g :Ag

5.1 pONQTIE FORMALXNOJ SISTEMY

QWLQ@TSQ FORMULAMI, I ESLI A { FORMULA I x { PEREMENNAQ, TOss 5.1.1 aKSIOMY fffmg 8 xAg I fffmg9 xAg aKSIOMA - \TO FORMULA, PRINADLEVA]AQ ODNOMU IZ QWLQ@TSQ FORMULAMI. SLEDU@]IH ESTI MNOVESTW. mY BUDEM OBOZNA^ATX NE\LEMENTARNYE FORMULY TAK, KAK \TO PRINQTO W MATEMATI^ESKOJLOGIKE, T.E. ZNAKO- 1. pUSTX SO^ETANIQMI T { PROIZWOLXNAQTAWTOLOGIQ LOGIKI WYSKAA ^B A_B ::: ZYWANIJ, I p1 ::: pn - SPISOKWSEHBULEWYH PEREMENNYH, SOOTWETSTWENNO. WHODQ]IH W T . pONQTIQ SWOBODNOGO I SWQZANNOGO WHOVDENIQ PEREMENNYH W FORMULY OPREDELQ@TSQ STANDARTNYM OBRAtOGDA DLQ KAVDOGO SPISKA FORMUL WIDA A1 ::: An ZOM (SM., NAPRIMER, 2]). FORMULA eSLI A { FORMULA, x { PEREMENNAQ, I e { WYRAVET (A1 =p1 ::: An=pn ) NIE, TOZNAKOSO^ETANIE A(e=x) OBOZNA^AET FORMULU, POLU^AEMU@ IZ A ZAMENOJ KAVDOGO SWOBODNOGOWHOVDENIQ (POLU^AEMAQIZ T ZAMENOJDLQ KAVDOGO i =1 ::: n PEREMENNOJ x W A NA WYRAVENIE e. pRI \TOM, ESLI NEKAVDOGOWHOVDENIQ PEREMENNOJ pi W T NA SOOTWETOBHODIMO, PROIZWODQTSQ PEREIMENOWANIQ SWQZANNYH PESTWU@]U@ EJ FORMULU Ai) QWLQETSQ AKSIOMOJ. REMENNYH W A (PODROBNOSTI SM. W 2], GL. 2). 2. kWANTORNYE AKSIOMY: pUSTX A { NEKOTORAQ FORMULA, I x1 ::: xn { SPISOK WSEHPEREMENNYH, IME@]IH SWOBODNYE WHOVDENIQ W A. oZNA^IWANIEM SWOBODNYH PEREMENNYH W FORMULE A NAZYWAETSQ PROIZWOLXNYJ SPISOK WIDA
a1 ::: an
4.2 iSTINNOSTX FORMUL
:(8xA) $ 9x(:

NOSTX AKSIOM I PRAWIL WYWODA, I BUDET NIVE OBOZNA^ATXSQ SIMWOLOM T . w IZLAGAEMYH NIVE FORMULIROWKAH SIMWOLY A B OBOZNA^A@T PROIZWOLXNYE FORMULY, SIMWOLY e e1 e2 - PROIZWOLXNYE WYRAVENIQ, SIMWOLY x y z { PROIZWOLXNYE PEREMENNYE.

fORMALXNAQ SISTEMA PREDSTAWLQET SOBOJ SOWOKUP

A)

:(9

xA)

$ 8x(:

A)

(10) (11) (12) (13) (14) (15) (16) (17)

A $ 8xA A $ 9xA (GDE x NEIMEET SWOB. WHOVDENIJ W A) A(e=x) ! 9xA 3. aKSIOMY RAWENSTWA x=x (x = y) ! (y = x) (x = y) ! ((y = z ) ! (x = z )) (e1 = e2 ) ! (e(e1 =x)= e(e2 =x)) (e1 = e2 ) ! (A(e1 =x) $ A(e2 =x)) 4. aKSIOMY DLQ BAZOWYH FUNKCIJ NA STROKAH (x =1) ! ((x ? y : z )= y) (x =0) ! ((x ? y : z )= z ) (eq(x y)=1) $ (x = y) (eq(x y)=0) $ :(x = y) :(x = ") ! (conc(head(x) tail(x)) = x)

KAVDAQ KOMPONENTA ai KOTOROGO QWLQETSQ ss I SOOTWETSTWUET PEREMENNOJ xi (STEM VENOMEROM) IZ SPISKA pONQTIE ISTINNOSTI FORMULY A NA OZNA^IWANII OPREDELQETSQ INDUKCIEJ POPOSTROENI@ FORMULY A: ESLI A IMEET WID e1 = e2 , TOONA QWLQETSQ ISTINNOJNA , ESLI ZNA^ENIQ WYRAVENIJ e1 ( a1 =x1 ::: an =xn ) I e2 ( a1 =x1 ::: an =xn) LIBO OBA NEOPREDELENY, LIBO OBA OPREDELENY I SOWPADA@T, ISTINNOSTX NE\LEMENTARNYH FORMULNA OZNA^IWANIQH OPREDELQETSQ STANDARTNYM OBRAZOM. fORMULA NAZYWAETSQ ISTINNOJ, ESLI ONA ISTINNA NA PROIZWOLXNOM OZNA^IWANII.
6 x1 ::: xn.

DLQ
{

KAVDOGOBAZOWOGOfs f , I


KAVDOGO SPISKA ss a1 ::: an b, TAKOGO, 5.1.3 pONQTIE DOKAZATELXSTWA ^TO ZNA^ENIE FUNKCII f NA KORTEVE AR- pUSTX A { NEKOTORAQ FORMULA. dOKAZATELXSTWOM (W GUMENTOW (a1 ::: an) RAWNO b SISTEME T ) FORMULY A NAZYWAETSQ ss WIDA FORMULA
{

QWLQETSQ AKSIOMOJ GDE A1 ::: An { FORMULY, PRI^EM 5. pUSTX u { fpWIDA (4), I i { PROIZWOLXNYJ INDEKS An = A, I IZ MNOVESTWA f1 ::: ng. tOGDA FORMULA fiu (xi1 ::: xik )= eiu DLQ KAVDOGO i =1 ::: n FORMULA Ai QWLQETSQ GDE eu POLU^AETSQ IZ WYRAVENIQ ei WPRAWOJ^ASTI i { LIBO AKSIOMOJ SISTEMY T , i{GO FUNKCIONALXNOGO URAWNENIQ W \TOJfpZAME{ LIBO ZAKL@^ENIEM NEKOTOROGO PRAWILA WYWONOJ KAVDOGOfs fj NA SOOTWETSTWU@]IJ EMU INDA, POSYLKI KOTOROGOSODERVATSQ W MNOVESTERPRETIRUEMYJ fs fju , QWLQETSQ AKSIOMOJ. TWE fA1 ::: Ai 1g. 6. dOPOLNITELXNOE MNOVESTWO AKSIOM Add Ax, OBLAfORMULA NAZYWAETSQ DOKAZUEMOJ (W T ), ESLI SUDA@]EE SLEDU@]IMI SWOJSTWAMI: ]ESTWUET DOKAZATELXSTWO W T \TOJFORMULY. KAVDAQFORMULA IZ Add Ax ISTINNA iZ WY ESKAZANNOGO SLEDUET, ^TO ESLI FORMULA QWMNOVESTWO Add Ax RAZRE IMO, T.E. SU]EST- LQETSQ DOKAZUEMOJ, TOONA QWLQETSQ ISTINNOJ. WUET ALGORITM, KOTORYJ DLQ KAVDOJFORMUiZ SWOJSTWA ALGORITMI^ESKOJPOLNOTY fp WYTEKALY OPREDELQET, PRINADLEVIT LI ONA \TOMU ET SU]ESTWOWANIE fp prf, OPREDELQ@]EJ FUNKCI@ S MNOVESTWU, ILI NET. DWUMQ ARGUMENTAMI, KOTORAQ NA PARE ARGUMENTOW (u v) iZ DANNOGO OPREDELENIQ SLEDUET, ^TO MNOVESTWO WSEH PRINIMAET ZNA^ENIE AKSIOM OBLADAET TEMI VE SWOJSTWAMI, ^TOI MNOVESTWO 1, ESLI u QWLQETSQ DOKAZATELXSTWOM v (W T ), I Add Ax, T.E. 0, INA^E. KAVDAQAKSIOMA QWLQETSQ ISTINNOJFORMULOJ, I
i
;

f (a1 ::: an)= b

ffproofgA1

::: An

g

(19)

MNOVESTWO WSEHAKSIOM RAZRE IMO. rAZRE IMOSTX MNOVESTWA AKSIOMSLEDUETIZTOGO, ^TO PRINADLEVNOSTX FORMULY K L@BOJIZ WY EPERE^ISLENNYH GRUPP (KROME POSLEDNEJ) OPREDELQETSQ PO SINTAKSI^ESKOJ STRUKTURE DANNOJFORMULY. pOSKOLXKU MY NE DETALIZIRUEM WID AKSIOM IZ POSLEDNEJ GRUPPY, TO W DEJSTWITELXNOSTI UPOMQNUTYJ WY E SIMWOL T OBOZNA^AET NEKONKRETNU@ FORMALXNU@ SISTEMU, A PROIZWOLXNU@ FORMALXNU@ SISTEMU, MNOVESTWO AKSIOMKOTOROJMOVET BYTX PREDSTAWLENOW WIDESOWOKUPNOSTI WY EPERE^ISLENNYH GRUPP.

oPISANNAQWY ESISTEMA T QWLQETSQ BOLEE OB]EJ, ^EM ARIFMETIKA pEANO (AKSIOMY I PRAWILA WYWODA KOTOROJ SM. W 2], GL.3), WTOMSMYSLE, ^TO OB_EKTY I FORMULY ARIFMETIKI pEANO MOVNO INTERPRETIROWATX W QZYKE SISTEMY T : NATURALXNYE ^ISLA MOVNO INTERPRETIROWATX STROKAMI IZ EDINIC: KAVDOE POLOVITELXNOE ^ISLO n INTERPRETIRUETSQ STROKOJ IZ n EDINIC, ^ISLO 0 INTERPRETIRUETSQ PUSTOJ STROKOJ, 5.1.2 pRAWILA WYWODA FUNKCIQ SLOVENIQ INTERPRETIRUETSQ BAZOWOJ FUNKpRAWILA WYWODA POZWOLQ@T POLU^ATX IZ ODNIH FORCIEJ conc KONKATENACII STROK MUL DRUGIE FORMULY, IIME@T SLEDU@]IJ WID: FUNKCIQ WZQTIQ SLEDU@]EGO ^ISLA INTERPRETIRU1. modus ponens: ETSQ FUNKCIEJ succ, OPREDELQEMOJSLEDU@]EJ fp: A!B A
B 2. NAWE IWANIE KWANTOROW A!B A 8xA ! 8xB 9xA succ(x)= conc(x 1)
!B ! 9xB

5.2 iNTERPRETIRUEMOSTX W T ARIFMETIKI pEANO

(18)

w KAVDOM PRAWILE WYWODA NAD ^ERTOJ IZOBRAVENY mult(x y)= eq(x ")? " : conc(x mult(tail(x) y)) ODNA ILI DWE FORMULY (NAZYWAEMYE POSYLKAMI), IZ KOTORYH WYWODITSQ FORMULA, RASPOLOVENNAQ POD ^ERTOJ (NAZYWAEMAQ ZAKL@^ENIEM). nETRUDNO DOKAZATX, dLQ KAVDOJFORMULY A QZYKA ARIFMETIKI pEANOOBO^TO ESLI POSYLKI (ILI POSYLKA) KAKOGO-LIBO IZ \TIH ZNA^IM SIMWOLOM I (A) FORMULU W QZYKE SISTEMY T , KOPRAWIL ISTINNY, TO ZAKL@^ENIE TOVEBUDET ISTINNYM. TORAQPOLU^AETSQ IZ A
7

FUNKCIQ UMNOVENIQ INTERPRETIRUETSQ FUNKCIEJ mult, OPREDELQEMOJSLEDU@]EJ fp:


ZAMENOJKONSTANT I FUNKCIONALXNYH SIMWOLOWNA SOOTWETSTWU@]IE IM KONSTANTY I FUNKCIONALXNYE SIMWOLY SISTEMY T , I ZAMENOJ KAVDOJPODFORMULY WIDA 8xB NA FORMULU WIDA
((nat(x)= 1) ! B ) GDE FUNKCIQ nat PRINIMAET NA SWOEM ARGUMENTE
8x

ZNA^ENIE (u1 ::: un) { 1, ESLI ON QWLQETSQ STROKOJ IZ EDINIC ILI 2. { t IMEET WID 1 ? e1 : e2 PUSTOJ STROKOJ, I { s RAWNO e1 { 0- INA^E. 3. { t IMEET WID 0 ? e1 : e2 { s RAWNO e2 nETRUDNO PROWERITX, ^TO DLQ KAVDOJAKSIOMY A ARIFMETIKI pEANOFORMULA I (A) QWLQETSQ ISTINNOJ. 4. { t IMEET WID fju (e1 ::: ek ) eSLI SISTEMA T TAKOWA, ^TOE< POSLEDNQQ GRUPPA AK{ s RAWNO eu (e1 =xj 1 ::: ek =xjk ) j SIOMSODERVIT FORMULY WIDA I (A), GDE A { KAKAQ-LIBO IZ AKSIOM ARIFMETIKI pEANO, TONETRUDNOUSTANOWITX, zAMETIM, ^TO W KAVDOM IZ \TIH SLU^AEW FORMULA ^TO DLQ KAVDOJFORMULY A, DOKAZUEMOJWARIFMETIKE t = s QWLQETSQ DOKAZUEMOJ. pEANO, FORMULA I (A) BUDET DOKAZUEMA W T . dLQ KAVDOGO l =1 ::: m ; 1 SWQZX MEVDU WYRAVENIQMI el I el+1 W SPISKE (21) MOVNO WYRAZITX SLEDU@]IM 5.3 wSPOMOGATELXNYE UTWERVDENIQ OBRAZOM: SU]ESTWUET WYRAVENIE e, TAKOE, ^TO w \TOM PUNKTE MY DOKAVEM DWE LEMMY, NEOBHODIMYE el = e(t=x) el+1 = e(s=x) DLQ DOKAZATELXSTWA TEOREMY gEDELQ. GDE FORMULA t = s DOKAZUEMA. iSPOLXZUQ AKSIOMY WIlEMMA 1. DA (16) I PRAWILO modus ponens, ZAKL@^AEM, ^TO DLQ pUSTX KAVDOGO j =1 ::: m ; 1 FORMULA ej = ej +1 DOKAZUEMA. nA OSNOWANII AKSIOM TRANZITIWNOSTI RAWENSTWA, OTf { BAZOWYJ ILI INTERPRETIRUEMYJ fs, I S@DA SLEDUET DOKAZUEMOSTX FORMULY e1 = em , KOTORAQ SOWPADAET S (20). a1 ::: ak b { SPISOKss, TAKOJ, ^TOFORMULA
0 0 0 0 0 0 0 0

DLQ KAVDOGO l = 1 ::: m ; 1 WYRAVENIE el+1 POLU^AETSQ IZ WYRAVENIQ el ZAMENOJ ODNOGO IZ EGO PODWYRAVENIJ t NA WYRAVENIE s, PRI^EM IMEET MESTOODNOIZ SLEDU@]IH USLOWIJ: 1. { t IMEET WID f (u1 ::: un), GDE f { BAZOWYJ fs, OTLI^NYJ OT if_then_else, { s RAWNOKONSTANTE v , GDE v { ZNA^ENIE BAZOWOJFUNKCII f NA KORTEVE ARGUMENTOW

j

0

0

j

j

f (a1 ::: ak )= b QWLQETSQ ISTINNOJ. tOGDA FORMULA (20) DOKAZUEMA.

(20)

subst : S2 ! S TOIZ OPISANIQ PROCESSA WY^ISLENIQ ZNA^ENIQ WYRAVE- SO SLEDU@]IM SWOJSTWOM: DLQ KAVDOJ PARY CC (a b) NIQ W PUNKTE 3.5 SLEDUET, ^TO, SU]ESTWUET POSLEDOWA- subst(a b) POLU^AETSQ IZ a ZAMENOJW NEJ KAVDOGOWHOVDENIQ PEREMENNOJ x NA ss b. TELXNOSTX WYRAVENIJ oBOZNA^IM SIMWOLOM B FORMULU A(subst(x x)=x). iSKOMAQFORMULA ' IMEET WID B ( B =x). pOSKOLXKU e1 ::: em (21) EDINSTWENNOJ SWOBODNOJPEREMENNOJW B QWLQETSQ TAKAQ, ^TO x, I e1 = fiu (a1 ::: ak ) WSE WHOVDENIQ x W B PRI PODSTANOWKE ( B =x) ZAem = b MENQ@TSQ NA KONSTANTU B i
2 f1

eSLI f { BAZOWYJ fs, TOFORMULA (20) QWLQETSQ AKdOKAZATELXSTWO. SIOMOJ (IZ ^ETWERTOJ GRUPPY). mY MOVEM PREDPOLAGATX, ^TO WSE WHOVDENIQ x W A eSLI VE f { INTERPRETIRUEMYJ fs, T.E. f IMEET QWLQ@TSQ SWOBODNYMI (ESLI \TONETAK, TOPEREIMENUEM WID fiu , GDE WSE SWQZANNYE WHOVDENIQ x W A). oBOZNA Z OSO^ETANIEM subst INT u { fp, KOTORAQPOLU^AETSQ IZ fpWIDA (4) ZAME- MYJ fs, K^IMRONAKSOOTWETSTWUET FUNKCIQERPRETIRUEOTO MU NOJ KAVDOGONE BAZOWOGOfs fj NA fs fju , I
::: ng

dOKAZATELXSTWO

dLQ KAVDOJFORMULY A SODNOJSWOBODNOJPEREMENNOJ x SU]ESTWUET ZAMKNUTAQ (T.E. NE SODERVA]AQ SWOBODNYH PEREMENNYH) FORMULA ', TAKAQ, ^TODOKAZUEMA FORMULA
'
$

lEMMA 2 (LEMMA O NEPODWIVNOJTO^KE
A( ' =x)

)

.

.

(22)

8


TO ' ZAMKNUTA. pOSKOLXKU PEREHOD OT B K ' ZAKL@^AETSQ W ZAMENEW ss B KAVDOGOWHOVDENIQ PEREMENNOJ x NA ss B , TO.PEREHODOT B K ' ZAKL@^AETSQ W ZAMENEW ss B KAVDOGO WHOVDENIQ PEREMENNOJ x NA ss B , T.E. ISTINNA FORMULA

subst( B B )= ' sOGLASNOLEMME 1, FORMULA (23) DOKAZUEMA. iSPOLXZUQ AKSIOMU WIDA (17) I PRAWILO modus ponens, ZAKL@^AtEPERX MOVNO PRISTUPITX K DOKAZATELXSTWU TOGO, EM, ^TOIZ DOKAZUEMOSTI FORMULY (23) SLEDUET DOKAZU- ^TOFORMULY ' I :' NEDOKAZUEMY. EMOSTX FORMULY 1. eSLI DOKAZUEMA ', TO PO LEMME 3 DOKAZUEMA 2'. iSPOLXZUQ DOKAZUEMU@ FORMULU (25), KOTORU@ MOVA(subst( B B )=x) $ A( ' =x)

(x A)= 1) (27) (KOTORAQ QWLQETSQ AKSIOMOJ WIDA (12)) POLU^AEM DOKA(23) ZUEMOSTXAZAKL@^ENIQ IMPLIKACII (27), KOTOROE SOWPADAET S 2 .
prf

QWLQETSQ ISTINNOJ. sOGLASNOLEMME 1, FORMULA (26) DOKAZUEMA. pO PRAWILU modus ponens, IZ (26) IIZFORMULY
( (u A)= 1)
! 9x (prf

KOTORAQ SOWPADAET S (22), TAK KAK LEWAQ ^ASTX W NEJ SOWPADAET S '.

tEOREMA gEDELQ tEOREMA gEDELQ UTWERVDAET, ^TO ESLI FORMALXNAQ SISTEMA T NEPROTIWORE^IWA (T.E. WNEJ NEDOKAZUEMA LOVNAQ FORMULA), TO SU]ESTWUET ZAMKNUTAQ FORMULA ', TAKAQ, ^TO OBE FORMULY ' I :' NEDOKAZUEMY W T . pOSKOLXKU ODNA IZ FORMUL ', :' ISTINNA, TO, SLEDOWATELXNO, SU]ESTWUET ISTINNAQFORMULA, KOTORAQNE QWLQETSQ DOKAZUEMOJ W SISTEME T . dLQ POSTROENIQ TAKOJFORMULY RASSMOTRIM FORMULU
:9

6

NOPEREPISATX \KWIWALENTNYM OBRAZOMW WIDE :' $ 2' (28) POLU^AEM DOKAZUEMOSTX :'. |TONEWOZMOVNO, ESLI T NEPROTIWORE^IWA. 2. eSLI DOKAZUEMA :', TOIZDOKAZUEMOSTI (28) SLEDUET, ^TODOKAZUEMA 2', T.E. DOKAZUEMA FORMULA
9

x(

prf

(x ')=1)

pOSKOLXKU KAVDAQDOKAZUEMAQFORMULA QWLQETSQ ISTINNOJ, TO, SLEDOWATELXNO, SU]ESTWUET CC u, TAKAQ, ^TOFORMULA
prf

eDINSTWENNOJ SWOBODNOJPEREMENNOJ\TOJFORMULY QWLQETSQ x. pO LEMME O NEPODWIVNOJ TO^KE, SU]ESTWUET ZAMKNUTAQFORMULA ', TAKAQ, ^TODOKAZUEMA FORMULA
'
$ : 9y (prf

y(

prf

(y x)= 1)

(u ')=1

(y ' )= 1)

(24)

nIVE MY DOKAVEM, ^TO OBE FORMULY ' I :' NEDOKAZUEMY. mY BUDEM ISPOLXZOWATX SLEDU@]EE OBOZNA^ENIE: DLQ KAVDOJ FORMULY A ZNAKOSO^ETANIE 2A QWLQETSQ SOKRA]ENNOJ ZAPISX@ FORMULY
9

x(

prf

(x A)= 1)

fORMULA 2A WYRAVAET UTWERVDENIE O TOM, ^TO FORMULA A QWLQETSQ DOKAZUEMOJ (W SISTEME T ). iSPOLXZUQ DANNOE OBOZNA^ENIE, MOVNOPEREPISATX (24) WWIDE ' $ : 2' (25) eSLI FORMULA A DOKAZUEMA, TODOKAZUEMA FORMULA 2A. dOKAZATELXSTWO. eSLI FORMULA A DOKAZUEMA, TO SU]ESTWUET ss u, TAKAQ, ^TOFORMULA (26) prf (u A)= 1
9

lEMMA

3

.

QWLQETSQ ISTINNOJ, T.E. SU]ESTWUET ss u, QWLQ@]AQSQ DOKAZATELXSTWOMFORMULY ', T.E. FORMULA ' DOKAZUEMA, ^TONEWOZMOVNO, ESLI T NEPROTIWORE^IWA. oTMETIM, ^TO NEDOKAZUEMOSTX NEKOTOROJ ISTINNOJ FORMULY NEWOZMOVNO USTRANITX PUTEM RAS IRENIQ SISTEMY T DOBAWLENIEM NEJ PROIZWOLXNOGO PERE^ISLIMOGOMNOVESTWA DOPOLNITELXNYH AKSIOM, T.E. TAKOGOMNOVESTWA DOPOLNITELXNYH AKSIOM, KAVDAQIZKOTORYH QWLQETSQ ISTINNOJFORMULOJI IMEET WID f (u), GDE f { NEKOTORAQFIKSIROWANNAQ WS@DU OPREDELENNAQ WY^ISLIMAQ FUNKCIQ NA ss, I u - PROIZWOLXNAQss POTOMU, ^TOPOLU^IW AQSQ SISTEMA T BUDET IMETX TO VEMNOVESTWO DOKAZUEMYH FORMUL, ^TOINEKOTORAQSISTEMA T S RAZRE IMYM MNOVESTWOM DOPOLNITELXNYH AKSIOM, AIMENNO, T POLU^AETSQ IZ T DOBAWLENIEM AKSIOMWIDA
0 00 00

sISTEMA T BUDET UDOWLETWORQTX TEM VE USLOWIQM, ^TO IISHODNAQ SISTEMA T . pO\TOMU, ESLI ONA NEPROTIWORE^IWA, TO W NEJ TOVE BUDET NEDOKAZUEMA NEKOTORAQ ISTINNAQFORMULA.
00

f (u) ^ (u = u)


nEDOKAZUEMOSTX NEPROTIWORE^IWOSTI oBOZNA^IM ZNAKOSO^ETANIEM C onsis(T ) FORMULU : 20, GDE 0 { TOVDESTWENNOLOVNAQFORMULA (OTRICANIE TAWTOLOGII). fORMULA C onsis(T ) WYRAVAET SWOJSTWO NEPROTIWORE^IWOSTI SISTEMY T . mOVNODOKAZATX, ^TODOKAZUEMA \KWIWALENCIQ
'
$

7

C onsis(T )

(29)

GDE ' { FORMULA, OPREDELENNAQ W PREDYDU]EM PUNKTE. kAK BYLO USTANOWLENO, ESLI T NEPROTIWORE^IWA, TO FORMULA ' NEDOKAZUEMA, PO\TOMU FORMULA C onsis(T ) TAKVENEDOKAZUEMA (W SISTEME T ). uTWERVDENIE O NEDOKAZUEMOSTI NEPROTIWORE^IWOSTI FORMALXNOJ SISTEMY SREDSTWAMI SAMOJ\TOJSISTEMY OBY^NO NAZYWA@T WTOROJTEOREMOJgEDELQ. oPI EM SHEMU DOKAZATELXSTWA \KWIWALENCII (29). iZ OPREDELENIJ ' I C onsis(T ) SLEDUET, ^TO DOKAZUEMOSTX (29) RAWNOSILXNA DOKAZUEMOSTI \KWIWALENCII (A ! (B ! C )) ! ((A ! B ) ! (A ! C )) 2' $ 20 (30) POLU^AEM DOKAZUEMOSTX IMPLIKACII 2' ! 20. mOVNODOKAZATX, ^TO DLQ L@BYH FORMUL A B DOKAZUEMY IMPLIKACII lITERATURA 2(A ! B ) ! (2A ! 2B ) (31) 1] Godel, K.: Uber Formal Unentscheidbare Satze der Principia Mathematica und Verwandter Systeme, I. I 2A ! 22A (32) 2] |.mENDELXSON: wWEDENIE W MATEMATI^ESKU@ LOoTMETIM, ^TO GIKU. m nAUKA (31) MOVNO RASSMATRIWATX KAK FORMALIZACI@ W 3] a.n.kOLMOGOROW, a.g.dRAGALIN: mATEMATIT PRAWILA modus ponens, I ^ESKAQLOGIKA. dOPOLNITELXNYE GLAWY. iZDATELX (32) MOVNO RASSMATRIWATX KAK FORMALIZACI@ UTSTWO mOSKOWSKOGO uNIWERSITETA . WERVDENIQ LEMMY 3. eSLI DOKAZUEMA IMPLIKACIQ A ! B , TO PO LEMME 3 DOKAZUEMA FORMULA 2(A ! B ), OTKUDA, NA OSNOWANII DOKAZUEMOSTI FORMUL WIDA (31), ZAKL@^AEM, ^TODOKAZUEMA IMPLIKACII 2A ! 2B . dLQ OBOSNOWANIQ DOKAZUEMOSTI \KWIWALENCII (30) MY DOKAVEM, ^TO DOKAZUEMY IMPLIKACII 2' ! 20 I 20 ! 2'. 1. pOSKOLXKUFORMULA 0 ! ' QWLQETSQ AKSIOMOJ (IZ PERWOJ GRUPPY), T.K. ONA IMEET WID (0 ! p)('=p), I 0 ! p { TAWTOLOGIQ LOGIKI WYSKAZYWANIJ TOIZWY ESKAZANNOGOSLEDUET, ^TODOKAZUEMA IMPLIKACIQ 20 ! 2'. 2. pOSKOLXKU FORMULA ' ! (:' ! 0) QWLQETSQ AKSIOMOJ (IZ PERWOJ GRUPPY), T.K. ONA IMEET WID (p ! (:p ! 0))('=p), I
Monatshefte Math. Phys. 38, 173-198, 1931. ., , 1976. , 1984

(p ! (:p ! 0)) { TAWTOLOGIQ LOGIKI WYSKAZYWANIJ TO, SLEDOWATELXNO, DOKAZUEMA IMPLIKACIQ 2' ! 2(:' ! 0) OTKUDA, ISPOLXZUQ DOKAZUEMOSTX FORMUL WIDA (31) I PRAWILOSILLOGIZMA, POLU^AEM DOKAZUEMOSTX FORMULY 2' ! (2:' ! 20) (33) iZ (28) SLEDUET DOKAZUEMOSTX FORMULY 2' ! :', OTKUDA SLEDUET DOKAZUEMOSTX FORMULY 22' ! 2:' (34) iZ DOKAZUEMOSTI FORMUL 2' ! 22' I (34) PO PRAWILU SILLOGIZMA SLEDUET DOKAZUEMOSTX FORMULY 2' ! 2:' OTKUDA, ISPOLXZUQ (33) IAKSIOMY IZ PERWOJ GRUPPY WIDA

10