MATEMATICKÁ LOGIKA Prezentace ke kurzu MA007 Antonín Kučera 2005 0 Bůh Logika (z řeckého Aoyocr) zkoumá způsob vyvozování závěrů z předpokladů. V běžné řeči se „logikou" označuje myšlenková cesta, která vedla k daným závěrům. Logika nezkoumá lidské myšlení (psychologie) ani obecné poznání (epistemologie). „Může (všemohoucí) Bůh stvořit kámen, který sám nedokáže uzved-nout?" 3 Neformální logika studuje problematiku správné argumentace v přirozeném jazyce. Formální logika definuje a studuje abstraktní odvozovací pravidla (tj. „formy úsudků"), jejichž platnost nezávisí na významu pojmů, které v nich vystupují. Pod pojem matematická logika jsou obvykle zahrnovány dvě různé oblasti výzkumu: ->- aplikace poznatků z oblasti formální logiky na matematiku (např. snaha „vnořit" matematiku do logiky ve formě konečného systému axiomů a odvozovacích pravidel); ->- aplikace matematických struktur a technik ve formální logice (např. teorie modelů, teorie důkazů, apod.) Aristoteles (384-322 př. Kr.) ISTOTELOVA LOGIKA. Logický čtverec. m Nechť S a P jsou neprázdné vlastnosti. Aristoteles rozlišuje následující základní kategorická tvrzení: A všechna S jsou? E žádná S nejsou P I některá S jsou? O některá S nejsou ? Mnemonika: Afflrmo—nEgO (tvrdím—popírám) IRISTOTELOVA LOGIKA. Logický čtverec (pokr.) A a O jsou kontradiktorická, tj. nemohou být současně pravdivá ani současně nepravdivá. I a E jsou rovněž kontradiktorická. A a E jsou kontrární, tj. mohou být současně nepravdivá ale ne současně pravdivá. I a O jsou subkontrární, tj. mohou být současně pravdivá ale ne současně nepravdivá. I je subalterní (podřízené) A, tj. I je pravdivé jestliže A je pravdivé, a současně A je nepravdivé jestliže I je nepravdivé. Podobně Oje subalterní E. Aristotelova logika, sylogismy. Sylogismy jsou jednoduché úsudky tvaru Hlavní premisa Vedlejší premisa .*. Závěr Obě premisy i závěr jsou kategorická tvrzení tvaru A, E, I, O obsahující dohromady právě tři vlastnosti (označme je S, M, P), kde hlavní premisa obsahuje SaM; vedlejší premisa obsahuje P a M; závěr je tvaru S z P. Lze tedy rozlišit následující čtyři formy sylogismů: I: M x P II: P x M III: M x P IV: P x M SyM SyM My S .'.S z? .'.S z? .'.S z? My S .'.S z P mi + Celkem tedy existuje 4 • 43 = 256 sylogismů. Aristotelova logika, sylogismy (pokrj 8 Jen 24 sylogismů je platných: Forma I: AAA, AII, EAE, EIO (Barbara, Darii, Celarent, Ferio), AAI, EAO (subalterní módy); Forma II: AEE, EAE, AOO, EIO (Camestres, Césare, Baroco, Festino), AEO, EAO (subalterní módy); Forma III: AAI, AII, EAO, EIO, OAO, IAI (Darapti, Datisi, Felapton, Ferison, Bocardo, Disamis); Forma IV: IAI, AAI, AEE, EAO, EIO (Dimatis, Bamalip, Calemes, Fesapo, Fresio), AEO (subalterní mód). O (ne) platnosti sylogismů se lze snadno přesvědčit pomocí Vennových diagramů (John Venn, 1834-1923). 9 A E I O (všechna S j sou V) (žádná S nejsou?) (některá S jsou?) (některá S nejsou?) šedé oblasti jsou prázdné; symbol „•" označuje neprázdné oblasti; ľ"* bílé oblasti mohou být prázdné i neprázdné. ISTOTELOVA LOGIKA. Platnost sylogismů (pokr.) »* Uvažme nyní napr. AEE sylogismus druhé formy (Camestres) Všechna P jsou M Žádná S nejsou M Žádná S nejsou P Tento sylogismus je tedy platný. Pro AIO sylogismus druhé formy dostáváme: Všechna P jsou M Některá S jsou M .*. Některá S nejsou P Druhý diagram podává protipříklad, sylogismus platný není. Ar ISTOTELOVA LOGIKA. Platnost sylogismů (pokr.) 11 Rozeberme ještě AAI sylogismus třetí formy (Darapti): Všechna M jsou P Všechna M jsou S .*. Některá S jsou P Tento sylogismus je v Aristotelově logice považován za platný. Je však třeba použít předpoklad, že každá vlastnost je neprázdná. Tento předpoklad ale přináší jisté problémy: Všechny skleněné hory jsou skleněné. Všechny skleněné hory jsou hory. .*. Některé hory jsou skleněné. Hlavní i vedlejší premisa jsou na intuitivní úrovni pravdivá tvrzení, závěr však nikoliv. BOOLEOVA „ALGEBRA LOGIKY. 44 12 Aplikoval algebraické techniky při formalizaci procesu odvozování. Nalezl souvislost mezi algebrou a sylogismy. Booleova „algebra logiky" se chová podobně jako algebra čísel. Násobení odpovídá logické spojce „a současně", sčítání logické spojce „nebo", apod. (Odtud pocházejí pojmy „logický součin" a „logický součet".). George Boole (1815-1864) GEBRA LOGIKY. Motivační příklad. m Uvažme následující sylogismus: Všechna S jsou M Žádná M nejsou P .*. Žádná S nejsou P Pokud vlastnosti identifikujeme se soubory objektů univerza, pro které platí, můžeme uvedený sylogismus přepsat na s c m sniví' = o (i) MnP = 0 a dále na MnP = 0 (2) .-. snp = o .-. snp = o (3) Pokusme se nyní „odvodit" (3) z (1) a (2): Al gebra logiky. Motivační příklad (pokr.) 14 Z toho, žeSnM; = OaXnO = 0 pro libovolné X dostáváme (S n M') n P = o (4) Podobně z (2) plyne (MnP)flS=0 (5). Ze (4), (5) a faktu, že 0 U 0 = 0, plyne ((S n M') nP)u((MnP)nS)=o (6) Užitím asociativity a komutativity U a n dostáváme z (6) ((S n P) n M') u ((S n P) n M) = o (7) Nyní podle distributivního zákona lze (7) přepsat na (SnP)n(M'uM) = o (8) Jelikož X U X' = 1 aXnl = X pro libovolné X, dostáváme z (8) konečně snP = o což bylo dokázat. Al gebra logiky. Motivační příklad (pokr.) 15 V předchozím příkladu jsme k dokázání sylogismu použili symbolickou manipulaci se symboly S, M a P podle následujících algebraických identit (tj. nezabývali jsme se tím, jaký mají symboly U, n, 0, 1, a ' význam). xux X xux7 i xnx X xnx7 0 XUY YUX x77 x xn Y Ynx XU 1 1 XU(YUZ) = (X U Y) U Z xn i x xn(Ynz) = (x n Y) n z xuo x xn(xuY) x xno 0 xu(xnY) x (XUY)7 = x7 n y7 xn(Yuz) = (x n Y) u (x n z) (x n Y)7 = X7 U Y7 xu(Ynz) = (x u Y) n (x u z) Al gebra logiky. Motivační příklad (pokr.) 16 Tyto identity definují algebraickou strukturu, které se později začalo říkat Booleva algebra (případně Booleův svaz). V původní Booleově notaci se ->- místo X n Y píše X.Y (případně jen XY); ->- místo X U Y píše X + Y; ->- místo X píše IX. V této notaci pak identity dostávají „číselnou podobu" a Boole sám se pokoušel převést další „číselné konstrukce" (např. dělení, ale i Taylorův rozvoj) do své „algebry logiky". Tyto úvahy však již byly zcela mylné. GEBRA LOGIKY. Dva základní problémy. 17 Podle Boolea je každý sylogismus možné zapsat ve tvaru Fi(P,M) = 0 F2(S,M) = 0 F(S,P) = 0 kde Fi (P, M), F2(S, M), F(S, P) jsou vhodné výrazy vytvořené ze symbolů 0, 1, U, n, ' a symbolů v závorkách. Boole uvážil obecnější úsudky tvaru Fi (Ai,..., Am,Bi,... ,Bn) = 0 Fic(Ai,..., Am, Bi,..., Bn) .'. F(Bi,... ,Bn) 0 0 Cílem jeho snah bylo vyvinout metodu, která umožní 1. zjistit, zdaje daný úsudek pravdivý', 2. nalézt nejobecnější závěr (F) pro dané předpoklady (Fi,. . . ,Fk) Al _gebra logiky. Booleova metoda. Definice 1. Nechť Ä = Ai,..., An. Ä-konstituentje výraz tvaru l\ n • • • n i kde íije buď Ai nebo A[. Věta 2. Pro každý výraz F(Xi, • • •, Xn) platí ¥{Xi, • • • ,xn) = y F(v) n u (v) n • • • n ťn(v) vG{0,1}^ kde ii{v)je buďXi nebo X[ podle toho, zdaje Ví rovno 1 nebo 0. Příklad 3. Nechť F (A, B) = (A U B') n (A' U B). Pak F(A,B) = (FtcojnA'nB') U (F(0,1)nA'nB) U (F(1,0) n AílB') U (F(1,1) n A n B) = (in A'n B') u (on A'n B) u (OnAnB') u (inAnB) = (A' n B') u (A n B) 18 n > Al gebra logiky. Řešení 1. problému. 19 Věta 4. Úsudek Fi(Ai,..., Am,Bi,... ,Bn) = 0 ■ ■ ■ Fk(Ai,..., Am,Bi,... ,Bn) = 0 F(B!,...,Bn) = 0 je platný právě když každý A, B-konstituent výrazu Tje A, B-konstituentem některého Ft. Příklad 5. Uvažme opět sylogismus srnu' = o mhp = o .-. snp = o Pak A = MaB = S,P. Uvažme A, B-konstituenty jednotlivých výrazů: srnu' : ivťnsnp, jvťnsnp' mhp : Mnsnp, Mns'nP snp : Mnsnp, M^snP ALGEBRA LOGIKY. Řešení 2. problému. ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Nechť A = Ai,..., Am, B = Bi,..., Bn. Uvažme předpoklady tvaru F!(A,B) =0,...,Fk(A,B) = 0 Cílem je nalézt nej obecnější závěr tvaru F(B) = 0. Označme E(A,B) =F1(A,B)U...UFk(A,B) Věta 6. Nejobecnější závěr F(B) = 0, který plyne z E(A, B) = 0, je ŕuaru F(B) = Q E(v,B) vG{0,1}™ Příklad 7. Nejobecnější závěr F(S, P) plynoucí z předpokladů S n M/ = 0 M n P = Oje ŕuaru F(S, P) = ((S n o7) u (o n P)) n ((S n ť) u (i n p)) snp VÝSTAVBA FORMÁLNÍCH LOGICKÝCH SYSTÉMŮ.[H Potřebujeme znát jisté pojmy a umět myslet {metaúroveň). ->- Musí být např. jasné, co myslíme symbolem, konečnou posloupností, atd. ->- Metapojmy a formální pojmy se bohužel často „značí" stejně. Tím vzniká (nesprávný) dojem, že formální pojmy jsou definovány pomocí „sebe sama" (typickým příkladem je důkaz nebo množina) ->- Co všechno si lze na metaúrovni dovolit? {potenciální vs. aktuální nekonečno). Základní kroky: ->- Vymezení užívaných symbolů (abeceda). Syntaxe formulí. ->- Sémantika (zde se objeví pojem pravdivost). ->- Odvozovací systém (zde se objeví pojem dokazatelnost). Definice 8. Abecedu výrokové logiky tvoří následující symboly: znaky pro výrokové proměnné A, B, C,..., kterých j e spočetně mnoho; logické spojky A, V, —>, -■ závorky ( a ) Definice 9. Formule výrokové logiky je slovo cp nad abecedou výrokové logiky, pro které existuje vytvořující posloupnost, tj. konečná posloupnost slov ipi, • • •, ipic, kde k > 1, je cp, a pro každé 1 < i < k má síouo % jeden z následujících tvarů: výroková proměnná, —-xpj pro nějaké 1 < j < i, (ipj o \|^,) pro nějaká 1 < j, f < i, kde o je jeden ze symbolů A, V, —». Poznámka 10. Notace: vnější závorky budeme zpravidla vynechávat Napr. místo (AV-B) budeme psát AV-B. VÝROKOVÁ LOGIKA. Sémantika. 23 Definice 11. Pravdivostní ohodnocení (valuace) je zobrazení v, které každé výrokové proměnné přiřadí hodnotu 0 nebo 1. Metamatematickou indukcí k délce vytvořující posloupnosti lze každou valuaci v jednoznačně rozšířit na všechny výrokové formule: v (A) je již definováno; 0 jestliže v(i|)) = 1; 1 jinak. um 0 jestliže v(ipi) jinak. jestliže v(ipi) jinak. 0 a současně v(^z) = 0; 0 jestliže v(ipi) = 1 a současně v (1^2) = 0; 1 jinak. 24 VÝROKOVÁ LOGIKA. Sémantika (pokr.) Definice 12. Výroková formule cp je pravdivá (resp. nepravdivá) při valuaciv, pokud v(cp) = 1 (resp. v(cp) = Oj; splnitelná, jestliže existuje valuacev taková, žev(cp) = 1; tautologie (také (logicky) pravdivá), jestliže v(cp) = 1 pro každou valuaciv. Soubor! výrokových formulí je splnitelný, jestliže existuje valuacev taková, že v(cp) = 1 pro každé cp z T. Definice 13. Formule cp ai|) jsou ekvivalentní, psáno cp « právě když pro každou valuaciv platí, že v(cp) = v(i|)). Příklad 14. Nechťcp, ^jsou výrokové formule. Pak: cp Ai|) « i|) A cp cpA(i|)A£,) « (cpAi|))A£, cpA(i|)V£,) « (cp Ai|)) V(cp AŽ,) ^(cpAij)) « ^(pV^ip ^^Cp Po cp 25 VÝROKOVÁ LOGIKA. Sémantika (pokr.) Poznámka 15. „Identity" z příkladu 14 umožňují dále zpřehlednit zápis formulí. Např. místo (A V B) V C můžeme (nejednoznačne) psát A V B V C. Tato nejednoznačnost nevede k problémům, neboť příslušné definice a tvrzení „fungují" pro libovolné možné uzávorkování. Poznámka 16. V teorii výpočetní složitosti se dokazuje, že problém zda daná výroková formule cp je splnitelná (resp. tautologie) je NP-ůplný (resp. co-NP-ůplný). Otázka, zda existuje efektivní (polynomiální) algoritmus pro uvedené problémy, je ekvivalentní otázce zda P = NP. Definice 17. Formule (pje tautologickým důsledkem souboru formulí T, psáno T \= cp, jestliže v(cp) = 1 pro každou valuaciv takovou, žev(ip) = 1 pro každou formuli i|) ze souboru T. Jestliže T \= cp pro prázdný soubor T, píšeme krátce \= cp. VÝROKOVÁ LOGIKA. Pravdivostní tabulky. 26 Někdy se sémantika výrokových spojek definuje „předem" pomocí pravdivostních tabulek: X Y X A Y X Y XVY 0 0 0 0 0 0 0 1 0 0 1 1 1 0 0 1 0 1 1 1 1 1 1 1 X Y X -> Y 0 0 1 0 1 1 1 0 0 1 1 1 x -x 0 1 1 0 Pojmy „pravdivostní tabulka" a „výroková spojka" je možné dále zobecnit a uvážit formální logické systémy budované na obecnějším základu: Definice 18. Výroková funkce je funkce F : {0, l}n -> {0,1}, kde n > 1. 27 VÝROKOVÁ LOGIKA. Formální systém £(Ft , ■ ■ ■, Fk). Nechť Fi, • • •, Fic je konečný soubor výrokových funkcí. Definujeme formální logický systém £(Fi, • • •, Fk), kde ->- Abeceda je tvořena znaky pro výrokové proměnné, závorkami a znaky T\, • • •, Ty pro uvedené výrokové funkce. ->- V definici vytvořující posloupnosti formule (viz definice 48) požadujeme, aby \|h bylo buď výrokovou proměnnou nebo tvaru T) ^, • • •, i\>jn), kde 1 < j i > • • • > jn < i a u je arita Fj. ->- Valuace rozšíříme z výrokových proměnných na formule předpisem v{T{^\)^, • • • ,\pn)) = F(v(i|)i), • • • ,v(\|0) V tomto smyslu je pak dosud uvažovaný systém výrokové logiky systémem £(A, V,—>,-■). Dříve zavedené sémantické pojmy (splnitelnost, pravdivost, atd.) se opírají pouze o pojem valuace a „fungují" tedy v libovolném systému £(Fi, • • •, Fk). VÝROKOVÁ LOGIKA. Formální systém £(Ft , ■ ■ ■, Fk). 28 Pro účely následující definice zvolme libovolné (ale dále pevné) lineární uspořádání □ na souboru všech výrokových proměnných. Definice 19. Nechť cp je formule £(Fi, • • •, Fk) a nechť X^, • • •, Xn je vzestupně uspořádaná posloupnost (vzhledem k Q) všech výrokových proměnných, které se ve cp vyskytují. Formule cp jednoznačně určuje výrokovou funkci F
{0,1} danou předpisem F
{0,1} je výroková funkce a nechť ui, • • •, Uk jsou všechny vektory z {0,1}n, pro které nabývá F hodnoty 1. Pokud žádný takový vektor není (tj. k = 0), klademe cp = Xi A --Xi A X2 A • • • A Xn. Jinak
k i=1
kde £j (uí) je buď Xj nebo --Xj podle toho, zda Ui(j) = 1 nebo ut(j) = 0. Nyní se lehce ověří, že F = F^. □
VÝROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.)
30
Uvažme následující výrokové funkce:
X Y X A Y X Y X 1 Y
0 0 1 0 0 1
0 1 0 0 1 1
1 0 0 1 0 1
1 1 0 1 1 0
X Y z 0(X,Y,Z)
0 0 0 1
0 0 1 0
0 1 0 1
0 1 1 0
1 0 0 1
1 0 1 0
1 1 0 0
1 1 1 0
Funkce X se nazývá Schróderův operátor. Platí cp A Funkce | se nazývá Shefferův operátor. Platí cp | \|;
~ -,(pA_,i|>. ■( 0((p>^>0((p>(p>(p)))
Následující systémy plnohodnotné nejsou:
-► £{A), £(V), £(-»), £H, atd.
VÝROKOVÁ LOGIKA. Shefferovské spojky. [32
Definice 22. Výroková funkce^ je Shejferovská jestliže C{E) je plnohodnotný systém.
Věta 23. NechťS(n) značí počet všech Shejferovských funkcí arity n > 1
PakS(n) = 2^_1 -1 )(2(2n_1 - 1).
Pro n = 1,2,3,4,5,... dostáváme postupně 0,2,56,16256,1073709056,...
Důsledek 24. Jelikož lim^oo ^w- = 1 /4, je (pro velká n) zhruba čtvrtina ze všech výrokových funkcí arity n Shefferovská.
Poznámka 25. Výsledky o Shejferovských funkcích nalézají uplatnění při výrobě logických obvodů; na „podkladové desce" se např. vytvoří hustá síť binárních | -hradel. Obvody různé funkce se pak realizují jejich vhodným propojením.
33
VÝROKOVÁ LOGIKA. Normální formy.
Definice 26.
Literál je formule tvaru X nebo --X, kde X je výroková proměnná;
Klauzule je formule tvaru U V • • • V £n, kde n > 1 a každé lije literál.
Duální klauzule je formule tvaru U A • • • A £n, kde n > 1 a každé lije literál.
Formule v koryunktivním normálním tvaru (CNF) je formule tvaru Ci A • • • A Cm, kde m > 1 a každé Čije klauzule.
Formule v disjunktivním normálním tvaru je formule tvaru Ci V • V C kde m > 1 a každé Čije duální klauzule.
Okamžitým důsledkem uěry 21 je následující:
Věta 27. Pro každou formuli cp existuje ekvivalentní formule v disjunktivním normálním tvaru.
34
Věta 28. Pro každou formuli cp existuje ekvivalentní formule v koryunktivním normálním tvaru.
Důkaz. Podle Věty 27 existuje k cp ekvivalentní formule v disjunktivním normálním tvaru, tj. cp « Ví!=i Dt, kde n > 1 a každé D t je duální klauzule. Metaindukcí vzhledem k n:
n = 1. Pak Vt=i Di je současně v CNF. "»» Indukční krok: Nechť D ^ = U A • • • A £k. Platí
n+1 n+1 m m m k
v Dt » DiV\ZDí « D,V/\Ci » ADtVQ « /\/\(«jVCí)
i=1 i=2 i=1 i=1 i=1 j = 1
□
Příklad 29. Formuli (A -> B) A (B -> C) A (C -> A) lze u CiVF reprezentovat jako (-A V B) A (-B V C) A (-C V A) nebo (-A V C) A (-C V B) A (-B V A). CNF tedy není určena jednoznačně až na pořadí klauzulí a literálů.
VÝROKOVÁ LOGIKA. Věta o
35
Věta 30 (o kompaktnosti). Nechť T je soubor formulí výrokové logiky. T je splnitelný právě když každá konečná část T je splnitelná.
Důkaz. Směr „=>" je triviální. Dokážeme „<=". Zavedeme pomocný pojem: soubor V výrokových formulí je dobrý, jestliže každý konečný podsoubor V je splnitelný. Nechťi|)i ,\p2,... Je posloupnost všech formulí výrokové logiky. Metamatematickou indukcí definujeme pro každé i > 1 dobrý soubor St:
Si = T. Soubor Si je dobrý neboť T je dobrý.
Alespoň jeden ze souborů St U a St U musí být dobrý; jinak
existují konečné Ví C St U {i|)t} a Vz C St U {-^i}, které nejsou splnitelné. Jestliže Ví C St nebo V2 C St, máme ihned spor s tím, že St je dobrý; jinak Ví U V2 obsahuje i|) i -op, proto i (Ví U V2) \ {i|h> C St je nesplnitelný, spor.)
i+1
jestliže St U {i|)t} je dobrý;
VÝROKOVÁ LOGIKA. Věta o kompaktnosti.
36
Nechť S = Uí=i Si. Dokážeme, že S má následující vlastnosti: S obsahuje cp právě když S neobsahuje ^cp.
S nutně obsahuje cp nebo --cp. Jestliže S obsahuje cp i --cp, existuje Si obsahující cp i --cp; tedy {cp,^(p} je nesplnitelný podsoubor St, spor.
S obsahuje cp Ai|) právě když S obsahuje cp í \p;
S obsahuje cp Vi|) právě když S obsahuje cp nebo \p;
S obsahuje cp —> \p právě když S neobsahuje cp nebo obsahuje
Buď v valuace definovaná takto: v(A) = 1 právě když A patří do S. Indukcí k délce vytvořující posloupnosti se nyní snadno ověří (s využitím výše uvedených vlastností S), že:
S obsahuje cp právě když v{cp) = 1.
Tedy S (a proto i T) je splnitelný. □
VÝROKOVÁ LOGIKA. Věta o kompaktnosti (použití).
37
Užitím věty 30 lze snadno dokázat řadu dalších tvrzení.
Graf Q je dvojice (U, H), kde U je nejvýše spočetný soubor uzlů a H je areflexivní a symetrická relace na U.
Podgraf grafu G je graf Q' = (U', H'), kde U'ciiaH'CH.
Graf G = (U, H) je k-obarvitelný jestliže existuje funkce f : U —> {1, • • •, k} taková, že f(u) ^ f (v) pro každé (u,v) G H.
VÝROKOVÁ LOGIKA. Věta o kompaktnosti (použití). [38
Věta 31. Graf Q — (U, H) je k-obarvitelný právě když každý konečný podgraj Q je k-obarvitelný.
Důkaz. NechťBuí je výroková proměnná pro každý uzel u a každé 1 < i < k. Buď T soubor tvořený následujícími formulemi:
Buj V • • • V Buk pro každý uzel u;
BU)i —> -Buj pro každý uzel u a každé 1 < i, j < k, kde i 7^ j;
Buí —> -Bví pro každé (u,v) e H a 1 < i < k.
Platí následující pozorování:
Graf (5 je k-obarvitelný právě když soubor T je splnitelný.
Každý konečný podgraf (5 je k-obarvitelný právě když každý konečný podsoubor T je splnitelný.
Nyní stačí aplikovat větu 30. □
VÝROKOVÁ LOGIKA. Odvozovací systém pro C{
V této části se soustředíme na £(—>,-■). Uvažme následující odvozovací systém pro £(—>,-■) (Lukasiewicz, 1928):
Schémata axiómů:
AI: cp —> (\p —> cp)
A2: (cp -> -> £,)) -> ((cp -> -> (cp -> £,)) A3: (--cp —> -op) —> —> cp) Odvozovací pravidlo:
MP: Z cp a cp —»i|) odvoď (modus ponens)
Výroková logika, odvozovací systém pro £(—>,-■)
40
Definice 32. Buď J soubor formulí.
Důkaz formule ty z předpokladů T je konečná posloupnost formulí
cpi, • • •, (Pio fote cpic jeip a pro každé cpt, kde 1 < i < k, platí alespoňjedna
z následujících podmínek:
cpt je prvek J;
cp i je instancí jednoho ze schémat A1-A3;
cpt vznikne aplikací pravidla MP na formule cpm, cpn pro vhodné 1 < m, n < i.
Formule ty je dokazatelná z předpokladů T, psáno T h ty, jestliže existuje důkaz ty z předpokladů T. Jestliže T \- ty pro prázdné T, říkáme že tyje dokazatelná a píšeme h
VÝROKOVÁ LOGIKA. Odvozovací systém pro
41
Příklad 33. Pro libovolnou formuli cp platí I- cp —> cp.
Důkaz. Následující posloupnost formulí je důkazem cp —» cp.
1) (cp -> ((cp -> cp) -> cp)) -> ((cp ^ (cp ^ cp)) ^ (cp ^ cp)) A2
2) cp-> ((cp-> cp)-> cp) AI
3) (cp ^ (cp ^ cp)) ^ (cp ^ cp) MPna2),1)
4) cp -» (cp -» cp) AI
5) cp -> cp MP na4),3)
□
VÝROKOVÁ LOGIKA. Odvozovací systém pro
42
Příklad 34. Pro libovolné formule cp, i|) platí {(p,^cp} h
Důkaz. Následující posloupnost formulí je důkazem ^ z {cp, -'cp}:
1) -cp -» (-i|j -» -cp) AI
2) — cp předpoklad
3) -i|;->-cp MPna2),1)
4) (-i|) -> -cp) -> (cp ->\p) A3
5) cp^ip MPna3),4)
6) cp předpoklad
7) i|) MP na 6),5)
□
VÝROKOVÁ LOGIKA. Věta o dedukci.
43
Věta 35 (o dedukci). Nechť cp, i|) jsou formule a T soubor formulí. Pak T U h cp právě když T h i|) —> cp.
Dů/caz.
„<=": Nechť £,1, • • •, £,k je důkaz formule \p —> cp z předpokladů T. Pak
£,1, • • •, £,ic,\|j, cp je důkaz formule cp z předpokladů T U (poslední formule
vznikne aplikací MP na i|) a £,iJ.
„=>": Nechť £,1, • • •, £,k je důkaz cp z předpokladů T U Metaindukcí k j dokážeme, že T h i|) —> £,j pro každé 1 < j < k.
m* j = 1. Je-li £,1 instance axiómu nebo formule z T, platí T h £,1. K důkazu £,1 z T nyní připojíme formule £,1 -> (\p —> £,1), \p —> £,1. První formule je instancí AI, druhá aplikací MP na £,1 a první formuli. Máme tedy důkaz i|) —> £,1 z T.
Je-li £,1 formule platí T h i|) —> i|) podle příkladu 33.
VÝROKOVÁ LOGIKA. Věta o dedukci.
44
Indukční krok: Je-li formule £,j instancí axiómu nebo prvek T U postupujeme stejně jako výše (místo £,1 použijeme £,j).
Je-li £,j výsledkem aplikace MP na £,m, £,n, kde 1 < m,ri < j, je £,n tvaru £,m —> £,j. Podle I.P. navíc platí Thi|)^£,maThi|)^ (£,m —> £,j). Důkazy i|) —> £,m a i|) —> (£,m —> £,j) z T nyní zřetězíme za sebe a připojíme následující formule:
- -> (£m -> ^)) -> ((^ -> £m) -> M> -> ti))
-> £,m) -> -> £,j)
První formule je instancí A2, další dvě vzniknou aplikací MP. Máme tedy důkaz formule i|) —» £,j z T.
□
VÝROKOVÁ LOGIKA. Věta o korektnosti.
45
Věta 36 (o korektnosti). Nechť cp je formule a J soubor formulí. Jestliže T h cp, pak T \= cp.
Důkaz. Nechť £,1, • • •, £,k je důkaz cp z T. Indukcí vzhledem k j dokážeme, že T h £j pro každé 1 < j < . (Stačí ověřit, že každá instance A1-A3 je tautologie, a že jestliže Th^aTh^^^, pak také T \= £,). □
Výroková logika. Věta o úplnosti. [46
Lema 37. Nechť cp, i|) jsou formule. Pak
(a) I—-cp —> (cp —> ip)
ÍW h —cp -> cp
fcj h cp -> —cp
(d) h (cp -» -» -» -cp)
fe) h cp -> (-l|) -> -(cp ->
É0 l-(cp->i|))->(h(p->i|))->i|)) Dů/coz.
"■^ (a): Podle příkladu 34 platí {cp, —-cp} h \|), proto I—-cp —> (cp —> opakovaným užitím věty o dedukci.
VÝROKOVÁ LOGIKA. Věta o úplnosti
* (b): Platí
1) I—^cp —> (^cp —> -,-,-,cp) podle (a)
2) {^^cp}l—1 cp —> ^^^cp věta o dedukci
3) h (--cp -» -,-,_,(p) —> (~'~,cp —> cp) A3
4) {— cp} I—— cp ^ cp MP na2),3)
5) {^^cp} h cp věta o dedukci
6) h -"-"(p —> cp věta o dedukci
* (c): Platí
1) I—^cp —> ^cp podle (b)
2) h (-'---'(p —> —> (cp —> ~,_,cp) A3
3) hcp->— cp MPna1),2)
VÝROKOVÁ LOGIKA. Věta o úplnosti.
48
(d): Platí
1) {(p —> h (p —> l|)
{— cp} h cp podle (b) a věty o dedukci
3) {cp cp}h\|; MP na2),1)
4) podle (c)
5) {cp Cp}h — \p MP na 3) ,4)
6) {cp —> 1—1—'cp —> --- věta o dedukci
7) h (—cp -> —-> (" —> -cp) A3
8) {cp -> h -> -cp MP na 6) ,7)
9) h (cp ->\|>) -> -> -cp) věta o dedukci
/ÝROKOVÁ LOGIKA. Věta o úplnosti.
(e): Platí
1) {cp, cp ->i|j}I-i|;
2) {cp} h (cp —> \p) —> \p věta o dedukci
3) h(( pakl h cp.
Důkaz. Nejprve uvážíme případ, kdy T je prázdný soubor. Nechť cp je tautologie a Xi, • • •, Xic všechny výrokové proměnné, které se ve cp vyskytují.
Podle Churchova lematu platí [X], • • •, X£} h cp pro libovolnou valuaci v.
Ukážeme, že všechny X^ lze postupně „eliminovat", až dostaneme důkaz cp z prázdného souboru formulí.
Předpoládejme, že pro dané O < n < k jsme již prokázali, že
pro libovolnou valuaci v. Dokážeme, že pak také {Xy-, • • •, X^} h cp pro libovolnou valuaci u.
OT> • • •
x;,x;+1}h(p
VÝROKOVÁ LOGIKA. Věta o úplnosti.
54
Buď tedy u libovolná valuace. Nechť ui, u2 jsou valuace definované takto: ui (Xk) = 1, u2(Xk) = 0, a pro každé Y^Xk platí m (Y) = u2(Y) = v(Y). Platí
1) {X^y • • •, X£, Xn+i} h cp předpoklad pro v = ui
2) {Xy-, • • •, X£, ^Xn+i} h cp předpoklad pro v = u2
3) {Xy, • • •, X^} h Xn+i —> cp věta o dedukci na 1)
4) {Xy, • • •, X^} I—'Xn+i —> cp věta o dedukci na 2)
5) h (Xn+i —> cp) —> ((--Xn+i —> cp) —> cp) podle lematu37 (fl
6) {Xy, • • •, X£} h cp 2x MP na 5) s využitím 3), 4)
VÝROKOVÁ LOGIKA. Věta o úplnosti.
55
Nyní uvážíme obecný případ. Buď T libovolný soubor formulí a cp formule taková, že T \= cp. Podle věty o kompaktnosti existuje konečný soubor {ipi, • • •,i|)n} formulí z T takový, že {ipi, • • •,i|)n} h ^) -> hp -> ~^)) -> p) -> y) -> ((y -> (p) -> (t -> (p))
• Odvozovací pravidlo: MP
Predikátová logika, vznik a vývoj.
61
Predikátová logika (také logika prvního řádu) se opírá o pojem vlastnosti (tj. predikátu). Umožňuje formulovat tvrzení o vlastnostech objektů s využitím kvantifikátorů.
Např. Aristotelova logika je z dnešního pohledu fragmentem predikátové logiky.
Formule prvního řádu byly součástí Fregeho systému, později se objevily ve 3. dílu Schrôderovy monografie Algebra der Logik (1910) a monografii Principia Maťhematica (Whitehead, Russel).
Logika prvního řádu byla definována jako samostatný systém až v monografii Hilberta a Ackermanna Grundzůgen der theoretischen Logik (1928).
Predikátová logika.
62
Definice 41. Jazyk (stejně jako jazyk s rovností) je systém predikátových symbolů a funkčních symbolů, kde u každého symbolu je dána jeho četnost (arita), která je nezáporným celým číslem.
Poznámka 42.
Predikáty arity nula v jistém smyslu odpovídají výrokovým proměnným, funkční symboly arity nula jsou symboly pro konstanty.
Predikátovým a funkčním symbolům se také říká mimologické symboly. Jazyk je tedy plně určen mimologickými symboly.
Rozdíl mezi jazykem a jazykem s rovností se projeví v tom, že do predikátové logiky pro jazyk s rovností pridáme speciální logický symbol =jehož sémantika bude definována speciálním způsobem.
Příklad 43.
Jazyk teorie množin je jazykem s rovností, který obsahuje jeden
predikátový symbol e arity 2.
Jazyk teorie pologrup je jazykem s rovností, který obsahuje jeden funkční symbol „•" arity 2.
Definice 44. Abecedu predikátové logiky pro jazyk C tvorí následující symboly:
Znaky pro proměnné x, y, z,..., kterých je spočetně mnoho
Mimologické symboly, tj. predikátové a funkční symboly jazyka C.
Je-li C jazyk s rovností, obsahuje abeceda speciální znak = pro rovnost.
Logické spojky —> a -■.
Symbol V pro univerzální kvantifikátor.
Závorky {a).
p
REDIKATOVA LOGIKA. Syntaxe.
64
Definice 45. Termem jazyka C je slovo t nad abecedou predikátové logiky pro jazyk C, pro které existuje vytvořující posloupnost slov ti, • • •, tk, kde k > 1, tie je t, a pro každé 1 < i < k má slovo tt jeden z následujících tvarú:
proměnná,
f (tíl, • • •, tírL), kde 1 < ii, • • •, in < k, í je funkční symbol jazyka C, a n je arita f.
Term je uzavřený, jestliže neobsahuje proměnné.
Poznámka 46. U binárních funkčních symbolů (a později také predikátů) dovolíme pro větší čitelnost infíxový zápis. U funkčních (a predikátových) symbolů arity nula budeme psát c místo c().
Příklad 47.
(x • y) • zje termem jazyka pologrup (v prefixové notaci • (• (x, y), z) j 0 + (S(0) + S(S(0)))je termemjazyka 0, S, +, kde 0, S a + jsou po řadě
funkční symboly arity nula, jedna a dva.
Predikátová logika.
Definice 48. Formule predikátového počtu jazyka C je slovo cp nad abecedou predikátové logiky pro jazyk C, pro které existuje vytvořující posloupnost slov ty^, • • •, ipic, kde k > 1, ty^ je cp, a pro každé 1 < i < k má síouo tyi jeden z následujících tvarů:
P (ti, • • •, tn), kde V je predikátový symbol jazyka C arity n a ti, • • •, t-n jsou termy jazyka C.
ti — tj, je-li C jazyk s rovností a ti, tjjsou termy jazyka C.
pro nějaké 1 < j < i, [ty] —> tyy) pro nějaká 1 < j, f < i, Vxi|)j, kde x je proměnná a 1 < j < i.
Poznámka 49. Ve zbytku přednášky budeme používat následující „zkratky":
3x cp značí --Vx --cp
cp V i|) značí —-cp —> \p
cp Ai|) značí ^(cp —>
cp <-> \p značí (cp —> A (i|) —> cp), kde symbol A dále „rozvineme"podle předchozího bodu.
Příklady formulí:
VxP(x,y) A3x(P(x,x) VQ(c)) Vx3x(P(x,x) V Vy VxQ(x))
Syntaxe.
68
Definice 50. Každý výskyt proměnné ve formuli predikátového počtu je buď volný nebo vázaný podle následujícího induktivního predpisu:
Ve formuli tvaru P(ti, • • •, t^)jsou všechny výskyty proměnných volné.
Výrokové spojky nemění charakter výskytů proměnných, tj. je-li daný výskyt proměnné ve formuli ty volný (resp. vázaný), je odpovídající výskyt ve formulích ^ty, cp —> ty, ty —> cp rovněž volný (resp. vázaný).
Ve formuli \/xtyje každý výskyt proměnné x (včetně výskytu za kvantifikátorem) vázaný; byl-li výskyt proměnné různé od x volný (resp. vázaný) ve formuli ty, je odpovídající výskyt ve formuli\/xty rovněž volný (resp. vázaný).
Příklady (volné výskyty jsou červené):
um
+ VxP(x,y) VVy P(x,y)
um
» Vx(P(x,y) VVyP(x,y))
Predikátová logika.
69
Definice 51.
Proměnná se nazývá volnou (resp. vázanou) ve formuli, má-li v ní volný (resp. vázaný) výskyt.
Formule je otevřená, jestliže v ní žádná proměnná nemá vázaný výskyt.
Formule je uzavřená (také sentence), jestliže v ní žádná proměnná nemá volný výskyt.
Zápis cp(xi, • • • ,xn) značí, že všechny volné proměnné ve formuli (pjsou mezi xi, • • •, xn (nemusí nutně platit, že každá z těchto proměnných je volná ve cpj.
Univerzální uzávěr formule cp je formule tvaru Vxi • • • Vxn cp, kde xi, • • •, x^jsou právě všechny volné proměnné formule cp.
Predikátová logika, substituce.
70
Definice 52. Term t je substituovatelný za proměnnou x ve formuli cp, jestliže žádný výskyt proměnné v termu t se nestane vázaným po provedení substituce termu t za každý volný výskyt proměnné x ve formuli cp. Je-li substituovatelný za x ve cp, značí zápis cp(x/t) formuli, která vznikne nahrazením každého volného výskytu x ve cp termem t.
Příklady:
Term y + 3 je substituovatelný za x ve formuli 3zx+ij=z Term ij + z není substituovatelný za x ve formuli 3zx+ij=z (P(x,y) A VxP(x,y))(x/3) je formule P(3,y) A VxP(x,y) P(x>y)(x/y)CyA) Je formule P(x,x)
Predikátová logika, substituce.
71
Definice 53. Nechť cp je formule a ti, • • •, tn termy, které jsou v uvedeném pořadí substituovatelné za proměnné xi, • • • ,xn ue cp (předpokládáme, že xi > • • • > Xnjsou různé). Symbol cp(xi /ti, • • •, xn/tn) značí formuli, která vznikne „simultánním nahrazením" každého volného výskytu x\ termem t\ pro každé 1 < i < n. Přesněji, cp(xi /ti, • • •, xn/'tn) je formule cp(xi /zi) • • • (xn/zn)(zi /ti) • • • (zn/tn), kde zi, • • •, z^jsou (různé) proměnné, které se nevyskytují v ti, • • •, tn ani mezi xi, • • •, xn.
Příklad:
PfeyHx/lMjA) Je formule P(y,x)
REDIKÁTOVÁ LOGIKA. Realizace jazyka.
72
Definice 54. Realizace M jazyka C je zadána
neprázdným souborem M, nazývaným univerzem (případně nosičem). Prvky univerza nazýváme individui.
přiřazením, které každému n-árnímu predikátovému symbolu P přiřadí n-ární relaci P m ticl
přiřazením, které každému m-árnímu funkčnímu symbolu přiřadí funkci f M : Mm -> M.
Ohodnocení j e zobrazení přiřazující proměnným prvky univerza M.
REDIKÁTOVÁ LOGIKA. Realizace jazyka
73
Definice 55. Realizaci termu t při ohodnocení e v relizaciM, psáno tM [e] (případnějen t[e] je-li M jasné z kontextu), definujeme induktivně takto:
x[e] = e{x)
f(ti, • • •, tm)[e] = fM(t! [e], • • •, tm[e])
(pro vn = 0je na pravé stane uvedené definující rovnosti f aa (0)7-
REDIKATOVA LOGIKA. Realizace jazyka.
74
Definice 56 (A. Tarski). Buď M realizace jazyka C, e ohodnocení a cp formule predikátového počtu jazyka C. Ternární vztah M \= cp[e] definujeme indukcí ke struktuře cp:
M h P(ti, • • • ,tm)[e] právě když (ti [e], • • •, tm[e]) G P^.
Jestliže C je jazyk s rovností, definujeme M \= (ti = ti)[e] právě když ti [e] a tj [e] jsou stejná individua.
M \= -i[)[e] právě když neníM \=^\>[é\.
lín*- |= (ajj> —> £J[e] právě když M \= £[e] nebo není M \=*ty[é\.
jVí h Vxi|)[e] právě když M \= i|)[e(x/a)] pro každý prvek a univerza M.
Jestliže M \= cp[e], říkáme, že cp je pravdivá v M při ohodnocení e. Jestliže M h (P(x) A-P(x)))
Neplatí M h PW ^ VxP(x)
Neplatí M h (VxP(x) -> Vx-P(x)) -> Vx(P(x) -> -P(x))
76
Definice 58. Buď £ jazyk (příp. jazyk s rovností).
Teorie (s jazykem Oje soubor T formulí predikátového počtu jazyka C. Prvky T se nazývají axiómy teorie T.
Realizace M jazyka Cje model teorie T, psáno M \= T, jestliže M \= (p pro každé (pzT.
Teorie je splnitelná, jestliže má model.
Je-li M realizace jazyka C, pak Th{M) označuje teorii tvořenou právě všemi uzavřenými formulemi, které jsou v M pravdivé.
Formule cp je sémantickým důsledkem teorie T, psáno T |= cp, jestliže cp je pravdivá v každém modelu teorie T.
Predikátová logika. Teorie.
77
Příklad 59. Uvažme jazyk s rovností obsahující j eden binární funkční symbol "■" a jednu konstantu 1. Nechť! je tvořena následujícími formulemi:
Vx Vij Vz x • (y • z) = (x • y) • z
Vx (x • 1 = x) A (1 • x = x)
Vx Ely (x • y = 1) A (y • x = 1)
Pak formule Vx Vy (x • y) = (y • x) není sémantickým důsledkem T, zatímco formule x • (1 • y) = (1 • x) • y ano.
Schémata výrokových axiómů: Pl: cp —> (\p —> cp)
- P2: (cp_>(^_>y)->((cp->^)->(cp->«) P3: (-cp -> -> -> cp)
Schéma axiómu specifikace:
->- P4: Vx cp —> cp(x/t), kde t je substituovatelný za x ve cp. Schéma axiómu distribuce:
->- P5: (Vx (cp —»—» (cp —» Vxi|)), kde x nemá volný výskyt ve cp. Odvozovací pravidla:
->- MP: Z cp a cp —> ty odvoď ty. {modus ponens] ->- GEN: Z cp odvoď Vxcp. [generalizace]
p
REDIKATOVA LOGIKA. Odvozovací systém.
Je-li C jazyk s rovností, přidáme dále následující axiómy rovnosti: Rl: x = x
R2: [xi=yi A • • •Axn=yn A P(xi, • • • ,xn)) -> P(m > • • • >yn). kde P je predikátový symbol arity n.
^ R3: {x^=y^ A--- Axm=ijm) -> (f (xi, • • • ,xm)=f (m, • • • ,ym)), kde f je funkční symbol arity m.
p
REDIKATOVA LOGIKA. Odvozovací systém.
80
Definice 60. Bud T teorie jazyka C.
Důkaz formule i|) v teorii T je konečná posloupnost formulí cpi, • • •, cpk, kde cp icje i|) a pro každé cpt, kde 1 < i < k, plaŕí alespoň jedna z následujících podmínek:
->- cp i je prvek J;
->- cp t je instancí jednoho ze schémat P1-P5;
£Je jazyk s rovností a cpi je instancí jednoho ze schémat R1-R3;
->- cpi vznikne aplikací pravidla MP na formule cpm, cpn pro vhodné 1 < m, n < i.
->- cpi vznikne aplikací pravidla GEN na formuli cpm pro vhodné 1 < m < i.
p
REDIKATOVA LOGIKA. Odvozovací systém.
81
Formule i|) je dokazatelná v teorii T, psáno T h ^, jestliže existuje důkaz i|) u T. Jestliže T h i|) pro prázdne T, říkáme že i|) je dokazatelná a píšeme
Formule i|) je vyvratitelná v teorii T, jestliže TI—^
Teorie T je sporná (též inkonzistentní), jestliže každá formule predikátové logiky jazyka C je v T dokazatelná.
Teorie je bezesporná (též konzistentní), jestliže není nekonzistentní.
Predikátová logika.
82
Poznámka 61 (Princip dosazení do tautologie výrokového počtu). Je-li cp tautologií £(-■,—>), ve které nahradíme výrokové proměnné formulemi predikátové logiky tak, že daná výroková proměnná je nahrazena vždy touž formulí, obdržíme formuli predikátové logiky, která je dokazatelná v odvozovacím systému predikátové logiky pouze pomocí P1-P3 a MP.
Poznámka 62 (Neplatnost „obecné" věty o dedukci). Za předpokladu korektnosti odvozovacího systému pro predikátovou logiku neplatí h cp —> Vx cp. Platí ovšem {cp} h Vx cp. Proto obecně neplatí, že T \= cp —> ty právě když T U {cp} \= ty.
83
Věta 63 (o dedukci). Nechť! je teorie jazyka C, i|) uzavřená formule jazyka C a cp (libovolná) formule jazyka C. Pak T h i|) —> cp právě když T U h cp.
Dů/caz.
Důkaz je velmi podobný důkazu uěry 35:
„=>": Nechť £,i, • • •, £,k je důkaz formule i|) —> cp v T. Pak £,i, • • •, £,k) \p, cp je důkaz formule cp v T U (poslední formule vznikne aplikací MP na i|) a £,k).
„<=": Nechť £,i, • • •, £,k je důkaz cp v T U Metaindukcí k j dokážeme, že T h i|) —> £,j pro každé 1 < j < k.
m* j = 1. Je-li £,i instance axiómu nebo formule z T, platí T h £,i. K důkazu £,i z T nyní připojíme formule £,i -> (\p —> £,i), \p —> £,i. První formule je instancí Pl, druhá aplikací MP na £,i a první formuli. Máme tedy důkaz i|) —> £,i v T.
Je-li £,i formule platí T h i|) —> i|) podle příkladu 33 a poznámky 62.
Predikátová logika, věta o dedukci.
84
Indukční krok: Je-li formule £,j instancí axiómu nebo prvek T U postupujeme stejně jako výše (místo £,1 použijeme £,j).
Je-li £,j výsledkem aplikace MP na £,m, £,n, kde 1 < m,ri < j, je £,n tvaru £,m —> £,j. Podle I.P. navíc platí Thi|)^£,maThi|)^ (£,m —> £,j). Důkazy i|) —» £,m a i|) —» (£,m —» £,j) v T nyní zřetězíme za sebe a připojíme následující formule:
-> £,m) —> (M^ —> )
První formule je instancí P2, další dvě vzniknou aplikací MP. Máme tedy důkaz formule i|) —> £,j v T.
Predikátová logika, věta o dedukci. \K
Je-li £,j výsledkem aplikace GEN na £,m, kde 1 < m < j, je £,j tvaru Vx £,m. Podle I.P. platí T h i|) —> £,m. K tomuto důkazu nyní stačí připojit formule
^ Vx -> £,m)
^ Vx (\|) -> £,m) -> -> Vx £,m) ty -> Vx£,m.
První vznikne aplikací GEN, druhá je instancí P5, třetí vznikne aplikací MP. Dostaneme tak důkaz formule i[) —> £,j v T.
□
p
REDIKATOVA LOGIKA. Vlastnosti kvantifikace. [86
Lema 64. Pro každé formule cp aty platí:
1. h (Vx (cp —> <-> (cp —> \/xty), pokudx není volná ve formuli cp;
2. h (Vx (cp —> <-> px cp —> , pokud x není volná veformulity;
3. h px (cp —> ty)) <-> (cp —> žbcíp), pokudx není volná ve formuli cp;
4. h px (cp —> <-> (Vx cp —> ty), pokud x není volná ve formulity.
Důkaz. Pozorování:
(a) Jestliže h cp —> ty a současně h i|) —> cp, pak h cp <-> To plyne z toho, že (A —> B) —> ((B —> A) —> (A <-> B)) je výroková tautologie (viz poznámka 61).
(b) (tranzitivita implikace). Jestliže T h cp —> £, a současně T h £, —> ty, pak T h cp —> Stačí použít poznámku 61 a tautologii
(A -> C) -> ((C -> B) -> (A -> B)).
REDIKATOVA LOGIKA. Vlastnosti kvantifikace.
87
(c) Nechť cp(x), i|)(x) jsou formule. Pak h Vx (cp —> —> Vx (-op —> --(p), neboť
1) h Vx(cp ->\|>) -> (cp P4
2) h (cp —> ip) —> (--i|j —> --cp) výr. tautologie
3) h Vx (cp —> —> (--ip —> --(p) tranz. impl. na 1), 2)
4) Vx (cp —> t|>) I—a|) —> --cp věta o dedukci
5) Vx(cph Vx(-\|>->-- —> Vx (--ip —> --(p) věta o dedukci
Tvrzení 1.-4. teď dokážeme za předpokladu, že cp(x) ai|)(x). Obecná podoba vyplyne užitím věty konstantách (viz dále).
PREDIKÁTOVÁ LOGIKA. Vlastnosti kvantifikace.
1. Platí h (Vx (cp —> ty)) —> (cp —> Vxi|)), neboť tato formule je instancí P5. Důkaz opačné implikace vypadá takto:
1) hVxty^ty
2) h (Vxi|) —> —> ((cp —> Vxi|)) —> (cp —>
(A -> B) -> ((C -> A) -> (C -> B)) je tautologie, viz pozn. 61
3) h (cp —> Vxi|)) —> (cp —>
4) (p ^ \/xty \- (p ^ ty
5) cp —> Vxi|) h Vx (cp —> ty)
P4
MP na 1),2) věta o dedukci
GEN
6) h (cp -> \/xty) -> (Vx (cp -> ty))
věta o dedukci
p
REDIKATOVA LOGIKA. Vlastnosti kvantifikace. [89
2. Nejprve ukážeme, že h Vx (cp —»\p) —» (3x cp —»
1) h Vx (--ip —> --cp) —> (--ip —> Vx^cp) podiel.
2) h Vx (cp —> —> Vx (^i|) —> --cp) podle (c)
3) h Vx (cp —> —> (--ip —> Vx^cp) tranz. impl. na 2), 1)
4) h (-i|) -> Vx-cp) -> (-Vx-cp -> taut. (-B -> A) -> (-A -> B)
5) h Vx (cp —> —> (^Vx^cp —> tranz. impl. na 3), 4)
6) h Vx (cp —»—» (3x cp —> \p) reformulace
i
REDIKATOVA LOGIKA. Vlastnosti kvantifikace.
90
Nyní opačný směr h (Ebc cp —> ^ Vx (cp —> ty):
1) -> Vx^cp) —> Vx(- ^ty —> - podle 1.
2) h (-Vx- ^cp —> \p) —> ^ Vx- cp) taut. (-B -> A) -> (-A -> B)
3) h (-Vx- ^cp —> \p) —> Vx(- —> - cp) tranz. impl. na 1), 2)
4) 3x cp —> ty \-\/x (-oj; —> věta o dedukci
5) 3x cp —> l|) 1—~> ~ -cp P4aMP
6) 3x cp —> \p I— cp —> \p (-A -> -B) -4(A^B)aMP
7) 3x cp —> l|) h Vx (cp - ^) GEN
S) h (3x (p —> \p) —> Vx (cp - věta o dedukci
□
Predikátová logika, věta o korektnosti.
91
Věta 65. Nechť T je teorie a cp formule jazyka teorie T. Jestliže T h cp, pak Thcp.
Důkaz. Stačí ověřit následující tvrzení:
Je-li i|) instancí jednoho ze schémat P1-P5 (příp. také R1-R3, pokud jazyk teorie T je jazyk s rovností) a M je model T, pak M \=
Je-li jVř model T a £, formule jazyka teorie T, kde M \= \p a
Je-li jVř model T a i|) formule jazyka teorie T, kde M \= pak .M |= Vxip.
Metaindukcí vzhledem k i je pak již triviální ukázat, že je-li ipi, • • • ,\pk důkaz formule cp v T a M je model T, pak T \= \|h pro každé 1 < i < k. □
Lema 66. Následující tvrzení jsou ekvivalentní:
1. Pro každou teorii T a pro každou formuli cp jazyka teorie T platí, že jestliže T \= cp, pak T h cp.
2. Každá bezesporná teorie má model. Důkaz.
(1. => 2.) Buď T bezesporná teorie. Pak existuje formule cp jazyka teorie T, která není v T dokazatelná (tj. T \f cp). Obměnou 1. pak ale dostáváme, že cp není sémantickým důsledkem T (tj. T ^ cp). To znamená, že existuje takový model T, kde není pravdivá cp. Zejména má tedy T model.
(2. => 1.) Užitím 2. dokážeme obměnu 1. Nechť tedy T \f cp, a nechť čp je univerzální uzávěr cp. Ukážeme, že T U {^čp} je bezesporná; pak podle 2. má T U {^čp} model, tedy T ^ cp.
T U {^čp} je bezesporná: Předpokládejme naopak, že T U {^čp} je sporná. Pak
1) TU{^čp} h "čp TUcp}je sporná
2) TI—'čp —» čp věta o dedukci
3) h (--"čp —> čp) —> čp (A —> B) —> B je tautologie, viz pozn. 62
4) Thčp MP na2),3)
5) T h cp opakovaně P4 a MP Obdrželi jsme tedy spor s tím, že T \f cp.
Cílem dalšího postupu je dokázat, že každá bezesporná teorie má model. Tato konstrukce obsahuje dva základní obraty:
Zavede se pojem kanonické struktury pro danou teorii T. Tato struktura obecně není modelem T. Ukážeme, že pokud T vyhovuje dalším podmínkám (je henkinovská a úplná), pak kanonická struktura je modelem T.
Ukážeme, že každou bezespornou teorii je možné vhodným způsobem rozšířit tak, aby byla henkinovská a úplná.
95
Definice 67.
Teorie S je rozšíření teorie T, jestliže jazyk teorie S obsahuje jazyk teorie Jav teorii S jsou dokazatelné všechny axiómy teorie T.
Rozšíření S teorie T se nazývá konzervativní, jestliže každá formule jazyka teorie T, která j e dokazatelná v S, je dokazatelná ivl.
Teorie S a T jsou ekvivalentní, jestliže S je rozšířením T a současně T je rozšířením S.
Predikátová logika, věta o konstantách.
96
Věta 68 (o konstantách). Nechť S je rozšíření! vzniklé obohacením jazyka teorie T o nové navzájem různé konstanty ci, • • •, Ck (nové axiómy nepřidáváme), a nechť x^, • • •, x^jsou navzájem různé proměnné. Pak pro každou formuli cp jazyka teorie T platí, žel h cp právě když
S h CpíXi/Cij-'-jXTc/Cic).
Důkaz. Jelikož ci, • • •, c^ jsou navzájem různé, stačí dokázat, že T h cp právě když S h cp (x/c).
=>: K důkazu cp v T pripojíme formule Vx cp, Vx cp —» cp(x/c), (p(x/c) a obdržíme tak důkaz formule (p(x/c) v S.
<=: Nechť , • • • je důkaz cp(x/c) v S. Nechť-y je proměnná, která se nevyskytuje v tomto důkazu. Indukcí k i ukážeme, že pro každé 1 < i < k je tyi (c/y)> • • • >^i(c/y) důkaz v T. Rozlišíme tyto možnosti:
Predikátová logika, věta o konstantách.
97
Je-li ipt instancí P1-P5 (příp. R1-R3), je také iMc/y) instancí téhož schématu.
Je-li i|)t axióm teorie T, pak se v \|h nevyskytuje c a formule \|h a iMc/y) jsou tedy totožné.
Jestliže i|)t vyplývá z a i|)m pomocí MP, je i|)m tvaru —> ipt a formule i|)m(c/ij) je tedy formulí ipj(c/y) —> i\>i{c/y). Takže formule iMc/y) vyplývá z {c/y) a ipm(c/y) pomocí MP.
Jestliže i|)t vyplývá z pomocí GEN, je ipt tvaru Vxi|)j. Stačí si uvědomit, že (Vxi|)j)(c/ij) je tatáž formule jako Vx (^(c/y)), neboťx a -y jsou různé.
Predikátová logika, věta o konstantách.
Ukázali jsme, že T h cp (x/c) (c/y). Dále
1) Thcp(x/y)
2) T^Vy (cp(x/y)(ij/x))
4) T h cp(x/y)(y/x)
5) Thcp
cp(x/y) je totéž co cp(x/c)(c/y)
GEN
P4
MP na 2) ,3)
cp(x/ij)(ij/x) je totéž co cp
Predikátová logika. Henkinovské a úplné teorie.
99
Definice 69.
Teorie T je henkinovská, jestliže pro každou formuli cp jazyka teorie T s jednou volnou proměnnou x existuje v jazyce teorie T konstanta c taková, žel h 3xcp —> cp(x/c).
Teorie T je úplná, jestliže je bezesporná a pro každou uzavřenou formuli cp jejího jazyka platí buď T h cp nebo TI—'(p.
^EDIKÁTOVÁ LOGIKA. Henkinovské a úplné teorie.[Jôô
t> -
Věta 70 (o henkinovské konstantě). Buď J teorie a cp(x) formule jejího jazyka. Je-li S rozšírení T, které vznikne přidáním nové konstanty a formule 3x cp —> (p(x/c 3y£,(x/y):
1) {Vryx/uiihVryx/u)
2) {Vy-£(x/y)}h-£(x/y)(y/x) P4 a MP
3) {Vij-£,(x/ij)} h přepis
4) {Vij-£,(x/ij)}h Vx-£, GEN
5) h Vy-,£,(x/-y) —> Vx-£, dedukce
6) h 3x£, -> 3y£,(x/y) taut. (A -> B) -> (-B -> -A) a MP.
ň
REDIKATOVA LOGIKA. Henkinovské a úplné teorie.
101
Nechť R značí teorii vzniklou pouhým přidáním konstanty c cp (x/c (p)) —> \p
3) T h pxcp —> (p (x/y)) —> ty
4) T h Vy (pxcp -> cp(x/y)) ->
5) T h Elijpxcp —» cp(x/y)) —» \p
6) h pxcp -> 3ijcp(x/ij))
7) T h pxcp -> 3ijcp(x/ij))
8) h Bxcp -> 3y cp {x/y)
9) T h ty
3y pxcp ty
předpoklad
S = R U pxcp —> cp(x/C(p)}
a dedukce
věta o konstantách
GEN
lema 64 (2) a MP cp (x/y)) lema 64 (3)
tranz. implikace dokázáno výše MP
□
p
102
REDIKATOVA LOGIKA. Henkinovské a úplné teorie.
Věta 71 (o henkinovském rozšírení). Ke každé teorii existuje henkinovská teorie, která je jejím konzervativním rozšířením.
Důkaz. Buď T (libovolná) teorie. Pro každé n > 0 definujeme teorii Tn takto:
To = T. Teorie Tí+i vznikne z Tt tak, že pro každou formuli cp(x) jazyka teorie Tt přidáme novou konstantu c -
V následující větě předpokládáme existenci dobrého uspořádání na souboru všech uzavřených formulí daného jazyka. Je-li uvažovaný jazyk nespočetný, opírá se tento předpoklad o axióm výběru.
Věta 72 (o zúplňování teorií). Ke každé bezesporné teorii existuje její rozšíření se stejným jazykem, které je úplnou teorií.
Důkaz. Buď T teorie, a nechť ^ je dobré uspořádání na množině všech uzavřených formulí jazyka teorie T. Pro každou uzavřenou formuli (p jazyka teorie T definujeme teorii induktivně takto:
Je-li cp nejmenší prvek v uspořádání ^, klademe = T,
um
+ Jinak To, = <
(J Te U{-cp} jinak.
p
REDIKATOVA LOGIKA. Henkinovské a úplné teorie] 104
f -
Indukcí vzhledem k -< dokážeme, že každé je bezesporné rozšírení T. Je-li cp nejmenší prvek v uspořádání není co dokazovat. Indukční krok: Označme symbolem S teorii U^cp
->- Teorie S je nutně bezesporná. Jinak S h i|) A --ip pro nějakou formuli Jelikož tento důkaz používá jen konečně mnoho axiómů teorie S, nutně existuje £, -< cp takové, že obsahuje všechny použité axiómy. Proto h i|) A -op, což je spor s IP.
->- Je-li T(p = SU {cp}, je bezesporná.
->- Je-li T(p = SU {^cp}, je teorie S U {cp} sporná. Pokud by byla sporná také teorie S U {^cp}, platilo by S U {cp} I—'(p a S U {^cp} h cp, proto i S h cp ^ ^(p a S I—'cp —» cp (užitím věty o dedukci). Z toho dostáváme S h i|) A-i|) pro libovolné neboť (A -> -A) -> ((-A -> A) -> A-i|))) je výroková tautologie (použijeme 2x MP). Tedy i S je sporná, což je spor s předchozím bodem.
^EDIKÁTOVÁ LOGIKA. Henkinovské a úplné teorieHôE
t> i-
Uvažme teorii U která vznikne sjednocením všech T " je triviální. Pro opačnou implikaci stačí ukázat, že T je bezesporná (pak T má model podle věty o úplnosti). Kdyby T byla sporná, existoval by důkaz formule i|) A v T. Tento důkaz je konečný, využívá tedy jen konečně mnoho axiómů T, které tvoří spornou podteorii T, spor. □
PREDIKÁTOVÁ LOGIKA. Lowenheimova-Skolemova větta
Poznámka 78. Z důkazu věty 71 plyne, že každá bezesporná teorie s jazykem bez rovnosti má model kardinality max{|L|, K0} (při rozšírení teorie na henkinovskou bylo přidáno |L| • Ko nových konstant). Toto pozorování neplatí pro teorie s jazykem s rovností (např. pro T = {Vxx=c}. Nicméně lze dokázat následující:
Věta 79. Nechť ~X je teorie a nechť pro každé u e N existuje model teorie T jehož nosič má mohutnost alespoň n. Pak T má nekonečný model.
Důkaz. Je-li jazyk teorie T jazykem bez rovnosti, plyne tvrzení ihned
z poznámky 78. Jinak pro každé n G N definujeme formuli
cpn = Vxi • • • Vxn3ij x! T^y A • • • A x^y a teorii Sn = T U {cpi, • • •, cpn}. Podle
předpokladu věty má každá Sn model. Podle věty o kompaktnosti má proto
model i teorie Uili Sn- Tento model je nutně nekonečný a je i modelem
teorie T. □
PREDIKÁTOVÁ LOGIKA. Lowenheimova-Skolemova ufefcK
Věta 80 (Lowenheimova-Skolemova). Nechť! je teorie s jazykem L, která má nekonečný model. Nechť k je nekonečný kardinál takový, že k > |L|. Pak ! má model mohutnosti k.
Důkaz. Nechť M je nekonečný model T. Jazyk L rozšíříme o systém {ct | i < k} nových konstant a k T přidáme axiómy {ct 7^ Cj | i, j < k}. Obdržíme tak teorii !f. Nechť K je konečná část !f, a nechť ci, • • •, cn jsou všechny nově přidané konstanty, které se vyskytují ve formulích teorie K (takových konstant je jen konečně mnoho). Pokud tyto konstanty realizujeme navzájem různými prvky nosiče M, obdržíme model teorie K. Každá konečná část !' je tedy splnitelná. Podle věty o kompaktnosti má tedy model i teorie !'. Nosič tohoto model ale nutně obsahuje alespoň k navzájem různých individuí. □
v
ETA O NEÚPLNOSTI. Úvod.
118
Jazyk aritmetiky je jazyk s rovností obsahující konstantu 0, unární funkční symbol S a dva binární funkční symboly * a +.
Význačnou realizací jazyka aritmetiky je (No, *, + ), kde univerzem je soubor všech nezáporných celých čísel, 0 je realizováno jako nula, S jako funkce následníka, * jako násobení, + jako sčítání. (Relační predikáty jako <, < lze snadno definovat.)
Jedním ze základních kroků Hubertova programu formalizace matematiky mělo být vytvoření rekurzivní a úplné teorie T jazyka aritmetiky.
ne-
šlovém „úplné" se myslí, že T h (p právě když (p e Th(No, *, +) (Tj. formule dokazatelné v T jsou právě formule pravdivé v (No, *, +)).
Slovo „rekurzívní" intuitivně znamená, že musí být „mechanicky ověřitelné", zda daná posloupnost symbolů je či není důkazem v T (možných formalizací tohoto pojmu je více).
Z Gôdelových výsledků plyne, že taková teorie neexistuje.
VĚTA O NEÚPLNOSTI. Turíngův stroj.
119
Alan Turing (1912-1954)
Definoval pojem Turingova stroje a s jeho pomocí ukázal, že problém pravdivosti formulí prvního řádu je nerozhodnutelný.
Považován za zakladatele informatiky (jako vědy).
Turíngův stroj je matematickým modelem „hloupého odvozovače", který má k dispozici papír, tužku a gumu, a který si pamatuje konečně mnoho schémat axiómů.
Význam Turingova stroje coby modelu reálných výpočetních zařízení se projevil až v druhé polovině 20. století.
120
VĚTA O NEÚPLNOSTI. Turíngův stroj (neformálně).
Základní pojmy:
Je-li I konečná abeceda, značí symbol I* soubor všech konečných slov složených z prvků I (prázdné slovo značíme symbolem e). Délku slova w značíme íen(w). Pro každé 1 < i < íen(w) značí symbol w(i) i-tý znak slova w (zleva). Jazyk nad abecedou I je podmnožina I*.
Turingův stroj je matematický model výpočetního zařízení, které je vybaveno konečně-stavovou řídící jednotkou („hlava odvozovače"), jednosměrně nekonečnou pracovní páskou („papír"), a čtecí/zápisovou hlavou („tužka/guma").
Na začátku výpočtu je na pásce zapsáno konečné vstupní slovo, hlava je na nejlevější pozici, a stavová jednotka je v počátečním stavu.
Stroj na základě svého momentálního kontrolního stavu a symbolu pod čtecí hlavou provede „výpočetní krok", tj. změní svůj kontrolní stav, nahradí symbol pod čtecí hlavou jiným symbolem, a posune čtecí hlavu vlevo nebo vpravo.
VĚTA O NEÚPLNOSTI. Turíngův stroj (neformálně).
121
Výpočet se zastaví, pokud stroj dojde do konfigurace, jejíž kontrolní stav je akceptující nebo zamítající. Pro některá slova může stroj také nezastavit (cyklit).
Vstupní slovo je akceptované, jestliže stroj po konečně mnoha krocích dojde do akceptující konfigurace. Soubor všech vstupních slov, která stroj akceptuje, tvoří jazyk akceptovaný daným strojem.
VĚTA O NEÚPLNOSTI. Turingův stroj (formálně). [t22
Definice 81. Turingův stroj je devítice M = (Q, I, r, B, •, 6, q o, Acc, Rej), kde + Q je konečný soubor kontrolních stavů; + L je konečná vstupní abeceda; + V je konečná pásková abeceda (kde I C V); ♦ B e V je prázdný znak; + • £ V je znak konce pásky;
+ 6 : Q x T ^ Q x ľ x {L, R} je přechodová funkce, kde pro každé y e Q platí Mp > •) = ( °í > •> R) Pro nějaké q e Q;
^ qo G Q je počáteční stav; + Acc C Q je množina akceptujících stavů; + Rej C Q \ Acc je množina zamítajících stavů.
VĚTA O NEÚPLNOSTI. Turíngův stroj (formálně).
Nechť o, # 0 Q u T, a nechť C (M) = (ľ U {#}) x (Q U {o}). Prvky C [M) zapisujeme ve tvaru [X, q].
Konfigurace stroje M. je slovo [Xi ,pi] • • • [Xn,Pn] [#, °] G C(M)* takové, že u > 1, Xi = •, Xi 7^ # pro každé 1 < i < u, a existuje právě jedno 1 < j < n, kde pj G Q Slovo Xi • • • Xn nazývame obsahem pásky dané konfigurace, a stav p j kontrolním stavem dané konfigurace.
Akceptující resp. zamítající konfigurace je konfigurace, jejíž kontrolní stav je akceptující resp. zamítající. Koncová konfigurace je konfigurace, která je akceptující nebo zamítající. Soubor všech konfigurací stroje M. značíme Conf(M).
Krok výpočtu je funkce step : Conf(M) —> Corif (M), která je pro koncové konfigurace definována jako identita a pro nekoncové konfigurace takto:
sŕep(y[X,q][Y,o]p) = y [Z, o] [Y, r] p jestliže ô (q, Y) = (r, Z, R)
sŕep(y [Y, o] [X, q] p) = y [Z, o] [Y, t] p jestliže ô (q, Y) = (r, Z, L)
step(y [X, q] [#,o]) =y[Z,o] [B,r] [#,o] jestliže 6(q,Y) = (r, Z, R)
123
VĚTA O NEÚPLNOSTI. Turíngův stroj (formálně).
124
Nechť w = ai • • • an je slovo nad abecedou I (w může být i prázdné). Iniciální konfigurace pro w je konfigurace oc(w) = [•, qo][ai, o] • • • [an, o] [#, o]. Slovo w je akceptované strojem M, jestliže existuje k g N takové, že stepk(a(w)) je akceptující konfigurace. Jazyk akceptovaný strojem M, označovaný L(M), je soubor všech w g I*, které jsou akceptované strojem M.
Nechť ([Xi ,pi], [X2,P2], [Yi, qi], [Y2, q2]) je čtveřice symbolů z C(M). Tato čtveřice je kompatibilní, jestliže existuje nekoncová konfigurace oc g Conf(M) a vhodné 1 < i < len(oc) takové, že a(i) = [Xi ,pi], a(i-hl) = [X2,P2] a dále (3(i) = [Yi, q 1 ], (3(i+l) = [Y2, q2] kde |3 = step(oc). Soubor všech kompatibilních čtveřic stroje M označme Comp(M). Soubor Comp(M) lze snadno „vypočítat" na základě toho, jak vypadá přechodová funkce 6.
Nechť oc g Conf (M.) je konfigurace a nechť |3 g C(M)* je slovo stejné délky, jako má oc. Pak (3 = step(oc) právě když pro každé 1 < i < len(oc) platí, že (a(i),a(i+l),P(i),P(i+l)) g Comp{M).
125
VĚTA O NEÚPLNOSTI. Vlastnosti jazyků.
Nyní zavedeme několik pojmů, které se týkají jazyků.
Jazyk L C I* je rekurzivně vyčíslitelný, jestliže L = L (M.) pro nějaký Turingův stroj M. Jazyk L C I* je rekurzivní, jestliže L = L (M.) pro nějaký Turingův stroj JVL, který zastaví pro každé vstupní slovo. Jednoduché pozorování je, že jazyk L C I* je rekurzivní právě když L i L jsou rekurzivně vyčíslitelné (kde L = I* \ L).
Předpokládejme, že kontrolní stavy a symboly páskové abecedy každého Turingova stroje jsou prvky nějaké fixní spočetné množiny (to lze bez újmy na obecnosti). Pak každý Turingův stroj M. lze jednoznačně zapsat jako slovo code(M) g {0,1}*. Podobně každé vstupní slovo w stroje M. lze jednoznačně zapsat jako slovo code(w) g {0,1}*. Navíc lze předpokládat, že každé v g {0,1}* je kódem nějakého stroje Mv a nějakého vstupního slova wv stroje Mv.
Uvedené kódování umožňuje zkonstruovat univerzální Turingův stroj U se vstupní abecedou {0,1, #} takový, že pro každé slovo tvaru u#v, kde u, v g {0,1 }*, platí, že U akceptuje u#v právě když stroj Mu akceptuje slovo wv.
Uvažme jazyk Accept= {u#v | Mu akceptuje wv}. Podle předchozího boduje Accept rekurzívně vyčíslitelný. Ukážeme, že Accept není rekurzívní. Podle jednoho z předchozích bodů pak jazyk Accept není rekurzivně vyčíslitelný.
126
VĚTA O NEÚPLNOSTI. Jazyk Accept.
Věta 82. Jazyk Accept není rekuzivní.
Důkaz. Předpokládejme, že existuje Turingův stroj M, který zastaví pro každé vstupní slovo a L(M) = Accept. Buď M/ stroj se vstupní abecedou {0,1}, který funguje následovně:
M/ pro dané vstupní slovo u nejprve „vyrobí" na pásce slovo u#u.
Pak M/ přesune čtecí hlavu úplně vlevo a dále se začne chovat jako stroj M s tím rozdílem, že se zamění akceptující a zamítající stavy.
Výsledkem je, že u e L(M/) právě když u#u 0 L(M)
Nechť v code(JVť). Platí wv e L(M')?
Ano. Pak v#v 0 L(M), tj. Mv = M/ neakceptuje wv, spor.
Ne. Pak v#v G L(M), tj. Mv = Mr akceptuje wv, spor.
Z předpokladu existence stroje M se nám podařilo odvodit spor. Stroj M tedy neexistuje. □
VĚTA O NEÚPLNOSTI. Peanova aritmetika. IH
Jedním z pokusů o vytvoření rekurzivní a úplné teorie aritmetiky byl následující systém nazývaný Peanova aritmetika (seznam Peanových axiómů bývá v literatuře uváděn v různých podobách):
Vx S(x) 7^0
VxVy S(x)=S(-y) —> x=y Vx x+0 = x
VxVy x+S(/y) = S(x+ij) Vx x*0 = 0
VxVij x*S(ij) = (x*-y) +x
(cp(0) AVx (cp(x) —> cp(S(x)))) —> Vxcp(x), kde cp je formule s jednou volnou proměnnou x.
v
ETA O NEÚPLNOSTI. Peanova aritmetika.
128
Každou formuli jazyka aritmetiky je možné zapsat jako slovo nad abecedou {v, + , *, 0, S, (,), V, —>, =, #}. Různé proměnné zapisujeme jako řetězce složené z v různé délky (např. místo x,y, z můžeme psát v, w, vvv apod.). Podobně můžeme i každou konečnou posloupnost formulí zapsat jako slovo nad uvedenou abecedou, kde symbol # použijeme pro oddělení jednotlivých formulí.
Definice 83. Teorie J jazyka aritmetiky je rekurzivní, jestliže jazyk tvořený zápisy všech důkazů v J je rekurzivní.
Lze snadno (i když technicky) dokázat, že např. Peanovy axiómy tvoří rekurzivní teorii. Definici rekurzivity teorie lze samozřejmě rozšířit i na teorie nad jinými jazyky. Rekurzivní teorie odpovídají (na intuitivní úrovni) právě teoriím, které umožňují „mechanické odvozování". Triviální pozorování o rekurzivních teoriích podává následující věta.
Věta 84. Nechť J je rekurzivní teorie jazyka aritmetiky. Pak jazyk tvořený všemi formulemi dokazatelnými v J je rekurzivně vyčíslitelný.
VĚTA O NEÚPLNOSTI. Jazyk Valid.
129
Nechť Valid je jazyk nad abecedou {v, + , *, 0, S, (,), V, —>, =} obsahující zápisy všech formulí teorie Th(No, *, + ). Naším cílem je dokázat, že Valid není rekurzivně vyčíslitelný jazyk.
Věta 85. Jazyk Valid není rekurzivně vyčíslitelný.
Důkaz. Ukážeme, že existuje Turingův stroj M, který pro každé vstupní slovo v nad abecedou {0,1, #} zastaví v konfiguraci, kdy je na pásce zapsáno slovo w nad abecedou {v, + , *, 0, S, (,), V, —>, =} takové, že v g Accept právě když w e Valid. Pokud by tedy jazyk Valid byl akceptovaný nějakým strojem M/, stačilo by „napojit stroje M a M' za sebe" a dostali bychom stroj akceptující jazyk Accept, což je spor.
VĚTA O NEÚPLNOSTI. Jazyk Valid. [Jšô
Stroj M. nejprve „prověří" vstupní slovo: pokud není tvaru u#v, M. smaže vstupní pásku a zapíše na ní (nějakou) pravdivou formuli. Jinak M. „nalezne" prvočíslo p, takové, že p > |C(MU)|. Pozorování:
Jestliže zapisujeme čísla v soustavě o základu p, potřebujeme p „číslic" [0], • • •, [p—1]. Každému symbolu z C(MU) lze tedy přiřadit jedinečnou „číslici". Dále nebudeme rozlišovat mezi symboly souboru C(MU) a jim přiřazenými číslicemi.
Každé konfiguraci stroje Mu pak odpovídá číslo v soustavě o základu p. Zápis tohoto čísla získáme tak, že symboly konfigurace zapíšeme v opačném pořadí. Např. konfiguraci [•, o] [X, o] [Y, q] [Z, o] [B, o] [C, o] [C, o] [#, o] zapíšeme jako číslo
[#, o] [C, o] [C, o] [B, o] [Z, o] [Y, q] [X, o] [•, o]
Mu akceptuje slovo wv právě když existuje konečná posloupnost konfigurací ocoy oči, • • •, an s následujícími vlastnostmi:
oco je počáteční konfigurace pro slovo wv.
(Xi+i = step(íXi) pro každé 0 < i < n
(xn je akceptující.
VĚTA O NEÚPLNOSTI. Jazyk Valid.
131
Bez újmy na obecnosti můžeme předpokládat, že zápisy konfigurací
oco, cxi, • • •, oírx mají stejnou délku. (Zápisy „krátkých" konfigurací lze „doplnit"
zprava symboly [B, o], zapsanými těsně před symbol [#, o].)
Posloupnost konfigurací oco, ai, • • •, an lze tedy opět zapsat jako číslo v soustavě o základu p. Zápis tohoto čísla vypadá takto: [an] [an_i] • • • [oco], kde [oci] je zápis konfigurace ocí tak, jak bylo popsáno výše.
Sestrojíme formuli ACOMP(y), která říká, že y reprezentuje akceptující výpočet stroje Mu na slově wv. Tj. ACOMP(y/k) platí právě když zápis čísla k v p-ární soustavě je zápisem akceptující výpočetní posloupnosti stroje Mu na slově wv.
Konstrukce ACOMP(y) je „algoritmická", tj. realizovatelná strojem M. Ten tuto formuli „vypočte", na pásku zapíše formuli ~^3y ACOMP(y) a přejde do akceptujícího stavu.
132
+ Formuli ACOMP(y) setrojíme postupně takto:
„Číslo y je mocninou p." (Zde p je prvočíslo vypočtené výše.) POWERv(y) = Vz((DJV(z,y) APRIME{z)) -> z=v)
„V p-árním zápisu v se na logp (y )-tém místě zprava vyskytuje symbol [b]". (Předpokládáme, že y je mocnina p)
DIGIT{v,y,b) = 3u3a {v=a+\)y+upy A a