MATEMATICKÁ LOGIKA Prezentace ke kurzu MA007 »» Logika (z řeckého Aoyoct) 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?" rlKA. Neformální, formální, matematická. Aristotelova logika. neformální logika studuje problematiku správné argumentace 1 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é 1 nich vystupují. 5od pojem matematická logika jsou obvykle zahrnovány dvě různé )blasti 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.) '»» Považován za zakladatele (formální) logiky. »» Zavedl a prozkoumal pojem sylogismu. "» Aristoteles zkoumal také pravdivostní módy a položil tak základy modálni logiky. Aristoteles (384-322 př. Kr.] stotelova logika. Logický čtverec. aristotelova logika. Logický čtverec (pokr.) Nechť S a P jsou neprázdné vlastnosti. Aristoteles rozlišuje následující základní kategorická tvrzení: '"»• A všechna S jsou P »» E žádná S nejsou P »» I některá S jsou P »» O některá S nejsou? »» Mnemonika: Afflrmo—nEgO (tvrdím—popírám) stotelova logika. Sylogismy. sylogismy jsou jednoduché úsudky tvaru Hlavní premisa Vedlejší premisa :. Závěr )bě premisy i závěr jsou kategorická tvrzení tvaru A, E, I, O obsahující lohromady právě tři vlastnosti (označme je S, M, P), kde ♦ hlavní premisa obsahuje S a M; ♦ vedlejší premisa obsahuje P a M; ♦ závěr je tvaru S z P. ^ze tedy rozlišit následující čtyři formy sylogismů: I: MxP II: PxM III: M x P IV: PxM SyM SyM MyS My S :. SzP .-. SzP .-.SzP .-.SzP celkem tedy existuje 4 • 43 = 256 sylogismů. "» 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 s íí (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 (pokr.) » 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). stotelova logika. Platnost sylogismů. Aristotelova logika, platnost sylogismů (pokr.) [To] A E I O •chna S jsou V) (žádná S nejsou V) (některá S jsou V) (některá S nejsou V) sedé oblasti jsou prázdné; symbol „•" označuje neprázdné oblasti; nlé oblasti mohou být prázdné i neprázdné. ""»• Uvažme nyní např. 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í. stotelova logika. Platnost sylogismů (pokr.) [TT] booleova „algebra logiky. 12 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 jev Aristotelově logice považován za platný. Je však řeba použít předpoklad, že každá vlastnost je neprázdná. Tento )ř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é. llavní i vedlejší premisa jsou na intuitivní úrovni pravdivá tvrzení, :ávěr však nikoliv. '»» 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) rEBRA LOGIKY. Motivační přiklad. 13 ALGEBRA LOGIKY. Motivační přiklad (pokr.) 14 íme následující sylogismus: fšechnaSjsou M Žádná M nejsou P . Žádná S nejsou P id vlastnosti identifikujeme se soubory objektů univerza, pro které , můžeme uvedený sylogismus přepsat na S c M s n M' 0 (1) MnP 0 a dále na MnP 0 (2) .-. snp o .-. snp o (3) isme se nyní „odvodit" (3) z (1) a (2): »» Z toho, žeSnM' = OaXnO = 0 pro libovolné X dostáváme (S n M') n P = 0 (4) <+■ Podobně z (2) plyne (M n P) n S = 0 (5). »*• Ze (4), (5) a faktu, že 0 U 0 = 0, plyne ((S n M') n P) u ((M n P) n S) = 0 (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) = 0 (7) '"»■ Nyní podle distributivního zákona lze (7) přepsat na (S n P) n (M' U M) = 0 (8) »* Jelikož X U X' = 1 aXnl = X pro libovolné X, dostáváme z (8) konečně SHP = 0 což bylo dokázat. rEBRA LOGIKY. Motivační přiklad (pokr.) 15 ALGEBRA LOGIKY. Motivační přiklad (pokr.) 16 edchozím příkladu jsme k dokázání sylogismu použili symbolickou ipulaci se symboly S, M a P podle následujících algebraických identit lezabývali jsme se tím, jaký mají symboly U, n, 0, 1, a ' význam). xux = X XUX' = 1 xnx = X xnx' 0 XUY = YUX X" X xn Y = Ynx XU 1 = 1 XU(YUZ) (XUY) U Z xn 1 = X xn(YnZ) (XnY)nz xuo X xn (xuY) = X xno = 0 xu(xnY) = X (XUY)' x'nY xn(Yuz) (XnY)u (xnz) (xnY)' X'UY xu(Ynz) (XuY) n (xuz) "» 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 XnY píše X.Y (případně jen XY); -*- místo XUY píše X + Y; místo X' píše 1 — X. 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é. EB BRA LOGIKY. Dva základní problémy. [uj 5odle Boolea je každý sylogismus možné zapsat ve tvaru Fi(P,M) = 0 F2(S,M) = 0 .-. F(S,P) = 0 ide Fi (P, M), F2(S, M), F(S, P) jsou vhodné výrazy vytvořené ze symbolů i, 1, U, n, ' a symbolů v závorkách. 3oole uvážil obecnější úsudky tvaru Fi(Ai,...,Am,Bi,...,Bn) = 0 Fk(Ai,..., Am, Bi .-. F(Bl ■,Bn) ■,Bn) Zílem jeho snah bylo vyvinout metodu, která umožní .. zjistit, zdaje daný úsudek pravdivý; 1. nalézt nejobecnější závěr (F) pro dané předpoklady (Fi, EBRA LOGIKY. Řešení 1. problému. ,Fk). 19 4. Úsudek Fi (Ai,..., Am, Bi,..., BT 0 ,Bn) = 0 ,Bn) = 0 Fk(Ai,..., Am, Bi,. .-. F(B1;. atný právě když každý A, Ťí-konstituent výrazu F Je A, Ťí-konstituentem erého Ft. lad 5. Uvažme opět sylogismus s n m' = o MnP = o .-. snP = o A = M a B = S, P. Uvažme A, Ťí-konstituenty jednotlivých výrazů: snM' MnP SnP M'nsnp M'nSnP' Mnsnp Mns'nP Mnsnp M'nSnP ALGEBRA LOGIKY. Booleova metoda. Definice 1. Nechť A = Ai,..., An. A-konstituentje výraz tvaru U n • • • n ÍT kde ti je buď At nebo A[. Věta 2. Pro každý výraz F(Xi, • • •, Xn) platí F(x1,---,xn)= (J F(v)nMv)n---nMv) ve{o,i}n kde £t(v) Je buďXt nebo X^ podle toho, zdaje Ví rovno 1 nebo 0. Příklad 3. JVechťF(A, B) = (A U B') n (A' U B). Pak F(A,B) = (F(O.O)nA'nB') U (F(0,1)nA'nB) u (F(l, 0) n A n B') u (F(l,l)nAnB) = (in A'n B') u (OnA'nB) u (OnAnB') u (inAnB) = (A'n B') u (A n B) IALGEBRA LOGIKY. Řešení 2. problému. Nechť A = Ai,..., Am, B = Bi,..., B^. Uvažme předpoklady tvaru F1(A,B)=0,---,Fk(A,B) = 0 Cílem je nalézt nejobecnější závěr tvaru F(B) = 0. Označme F-(A, B) = Fi (A, B) U • • • U Fk(A, B) Věta 6. Nejobecnější závěr F(B) = 0, který plyne z E(A, B) = 0, Je tvaru F(B) = f] E(v,B) ve{o,i}m Příklad 7. Nejobecnější závěr F (S, P) plynoucí z předpokladů S n M' = 0 a M n P = Oje tvaru F(s,P) = ((sno')u(onP))n((snľ)u(inP)) = snP 18 20 TAVBA FORMÁLNÍCH LOGICKÝCH SYSTÉMŮ.EU VÝROKOVÁ LOGIKA. Syntaxe. 22 5otř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). nákladní kroky: Vymezení užívaných symbolů (abeceda). Syntaxe formulí. Sémantika (zde se objeví pojem pravdivost). Odvozovací systém (zde se objeví pojem dokazatelnosť). KOKOVA LOGIKA. Sémantika. 23 nice 11. Pravdivostní ohodnocení (váluace) je zobrazení v, které každé kové proměnné přiřadí hodnotu 0 nebo 1. imatematickou indukcí k délce vytvořující posloupnosti lze každou aci v jednoznačně rozšířit na všechny výrokové formule: '(A) je již definováno; 0 jestliže v(ty) = 1; 1 jinak. '((^i Ai|)2)) I 0 jestliže v(tyi) = 0 nebo v(ty2) = 0; 1 jinak. 0 jestliže v(ty-\) = 0 a současně v(ty2) = 0; 1 jinak. ,,. , u 0 jestliže víibi ) = 1 a současně v(ty2) = 0; 1 jinak. Definice 8. Abecedu výrokové logiky tvoří následující symboly: "» znaky pro výrokové proměnné A, B, C,..., kterých je 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 ty-\, • • • ,i|)k, kde k > 1, ty-^ Je cp, a pro každé 1 < i < k má síouo jeden z následujících tvarů: "» uýroJcouá proměnná, ""»• ~^tyj pro nějaké 1 < j < i, ""»• (tyj o tyy) pro nějaká 1 <),)'< i, kde o je jeden ze symbolů A, V, —>. Poznámka 10. Notace: vnější závorky budeme zpravidla vynechávat. Např. místo (AV-B) budeme psát AV-B. VÝROKOVÁ LOGIKA. Sémantika (pokr.) 24 Definice 12. Výroková formule cp je ""»• pravdivá (resp. nepravdivá)při valuaciv, pokudv((p) = 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 J výrokových formulí je splnitelný, jestliže existuje valuacev taková, že v(cp) = 1 pro každé cp z T. Definice 13. Formuíe cp a ty jsou ekvivalentní, psáno cp « právě když pro každou valuaciv platí, že v(cp) = v(i|j). Příklad 14. Nechť cp, \|), E, j sou výrokové formule. Pak: (pAty cp A (t|> A £,) cpA(t|)V£,) — cp t4j> Acp (cpAi|>) A^ (cpAi|))V((pA£,) cp [OKC OKOVA LOGIKA. Sémantika (pokr.) 25 VÝROKOVÁ LOGIKA. Pravdivostní tabulky. 26 íámka 15. „Identity" z příkladu 14 umožňují dále zpřehlednit zápis ulí. Např. místo (A V B) V C můžeme (nejednoznačne) psát A V B V C. nejednoznačnost nevede k problémům, neboť příslušné definice a mí „fungují" pro libovolné možné uzávorkování. íámka 16. V teorii výpočetní složitosti se dokazuje, že problém zda i výroková formule (pje splnitelná (resp. tautologie) je NP-úplný (resp. P-úplný). Otázka, zda existuje efektivní (polynomiální) algoritmus pro lené problémy, je ekvivalentní otázce zda P = NP. nice 17. Formule (pje tautologickým důsledkem souboru formulí T', io T h cp, jestliže v(cp) = 1 pro každou valuaciv takovou, žev(ty) = 1 pro lou formuli ty ze souboru T. Jestliže T h

{0,1}, kde n > 1. [OKOVÁ LOGIKA. Formálni systém £(F,, • • •, Fk). Hf] I VÝROKOVÁ LOGIKA. Formálni systém £(F, 28 íť Fi, • • •, Fk je konečný soubor výrokových funkcí. Definujeme formální ký systém £(Fi, • • •, Fk), kde abeceda je tvořena znaky pro výrokové proměnné, závorkami a znaky ri, • • •, JFk pro uvedené výrokové funkce. 7 definici vytvořující posloupnosti formule (viz definice 48} požadujeme, iby tyi bylo buď výrokovou proměnnou nebo tvaru T) [ty^ tyjn), kde < j i, • • •, jn. < i- a ti je arita Fj. raluace rozšíříme z výrokových proměnných na formule předpisem v(^(t|)1,---,t|)n))=F(v(t|)1),---,v(t|)n)) íito smyslu je pak dosud uvažovaný systém výrokové logiky systémem V,—>,-■). Dříve zavedené sémantické pojmy (splnitelnost, pravdivost, se opírají pouze o pojem valuace a „fungují" tedy v libovolném ;mu£(F1,---,Fk). Pro účely následující definice zvolme libovolné (ale dále pevné) lineární uspořádání C na souboru všech výrokových proměnných. Definice 19. Nechť cp je formule £(Fi, • • •, Fk) a nechťX^, • • •, Xnje vzestupně uspořádaná posloupnost (vzhledem k C.) 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 T ^(ú) = v(F), kde v je valuace definovaná takto: v(Xt) = u(i) pro každé 1 < i < n, v(Y) = 0 pro ostatní Y. Definice 20. Systém £(Fi ,Fk) je plnohodnotný, jestliže pro každou výrokovou funkci F existuje formule cp systému £(Fi, • • •, Fk) taková, že F = F {0,1} je výroková funkce a nechť úi,•• •, úk jsou hny vektory z {0,pro které nabývá F hodnoty 1. Pokud žádný vý vektor není (tj. k = 0), klademe cp = A -Xi A X2 A • • • A Xn. Jinak k cp = \/ í, (utJA-.-A^fui) i=l tj (ut) je buď Xj nebo -Xj podle toho, zda ut(j) = 1 nebo ut(j) = 0. Nyní hce ověří, že F = F), £(-), atd. VÝROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) [šo 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 ©(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 á se nazývá Schroderův operátor. Platí cp x ty « -cp A ""»• Funkce | se nazývá Shefferův operátor. Platí cp | ty « -(cp Aty). VÝROKOVÁ LOGIKA. Shejferovské spojky. Definice 22. Výroková funkce T je Shejferovskájestliže £(F) je plnohodnotný systém. Věta 23. Nechť S (n) značí počet všech Shejferovských funkcí arity n > 1. PaJcS(n) = 2<2^,-1>(2í2^,-1>-1). 32 Pro n = 1,2,3,4,5,... dostáváme postupně 0,2,56,16256,1073709056,... Důsledek 24. Jelikož lim^oo -|jír = 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. [OKC OKOVA LOGIKA. Normální formy. [33 nice 26. Aterál je formule tvaru X nebo -■X, kde Xje výroková proměnná; Uauzule je formule tvaru £1 V • • • V ín, kde n > 1 a každé ti je literát Duální klauzule je formule tvaru £i A • • • A ín, kde n > 1 a každé ti je iterál. ^ormule v konjunktivním normálním tvaru (CNF) je formule tvaru ľi A • • • A Cm, kde m > 1 a každé Čije klauzule. 7ormule v disjunktivním normálním tvaru je formule tvaru Ci V • • V Cm, cde m > 1 a každé Čije duální klauzule. mžitým důsledkem věty 21 je následující: . 27. Pro každou formuli cp existuje ekvivalentní formule v disjunktivním lálním tvaru. VÝROKOVÁ LOGIKA. Normální formy (pokr.) [š± Věta 28. Pro každou formuli cp existuje ekvivalentní formule v konjunktivní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 « N/ILi Dt, kde n > 1 a každé Dt je duální klauzule. Metaindukcí vzhledem k n: ""»• n = 1. Pak \/r=i je současně v CNF. Indukční krok: Nechť Di = U A • • • A£k. Platí n+1 n+1 m m m k \J Dt « D,V\jDi « D,V/\d « /\DiVCt « AA^VCi) i=1 i=2 i=1 i=1 i=1 j = 1 □ Příklad 29. Formuli (A -> B) A (B -> C) A (C -> A) íze u CNF reprezentouaŕ jato (-AVB) A(-BVC) A(-CVA) nebo (-A V C) A (-C VB) A (-B V A). CNF tedy není určena jednoznačně až na pořadí klauzulí a literálů. 35 KOKOVA LOGIKA. Věta o kompaktnosti. . 30 (o kompaktnosti). Nechť J je soubor formulí výrokové logiky. J je itelný právě když každá konečná část J je splnitelná. iz. Směr „=>" je triviální. Dokážeme „<=". Zavedeme pomocný pojem: >or V výrokových formulí je dobrý, jestliže každý konečný podsoubor V Initelný. Nechť 14^1 ,^2,... je posloupnost všech formulí výrokové logiky, imatematickou indukcí definujeme pro každé i > 1 dobrý soubor St: li = T. Soubor Si je dobrý neboť T je dobrý. Si u {iKl jestliže St u {i^} je dobrý; = St u {^iK} jinak. Uespoňjeden ze souborů St u {tyi} a St u {-^tyi} musí být dobrý; jinak ixistují konečné Ví c St u {tyi} a V2 c St u {^i|h}> které nejsou splnitelné. Testliže Ví c St nebo V2 c St, máme ihned spor s tím, že St je dobrý; inak V u V2 obsahuje ty i ~^ty, proto i (V u V2) \ {tyi, ~^tyi\ c St je íesplnitelný, spor.) VÝROKOVÁ LOGIKA. Věta o kompaktnosti. [šě Nechť S = Uili 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 St obsahující cp i -■cp; tedy {cp,^cp}je nesplnitelný podsoubor St, spor. ""»• S obsahuje (p Aty právě když S obsahuje cp i tJj; ""»• S obsahuje cp V ty právě když S obsahuje cp nebo \Jj; ""»• S obsahuje cp —> \Jj právě když S neobsahuje cp nebo obsahuje ty. 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ý. □ [OKC OKOVA LOGIKA. Věta o kompaktnosti (použití). 37 m věty 30 lze snadno dokázat radu dalších tvrzení. líraf Q je dvojice (U,H), kde U je nejvýše spočetný soubor uzlů a H je ireflexivní a symetrická relace na U. Jodgraf grafu G je graf Q' = (lť, H'), kde U'CUaH'CH. >raf G = (U, H) je k-obarvitelný jestliže existuje funkce f : U aková, že f(u) ^ f (v) pro každé (u,v) e H. VÝROKOVÁ LOGIKA. Věta o kompaktnosti (použití). Věta 31. Graf G = (U, H) Je k-obarvitelný právě když každý konečný podgraf G je k-obarvitelný. Důkaz. Nechť BU)i 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 BU)ic pro každý uzel u; BU)i —> "'Bu.j pro každý uzel u a každé 1 < i, j < k, kde i ^ j; BU)Í —> ^Bvi pro každé (u,v) e H a 1 < i < k. Platí následující pozorování: '»» Graf G je k-obarvitelný právě když soubor T je splnitelný. '»» Každý konečný podgraf G je k-obarvitelný právě když každý konečný podsoubor T je splnitelný. Nyní stačí aplikovat větu 30. 38 □ KOKOVA LOGIKA. Odvozovací systém pro C{ 39 VÝROKOVÁ LOGIKA. Odvozovací systém pro C{ 40 :o části se soustředíme na £(—>,-■). Uvažme následující odvozovací :mpro£(^,-) (Lukasiewicz, 1928): imata axiómů: U: cp->(t|>->cp) V2: ((p_>(t|,->£,))->(((p->t|,)->((p _>£,)) V3: hcp -> -^|>) -> (t|> -> cp) Dzovací pravidlo: ŕlP: Z cp a cp —> i); odvoď \|). (modus ponens) Definice 32. Buď T soubor formulí. "» Důkaz formule ty z předpokladů J je konečná posloupnost formulí cpi, • • •, cpic, kde cpk Je a pro každé cpt, kde 1 < i < k, píaíí alespoň jedna z následujících podmínek: cptje prvek J; cp. xz. Následující posloupnost formulí je důkazem cp —> cp. 1) (cp -> ((cp -> cp) -> cp)) -> ((cp 2) cp -> ((cp -> cp) -> cp) 3) (cp -> (cp -> cp)) -> (cp -> cp) 4) cp^(cp^cp) 5) cp ^ cp (cp -> cp)) -> (cp -> cp)) A2 AI MP na2),1) AI MP na 4),3) □ Příklad 34. Pro libovolné formule cp, ty platí {cp, —'cp} h ip. Důkaz. Následující posloupnost formulí je důkazem \p z {cp,^cp}: 1) ^cp 2) ^cp 3) —xp ^ — cp 4) M,-^cp 5) (p^ty 6) cp 7) -n|>->-cp) AI předpoklad MP na2),1) (cp->t|>) A3 MP na 3),4) předpoklad MP na 6),5) □ KOKOVA LOGIKA. Věta o dedukci. 43 VÝROKOVÁ LOGIKA. Věta o dedukci. 44 . 35 (o dedukci). Nechť cp, ty j sou formule a J soubor formulí. Pak \\>} h cp právě když T h ty —> cp. iz. Nechť £,i, • • •, £k je důkaz formule \p —> cp z předpokladů T. Pak •, £k,ip, cp je důkaz formule cp z předpokladů T U {ip} (poslední formule mé aplikací MP na. ty a. £k). Nechť £,i, • • •, £k je důkaz cp z předpokladů T U {ty}. Metaindukcí k j lžeme, že T h ty —> £j pro každé 1 < j < k. = 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 —> (t|> —> f,i), \p —> f,i. První formule je nstancí AI, druhá aplikací MP na £i a první formuli. Máme tedy důkaz !>->£,! z T. fe-li £i formule ty, platí T h ty —> ip podle příkladu 33. ""»• Indukční krok: Je-li formule £j instancí axiómu nebo prvek T U {ip}, postupujeme stejně jako výše (místo £t použijeme £j). Je-li £j výsledkem aplikace MP na £m, £Tl, kde 1 < m,n < j, je £,n tvaru £m —> £j. Podle I.P. navíc platí T h ip —> £m aT h \p —> (£,m —> £,j). Důkazy 4> —> £m a \p —> (£m —> £j) z T nyní zřetězíme za sebe a připojíme následující formule: - [ty -> (£m -> £j)) -> ((t|> -> £m) -> (t|> -> E,j)) - ^^£j První formule je instancí A2, další dvě vzniknou aplikací MP. Máme tedy důkaz formule \p —> f,j z T. □ KOKOVA LOGIKA. Věta o korektnosti. 45 VÝROKOVÁ LOGIKA. Věta o úplnosti. Lema 37. Nechť cp, ty jsou formule. Pak . 36 (o korektnosti). Nechť cp je formule a J soubor formulí. Jestliže 3, pak T |= cp. až. Nechť £,i, • • •, £,k je důkaz cp z T. Indukcí vzhledem k j dokážeme, že E,j pro každé 1 < j < k. (Stačí ověřit, že každá instance A1-A3 je alogie, a že jestliže Th^aTh^^í, pak také T |= £,). □ (a) h -cp - ->(cp- (b) h — cp -> cp fcJ h cp -> — cp fd; i- (cp - •H- >^cp) (e) h cp -> ^-(cp- 0) 1- (cp — .((-cp- Důkaz. ""»• (a): Podle příkladu 34 platí {cp,- cp} h ty, proto I—cp opakovaným užitím věty o dedukci. (cp->t|>) KOKOVA LOGIKA. Věta o úplnosti. b): Platí 47 1) h—cp -> (-cp — cp) podle (a) 2) {—cp} h -cp -> —cp věta o dedukci 3) h (-cp -> —cp) -> (—cp -> cp) A3 4) {—cp} h —cp -> cp MPna2),3) 5) {—cp} h cp věta o dedukci 6) h —cp -> cp věta o dedukci c): Platí 1) h —cp -> -cp podle (b) 2) h (—cp -> -cp) (cp ^ —cp) A3 3) h cp cp MP na 1),2) VÝROKOVÁ LOGIKA. Věta o úplnosti. '"»• (d): Platí 1) { ip,— cp} h ty 4) h ty -> — 5) {cp -> ip,— cp} h — t4j 6) {cp -> ip} h —cp -> — 7) h (—cp -> —t|>) -> (-^ - 8) {cp -> ^} h -> -cp 9) h(cp^)^(-^-cp) -cpj podle (b) a věty o dedukci MP na2),l) podle (c) MP na 3),4) věta o dedukci A3 MP na 6), 7) věta o dedukci [OKC OKOVA LOGIKA. Věta o úplnosti. 49 e): Platí 1) {cp, cp -> \Jj} h ty 2) {cp}h(cp^)^ 3) h((cp^)^)^(^- 4) {(p}h-t|)->-(cp->t|)) 5) hcp-^Mí-^cp-^)) věta o dedukci -(cp->t|>)) podle (d) MPna2),3) věta o dedukci KOKOVA LOGIKA. Věta o úplnosti. 51 nice 38. Nechť v je valuace a cp formule. Jestliže v(cp) = 1, označuje bol cpv formuli cp. Jinak cpv označuje formuli -■cp. a 39 (A. Church). Nechť v je valuace, cp formule, a{Xi, • • • ,Xk} konečný )or výrokových proměnných, kde všechny proměnné vyskytující se ve cp mezi{Xi, • • •,Xk}. Pak{X^, • • •,X£} h cpv. iz. Indukcí k délce vytvořující posloupnosti pro . Te-li cp = X, pak X je mezi {Xt , • • • ,Xk} a tedy {X^, • • • ,X£} h Xv. Te-li cp = —^t4j>, kde {X^, • • •, X£} h \pv, rozlišíme dvě možnosti: v(ip) = 0. Pak tyv = —^t4j> a cpv = není co dokazovat. - v(ty) = 1. Pak tyv = i|j a cpv = —Podle lematu 37 (c) platí h t|> -> —proto {Xy, • • •, X]J} h —1|) užitím MP VÝROKOVÁ LOGIKA. Věta o úplnosti. 50 '"»• (f): Platí 1) 2) 3) 4) 5) 6) 7) 8) 9) -cp)) h(cp->t|>)->Hp {cp -> I- -cp {cp -> t+>, —t|j, —cp ->t|)}ht|j {cp -> ty, -cp -> t4j} h -> h h^-h^^)) h (-ll> -> tl>) -> 10) {cp->t|>,-cp->t|>}l-tp 11) [-(cp-^-^hcp-^)-^) VÝROKOVÁ LOGIKA. Věta o úplnosti. -i|>->t|>)->t|>) podle (d) 2x MP na 1) MPna2),-cp -> \p věta o dedukci podle (e) 2x věta o dedukci věta o dedukci A3 MP na 7), 8) MP na 4), 9) 2x věta o dedukci □ 52 "|» Je-li cp = ty -> £,, kde {X^, • • •, X£} h a {X^, • • •, X£} h £,v rozlišíme následující možnosti: v(t|> ->£,) = 1. Máme tedy dokázat, že {X^, • • •, h ty -> £,. • Jestliže v(t|>) = 0, platí {Xy, • • •, X]J} h -ip. Podle íemaru 37 faj dále platí h --ty -> (ty -> £,), proto {X^, • • •, X£} h ty -> L, užitím MP • Jestliže v(£,) = 1, platí {X?, • • •, X£} h £,. Podle AI platí h £, -> -> £,), proto {X^, • • •, Xy h -> £, užitím MP v(t|> ->£,) = 0. Pak {X^, • • •, Xy h ty a {X^, • • •, X£} h -£,. Máme dokázat, že {Xy, • • •, X£} h -> £,). Podle Íemaru 37 fej platí h t|) -> (-£, -> - -> £,)), proto {X^, • • • ,X£} h -> £,) opakovaným užitím MP □ [OKC OKOVA LOGIKA. Věta o úplnosti. 53 VÝROKOVÁ LOGIKA. Věta o úplnosti. 54 . 40 (o úplnosti). Nechť cp je formule a J soubor formulí. Jestliže T |= cp, T h cp. ~xz. Nejprve uvážíme případ, kdy T je prázdný soubor. Nechť cp je alogie a Xi, • • •, Xic všechny výrokové proměnné, které se ve cp vyskytují. 5odle Churchova lematu platí {X^, • • •, X£} h cp pro libovolnou valuaci v. Jkážeme, že všechny X\ lze postupně „eliminovat", až dostaneme lůkaz cp z prázdného souboru formulí. poládejme, že pro dané O < n< k jsme již prokázali, že {Xy,---,X^,X^+1}h(p .ibovolnou valuaci v. Dokážeme, že pak také {X^1, • • •, X^} h cp pro rolnou valuaci u. Buď tedy u libovolná valuace. Nechť ui, U2 jsou valuace definované takto: U! (Xk) = 1, u2(Xk) = O, a pro každé Y ^ Xk platí m (Y) = u2(Y) = v(Y). Platí předpoklad pro v = ui předpoklad pro v = u2 věta o dedukci na 1) věta o dedukci na 2) cp) —> cp) podle lematu 37 (f 2x MP na 5) s využitím 3),4) 1) W, ••,XS,Xn+1}l- cp 2) W, ••,X-,^+1}hcp 3) W, ••,>Qi}hxn+, ^cp 4) W, ••,X-}h^+1 ^cp 5) h(X^+1 -xp)->((^xn+i 6) ••,X-}hcp KOKOVA LOGIKA. Věta o úplnosti. 55 '. uvážíme obecný případ. Buď T libovolný soubor formulí a cp formule vá, že T |= cp- Podle věty o kompaktnosti existuje konečný soubor ■ • •,tyn} formulí z T takový, že {i|>i, • • •, tyn} h cp. Lehce se ověří, že = tyl -> [ty2 -> [ty 3 ~> • • • {ty n > CpJ • • -J e předchozího bodu tedy platí h tyl -> {ty2 ~> {M>3 ~> ■ ■ ■ {ty n ^ CpJ • • 'J aplikacích věty o dedukci dostáváme {tyi, ■ ■ ■, tyn} h cp, tedy také 3. □ VÝROKOVÁ LOGIKA. Historické poznámky. Výroková logika byla nebyla rozvíjena samostatně, ale jako součást složitějších formálních systémů. '»» Gottlob Frege (1848-1925) položil základy predikátové logiky a zavedl „moderní" odvozovací systém. „Výrokový fragment" tohoto systému vypadá takto (verze z roku 1879): 56 P^(Q^P) (P->(Q->R))->((P-(P^(Q^R))^(Q-(P-> Q)-> hQ-> H>) Q) (P (P R)) R)) —p -> P p P Odvozovací pravidla: MP a substituce Fregeho výsledky byly vědeckou komunitou ignorovány zhruba 20 let. [OKC OKOVA LOGIKA. Historické poznámky. 57 >iuseppe Peano (1858-1932) doporučil na mezinárodním natematickém kongresu v Paříži (rok 1900) mladému Bertrandu lussellovi (1872-1970) studovat Fregeho práce. Russell v roce 1901 )bjevil inkonzistenci ve Fregeho systému (Russelův paradox), současně )lně docenil Fregeho myšlenky. V letech 1910-1913 byla publikována řídílná Principia Mathematica (autoři Whitehead, Russel). Tato nonografie měla hluboký vliv na vývoj logiky v následujících lesetiletích. Věnována byla Fregemu. Pro fragment výrokové logiky byly >oužity následující axiómy a odvozovací pravidla: ► 1 - 2 ► 3 ► 4 ► 5 (PVP) -> P Q^(PVQ) (PVQ)^(QVP) (PV(QVR)) -> (QV(PVR)) (Q^R)^((PVQ)^(PVR)) Odvozovací pravidla: MP a substituce KOKOVA LOGIKA. Historické poznámky. David Hilbert (1862-1943) a Wilhelm Ackermann (1896-1962) )ublikovali v roce 1928 následující systém: 59 ► 1 - 2 ► 4 ► 5 (PVP) -> P P^(PVQ) (PVQ)^(QVP) (Q^K)^f(PVQ) (PVR)) Odvozovací pravidla: MP a substituce 7 roce 1927 navrhl John von Neumann (1903-1957) aplikovat substituci pouze na axiómy. Vznikly systémy založené na schématech vciómů. Tan Lukasiewicz (1878-1956) prezentoval svůj odvozovací systém použitý v přednášce) v roce 1928. VÝROKOVÁ LOGIKA. Historické poznámky. 58 '»» V roce 1917 nalezl Jean Nicod následující zjednodušení axiomatického systému z Principia Mathematica: ^ 1: (PVP)^P ^2: P -> (PVQ) ^4: (PV(QVR))^(QV(PVR)) -5: (Q^R)^((PVQ)^(PVR)) Odvozovací pravidla: MP a substituce '»» Ve stejném roce publikoval Henry Sheffer následující axiomatický systém založený na Shefférově operátoru: - Axióm: (P|(Q|R))|((S|(S|S))|((U|Q)|((P|U)|(P|U)))) Odvozovací pravidla: substituce a „z F a F|(G|H) odvoď H" VÝROKOVÁ LOGIKA. Historické poznámky. » Další odvozovací systémy: »+ V roce 1947 zjednodušili Gótling a Rasiowa systém z Principia Mathematica do následující podoby: 60 • 1 • 2 • 3 (PVP)^P P -> (PVQ) (Q^R)^((PVQ) (PVR)) • Odvozovací pravidla: MP a substituce V roce 1953 prezentoval Meredith systém s jediným schématem a jediným odvozovacím pravidlem: • Schéma axiómu: ((((cp ->t|>) -> hp -> -> p) -> y) -> ((y -> cp) -> (£, -> cp)) • Odvozovací pravidlo: MP dikatova logika. Vznik a vývoj. 61 Predikátová logika, syntaxe. 62 Predikátová logika (také logika prvního řádu) se opírá o pojem Mastnosti (tj. predikátu). Umožňuje formulovat tvrzení o vlastnostech )bjektů s využitím kvantifikátorů. víapř. Aristotelova logika je z dnešního pohledu fragmentem >redikátové logiky. rormule prvního řádu byly součástí Fregeho systému, později se )bjevily ve 3. dílu Schrôderovy monografie Algebra der Logik (1910) a nonografii Principia Mathematica (Whitehead, Russel). xigika prvního řádu byla definována jako samostatný systém až r monografii Hilberta a Ackermanna Grundzůgen der theoretischen xygik (1928). Definice 41. Jazyk (stejně jako jazyk s rovností) je systém predikátových symbolů afunkčních symbolů, kde u každého symboluje dánajeho č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 afunkč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í přidáme speciální logický symbol jehož sémantika bude definována speciálním způsobem dikatova logika. Syntaxe. 63 lad 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 unkční symbol „■" arity 2. nice 44. Abecedu predikátové logiky pro jazyk L tvoří následující boly: Znaky pro proměnné x, y, z,..., kterých je spočetně mnoho Aimologické symboly, tj. predikátové a funkční symboly jazyka L. Je-li L jazyk s rovností, obsahuje abeceda speciální znak = pro rovnost. jjgické spojky —> a^. symbol V pro univerzální kvantifikátor. Závorky (a). Predikátová logika, syntaxe. Definice 45. Termem jazyka C je slovo t nad abecedou predikátové logiky pro jazyk L, pro které existuje vytvořující posloupnost slov ti, • • •, tk, kde k > 1»tk je t, a pro každé 1 < i < k má slovo tt jeden z následujících tvarů: 64 ""»• proměnná, ""»• f(ti,, • • • ,tij, kde) 1, ty-^ je cp, a pro každé 1 < i < k má slovo tyi jeden z následujících tvarů: ""»• P(ti, • • •, tn), kde V je predikátový symbol jazyka L arity n a ti, • • •, tn jsou termy jazyka L. ""»• ti = t2, je-li L jazyk s rovností a ti, t2Jsou termy jazyka L. ""»• —'i|>j pro nějaké 1 < j < i, ""»• (tyj —> tyj') pro nějaká 1 <],]'< i, ""»• \fxtyj, kde xje proměnná a 1 < j < i. dikatova logika. Syntaxe. 67 Predikátová logika, syntaxe. 68 íámka 49. Ve zbytku přednášky budeme používat následující etiky ": becp značí ^Vx—cp o V ty značila? —> \p ?A\|) značí — (cp —> —'xIj). 3 <-> t4j> značí (cp —> A předchozího bodu. lady formulí: 'xP(x,d)A3x(P(x,x)VQ(c)) 'x3x(P(x,x) VVyVxQ(x)) cp), Jede symbol A dále „rozvineme"podle 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 předpisu: ""»• Ve formuli tvaru P (ti. ) 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é veformulity volný (resp. vázaný), je odpovídající výskyt ve formulích ^ty, cp —> i|j —> cp rovněž volný (resp. vázaný). ""»• Ve formuli\fxty je 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 formuliMxty rovněž volný (resp. vázaný). Příklady (volné výskyty jsou červené): VxP(x,y)VVyP(x,y) Vx(P(x,y)VVyP(x,y)) dikatova logika. Syntaxe. 69 Predikátová logika, substituce. 70 nice 51. ^roměnná se nazývá volnou (resp. vázanou) ve formuli, máli v ní volný resp. vázaný) výskyt. ^ormuleje otevřená, jestliže v ní žádná proměnná nemá vázaný výskyt. ^ormuleje uzavřená (také sentence), jestliže v ní žádná proměnná nemá )olný výskyt. Zápis cp(xi, • • •, xn) značí, že všechny volné proměnné ve formuli (pjsou nezi xi, • • •, xn (nemusí nutně platit, že každá z těchto proměnných je )olná ve cpj. Jniverzální uzávěr formule cp je formule tvaruMx^ ■ ■ ■ Vxn cp, kde :i , • • • ,xn jsou právě všechny volné proměnné formule cp. 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 t substituovatelný zax 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+y=z ""»• Term y + z není substituovatelný za x ve formuli 3zx+y=z ""»• (P(x,y) A VxP(x,y))(x/3) je formule P(3,y) A VxP(x,y) ""»• P(x,-y)(x/y)(-y/x) je formule P(x,x) dikatova logika. Substituce. 71 predikátová logika. Realizace jazyka. 72 nice 53. Nechť cp je formule a ti, • • •, termy, které jsou v uvedeném dí substituovatelné za proměnné x^, - ■ ■ ,xn ve cp (předpokládáme, že ■ ,xnjsou různé). Symbol cp(xi/ti, • • • ,xn/tn) značí formuli, která kne „simultánním nahrazením" každého volného výskytu xt termem tt caždé 1 < i < n. Přesněji, cp(xi/ti, • • • ,xn/tn) je formule /zi) • • • (xrt/znHzi/ti) • • • (zn/tn), kde zi, • • • ,-Lnjsou (různé)proměnné, i se nevyskytují v ti, • • •, ani mezi xi, • • •, x^. lad: >(x,y)(x/y,y/x) je formule P(y,x) Definice 54. Realizace M jazyka Ľ 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 PM na M "» přiřazením, které každému m-árnímu funkčnímu symbolu přiřadí funkci f m : Mm -> M. Ohodnocení je zobrazení přiřazující proměnným prvky univerza M. dikatova logika. Realizace jazyka. 73 predikátová logika. Realizace jazyka. 74 nice 55. Realizaci termu t při ohodnocení e v relizaci M, psáno tM [e] adnějen t[e] je-li M jasné z kontextu), definujeme induktivně takto: :[e] ex (ti ,• • • ,tm)[e] = f m (ti [e], • • • ,tm[e]) pro m = Oje na pravé stane uvedené definující rovnosti f m(0)J. Definice 56 (A. Tarski). Buď M realizace jazyka Ľ, e ohodnocení a formule predikátového počtu jazyka L. Ternární vztah M h [e]. ""»• M h (ty —> právě když M h nebo není M \=ty[e]. M h Vxip[e] právě když M h ^p[e(x/a)] pro každý prvek a univerza M. Jestliže M\= (p[e], říkáme, že cp Je pravdivá v M při ohodnocení e. Jestliže M h (P(x) A-P(x))) neplatí M \= P(x) -> VxP(x) VeplatíM \= (VxP(x) -> Vx-P(x)) -> Vx(P(x) -> -P(x)) Definice 58. Buď Ľ jazyk (příp. jazyk s rovností). "» Teorie (s jazykem Oje soubor T formulí predikátového počtu jazyka L. Prvky T se nazývají axiómy teorie T. '»» Realizace M jazyka Ľ je model teorie T, psáno M h J, jestliže M h

, jestliže cp Je pravdivá v každém modelu teorie T. hkatova logika. Teorie. 77 Predikátová logika, odvozovací systém. 78 lad 59. Uvažme jazyk s rovností obsahující jeden binární funkční bol "■" a jednu konstantu 1. Nechť'T je tvořena následujícími formulemi: 'xVy Vz x • (y ■ z) 'x (x-1 = x) A(1 - x = x) 'x3y (x-y = 1)A(y-x = r formule Vx Vy (x • y) = (y • x) není sémantickým důsledkem T, zatímco ule x • (1 • y) = (1 • x) • y ano. «<» Schémata výrokových axiómů: - PI: cp^(^cp) - P2: ((t|,->y)->((M»)->(«) - P3: (^cp->-i|>)-» (x|>-» cp) »*■ Schéma axiómu specifikace: P4: Vxcp —> cp(x/t), kde t je substituovatelný za x ve cp. »» Schéma axiómu distribuce: -*~ P5: (Vx (cp —> i|>)) —> (cp —> Vxi|>), kde x nemá volný výskyt ve cp. »* Odvozovací pravidla: -*- MP: Z cp a cp —> \p odvoď tp. (modus poueus) -»- GEN: Z cp odvoď Vx cp. (generalizace) dikatova logika. Odvozovací systém. 79 Predikátová logika, odvozovací systém. 80 £ jazyk s rovností, přidáme dále následující axiómy rovnosti: U: x = x *2: (xi=yi A • • • Axn=yn A P(xi, • • • ,xn)) -> P(yi, • • • ,yn), wde P je predikátový symbol arity n. 13: (xi =yi A • • • A xm=ym) —» (f (xi. ide f je funkční symbol arity m. ,xm)=f(yi,"-,ym)), Definice 60. Buď T teorie jazyka C. '«*■ Důkaz formule ty v teorii J je konečná posloupnost formulí cpi, • • •, cpk, kde cpk je ty a pro každé cpi( kde 1 < i < k, platí alespoň jedna z následujících podmínek: cptje prvek J: cpt je instancí jednoho ze schémat P1-P5; -*~ Ľ je jazyk s rovností a cpt je instancí jednoho ze schémat R1-R3; cpt vznikne aplikací pravidla MP na formule cpm, cpn pro vhodné 1 < m, n < i. cpt vznikne apliltací pravidla GEN na formuli cpm pro vhodné 1 < m < i. dikatova logika. Odvozovací systém. 81 Predikátová logika. Důkazy. 82 ^ormule tyje dokazatelná v teorii T, psáno T h ty, jestliže existuje důkaz \> v T. Jestliže J \- ty pro prázdné T, říkáme že tyje dokazatelná a píšeme -ty. ^ormule tyje vyvratitelná v teorii T, jestliže T I—ty Teorie 1 je sporná {též inkonzistentní), jestliže každá formule predikátové ogiky jazyka Ľ je v J dokazatelná. Teorie je bezesporná {též konzistentní), jestliže není nekonzistentní 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 |=

ty právě když T U {cp} \=ty. dikatova logika. Věta o dedukci. 83 Predikátová logika, věta o dedukci. 84 . 63 (o dedukci). Nechť J je teorie jazyka L, ty uzavřená formule jazyka p (libovolná) formule jazyka L. Pak T h ty —> cp právě když T U {ty} h cp. iz. az je velmi podobný důkazu věty 35: Nechť £,!,•••, £,k je důkaz formule ty —> cp v T. Pak £,!,•••, £,k,i|), cp je iz formule cp v T U {ty} (poslední formule vznikne aplikací MP na ty a £k). Nechť £,i, • • •, £k je důkaz cp v T U {ty}. Metaindukcí k j dokážeme, že |j> > £,j pro každé 1 < j < k. = 1. Je4i £i instance axiómu nebo formule z T, platí T h £i. K důkazu ,i z T nyní připojíme formule £i —> (ty —> £i), i|) —> £i. První formule je nstancí Pl, druhá aplikací MP na £t a první formuli. Máme tedy důkaz |> -> £,! v T. Te4i £i formule ty, platí T h ty —> i|) podle příkladu 33 a poznámky 62. ""»• Indukční krok: Je-li formule £j instancí axiómu nebo prvek T U {ty}, postupujeme stejně jako výše (místo £i použijeme £j). ""»• Je4i £j výsledkem aplikace MP na £m, £Tl, kde 1 < m,n < j, je £n tvaru £m —> £j. Podle I.P. navíc platí Th\|)^£maTh\|)^(£m^£j). Důkazy ty —> £m a i|) —> (£m —> £j) v T nyní zřetězíme za sebe a připojíme následující formule: - [ty -> (£m -> £,j)) -> £m) -> -> £j)) - (ty ^ tm) ^ (ty ^ ^ ^ ty^li První formule je instancí P2, další dvě vzniknou aplikací MP. Máme tedy důkaz formule ty —> £j v T. DIKATOVA LOGIKA. Věta o dedukci. 85 PREDIKÁTOVÁ LOGIKA. Vlastnosti kvantifikace. 86 '»• Je-li £,j výsledkem aplikace GEN na £,m, kde 1 < m < j, je £,j tvaru Vx£,m. Podle I.P. platí T h ty —> £,m. K tomuto důkazu nyní stačí připojit formule - Vx(t|>->£,m) - Vx(t|>->£,m)->(t|>->Vx£,m) ty -> Vx£,m. První vznikne aplikací GEN, druhá je instancí P5, třetí vznikne aplikací MP. Dostaneme tak důkaz formule ty —> £,j v T. □ Lema 64. Pro každé formule

t4j) ) <-> (cp —> \fxty), pokud x není uoíná ve formuli cp; 2. h (Vx (cp —> <-> (3xcp —> xp), pokud x není uoíná ue/ormuZi 3. h (3x (cp —> \p)) <-> (cp —> 3xi|)), pokud x není uoíná ve formuli cp; 4. h (3x (cp —> \p)) <-> (Vx cp —> \p), pokud x není uoíná ue/ormuíii|). Důkaz. Pozorování: (a) Jestliže h cp —> \p a současně h \p —> cp, pak h cp <-> ty. 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 £, —> \p, pak T h cp —> Stačí použít poznámku 61 a. tautologii (A^C)^((C^B)^(A^B)). ;DIKATOVA LOGIKA. Vlastnosti kvantifikace. 87 PREDIKÁTOVÁ LOGIKA. Vlastnosti kvantifikace. 88 víechť cp(x), ty(x) jsou formule. Pak h Vx (cp —> \p) —> Vx (—^xp —> -cp), neboť 1) hVx(cp^)^(cp^) 2) h(cp^^)^h^^-cp) 3) hVx(cp^)^h^-cp) 4) Vx(cp->t|>)l--i|>->-cp 5) Vx(cp->t|>)l-Vxhi|>->-cp) 6) h Vx(cp ->t|>) -^Vxhi|) ->-cp) P4 výr. tautologie tranz. impl. na 1), 2) věta o dedukci GEN věta o dedukci ení 1.-4. teď dokážeme za předpokladu, že cp(x) a ty(x). Obecná podoba yne užitím věty konstantách (viz dále). 1. Platí h (Vx (cp —> —> (cp —> Vxi|j), neboť tato formule je instancí P5. Důkaz opačné implikace vypadá takto: 1) h\/xty- 2) h (Vxty (A- ■ty ^ty) B)- ^((cp^Vx^)-((C->A)->(C je tautologie, viz pozn. 61 3) h ((p->Vxt|>)-> (cp->t|>) 4) cp —> Vxi|) h cp —> \p 5) cp->Vxt|> h Vx(cp->t|>) 6) h (cp -> Vxt|>) -> (Vx(cp ->t|>)) (cp->t|>)) P4 MPna 1),2) věta o dedukci GEN věta o dedukci ;dikatova logika. Vlastnosti kvantifikace. 89 predikátová logika. Vlastnosti kvantifikace. 90 Nyní opačný směr h (3x cp —> \Jj) —> Vx (cp —> \p): nejprve ukážeme, že h Vx (cp —> —> (3x cp —> 1) hVxM>->-cp) —> (-i|) —> Vx-cp) podle 1. 2) h Vx(cp ->t|>) -> Vx(-^-cp) podle (c) 3) hVx(cp->t|>))- + (-^ Vx-cp) tranz. impl. na 2), 1) 4) h (-i|> -> Vx-cp) —> (-Vx-cp —> \p) taut. (-B -> A) -> (-A -> B 5) h Vx(cp ->t|>) -> (-Vx-cp ^) tranz. impl. na 3), 4) 6) h Vx(cp ->t|>) -> (Ebccp ->t|>) reformulace 1) h M>- Vx-cp) -> Vx -> -cp) podle 1. 2) h (-Vx -cp ->t|>) -> hi|> -> Vx -cp) taut. (-B -> A) -> (-A -> B) 3) h (-Vx -cp ->t|>) -> Vx -> -cp) tranz. impl. na 1), 2) 4) 3x cp —> ty h Vx (-ip ^-cp) věta o dedukci 5) Elx cp —> ^ h -> - -cp P4aMP 6) Ex cp —> 4> h cp —> (-A -> -B) -)(A-)B)aMP 7) Elx cp —> i|) h Vx(cp - GEN 8) h (Excp -> t|>) -> Vx (cp->t|>) věta o dedukci □ dikatova logika. Věta o korektnosti. 91 Predikátová logika, věta o úplnosti (úvod). 92 . 65. Nechť J je teorie a cp formule jazyka teorie T. Jestliže T h cp, pak V- iz. Stačí ověřit následující tvrzení: Te-li ty instancí jednoho ze schémat P1-P5 (příp. také R1-R3, pokud azyk teorie T je jazyk s rovností) a M je model T, pak M h ty- Te-li M model T a ty, L, formule jazyka teorie T, kde M h ty a \4 h ty -> pak A4 h l- Te-li jVÍ model T a \p formule jazyka teorie T, kde M^ty, pak jVÍ h Vxi|). dndukcí vzhledem k i je pak již triviální ukázat, že je-li ty-\, ■ ■ ■ ,tyy_ iz formule cp v T a M je model T, pak Th^i 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 |= 2.) Buď T bezesporná teorie. Pak existuje formule cp jazyka teorie T, která není v T dokazatelná (tj. T 1/ cp). Obměnou 1. pak ale dostáváme, že cp není sémantickým důsledkem T (tj. T \f cp). To znamená, že existuje takový model T, kde není pravdivá cp. Zejména má tedy T model. ikátová logika. Věta o úplnosti (úvod). 93 Predikátová logika, věta o úplnosti (úvod). 94 > 1.) Užitím 2. dokážeme obměnu 1. Nechť tedy T 1/ cp, a nechť čp je miverzální uzávěr cp. Ukážeme, že T U {-čp] je bezesporná; pak podle 2. ná T u {-čp} model, tedy T ^ cp. U \~V Je bezesporná: Předpokládejme naopak, že je sporná. 1) TU {-čp} h čp TU {-čp} 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 MPna2),3) 5) T h cp opakovaně P4 a MP obdrželi jsme tedy spor s tím, že T 1/ 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á. ídikatova logika. Rozšíření teorie. 95 Predikátová logika, věta o konstantách. 96 nice 67. reorie Sje rozšíření teorie T, jestliže jazyk teorie S obsahuje jazyk teorie a v teorii S jsou dokazatelné všechny axiómy teorie T. rozšíření S teorie T se nazývá konzervativní, jestliže každá formule azyka teorie T, která je dokazatelná v S, je dokazatelná i v T. Teorie S a T jsou ekvivalentní, jestliže S je rozšířením T a současně T je ■ozšířením S. Věta 68 (o konstantách). Nechť S je rozšíření 1 vzniklé obohacením jazyka teorie T o nové navzájem různé konstanty ci, • • •, c k (nové axiómy nepřidáváme), a nechť, • • • ^^jsou navzájem různé proměnné. Pak pro každou formuli cp jazyka teorie T platí, že T h cp právě když S h cp(xi/ci, • • • ,xk/ck). Důkaz. Jelikož ci, • • •, jsou navzájem různé, stačí dokázat, že T I cp právě když S h cp(x/c). ==>: K důkazu cp v T připojíme formule Vx cp, Vx cp —> cp(x/c I, cp(x/c) a obdržíme tak důkaz formule cp(x/c) v S. < : Nechť\pi, • • • ,ipk 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 (c/y), • • • ,ipi(c/y) důkaz v T. Rozlišíme tyto možnosti: ;dikatova logika. Věta o konstantách. 97 Predikátová logika, věta o konstantách. 98 Te-li tyi instancí P1-P5 (příp. R1-R3), je také ^(c/y) instancí téhož ichématu. Te-li tyi axióm teorie T, pak se v tyi nevyskytuje c a formule tyi a ^t(c/y) sou tedy totožné. Testliže tyi vyplývá z tyj a tym pomocí MP, je tym tvaru tyj ^> tyi a. formule l^mtc/y) je tedy formulí tyj (c/y) —> tyi(c/y). Takže formule tK(c/y) yplývá z tyj (c/y) a tym{c/y) pomocí MP. Testliže tyi vyplývá z tyj pomocí GEN, je tyi tvaru \fxtyj. Stačí si ivědomit, že (\fxtyj )(c/y) je tatáž formule jako Vx [tyj (c/y)), neboťxaij sou různé. Ukázali jsme, že T h cp(x/c)(c/y). Dále 1) T h cp(x/y) cp(x/y) je totéž co cp(x/c)(c/y) 2) ThVycp(x/y) GEN 3) hVycp(x/y)^(cp(x/y)(y/x)) P4 4) Th jednou volnou proměnnou x existuje v jazyce teorie T konstanta c aková, že T h 3x cp —> cp(x/c). Teorie 1 je úplná, jestliže je bezesporná a pro každou uzavřenou formuli i jejího jazyka platí buď J h cp nebo TI—'cp. Věta 70 (o henkinovské konstantě). Buď T teorie a cp(x) formule jejího jazyka. Je-li S rozšíření T', tóeré vznikne přidáním nové konstanty cv a formule 3x cp —> cp (x/c3y£,(x/y): 1) {Vy-£,(x/y)}l-Vy-£,(x/y) 2) {yy-£,(x/y)}h-£,(x/y)(y/x) P4 a MP 3) {Vy-£,(x/y)} h přepis 4) {Vy-£,(x/y)}l-Vx-£, GEN 5) h Vy-£,(x/y) -> Vx-£, dedukce 6) h 3x£,^ 3y£,(x/y) taut. (A- (-B -> -A) a MP. DIKATOVA LOGIKA. Henkinovské a úplné teorie. 101 PREDIKÁTOVÁ LOGIKA. Henkinovské a úplné teorieJjTÔ2 íťR značí teorii vzniklou pouhým pridaním konstanty c,pkT. Nechť ty rmule jazyka teorie T taková, že S h ty. Nechť y je proměnná, která se skytuje ani ve cp, ani v ty. Platí: 1) 2) 3) 4) 5) 6) 7) 8) 9) S hty R h (3xcp cp(x/c cp(x/y)) -^\p ThVy((3xcp^cp(x/y))^) T h 3y(3xcp -> cp(x/y)) -> \p h (3xcp -> 3ycp(x/y)) -> 3y(3xcp T h (3xcp -> 3ycp(x/y)) -> ty h 3xcp -> 3ycp(x/y) Jhty předpoklad S = RU{3xcp -> 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 □ Věta 71 (o henkinovském rozšíření). Ke každé teorii existuje henkinovská teorie, kterájejejím konzervativním rozšířením. Důkaz. Buď T (libovolná) teorie. Pro každé n > 0 definujeme teorii Jn takto: ""»• T0 = T. Teorie Ti+i vznikne z T tak, že pro každou formuli cp(x) jazyka teorie T přidáme novou konstantu c

cp(x/cočetný, opírá se tento předpoklad o axióm výběru. . 72 (o zúplňování teorií). Ke každé bezesporné teorii existuje její íření se stejným jazykem, které je úplnou teorií. xz. Buď T teorie, a nechť r< je dobré uspořádání na množině všech Ťených formulí jazyka teorie T. Pro každou uzavřenou formuli cp ta teorie T definujeme teorii lv induktivně takto: íe-li cp nejmenší prvek v uspořádání klademe lv = T, [J T£U{cp} je-li [J T£ U {cp} bezesporná; íinak Tp = \ £^ £^ |jT£U{-cp} jinak. ř,X

cp (užitím věty o dedukci). Z toho dostáváme S h ty A^ty pro libovolné ty, neboť (A -> -A) -> ((-A -> A) -> {ty A^ty)) je výroková tautologie (použijeme 2x MP). Tedy i S je sporná, což je spor s předchozím bodem. DIKÁTOVÁ LOGIKA. Henkinovské a úplné teoneJTôŠ] PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 106 íme teorii U která vznikne sjednocením všech Jv. Zjevně Uje rozšíření ná stejný jazyk jako T. Pokud by U byla sporná, existoval by důkaz -np v U. Tento důkaz využívá pouze konečně mnoho axiómů U, proto -^ty je dokazatelná i v nějaké Jv, což je spor. □ Definice 73. Buď T teorie, kde jazyk teorie T obsahuje alespoň jednu konstantu. Kanonická struktura teorie T je realizace M jazyka teorie T, kde '»» univerzum M je tvořeno všemi uzavřenými termy jazyka teorie T; '»» relizace funkčního symbolu f arity n je funkce f M, která uzavřeným termům ti, • • •, t^ přiřadí uzavřený term f (ti, • • •, tn); '»» realizace predikátového symbolu P arity m je predikát PM definovaný takto: PjVL(ti, • • •, tm) platíprávě když T h P(ti, • • •, tm). DIKATOVA LOGIKA. Kanonická struktura. 107 PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 108 . 74 (o kanonické struktuře). Nechť J je úplná henkinovské teorie, a iťjazyk teorie J je jazykem bez rovnosti. Pak kanonická struktura teorie modelem T. iz. Nechť M je kanonická struktura teorie T. Ukážeme, že pro rolnou formuli cp jazyka teorie T platí následující: Testliže (p je uzavřená instance formule cp, pak Thíp právě když M h Q- íož lze (bez újmy na obecnosti) předpokládat, že prvky T jsou uzavřené Lule, plyne z výše uvedeného, že M je model T. ikcí ke struktuře cp: p = P(ti, • • •, tn). Buď ?(t\, ■ ■ ■ ,ťn) libovolná uzavřená instance. Podle lefmice kanonické struktury M \=P{t\, - ■ ■ ,ťn) právě když >p(ť„'",t;). '»» cp = -'ip. Buď -'ip libovolná uzavřená instance. Jelikož ty je uzavřená instance ty, podle IP platí T h -$ právě když M h í • Dále T I—-$ právě když T (/-$ (T je bezesporná) právě když M \£ $ (IP) právě když M h ""»• cp = ty —> £,. Každá uzavřená instance této formule je tvaru $ —> £, kde $ je uzavřená instance ty a % je uzavřená instance £,. Nechť T h -$ —> t- Jelikož $ je uzavřená formule a T je upíná, platí buď T h -$ nebo T I—V prvém případě dále T h t (MP) a užitím IP celkem dostáváme M h $ a M. h t- Proto také h $ —> £• V druhém případě T (/-$ (T je bezesporná), proto ^ $ (IP), tudíž Nechť M h $ —> %■ Pak buď ^ $ nebo h t- V prvém případě T 1/ •$ podle IP, tudíž T I—op neboť T je úplná. Proto T h -$ —> t užitím tautologie -A —> (A —> B) a MP. V druhém případě T h £, proto T h -$ —> t užitím tautologie A —> (B —> A) a MP. ©IKATOVA LOGIKA. Kanonická struktura. 109 PREDIKÁTOVÁ LOGIKA. Kanonická struktura. o = Vxty. Buď Vxi|) libovolná uzavřená instance. Pak ty(x), jinak by Vxip íebyla uzavřená. Nechť T h Vxif). Pak pro libovolný uzavřený term t platí T h ty [x/1) (P4 a MP). Podle IP M h ty(x/t). Jelikož tento argument funguje pro libovolný uzavřený term t, platí také M |= Vxi|>. Nechť T I/Vxij). Pak také T l/Vx— ty (kdyby T h Vx— ty, dostaneme dále T h — ty (P4 a MP) a T h ty (tautologie —A -> A a MP), T h Vxt|) (GEN), spor). Jelikož T \f Vx^^tJ), platí T I—Nx-^^ty neboť T je úplná. Tedy T h 3x-^ty. Jelikož T je henkinovská, platí T h 3x~^ty —> -aj>(x/c). Tedy T I—ty(x/c) a proto T \f ty(x/c) neboť T je bezesporná. Podle IP M \f ty(x/c), tedy M h -ty{x/c). Proto A4 ^ VxtJ). Věta 75. Nechť J je úplná henkinovské teorie, a nechť jazyk teorie T je jazykem s rovností. Pak T má model. Důkaz. Buď S teorie (s jazykem bez rovnosti), která vznikne rozšířením T o nový binární predikátový symbol = a axiomy R1-R3. Symbol = v teorii S je tedy mimologický a může být realizován „jakkoliv". Axiomy R1-R3 jsou v S „normální" axiómy. Stačí nám ukázat, že S má takový model, kde = je realizován jako identita. Takový model pak jistě bude i modelem T (kde = je chápáno jako logický symbol). □ DIKATOVA LOGIKA. Kanonická struktura. [HII PREDIKÁTOVÁ LOGIKA. Kanonická struktura. M kanonická struktura teorie S, a nechť ~ je realizace = v S (tj. ti ě když S h ti = t2). Dokážeme, že ~ je nutně ekvivalence: t2 ■eflexivita: S h x=x (Rl), S h Vxx=x (GEN), S h Vxx=x MP). Tedy t ~ t. t=t (P4), S h t=t symetrie: nechť s ~ t, tj. S h s=t. Platí I h (xi=yi Ax2=y2) —> (xi=*2 —> 1^1=^2) (R2, = hraje i roli P). Užitím >EN, P4 a MP dostaneme S h (s=t A s=s) -> (s=s -> t=s). Užitím MP lostaneme S h t=s. ľranzitivita: podobně. Nyní již můžeme definovat strukturu O pro jazyk teorie S: '»» Nosičem O jsou třídy rozkladu nosiče M podle ~. '»» Funkční symbol f arity n je realizován takto: fo([tl],-",[tn]) = [fAí(tl,---,tn)] Predikátový symbol P arity m je realizován takto: Po ([ti ], • • •, [tm]) právě když F'm (ti, • • •, tm) Korektnost této definice (tj. nezávislost na volbě reprezentantů) se dokáže pomocí R1-R3 podobným stylem jako výše. Snadno se ověří, že realizací uzavřeného termu t je ve struktuře Oje [s] právě když S h s=t. To znamená, že predikátový symbol = je v O realizován jako identita. dikatova logika. Kanonická struktura. 113 Predikátová logika, věta o úplnosti. 114 rá ukázat, že Oje modelem S. Podobně jako ve větě 75 budeme chtít :ázat, že pro libovolnou formuli cp(xi,... ,xrL) jazyka teorie S platí: Testliže ti, • • •, jsou uzavřené termy jazyka teorie S, pak "h q>(xi/tu - ■ ■ ,xn/tn) právě když O h pak J h cp. Důkaz. Jde o jednoduchý důsledek předchozích vět. □ Kurt Gôdel (1906-1978) dikatova logika. Věta o kompaktnosti. 115 . 77. Teorie T má model, právě když každá její podteorie s konečně ha axiómy (a s minimálním jazykem, v němž jsou tyto axiómy ulovatelné) má model. iz. Směr „=>" je triviální. Pro opačnou implikaci stačí ukázat, že T je sporná (pak T má model podle věty o úplnosti). Kdyby T byla sporná, :oval by důkaz formule ty A^ty v T. Tento důkaz je konečný, využívá jen konečně mnoho axiómů T, které tvoří spornou podteorii T, □ Ipredikátová logika. Lowenheimova-Skolemova uSS Poznámka 78. Z důkazu věty 71 plyne, že každá bezesporná teorie s jazykem bez rovnosti má model kardinálity max{|L|, K0} (při rozšíření teorie na henkinovskou bylo přidáno |L| • K0 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ť J je teorie a nechť pro každé n 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 e N definujeme formuli (spn = Vxi • • • Vx^By xi =£y A • • • A x^y a teorii Sn = T u {cpi, • • •, cp^}. Podle předpokladu věty má každá 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. □ DIKÁTOVÁ LOGIKA. Lowenheimova-Skolemova v&JáLl VĚTA O NEÚPLNOSTI. Úvod. 118 . 80 (Lowenheimova-Skolemova). Nechť J je teorie sjazykemL, která lekonečný model. Nechť k je nekonečný kardinál takový, že k > |L|. Pak i model mohutnosti k. ■xz. Nechť M je nekonečný model T. Jazyk L rozšíříme o systém . < k} nových konstant a k T přidáme axiómy {ct ^ Cj i, j < k}. ržíme tak teorii T'. Nechť K je konečná část T, a nechť ci, • • •, cn jsou hny nově přidané konstanty, které se vyskytují ve formulích teorie K )vých konstant je jen konečně mnoho). Pokud tyto konstanty zujeme navzájem různými prvky nosiče M, obdržíme model teorie K. lá konečná část T' je tedy splnitelná. Podle věty o kompaktnosti má model i teorie T. Nosič tohoto model ale nutně obsahuje alespoň k ;ájem různých individuí. □ »"» Jazyk aritmetiky je jazyk s rovností obsahující konstantu O, 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, Oje 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. »"» Slovem „úplné" se myslí, že T h cp právě když cp e Tfa(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. O NEÚPLNOSTI. Turíngův stroj. 119 Uan Turing (1912-1954) »"» Definoval pojem Turingova stroje a s jeho pomocí ukázal, že problém pravdivosti formulí prvního řádu je nerozhodnutélný. »"» Považován za zakladatele informatiky (jako vědy). »"» Turingů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í. VĚTA O NEÚPLNOSTI. Turingův stroj (neformálně). 120 P 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 nej levě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. A O NEÚPLNOSTI. Turingův stroj (neformálně). 121 VĚTA O NEÚPLNOSTI. Turingův stroj (formálně). 122 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é lezastavit (cyklit). /stupni slovo je akceptované, jestliže stroj po konečně mnoha krocích lojde do akceptující konfigurace. Soubor všech vstupních slov, která ■troj akceptuje, tvoří jazyk akceptovaný daným strojem. Definice 81. Turingův stroj je devítice M — (Q, 1, 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 g ľ je prázdný znak; '* • g V je znak konce pasky; * 6 : Q x r —> Q x r x {L, R} je přechodová funkce, kde pro každej e Q platí 5(p, •) = (<ť •> R) Pm nějaké q g Q; '* q o g Q je počáteční stav; * Acc c Q je množina akceptujících stavů; '* Rej Q Q\Accje množina zamítajících stavů. O NEÚPLNOSTI. Turingův stroj (formálně). 123 VĚTA O NEÚPLNOSTI. Turingův stroj (formálně). 124 Jechťo,# e" Q u T, a nechť C (M) -e tvaru [X, q]. (ľu{#}) x (Q U {o}). Prvky C(M) zapisujeme konfigurace stroje M je slovo [Xi ,pi] ■ ■ ■ [Xn,pn] [#,o] g C(M)* takové, že n > 1, U = •, Xi / # pro každé 1 < i < n, a existuje právě jedno 1 < j < n, kde p j g Q. >lovo Xi ■ ■ ■ Xn nazýváme obsahem pásky dané konfigurace, a stav p, kontrolním stavem dané konfigurace. ikceptující resp. zamítající konfigurace je konfigurace, jejíž kontrolní stav je ikceptující resp. zamítající. Koncová konfigurace je konfigurace, která je ikceptující nebo zamítající. Soubor všech konfigurací stroje M značíme :onf(M). Írok výpočtu je funkce step : Conf(M) —> Conf (M), která je pro koncové konfigurace definována jako identita a pro nekoncové konfigurace takto: - step(y [X, q] [Y, o] p) = y [Z, o] [Y,r] p jestliže 6(q,Y) — (r, Z,R) »- step{y[Y,o] [X,q] p) =y[Z,o\ [Y, r] p jestliže 6(q,Y) = (r,Z,L) »- síep(y[X,q] [#,o]) = y[Z,o] [B,r] [#,o] jestliže 6(q,Y) — (r, Z,R) in» Nechť w — ai ■ ■ ■ an je slovo nad abecedou I {w může být i prázdné). Iniciální konfigurace pro w je konfigurace a(w) = [•, qo][ai, °] ■ ■ ■ [an, o] [#, o]. Slovo w je akceptované strojem M, jestliže existuje k g N takové, že síepk(a(w)) je akceptující konfigurace. Jazyk akceptovaný strojem M, označovaný L(M), je soubor všech weľ, které jsou akceptované strojem M. Nechť ([Xi ,pi], [X2,P2], [Yi, qi], [Yz, qi\) je čtveřice symbolů z C(M). Tato čtveřice je kompatibilní, jestliže existuje nekoncová konfigurace a g Conf (M) a vhodné 1 < i < íen(a) takové, že a(i) = [Xi ,pi], a(i+1) = [X.2,P2] a dále (3(i) = [Yi, qi], |3(i+1) = [Yz, cli] kde (3 = step(oí). 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ť a g Conf (M) je konfigurace a nechť (3 g C(M)* je slovo stejné délky, jako má a. Pak (3 = step(oC) právě když pro každé 1 < i < íen(a) platí, že (a(i),a(i+1),|3(i),|3(i+1)) g Comp(M). 125 A O NEÚPLNOSTI. Vlastnosti jazyků. zavedeme několik pojmů, které se týkají jazyků. íazyk L c I* je rekurzivně vyčíslitelný, jestliže L — L (M) pro nějaký Turingův troj M. Jazyk L c I* je rekurzivní, jestliže L — L (M) pro nějaký Turingův stroj A, který zastaví pro každé vstupní slovo. Jednoduché pozorování je, že jazyk . 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 "uringova stroje jsou prvky nějaké fixní spočetné množiny (to lze bez újmy na >becnosti). Pak každý Turingův stroj M lze jednoznačně zapsat jako slovo ■ode(M) g {0,1}*. Podobně každé vstupní slovo w stroje M lze jednoznačně ;apsat jako slovo code(w) e {0,1}*. Navíc lze předpokládat, že každé v e {0,1}* e kódem nějakého stroje Mv a nějakého vstupního slova wv stroje Mv. Jvedené kódování umožňuje zkonstruovat univerzálni Turingův stroj li se -stupni abecedou {0,1, #} takový, že pro každé slovo tvaru u#v, kde u,v g {0,1}*, )latí, že li akceptuje u#v právě když stroj Mu akceptuje slovo wv. Jvažme jazyk Accept = {u#v | Mu akceptuje wv}- Podle předchozího boduje \ccept rekurzívně vyčíslitelný. Ukážeme, že Accept není rekurzívní. Podle ednoho z předchozích bodů pak jazyk Accept není rekurzivně vyčíslitelný. 127 A O NEÚPLNOSTI. Peanova aritmetika. lim z pokusů o vytvoření rekurzivní a úplné teorie aritmetiky byl edující systém nazývaný Peanova aritmetika (seznam Peanových mů bývá v literatuře uváděn v různých podobách): 'x S(x) ^ 0 Wy S(x)=S(y) -> x=y cp(S(x)))) —> Vxcp(x), kde cp je formule s jednou volnou iroměnnou x. 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ď JVť 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, žeueL(M') právě když u#u ^ L(M) Nechť v = code(M'). Platí wv e L(M')? ""»• Ano. Pak v#v ^ L(M), tj. Mv = M' neakceptuje wv, spor. '»'»• Ne. Pak v#v e L(M), tj. Mv = M' akceptuje wv, spor. Z předpokladu existence stroje M se nám podařilo odvodit spor. Stroj M tedy neexistuje. 126 □ VĚTA O NEÚPLNOSTI. Peanova aritmetika. f 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,vv,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 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ý. 128 A O NEÚPLNOSTI. Jazyk Valid. 129 VĚTA O NEÚPLNOSTI. Jazyk Valid. 130 ť Valid je jazyk nad abecedou {v, + , *, 0, S, (,), V, —>, =} obsahující zápisy všech ulí teorie Tfa(No, *, +). Naším cílem je dokázat, že Valid není rekurzivně li telný jazyk. 85. Jazyk Valid není rekurzivně vyčíslitelný. iz. Ukážeme, že existuje Turingův stroj M, který pro každé vstupní slovo v nad sáou {0,1, #} zastaví v konfiguraci, kdy je na pásce zapsáno slovo w nad sáou {v, + , *,0, S, (,), V, —>,=} takové, že v g Accept právě když w e Valid. á by tedy jazyk Valid byl akceptovaný nějakým strojem M', stačilo by „napojit 2 M a M' za sebe" a dostali bychom stroj akceptující jazyk Accept, což je spor. O NEÚPLNOSTI. Jazyk Valid. 131 3ez újmy na obecnosti můžeme předpokládat, že zápisy konfigurací co, ai, ■ ■ ■, ocn mají stejnou délku. (Zápisy „krátkých" konfigurací lze „doplnit" ;prava symboly [B, o], zapsanými těsně před symbol [#, o].) 'osloupnost konfigurací cto, základu p. Zápis tohoto čísla vypadá takto: [an] [k„_i] ■ ■ ■ [cto], kde [ccj je zápis konfigurace oa 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 ormuli „vypočte", na pásku zapíše formuli -^3y ACOMP(y) a přejde do ikceptujícího stavu. 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í oío , oít , • • •, oín s následujícími vlastnostmi: -*- ao je počáteční konfigurace pro slovo wv. z=p) -*- „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+by+upij A a MATCH{v, y, yc)) A O NEÚPLNOSTI. Jazyk Valid. 133 VĚTA O NEÚPLNOSTI. Jazyk Valid. 134 „V p-árním zápisu v je jako první (zprava) zapsána konfigurace [.,q0] [a,,o]..-[an,o] [B, o] ■ ■ ■ [B, o] [#,o] kde wv = ai ■ ■ ■ an a délka této kofigurace je logp (c) — 1." (Předpokládáme, že c je mocnina p.) START{v,c) = pn+1 DIGIT{v,y, [B, o])] „V p-árním zápisu v se vyskytuje symbol s akceptujícím kontrolním stavem." (Předpokládáme, že d je mocnina p.) Nechť H je soubor všech p-árních číslic tvaru [X, q], kde X g ľ a q je akceptující kontrolní stav stroje Mu. ACC{v,d) =3y{POWERv{y) A y, —, —} a lze je tedy kódovat čísly stejným způsobem jako konfigurace Turingových strojů. Pro každou formuli cp označíme symbolem [cp] číslo, které je jejím kódem. Lema 87 (Gôdelovo lema o pevném bodě). Pro každou formuli 4> (x) existuje uzavřená formule i taková, že PA I- t <-> ip( pr]). (Formule i říká „4> platí pro můj kód".) Důkaz, (osnova) Pro libovolnou fixní proměnnou xo lze sestrojit formuli SUBST(x,y,z), která říká následující: »"» „Číslo zje kódem formule, kterou získáme substitucí proměnné x0 za konstantu s hodnotou x ve formuli s kódem y." Např. SUBST{5, |~ ip(y)) právě když ^hVy (y = r^l>(y)) 'y (y = fo-í r«r(xo)l)l ->*|>(y)) = Vy (y = |Y| -> ip(y)) \f h Vy (y = |Y| -> ip(y)) právě když JV \= ip( |Y|] íhozí argument se opírá o sémantickou ekvivalenci jistých formulí; ekvivalence o formulí je ale ve skutečnosti dokazatelná v PA. Např. RAh(Vy (y = |Y| -> ip(y))) <-> ip(prl) t třeba v posledním bodu. Proto PA h t <-> 4> ( [t] ). □ O NEÚPLNOSTI. Godelův důkaz. íule p tedy říká Já nejsem dokazatelná", přičemž toto tvrzení je v PA zatelné. Z korektnosti PA dostáváme, že V h p <-> -PROVABLEf [p] ] de musí platit JV \= p; kdyby totiž TV |= -■p, dostaneme A/" h PROVABLEf [p]), > PA h p a tedy JV \= p, spor. ož AT h p, platí AT h -PROVABLEf [p]), tedy JV ^ PROVABLEf [p]), proto PA \f p. íule p je tedy pravdivá v JV, ale není dokazatelná v PA. □ VĚTA O NEÚPLNOSTI. Godelův důkaz. 138 Věta 88 (1. věta o neúplnosti, Gódelova). Lze sestrojit uzavřenou formuli p, která je pravdivá v JV, ale není dokazatelná v PA. Důkaz, (osnova) Ukáže se, že i důkazy (tj. konečné posloupnosti formulí) je možné kódovat čísly, a že existuje formule PROOE(x,y), která říká, že x je kódem důkazu (v PA) pro formuli s kódem y. Dokazatelnost v PA lze pak zapsat formulí »4 PROVABLE(y) = 3xPROOF{x,y) Pak pro každou uzavřenou formuli cp platí »'4- PA h cp právě když JV \= PROVABLE{ [cp] ] Dále lze ukázat »'4- PA h cp právě když PA h PROVABLE{ [cp] ] Směr „<=" plyne ihned z korektnosti PA (indukcí se snadno ukáže, že jestliže PA h cp, pak JV \= cp). Opačný směr je výrazně pracnější. Nyní stačí aplikovat lema 87 na formuli -^PROVABLE(x). Dostaneme tak sentenci p takovou, že platí »4 PAh pH -PROVABLEf [p] ] VĚTA O NEÚPLNOSTI. Kódování tvrzení oPAv PA. 140 Pozorování: '»» Důkaz věty 88 se opírá o možnost vyjádřit jistá matatvrzení o formulích aritmetiky a teorii PA jako formule aritmetiky. Typicky lze takto vyjádřit tvrzení, která se týkají dokazatelnosti. Metatvrzení „PA h cp" lze vyjádřit formulí PROVABLE( [cp]). Dokonce platí PA h cp právě když PA h PROVABLE( [cp]). I metatvrzení „PA h cp právě když PA h PROVABLE( [cp])" lze vyjádřit v PA pomocí formule PROVABLE( [cp]) <-> PROVABLE( \PROVABLE{ [cp])]) I tato formule je v PA dokazatelná. Bezespornost teorie PA lze vyjádřit formulí CONSIS = ~^PROVABLE( [£, A -■£,]), kde £Je (nějaká) formule. O NEÚPLNOSTI. Kódování tvrzení oPAv PA. 141 VĚTA O NEÚPLNOSTI. Druhá věta o neúplnosti. 142 Tsou ale i metatvrzení o formulích aritmetiky, která jako formule iritmetiky vyjádřit nelze. Typicky se jedná o tvrzení týkající se pravdivosti. Tvrzení JV" h (PROVABLE{ \PROVABLE{ [p])]) A PROVABLE{ \^PROVABLE{ [p])])] Proto platí také PA h PROVABLE{ [p]) -> -^CONSIS. O NEÚPLNOSTI. Druhá věta o neúplnosti. 143 ěnou uvedeného tvrzení dostáváme 5A h CONSIS -> -^PROVABLE{ [p] ] y PA h CONSIS, platilo by také PA h -^PROVABLE{ [p]) (aplikací MP). Už dříve ale ukázali (viz důkaz věty 88), že ÍAhpH -^PROVABLE{ [p] ] i aplikací MP tedy dostáváme PA h p. Výše jsme ale ukázali, že předpoklad p implikuje, že PA je sporná. Celkem tedy dostáváme, že předpoklad CONSIS implikuje, že PA je sporná. □ ítuitivní úrovni: druhá věta o neúplnosti říká, že bezespornost „dostatečně " teorie (např. teorie množin) nelze v této teorii dokázat. Jediná možnost je ít metaargumenty, tj. zdůvodnit bezespornost dané teorie pomocí teorie „vyšší". >ezespornost této vyšší teorie není ovšem možno prokázat v ní samé. Na nějaké ni nám prostě nezbývá, než v bezespornost uvěřit, resp. ji předpokládat. lovy výsledky o neúplnosti mají tedy i svůj epistemologický význam.