1 MATEMATICKÁ LOGIKA Prezentace ke kurzu MA007 Antonín Kučera 2005 LOGIKA. 2 Bů h Lidské uvažová ní Logika LOGIKA. 2 Bů h Lidské uvažová ní Logika Logika (z řeckého oo) zkoumá způ sob vyvozování závěrů z před- pokladů . LOGIKA. 2 Bů h Lidské uvažová ní Logika Logika (z řeckého oo) zkoumá způ sob vyvozování závěrů z před- pokladů . V běžné řeči se ,,logikou" označuje myšlenková cesta, která vedla k daným závěrů m. LOGIKA. 2 Bů h Lidské uvažová ní Logika Logika (z řeckého oo) zkoumá způ sob vyvozování závěrů z před- pokladů . 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). LOGIKA. 2 Bů h Lidské uvažová ní Logika Logika (z řeckého oo) zkoumá způ sob vyvozování závěrů z před- pokladů . 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?" LOGIKA. Neformá lní, formá lní, matematická . 3 LOGIKA. Neformá lní, formá lní, matematická . 3 Neformá lní logika studuje problematiku správné argumentace v přirozeném jazyce. LOGIKA. Neformá lní, formá lní, matematická . 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í. LOGIKA. Neformá lní, formá lní, matematická . 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: LOGIKA. Neformá lní, formá lní, matematická . 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); LOGIKA. Neformá lní, formá lní, matematická . 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.) ARISTOTELOVA LOGIKA. 4 Aristoteles (384-322 př. Kr.) Považován za zakladatele (formální) logiky. Zavedl a prozkoumal pojem sylo- gismu. Aristoteles zkoumal také pravdi- vostní módy a položil tak základy modální logiky. ARISTOTELOVA LOGIKA. Logický čtverec. 5 I A O E Necht' S a P jsou neprá zdné vlast- nosti. Aristoteles rozlišuje následu- jící základní kategorická tvrzení: ARISTOTELOVA LOGIKA. Logický čtverec. 5 I A O E Necht' S a P jsou neprá zdné vlast- nosti. Aristoteles rozlišuje následu- jící základní kategorická tvrzení: A všechna S jsou P ARISTOTELOVA LOGIKA. Logický čtverec. 5 I A O E Necht' S a P jsou neprá zdné vlast- nosti. Aristoteles rozlišuje následu- jící základní kategorická tvrzení: A všechna S jsou P E žá dná S nejsou P ARISTOTELOVA LOGIKA. Logický čtverec. 5 I A O E Necht' S a P jsou neprá zdné vlast- nosti. Aristoteles rozlišuje následu- jící základní kategorická tvrzení: A všechna S jsou P E žá dná S nejsou P I některá S jsou P ARISTOTELOVA LOGIKA. Logický čtverec. 5 I A O E Necht' S a P jsou neprá zdné vlast- nosti. Aristoteles rozlišuje následu- jí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 P ARISTOTELOVA LOGIKA. Logický čtverec. 5 I A O E Necht' S a P jsou neprá zdné vlast- nosti. Aristoteles rozlišuje následu- jí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 P Mnemonika: AffIrmo--nEgO (tvrdím--popírám) ARISTOTELOVA LOGIKA. Logický čtverec (pokr.) 6 I A O E ARISTOTELOVA LOGIKA. Logický čtverec (pokr.) 6 I A O E A a O jsou kontradiktorická, tj. nemohou být současně pravdivá ani současně nepravdivá. I a E jsou rovněž kontradiktorická. ARISTOTELOVA LOGIKA. Logický čtverec (pokr.) 6 I A O E 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á. ARISTOTELOVA LOGIKA. Logický čtverec (pokr.) 6 I A O E 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á. ARISTOTELOVA LOGIKA. Logický čtverec (pokr.) 6 I A O E 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ě O je subalterní E. ARISTOTELOVA LOGIKA. Sylogismy. 7 ARISTOTELOVA LOGIKA. Sylogismy. 7 Sylogismy jsou jednoduché ú sudky tvaru Hlavní premisa Vedlejší premisa Zá věr ARISTOTELOVA LOGIKA. Sylogismy. 7 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 S a M; vedlejší premisa obsahuje P a M; závěr je tvaru S z P. ARISTOTELOVA LOGIKA. Sylogismy. 7 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 S a M; 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 S y M S z P II: P x M S y M S z P III: M x P M y S S z P IV: P x M M y S S z P ARISTOTELOVA LOGIKA. Sylogismy. 7 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 S a M; 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 S y M S z P II: P x M S y M S z P III: M x P M y S S z P IV: P x M M y S S z P Celkem tedy existuje 4 43 = 256 sylogismů . ARISTOTELOVA LOGIKA. Sylogismy (pokr.) 8 ARISTOTELOVA LOGIKA. Sylogismy (pokr.) 8 Jen 24 sylogismů je platných: ARISTOTELOVA LOGIKA. Sylogismy (pokr.) 8 Jen 24 sylogismů je platných: Forma I: AAA, AII, EAE, EIO (Barbara, Darii, Celarent, Ferio), AAI, EAO (subalterní módy); ARISTOTELOVA LOGIKA. Sylogismy (pokr.) 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, Cesare, Baroco, Festino), AEO, EAO (subalterní módy); ARISTOTELOVA LOGIKA. Sylogismy (pokr.) 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, Cesare, Baroco, Festino), AEO, EAO (subalterní módy); Forma III: AAI, AII, EAO, EIO, OAO, IAI (Darapti, Datisi, Felapton, Ferison, Bocardo, Disamis); ARISTOTELOVA LOGIKA. Sylogismy (pokr.) 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, Cesare, 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). ARISTOTELOVA LOGIKA. Sylogismy (pokr.) 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, Cesare, 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). ARISTOTELOVA LOGIKA. Platnost sylogismů . 9 S P A (všechna S jsou P) S P E (žá dná S nejsou P) S P ˇ I (některá S jsou P) S P ˇ O (některá S nejsou P) šedé oblasti jsou prázdné; symbol ,,ˇ" označuje neprázdné oblasti; bílé oblasti mohou být prázdné i neprázdné. ARISTOTELOVA LOGIKA. Platnost sylogismů (pokr.) 10 ARISTOTELOVA LOGIKA. Platnost sylogismů (pokr.) 10 Uvažme nyní např. AEE sylogismus druhé formy (Camestres): Všechna P jsou M Žádná S nejsou M Žádná S nejsou P S P M Tento sylogismus je tedy platný. ARISTOTELOVA LOGIKA. Platnost sylogismů (pokr.) 10 Uvažme nyní např. AEE sylogismus druhé formy (Camestres): Všechna P jsou M Žádná S nejsou M Žádná S nejsou P S P M 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 S P M ˇ S P M ˇ Druhý diagram podává protipříklad, sylogismus platný není. ARISTOTELOVA LOGIKA. Platnost sylogismů (pokr.) 11 ARISTOTELOVA 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 S P M ? ARISTOTELOVA 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 S P M ? 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." 12 George Boole (1815­1864) 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í po- jmy ,,logický součin" a ,,logický sou- čet".). ALGEBRA LOGIKY. Motivační příklad. 13 ALGEBRA LOGIKY. Motivační příklad. 13 Uvažme následující sylogismus: Všechna S jsou M Žá dná M nejsou P Žá dná S nejsou P ALGEBRA LOGIKY. Motivační příklad. 13 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 M M P = 0 S P = 0 ALGEBRA LOGIKY. Motivační příklad. 13 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 M M P = 0 S P = 0 a dále na S M = 0 (1) M P = 0 (2) S P = 0 (3) ALGEBRA LOGIKY. Motivační příklad. 13 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 M M P = 0 S P = 0 a dále na S M = 0 (1) M P = 0 (2) S P = 0 (3) Pokusme se nyní ,,odvodit" (3) z (1) a (2): ALGEBRA LOGIKY. Motivační příklad (pokr.) 14 ALGEBRA LOGIKY. Motivační příklad (pokr.) 14 Z toho, že S M = 0 a X 0 = 0 pro libovolné X dostáváme (S M ) P = 0 (4) ALGEBRA LOGIKY. Motivační příklad (pokr.) 14 Z toho, že S M = 0 a X 0 = 0 pro libovolné X dostáváme (S M ) P = 0 (4) Podobně z (2) plyne (M P) S = 0 (5). ALGEBRA LOGIKY. Motivační příklad (pokr.) 14 Z toho, že S M = 0 a X 0 = 0 pro libovolné X dostáváme (S M ) P = 0 (4) Podobně z (2) plyne (M P) S = 0 (5). Ze (4), (5) a faktu, že 0 0 = 0, plyne ((S M ) P) ((M P) S) = 0 (6) ALGEBRA LOGIKY. Motivační příklad (pokr.) 14 Z toho, že S M = 0 a X 0 = 0 pro libovolné X dostáváme (S M ) P = 0 (4) Podobně z (2) plyne (M P) S = 0 (5). Ze (4), (5) a faktu, že 0 0 = 0, plyne ((S M ) P) ((M P) S) = 0 (6) Užitím asociativity a komutativity a dostáváme z (6) ((S P) M ) ((S P) M) = 0 (7) ALGEBRA LOGIKY. Motivační příklad (pokr.) 14 Z toho, že S M = 0 a X 0 = 0 pro libovolné X dostáváme (S M ) P = 0 (4) Podobně z (2) plyne (M P) S = 0 (5). Ze (4), (5) a faktu, že 0 0 = 0, plyne ((S M ) P) ((M P) S) = 0 (6) Užitím asociativity a komutativity a dostáváme z (6) ((S P) M ) ((S P) M) = 0 (7) Nyní podle distributivního zákona lze (7) přepsat na (S P) (M M) = 0 (8) ALGEBRA LOGIKY. Motivační příklad (pokr.) 14 Z toho, že S M = 0 a X 0 = 0 pro libovolné X dostáváme (S M ) P = 0 (4) Podobně z (2) plyne (M P) S = 0 (5). Ze (4), (5) a faktu, že 0 0 = 0, plyne ((S M ) P) ((M P) S) = 0 (6) Užitím asociativity a komutativity a dostáváme z (6) ((S P) M ) ((S P) M) = 0 (7) Nyní podle distributivního zákona lze (7) přepsat na (S P) (M M) = 0 (8) Jelikož X X = 1 a X 1 = X pro libovolné X, dostáváme z (8) konečně S P = 0 což bylo dokázat. ALGEBRA 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 , , 0, 1, a význam). X X = X X X = 1 X X = X X X = 0 X Y = Y X X = X X Y = Y X X 1 = 1 X (Y Z) = (X Y) Z X 1 = X X (Y Z) = (X Y) Z X 0 = X X (X Y) = X X 0 = 0 X (X Y) = X (X Y) = X Y X (Y Z) = (X Y) (X Z) (X Y) = X Y X (Y Z) = (X Y) (X Z) ALGEBRA LOGIKY. Motivační příklad (pokr.) 16 ALGEBRA 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). ALGEBRA 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 Y píše X.Y (případně jen XY); místo X Y 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é. ALGEBRA LOGIKY. Dva zá kladní problémy. 17 ALGEBRA LOGIKY. Dva zá kladní problémy. 17 Podle Boolea je každý sylogismus možné zapsat ve tvaru F1(P, M) = 0 F2(S, M) = 0 F(S, P) = 0 kde F1(P, M), F2(S, M), F(S, P) jsou vhodné výrazy vytvořené ze symbolů 0, 1, , , a symbolů v závorkách. ALGEBRA LOGIKY. Dva zá kladní problémy. 17 Podle Boolea je každý sylogismus možné zapsat ve tvaru F1(P, M) = 0 F2(S, M) = 0 F(S, P) = 0 kde F1(P, M), F2(S, M), F(S, P) jsou vhodné výrazy vytvořené ze symbolů 0, 1, , , a symbolů v závorkách. Boole uvážil obecnější ú sudky tvaru F1(A1, . . . , Am, B1, . . . , Bn) = 0 ... Fk(A1, . . . , Am, B1, . . . , Bn) = 0 F(B1, . . . , Bn) = 0 ALGEBRA LOGIKY. Dva zá kladní problémy. 17 Podle Boolea je každý sylogismus možné zapsat ve tvaru F1(P, M) = 0 F2(S, M) = 0 F(S, P) = 0 kde F1(P, M), F2(S, M), F(S, P) jsou vhodné výrazy vytvořené ze symbolů 0, 1, , , a symbolů v závorkách. Boole uvážil obecnější ú sudky tvaru F1(A1, . . . , Am, B1, . . . , Bn) = 0 ... Fk(A1, . . . , Am, B1, . . . , Bn) = 0 F(B1, . . . , Bn) = 0 Cílem jeho snah bylo vyvinout metodu, která umožní ALGEBRA LOGIKY. Dva zá kladní problémy. 17 Podle Boolea je každý sylogismus možné zapsat ve tvaru F1(P, M) = 0 F2(S, M) = 0 F(S, P) = 0 kde F1(P, M), F2(S, M), F(S, P) jsou vhodné výrazy vytvořené ze symbolů 0, 1, , , a symbolů v závorkách. Boole uvážil obecnější ú sudky tvaru F1(A1, . . . , Am, B1, . . . , Bn) = 0 ... Fk(A1, . . . , Am, B1, . . . , Bn) = 0 F(B1, . . . , Bn) = 0 Cílem jeho snah bylo vyvinout metodu, která umožní 1. zjistit, zda je daný ú sudek pravdivý; ALGEBRA LOGIKY. Dva zá kladní problémy. 17 Podle Boolea je každý sylogismus možné zapsat ve tvaru F1(P, M) = 0 F2(S, M) = 0 F(S, P) = 0 kde F1(P, M), F2(S, M), F(S, P) jsou vhodné výrazy vytvořené ze symbolů 0, 1, , , a symbolů v závorkách. Boole uvážil obecnější ú sudky tvaru F1(A1, . . . , Am, B1, . . . , Bn) = 0 ... Fk(A1, . . . , Am, B1, . . . , Bn) = 0 F(B1, . . . , Bn) = 0 Cílem jeho snah bylo vyvinout metodu, která umožní 1. zjistit, zda je daný ú sudek pravdivý; 2. nalézt nejobecnější závěr (F) pro dané předpoklady (F1,. . . ,Fk). ALGEBRA LOGIKY. Booleova metoda. 18 ALGEBRA LOGIKY. Booleova metoda. 18 Definice 1. Necht'A = A1, . . . , An. A-konstituent je výraz tvaru 1 n, kde i je bud' Ai nebo A i. ALGEBRA LOGIKY. Booleova metoda. 18 Definice 1. Necht'A = A1, . . . , An. A-konstituent je výraz tvaru 1 n, kde i je bud' Ai nebo A i. Věta 2. Pro každý výraz F(X1, , Xn) platí F(X1, , Xn) = v{0,1}n F(v) 1(v) n(v) kde i(v) je bud' Xi nebo X i podle toho, zda je vi rovno 1 nebo 0. ALGEBRA LOGIKY. Booleova metoda. 18 Definice 1. Necht'A = A1, . . . , An. A-konstituent je výraz tvaru 1 n, kde i je bud' Ai nebo A i. Věta 2. Pro každý výraz F(X1, , Xn) platí F(X1, , Xn) = v{0,1}n F(v) 1(v) n(v) kde i(v) je bud' Xi nebo X i podle toho, zda je vi rovno 1 nebo 0. Příklad 3. Necht'F(A, B) = (A B ) (A B). Pak F(A, B) = (F(0, 0) A B ) (F(0, 1) A B) (F(1, 0) A B ) (F(1, 1) A B) = (1 A B ) (0 A B) (0 A B ) (1 A B) = (A B ) (A B) ALGEBRA LOGIKY. Řešení 1. problému. 19 ALGEBRA LOGIKY. Řešení 1. problému. 19 Věta 4. Úsudek F1(A1, . . . , Am, B1, . . . , Bn) = 0 ... Fk(A1, . . . , Am, B1, . . . , Bn) = 0 F(B1, . . . , Bn) = 0 je platný prá vě když každý A, B-konstituent výrazu F je A, B-konstituentem některého Fi. ALGEBRA LOGIKY. Řešení 1. problému. 19 Věta 4. Úsudek F1(A1, . . . , Am, B1, . . . , Bn) = 0 ... Fk(A1, . . . , Am, B1, . . . , Bn) = 0 F(B1, . . . , Bn) = 0 je platný prá vě když každý A, B-konstituent výrazu F je A, B-konstituentem některého Fi. Příklad 5. Uvažme opět sylogismus S M = 0 M P = 0 S P = 0 Pak A = M a B = S, P. Uvažme A, B-konstituenty jednotlivých výrazů : S M : M S P, M S P M P : M S P, M S P S P : M S P, M S P ALGEBRA LOGIKY. Řešení 2. problému. 20 ALGEBRA LOGIKY. Řešení 2. problému. 20 Necht' A = A1, . . . , Am, B = B1, . . . , Bn. 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. ALGEBRA LOGIKY. Řešení 2. problému. 20 Necht' A = A1, . . . , Am, B = B1, . . . , Bn. 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 E(A, B) = F1(A, B) Fk(A, B) ALGEBRA LOGIKY. Řešení 2. problému. 20 Necht' A = A1, . . . , Am, B = B1, . . . , Bn. 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 E(A, B) = F1(A, B) 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) = v{0,1}m E(v, B) ALGEBRA LOGIKY. Řešení 2. problému. 20 Necht' A = A1, . . . , Am, B = B1, . . . , Bn. 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 E(A, B) = F1(A, B) 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) = v{0,1}m E(v, B) Příklad 7. Nejobecnější zá věr F(S, P) plynoucí z předpokladů S M = 0 a M P = 0 je tvaru F(S, P) = ((S 0 ) (0 P)) ((S 1 ) (1 P)) = S P VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 Potřebujeme znát jisté pojmy a umět myslet (metaú roveň). VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 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. VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 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). VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 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). VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 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: VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 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). VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 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í. VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 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). VÝ STAVBA FORMÁ LNÍCH LOGICKÝ CH SYSTÉ MŮ . 21 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). VÝ ROKOVÁ LOGIKA. Syntaxe. 22 VÝ ROKOVÁ LOGIKA. Syntaxe. 22 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 , , , zá vorky ( a ) VÝ ROKOVÁ LOGIKA. Syntaxe. 22 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 , , , zá vorky ( a ) Definice 9. Formule výrokové logiky je slovo nad abecedou výrokové logiky, pro které existuje vytvořující posloupnost, tj. konečná posloupnost slov 1, , k, kde k 1, k je , a pro každé 1 i k má slovo i jeden z ná sledujících tvarů : výroková proměnná , j pro nějaké 1 j < i, (j j ) pro nějaká 1 j, j < i, kde je jeden ze symbolů , , . VÝ ROKOVÁ LOGIKA. Syntaxe. 22 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 , , , zá vorky ( a ) Definice 9. Formule výrokové logiky je slovo nad abecedou výrokové logiky, pro které existuje vytvořující posloupnost, tj. konečná posloupnost slov 1, , k, kde k 1, k je , a pro každé 1 i k má slovo i jeden z ná sledujících tvarů : výroková proměnná , j pro nějaké 1 j < i, (j j ) pro nějaká 1 j, j < i, kde je jeden ze symbolů , , . Poznámka 10. Notace: vnější zá vorky budeme zpravidla vynechá vat. Např. místo (A B) budeme psá t A B. VÝ ROKOVÁ LOGIKA. Sémantika. 23 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. 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; v() = 0 jestliže v() = 1; 1 jinak. v((1 2)) = 0 jestliže v(1) = 0 nebo v(2) = 0; 1 jinak. v((1 2)) = 0 jestliže v(1) = 0 a současně v(2) = 0; 1 jinak. v((1 2)) = 0 jestliže v(1) = 1 a současně v(2) = 0; 1 jinak. VÝ ROKOVÁ LOGIKA. Sémantika (pokr.) 24 VÝ ROKOVÁ LOGIKA. Sémantika (pokr.) 24 Definice 12. Výroková formule je pravdivá (resp. nepravdivá ) při valuaci v, pokud v() = 1 (resp. v() = 0); splnitelná , jestliže existuje valuace v taková , že v() = 1; tautologie (také (logicky) pravdivá ), jestliže v() = 1 pro každou valuaci v. Soubor T výrokových formulí je splnitelný, jestliže existuje valuace v taková , že v() = 1 pro každé z T. VÝ ROKOVÁ LOGIKA. Sémantika (pokr.) 24 Definice 12. Výroková formule je pravdivá (resp. nepravdivá ) při valuaci v, pokud v() = 1 (resp. v() = 0); splnitelná , jestliže existuje valuace v taková , že v() = 1; tautologie (také (logicky) pravdivá ), jestliže v() = 1 pro každou valuaci v. Soubor T výrokových formulí je splnitelný, jestliže existuje valuace v taková , že v() = 1 pro každé z T. Definice 13. Formule a jsou ekvivalentní, psá no , prá vě když pro každou valuaci v platí, že v() = v(). VÝ ROKOVÁ LOGIKA. Sémantika (pokr.) 24 Definice 12. Výroková formule je pravdivá (resp. nepravdivá ) při valuaci v, pokud v() = 1 (resp. v() = 0); splnitelná , jestliže existuje valuace v taková , že v() = 1; tautologie (také (logicky) pravdivá ), jestliže v() = 1 pro každou valuaci v. Soubor T výrokových formulí je splnitelný, jestliže existuje valuace v taková , že v() = 1 pro každé z T. Definice 13. Formule a jsou ekvivalentní, psá no , prá vě když pro každou valuaci v platí, že v() = v(). Příklad 14. Necht', , jsou výrokové formule. Pak: ( ) ( ) ( ) ( ) ( ) ( ) VÝ ROKOVÁ LOGIKA. Sémantika (pokr.) 25 VÝ ROKOVÁ LOGIKA. Sémantika (pokr.) 25 Poznámka 15. ,,Identity" z příkladu 14 umožňují dá le zpřehlednit zá pis formulí. Např. místo (A B) C mů žeme (nejednoznačně) psá t A B C. Tato nejednoznačnost nevede k problémů m, nebot'příslušné definice a tvrzení ,,fungují" pro libovolné možné uzá vorková ní. VÝ ROKOVÁ LOGIKA. Sémantika (pokr.) 25 Poznámka 15. ,,Identity" z příkladu 14 umožňují dá le zpřehlednit zá pis formulí. Např. místo (A B) C mů žeme (nejednoznačně) psá t A B C. Tato nejednoznačnost nevede k problémů m, nebot'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 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. VÝ ROKOVÁ LOGIKA. Sémantika (pokr.) 25 Poznámka 15. ,,Identity" z příkladu 14 umožňují dá le zpřehlednit zá pis formulí. Např. místo (A B) C mů žeme (nejednoznačně) psá t A B C. Tato nejednoznačnost nevede k problémů m, nebot'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 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 je tautologickým dů sledkem souboru formulí T, psá no T |= , jestliže v() = 1 pro každou valuaci v takovou, že v() = 1 pro každou formuli ze souboru T. Jestliže T |= pro prá zdný soubor T, píšeme krá tce |= . VÝ ROKOVÁ LOGIKA. Pravdivostní tabulky. 26 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 Y 0 0 0 0 1 0 1 0 0 1 1 1 X Y X Y 0 0 0 0 1 1 1 0 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 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 Y 0 0 0 0 1 0 1 0 0 1 1 1 X Y X Y 0 0 0 0 1 1 1 0 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, 1}n {0, 1}, kde n 1. VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , Fk). 27 VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , Fk). 27 Necht' F1, , Fk je konečný soubor výrokových funkcí. Definujeme formální logický systém L(F1, , Fk), kde VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , Fk). 27 Necht' F1, , Fk je konečný soubor výrokových funkcí. Definujeme formální logický systém L(F1, , Fk), kde Abeceda je tvořena znaky pro výrokové proměnné, závorkami a znaky F1, , Fk pro uvedené výrokové funkce. VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , Fk). 27 Necht' F1, , Fk je konečný soubor výrokových funkcí. Definujeme formální logický systém L(F1, , Fk), kde Abeceda je tvořena znaky pro výrokové proměnné, závorkami a znaky F1, , Fk pro uvedené výrokové funkce. V definici vytvořující posloupnosti formule (viz definice 48) požadujeme, aby i bylo bud' výrokovou proměnnou nebo tvaru Fj(j1 , , jn ), kde 1 j1, , jn < i a n je arita Fj. VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , Fk). 27 Necht' F1, , Fk je konečný soubor výrokových funkcí. Definujeme formální logický systém L(F1, , Fk), kde Abeceda je tvořena znaky pro výrokové proměnné, závorkami a znaky F1, , Fk pro uvedené výrokové funkce. V definici vytvořující posloupnosti formule (viz definice 48) požadujeme, aby i bylo bud' výrokovou proměnnou nebo tvaru Fj(j1 , , jn ), kde 1 j1, , jn < i a n je arita Fj. Valuace rozšíříme z výrokových proměnných na formule předpisem v(F(1, , n)) = F(v(1), , v(n)) VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , Fk). 27 Necht' F1, , Fk je konečný soubor výrokových funkcí. Definujeme formální logický systém L(F1, , Fk), kde Abeceda je tvořena znaky pro výrokové proměnné, závorkami a znaky F1, , Fk pro uvedené výrokové funkce. V definici vytvořující posloupnosti formule (viz definice 48) požadujeme, aby i bylo bud' výrokovou proměnnou nebo tvaru Fj(j1 , , jn ), kde 1 j1, , jn < i a n je arita Fj. Valuace rozšíříme z výrokových proměnných na formule předpisem v(F(1, , n)) = F(v(1), , v(n)) V tomto smyslu je pak dosud uvažovaný systém výrokové logiky systémem L(, , , ). Dříve zavedené sémantické pojmy (splnitelnost, pravdivost, atd.) se opírají pouze o pojem valuace a ,,fungují" tedy v libovolném systému L(F1, , Fk). VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , Fk). 28 VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , 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. VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , 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. Necht' je formule L(F1, , Fk) a necht'X1, , Xn je vzestupně uspořá daná posloupnost (vzhledem k ) všech výrokových proměnných, které se ve vyskytují. Formule jednoznačně určuje výrokovou funkci F : {0, 1}n {0, 1} danou předpisem F(u) = v(F), kde v je valuace definovaná takto: v(Xi) = u(i) pro každé 1 i n, v(Y) = 0 pro ostatní Y. VÝ ROKOVÁ LOGIKA. Formá lní systém L(F1, , 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. Necht' je formule L(F1, , Fk) a necht'X1, , Xn je vzestupně uspořá daná posloupnost (vzhledem k ) všech výrokových proměnných, které se ve vyskytují. Formule jednoznačně určuje výrokovou funkci F : {0, 1}n {0, 1} danou předpisem F(u) = v(F), kde v je valuace definovaná takto: v(Xi) = u(i) pro každé 1 i n, v(Y) = 0 pro ostatní Y. Definice 20. Systém L(F1, , Fk) je plnohodnotný, jestliže pro každou výrokovou funkci F existuje formule systému L(F1, , Fk) taková , že F = F. VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů . 29 VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů . 29 Věta 21. Systém L = (, , ) je plnohodnotný. VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů . 29 Věta 21. Systém L = (, , ) je plnohodnotný. Dů kaz. Necht' F : {0, 1}n {0, 1} je výroková funkce a necht' u1, , 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 = X1 X1 X2 Xn. Jinak = k i=1 1(ui) k(ui) kde j(ui) je bud' Xj nebo Xj podle toho, zda ui(j) = 1 nebo ui(j) = 0. Nyní se lehce ověří, že F = F. VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 30 VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 30 Uvažme následující výrokové funkce: X Y X Y 0 0 1 0 1 0 1 0 0 1 1 0 X Y X | Y 0 0 1 0 1 1 1 0 1 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á Schro¨derů v operátor. Platí . Funkce | se nazývá Shefferů v operátor. Platí | ( ). VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 31 VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 31 Následující systémy výrokové logiky jsou plnohodnotné: L(, , ) Věta 21. VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 31 Následující systémy výrokové logiky jsou plnohodnotné: L(, , ) Věta 21. L(, ) ( ) VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 31 Následující systémy výrokové logiky jsou plnohodnotné: L(, , ) Věta 21. L(, ) ( ) L(, ) ( ) VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 31 Následující systémy výrokové logiky jsou plnohodnotné: L(, , ) Věta 21. L(, ) ( ) L(, ) ( ) L(, ) VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 31 Následující systémy výrokové logiky jsou plnohodnotné: L(, , ) Věta 21. L(, ) ( ) L(, ) ( ) L(, ) L( ) , ( ) ( ) VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 31 Následující systémy výrokové logiky jsou plnohodnotné: L(, , ) Věta 21. L(, ) ( ) L(, ) ( ) L(, ) L( ) , ( ) ( ) L(|) | , ( | ) | ( | ) VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 31 Následující systémy výrokové logiky jsou plnohodnotné: L(, , ) Věta 21. L(, ) ( ) L(, ) ( ) L(, ) L( ) , ( ) ( ) L(|) | , ( | ) | ( | ) L() (, , ), (, (, , ), (, , (, , ))) VÝ ROKOVÁ LOGIKA. Plnohodnotnost systémů (pokr.) 31 Následující systémy výrokové logiky jsou plnohodnotné: L(, , ) Věta 21. L(, ) ( ) L(, ) ( ) L(, ) L( ) , ( ) ( ) L(|) | , ( | ) | ( | ) L() (, , ), (, (, , ), (, , (, , ))) Následující systémy plnohodnotné nejsou: L(), L(), L(), L(), atd. VÝ ROKOVÁ LOGIKA. Shefferovské spojky. 32 VÝ ROKOVÁ LOGIKA. Shefferovské spojky. 32 Definice 22. Výroková funkce F je Shefferovská jestliže L(F) je plnohodnotný systém. VÝ ROKOVÁ LOGIKA. Shefferovské spojky. 32 Definice 22. Výroková funkce F je Shefferovská jestliže L(F) je plnohodnotný systém. Věta 23. Necht'S(n) značí počet všech Shefferovských funkcí arity n 1. Pak S(n) = 2(2n-1 -1) (2(2n-1 -1) - 1). VÝ ROKOVÁ LOGIKA. Shefferovské spojky. 32 Definice 22. Výroková funkce F je Shefferovská jestliže L(F) je plnohodnotný systém. Věta 23. Necht'S(n) značí počet všech Shefferovských funkcí arity n 1. Pak S(n) = 2(2n-1 -1) (2(2n-1 -1) - 1). Pro n = 1, 2, 3, 4, 5, . . . dostáváme postupně 0, 2, 56, 16256, 1073709056, . . . VÝ ROKOVÁ LOGIKA. Shefferovské spojky. 32 Definice 22. Výroková funkce F je Shefferovská jestliže L(F) je plnohodnotný systém. Věta 23. Necht'S(n) značí počet všech Shefferovských funkcí arity n 1. Pak S(n) = 2(2n-1 -1) (2(2n-1 -1) - 1). Pro n = 1, 2, 3, 4, 5, . . . dostáváme postupně 0, 2, 56, 16256, 1073709056, . . . Dů sledek 24. Jelikož limn S(n) 22n = 1/4, je (pro velká n) zhruba čtvrtina ze všech výrokových funkcí arity n Shefferovská . VÝ ROKOVÁ LOGIKA. Shefferovské spojky. 32 Definice 22. Výroková funkce F je Shefferovská jestliže L(F) je plnohodnotný systém. Věta 23. Necht'S(n) značí počet všech Shefferovských funkcí arity n 1. Pak S(n) = 2(2n-1 -1) (2(2n-1 -1) - 1). Pro n = 1, 2, 3, 4, 5, . . . dostáváme postupně 0, 2, 56, 16256, 1073709056, . . . Dů sledek 24. Jelikož limn S(n) 22n = 1/4, je (pro velká n) zhruba čtvrtina ze všech výrokových funkcí arity n Shefferovská . Poznámka 25. Výsledky o Shefferovských funkcích nalézají uplatnění při výrobě logických obvodů ; na ,,podkladové desce" se např. vytvoří hustá sít' biná rních |-hradel. Obvody rů zné funkce se pak realizují jejich vhodným propojením. VÝ ROKOVÁ LOGIKA. Normá lní formy. 33 VÝ ROKOVÁ LOGIKA. Normá lní formy. 33 Definice 26. Literá l je formule tvaru X nebo X, kde X je výroková proměnná ; Klauzule je formule tvaru 1 n, kde n 1 a každé i je literá l. Duá lní klauzule je formule tvaru 1 n, kde n 1 a každé i je literá l. Formule v konjunktivním normá lním tvaru (CNF) je formule tvaru C1 Cm, kde m 1 a každé Ci je klauzule. Formule v disjunktivním normá lním tvaru je formule tvaru C1 Cm, kde m 1 a každé Ci je duá lní klauzule. VÝ ROKOVÁ LOGIKA. Normá lní formy. 33 Definice 26. Literá l je formule tvaru X nebo X, kde X je výroková proměnná ; Klauzule je formule tvaru 1 n, kde n 1 a každé i je literá l. Duá lní klauzule je formule tvaru 1 n, kde n 1 a každé i je literá l. Formule v konjunktivním normá lním tvaru (CNF) je formule tvaru C1 Cm, kde m 1 a každé Ci je klauzule. Formule v disjunktivním normá lním tvaru je formule tvaru C1 Cm, kde m 1 a každé Ci je duá lní klauzule. Okamžitým dů sledkem věty 21 je následující: Věta 27. Pro každou formuli existuje ekvivalentní formule v disjunktivním normá lním tvaru. VÝ ROKOVÁ LOGIKA. Normá lní formy (pokr.) 34 VÝ ROKOVÁ LOGIKA. Normá lní formy (pokr.) 34 Věta 28. Pro každou formuli existuje ekvivalentní formule v konjunktivním normá lním tvaru. VÝ ROKOVÁ LOGIKA. Normá lní formy (pokr.) 34 Věta 28. Pro každou formuli existuje ekvivalentní formule v konjunktivním normá lním tvaru. Dů kaz. Podle Věty 27 existuje k ekvivalentní formule v disjunktivním normálním tvaru, tj. n i=1 Di, kde n 1 a každé Di je duální klauzule. Metaindukcí vzhledem k n: n = 1. Pak n i=1 Di je současně v CNF. Indukční krok: Necht' D1 = 1 k. Platí n+1 i=1 Di D1 n+1 i=2 Di D1 m i=1 Ci m i=1 D1 Ci m i=1 k j=1 (j Ci) VÝ ROKOVÁ LOGIKA. Normá lní formy (pokr.) 34 Věta 28. Pro každou formuli existuje ekvivalentní formule v konjunktivním normá lním tvaru. Dů kaz. Podle Věty 27 existuje k ekvivalentní formule v disjunktivním normálním tvaru, tj. n i=1 Di, kde n 1 a každé Di je duální klauzule. Metaindukcí vzhledem k n: n = 1. Pak n i=1 Di je současně v CNF. Indukční krok: Necht' D1 = 1 k. Platí n+1 i=1 Di D1 n+1 i=2 Di D1 m i=1 Ci m i=1 D1 Ci m i=1 k j=1 (j Ci) Příklad 29. Formuli (A B) (B C) (C A) lze v CNF reprezentovat jako (A B) (B C) (C A) nebo (A C) (C B) (B A). CNF tedy není určena jednoznačně až na pořadí klauzulí a literá lů . VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti. 35 VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti. 35 Věta 30 (o kompaktnosti). Necht'T je soubor formulí výrokové logiky. T je splnitelný prá vě když každá konečná čá st T je splnitelná . VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti. 35 Věta 30 (o kompaktnosti). Necht'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í. VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti. 35 Věta 30 (o kompaktnosti). Necht'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ý. VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti. 35 Věta 30 (o kompaktnosti). Necht'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ý. Necht' 1, 2, . . . je posloupnost všech formulí výrokové logiky. Metamatematickou indukcí definujeme pro každé i 1 dobrý soubor Si: S1 = T. Soubor S1 je dobrý nebot' T je dobrý. Si+1 = Si {i} jestliže Si {i} je dobrý; Si {i} jinak. VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti. 35 Věta 30 (o kompaktnosti). Necht'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ý. Necht' 1, 2, . . . je posloupnost všech formulí výrokové logiky. Metamatematickou indukcí definujeme pro každé i 1 dobrý soubor Si: S1 = T. Soubor S1 je dobrý nebot' T je dobrý. Si+1 = Si {i} jestliže Si {i} je dobrý; Si {i} jinak. Alespoň jeden ze souborů Si {i} a Si {i} musí být dobrý; jinak existují konečné V1 Si {i} a V2 Si {i}, které nejsou splnitelné. Jestliže V1 Si nebo V2 Si, máme ihned spor s tím, že Si je dobrý; jinak V1 V2 obsahuje i , proto i (V1 V2) {i, i} Si je nesplnitelný, spor.) VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti. 36 Necht' S = i=1 Si. Dokážeme, že S má následující vlastnosti: S obsahuje prá vě když S neobsahuje . S nutně obsahuje nebo . Jestliže S obsahuje i , existuje Si obsahující i ; tedy {, } je nesplnitelný podsoubor Si, spor. S obsahuje prá vě když S obsahuje i ; S obsahuje prá vě když S obsahuje nebo ; S obsahuje prá vě když S neobsahuje nebo obsahuje . VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti. 36 Necht' S = i=1 Si. Dokážeme, že S má následující vlastnosti: S obsahuje prá vě když S neobsahuje . S nutně obsahuje nebo . Jestliže S obsahuje i , existuje Si obsahující i ; tedy {, } je nesplnitelný podsoubor Si, spor. S obsahuje prá vě když S obsahuje i ; S obsahuje prá vě když S obsahuje nebo ; S obsahuje prá vě když S neobsahuje nebo obsahuje . Bud' 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 prá vě když v() = 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 G 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 G = (U , H ), kde U U a H H. 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) H. VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti (použití). 38 VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti (použití). 38 Věta 31. Graf G = (U, H) je k-obarvitelný prá vě když každý konečný podgraf G je k-obarvitelný. VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti (použití). 38 Věta 31. Graf G = (U, H) je k-obarvitelný prá vě když každý konečný podgraf G je k-obarvitelný. Dů kaz. Necht' Bu,i je výroková proměnná pro každý uzel u a každé 1 i k. Bud' T soubor tvořený následujícími formulemi: Bu,1 Bu,k 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,i Bv,i pro každé (u, v) H a 1 i k. VÝ ROKOVÁ LOGIKA. Věta o kompaktnosti (použití). 38 Věta 31. Graf G = (U, H) je k-obarvitelný prá vě když každý konečný podgraf G je k-obarvitelný. Dů kaz. Necht' Bu,i je výroková proměnná pro každý uzel u a každé 1 i k. Bud' T soubor tvořený následujícími formulemi: Bu,1 Bu,k 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,i Bv,i pro každé (u, v) 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. VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 39 V této části se soustředíme na L(, ). Uvažme následující odvozovací systém pro L(, ) (Lukasiewicz, 1928): Schémata axiómů : A1: ( ) A2: ( ( )) (( ) ( )) A3: ( ) ( ) Odvozovací pravidlo: MP: Z a odvod' . (modus ponens) VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 40 Definice 32. Bud' T soubor formulí. VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 40 Definice 32. Bud' T soubor formulí. Dů kaz formule z předpokladů T je konečná posloupnost formulí 1, , k, kde k je a pro každé i, kde 1 i k, platí alespoň jedna z ná sledujících podmínek: i je prvek T; i je instancí jednoho ze schémat A1­A3; i vznikne aplikací pravidla MP na formule m, n pro vhodné 1 m, n < i. VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 40 Definice 32. Bud' T soubor formulí. Dů kaz formule z předpokladů T je konečná posloupnost formulí 1, , k, kde k je a pro každé i, kde 1 i k, platí alespoň jedna z ná sledujících podmínek: i je prvek T; i je instancí jednoho ze schémat A1­A3; i vznikne aplikací pravidla MP na formule m, n pro vhodné 1 m, n < i. Formule je dokazatelná z předpokladů T, psá no T , jestliže existuje dů kaz z předpokladů T. Jestliže T pro prá zdné T, říká me že je dokazatelná a píšeme . VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 41 VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 41 Příklad 33. Pro libovolnou formuli platí . VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 41 Příklad 33. Pro libovolnou formuli platí . Dů kaz. Následující posloupnost formulí je dů kazem . 1) ( (( ) )) (( ( )) ( )) A2 2) (( ) ) A1 3) ( ( )) ( ) MP na 2), 1) 4) ( ) A1 5) MP na 4), 3) VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 42 VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 42 Příklad 34. Pro libovolné formule , platí {, } . VÝ ROKOVÁ LOGIKA. Odvozovací systém pro L(, ) 42 Příklad 34. Pro libovolné formule , platí {, } . Dů kaz. Následující posloupnost formulí je dů kazem z {, }: 1) ( ) A1 2) předpoklad 3) MP na 2), 1) 4) ( ) ( ) A3 5) MP na 3), 4) 6) předpoklad 7) MP na 6), 5) VÝ ROKOVÁ LOGIKA. Věta o dedukci. 43 VÝ ROKOVÁ LOGIKA. Věta o dedukci. 43 Věta 35 (o dedukci). Necht', jsou formule a T soubor formulí. Pak T {} prá vě když T . VÝ ROKOVÁ LOGIKA. Věta o dedukci. 43 Věta 35 (o dedukci). Necht', jsou formule a T soubor formulí. Pak T {} prá vě když T . Dů kaz. ,,": Necht' 1, , k je dů kaz formule z předpokladů T. Pak 1, , k, , je dů kaz formule z předpokladů T {} (poslední formule vznikne aplikací MP na a k). VÝ ROKOVÁ LOGIKA. Věta o dedukci. 43 Věta 35 (o dedukci). Necht', jsou formule a T soubor formulí. Pak T {} prá vě když T . Dů kaz. ,,": Necht' 1, , k je dů kaz formule z předpokladů T. Pak 1, , k, , je dů kaz formule z předpokladů T {} (poslední formule vznikne aplikací MP na a k). ,,": Necht' 1, , k je dů kaz z předpokladů T {}. Metaindukcí k j dokážeme, že T j pro každé 1 j k. VÝ ROKOVÁ LOGIKA. Věta o dedukci. 43 Věta 35 (o dedukci). Necht', jsou formule a T soubor formulí. Pak T {} prá vě když T . Dů kaz. ,,": Necht' 1, , k je dů kaz formule z předpokladů T. Pak 1, , k, , je dů kaz formule z předpokladů T {} (poslední formule vznikne aplikací MP na a k). ,,": Necht' 1, , k je dů kaz z předpokladů T {}. Metaindukcí k j dokážeme, že T j pro každé 1 j k. j = 1. Je-li 1 instance axiómu nebo formule z T, platí T 1. K dů kazu 1 z T nyní připojíme formule 1 ( 1), 1. První formule je instancí A1, druhá aplikací MP na 1 a první formuli. Máme tedy dů kaz 1 z T. Je-li 1 formule , platí T 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 {}, postupujeme stejně jako výše (místo 1 použijeme j). VÝ ROKOVÁ LOGIKA. Věta o dedukci. 44 Indukční krok: Je-li formule j instancí axiómu nebo prvek T {}, postupujeme stejně jako výše (místo 1 použijeme j). Je-li j výsledkem aplikace MP na m, n, kde 1 m, n < j, je n tvaru m j. Podle I.P. navíc platí T m a T (m j). Dů kazy m a (m j) z T nyní zřetězíme za sebe a připojíme následující formule: ( (m j)) (( m) ( j)) ( m) ( j) j První formule je instancí A2, další dvě vzniknou aplikací MP. Máme tedy dů kaz formule j z T. VÝ ROKOVÁ LOGIKA. Věta o korektnosti. 45 VÝ ROKOVÁ LOGIKA. Věta o korektnosti. 45 Věta 36 (o korektnosti). Necht' je formule a T soubor formulí. Jestliže T , pak T |= . VÝ ROKOVÁ LOGIKA. Věta o korektnosti. 45 Věta 36 (o korektnosti). Necht' je formule a T soubor formulí. Jestliže T , pak T |= . Dů kaz. Necht' 1, , k je dů kaz z T. Indukcí vzhledem k j dokážeme, že T |= j pro každé 1 j k. (Stačí ověřit, že každá instance A1­A3 je tautologie, a že jestliže T |= a T |= , pak také T |= ). VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 46 Lema 37. Necht', jsou formule. Pak (a) ( ) (b) (c) (d) ( ) ( ) (e) ( ( )) (f) ( ) (( ) ) Dů kaz. (a): Podle příkladu 34 platí {, } , proto ( ) opakovaným užitím věty o dedukci. VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 47 VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 47 (b): Platí 1) ( ) podle (a) 2) {} věta o dedukci 3) ( ) ( ) A3 4) {} MP na 2), 3) 5) {} věta o dedukci 6) věta o dedukci VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 47 (b): Platí 1) ( ) podle (a) 2) {} věta o dedukci 3) ( ) ( ) A3 4) {} MP na 2), 3) 5) {} věta o dedukci 6) věta o dedukci (c): Platí 1) podle (b) 2) ( ) ( ) A3 3) MP na 1), 2) VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 48 (d): Platí 1) { } 2) {} podle (b) a věty o dedukci 3) { , } MP na 2), 1) 4) podle (c) 5) { , } MP na 3), 4) 6) { } věta o dedukci 7) ( ) ( ) A3 8) { } MP na 6), 7) 9) ( ) ( ) věta o dedukci VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 49 (e): Platí 1) {, } 2) {} ( ) věta o dedukci 3) (( ) ) ( ( )) podle (d) 4) {} ( ) MP na 2), 3) 5) ( ( )) věta o dedukci VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 50 (f): Platí 1) ( ) ( )) podle (d) 2) { , } 2x MP na 1) 3) { , , } MP na 2), 4) { , } věta o dedukci 5) ( ( )) podle (e) 6) {} ( ) 2x věta o dedukci 7) ( ) věta o dedukci 8) ( ( )) (( ) ) A3 9) ( ) MP na 7), 8) 10) { , } MP na 4), 9) 11) ( ) (( ) ) 2x věta o dedukci VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 51 VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 51 Definice 38. Necht'v je valuace a formule. Jestliže v() = 1, označuje symbol v formuli . Jinak v označuje formuli . VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 51 Definice 38. Necht'v je valuace a formule. Jestliže v() = 1, označuje symbol v formuli . Jinak v označuje formuli . Lema 39 (A. Church). Necht'v je valuace, formule, a {X1, , Xk} konečný soubor výrokových proměnných, kde všechny proměnné vyskytující se ve jsou mezi {X1, , Xk}. Pak {Xv 1, , Xv k} v . VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 51 Definice 38. Necht'v je valuace a formule. Jestliže v() = 1, označuje symbol v formuli . Jinak v označuje formuli . Lema 39 (A. Church). Necht'v je valuace, formule, a {X1, , Xk} konečný soubor výrokových proměnných, kde všechny proměnné vyskytující se ve jsou mezi {X1, , Xk}. Pak {Xv 1, , Xv k} v . Dů kaz. Indukcí k délce vytvořující posloupnosti pro . VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 51 Definice 38. Necht'v je valuace a formule. Jestliže v() = 1, označuje symbol v formuli . Jinak v označuje formuli . Lema 39 (A. Church). Necht'v je valuace, formule, a {X1, , Xk} konečný soubor výrokových proměnných, kde všechny proměnné vyskytující se ve jsou mezi {X1, , Xk}. Pak {Xv 1, , Xv k} v . Dů kaz. Indukcí k délce vytvořující posloupnosti pro . Je-li = X, pak X je mezi {X1, , Xk} a tedy {Xv 1, , Xv k} Xv . VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 51 Definice 38. Necht'v je valuace a formule. Jestliže v() = 1, označuje symbol v formuli . Jinak v označuje formuli . Lema 39 (A. Church). Necht'v je valuace, formule, a {X1, , Xk} konečný soubor výrokových proměnných, kde všechny proměnné vyskytující se ve jsou mezi {X1, , Xk}. Pak {Xv 1, , Xv k} v . Dů kaz. Indukcí k délce vytvořující posloupnosti pro . Je-li = X, pak X je mezi {X1, , Xk} a tedy {Xv 1, , Xv k} Xv . Je-li = , kde {Xv 1, , Xv k} v , rozlišíme dvě možnosti: v() = 0. Pak v = a v = , není co dokazovat. v() = 1. Pak v = a v = . Podle lematu 37 (c) platí , proto {Xv 1, , Xv k} užitím MP. VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 52 VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 52 Je-li = , kde {Xv 1, , Xv k} v a {Xv 1, , Xv k} v rozlišíme následující možnosti: VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 52 Je-li = , kde {Xv 1, , Xv k} v a {Xv 1, , Xv k} v rozlišíme následující možnosti: v( ) = 1. Máme tedy dokázat, že {Xv 1, , Xv k} . ˇ Jestliže v() = 0, platí {Xv 1, , Xv k} . Podle lematu 37 (a) dále platí ( ), proto {Xv 1, , Xv k} užitím MP. ˇ Jestliže v() = 1, platí {Xv 1, , Xv k} . Podle A1 platí ( ), proto {Xv 1, , Xv k} užitím MP. VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 52 Je-li = , kde {Xv 1, , Xv k} v a {Xv 1, , Xv k} v rozlišíme následující možnosti: v( ) = 1. Máme tedy dokázat, že {Xv 1, , Xv k} . ˇ Jestliže v() = 0, platí {Xv 1, , Xv k} . Podle lematu 37 (a) dále platí ( ), proto {Xv 1, , Xv k} užitím MP. ˇ Jestliže v() = 1, platí {Xv 1, , Xv k} . Podle A1 platí ( ), proto {Xv 1, , Xv k} užitím MP. v( ) = 0. Pak {Xv 1, , Xv k} a {Xv 1, , Xv k} . Máme dokázat, že {Xv 1, , Xv k} ( ). Podle lematu 37 (e) platí ( ( )), proto {Xv 1, , Xv k} ( ) opakovaným užitím MP. VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 53 VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 53 Věta 40 (o ú plnosti). Necht' je formule a T soubor formulí. Jestliže T |= , pak T . VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 53 Věta 40 (o ú plnosti). Necht' je formule a T soubor formulí. Jestliže T |= , pak T . Dů kaz. Nejprve uvážíme případ, kdy T je prá zdný soubor. Necht' je tautologie a X1, , Xk všechny výrokové proměnné, které se ve vyskytují. Podle Churchova lematu platí {Xv 1, , Xv k} pro libovolnou valuaci v. Ukážeme, že všechny Xv i lze postupně ,,eliminovat", až dostaneme dů kaz z prázdného souboru formulí. VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 53 Věta 40 (o ú plnosti). Necht' je formule a T soubor formulí. Jestliže T |= , pak T . Dů kaz. Nejprve uvážíme případ, kdy T je prá zdný soubor. Necht' je tautologie a X1, , Xk všechny výrokové proměnné, které se ve vyskytují. Podle Churchova lematu platí {Xv 1, , Xv k} pro libovolnou valuaci v. Ukážeme, že všechny Xv i lze postupně ,,eliminovat", až dostaneme dů kaz z prázdného souboru formulí. Předpoládejme, že pro dané 0 n < k jsme již prokázali, že {Xv 1, , Xv n, Xv n+1} pro libovolnou valuaci v. Dokážeme, že pak také {Xu 1 , , Xu n} pro libovolnou valuaci u. VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 54 VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 54 Bud' tedy u libovolná valuace. Necht' u1, u2 jsou valuace definované takto: u1(Xk) = 1, u2(Xk) = 0, a pro každé Y = Xk platí u1(Y) = u2(Y) = v(Y). VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 54 Bud' tedy u libovolná valuace. Necht' u1, u2 jsou valuace definované takto: u1(Xk) = 1, u2(Xk) = 0, a pro každé Y = Xk platí u1(Y) = u2(Y) = v(Y). Platí 1) {Xu 1 , , Xu n, Xn+1} předpoklad pro v = u1 2) {Xu 1 , , Xu n, Xn+1} předpoklad pro v = u2 3) {Xu 1 , , Xu n} Xn+1 věta o dedukci na 1) 4) {Xu 1 , , Xu n} Xn+1 věta o dedukci na 2) 5) (Xn+1 ) ((Xn+1 ) ) podle lematu 37 (f) 6) {Xu 1 , , Xu n} 2x MP na 5) s využitím 3), 4) VÝ ROKOVÁ LOGIKA. Věta o ú plnosti. 55 Nyní uvážíme obecný případ. Bud' T libovolný soubor formulí a formule taková, že T |= . Podle věty o kompaktnosti existuje konečný soubor {1, , n} formulí z T takový, že {1, , n} |= . Lehce se ověří, že |= 1 (2 (3 (n ) ) Podle předchozího bodu tedy platí 1 (2 (3 (n ) ) Po n aplikacích věty o dedukci dostáváme {1, , n} , tedy také T . VÝ ROKOVÁ LOGIKA. Historické pozná mky. 56 VÝ ROKOVÁ LOGIKA. Historické pozná mky. 56 Výroková logika byla nebyla rozvíjena samostatně, ale jako součást složitějších formálních systémů . VÝ ROKOVÁ LOGIKA. Historické pozná mky. 56 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): 1: P (Q P) 2: (P (Q R)) ((P Q) (P R)) 3: (P (Q R)) (Q (P R)) 4: (P Q) (Q P) 5: P P 6: P P Odvozovací pravidla: MP a substituce Fregeho výsledky byly vědeckou komunitou ignorovány zhruba 20 let. VÝ ROKOVÁ LOGIKA. Historické pozná mky. 57 Giuseppe Peano (1858-1932) doporučil na mezinárodním matematickém kongresu v Paříži (rok 1900) mladému Bertrandu Russellovi (1872-1970) studovat Fregeho práce. Russell v roce 1901 objevil inkonzistenci ve Fregeho systému (Russelů v paradox), současně plně docenil Fregeho myšlenky. V letech 1910-1913 byla publikována třídílná Principia Mathematica (autoři Whitehead, Russel). Tato monografie měla hluboký vliv na vývoj logiky v následujících desetiletích. Věnována byla Fregemu. Pro fragment výrokové logiky byly použity následující axiómy a odvozovací pravidla: 1: (P P) P 2: Q (P Q) 3: (P Q) (Q P) 4: (P (Q R)) (Q (P R)) 5: (Q R) ((P Q) (P R)) Odvozovací pravidla: MP a substituce VÝ ROKOVÁ LOGIKA. Historické pozná mky. 58 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: (P P) P 2: P (P Q) 4: (P (Q R)) (Q (P R)) 5: (Q R) ((P Q) (P R)) Odvozovací pravidla: MP a substituce 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: (P P) P 2: P (P Q) 4: (P (Q R)) (Q (P R)) 5: (Q R) ((P Q) (P R)) Odvozovací pravidla: MP a substituce Ve stejném roce publikoval Henry Sheffer následující axiomatický systém založený na Shefferově 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) odvod' H" VÝ ROKOVÁ LOGIKA. Historické pozná mky. 59 VÝ ROKOVÁ LOGIKA. Historické pozná mky. 59 David Hilbert (1862­1943) a Wilhelm Ackermann (1896-1962) publikovali v roce 1928 následující systém: 1: (P P) P 2: P (P Q) 4: (P Q) (Q P) 5: (Q R) ((P Q) (P R)) Odvozovací pravidla: MP a substituce VÝ ROKOVÁ LOGIKA. Historické pozná mky. 59 David Hilbert (1862­1943) a Wilhelm Ackermann (1896-1962) publikovali v roce 1928 následující systém: 1: (P P) P 2: P (P Q) 4: (P Q) (Q P) 5: (Q R) ((P Q) (P R)) Odvozovací pravidla: MP a substituce V roce 1927 navrhl John von Neumann (1903-1957) aplikovat substituci pouze na axiómy. Vznikly systémy založené na schématech axiómů . VÝ ROKOVÁ LOGIKA. Historické pozná mky. 59 David Hilbert (1862­1943) a Wilhelm Ackermann (1896-1962) publikovali v roce 1928 následující systém: 1: (P P) P 2: P (P Q) 4: (P Q) (Q P) 5: (Q R) ((P Q) (P R)) Odvozovací pravidla: MP a substituce V roce 1927 navrhl John von Neumann (1903-1957) aplikovat substituci pouze na axiómy. Vznikly systémy založené na schématech axiómů . Jan Lukasiewicz (1878­1956) prezentoval svů j odvozovací systém (použitý v přednášce) v roce 1928. VÝ ROKOVÁ LOGIKA. Historické pozná mky. 60 Další odvozovací systémy: VÝ ROKOVÁ LOGIKA. Historické pozná mky. 60 Další odvozovací systémy: ¸ V roce 1947 zjednodušili Go¨tling a Rasiowa systém z Principia Mathematica do následující podoby: ˇ 1: (P P) P ˇ 2: P (P Q) ˇ 3: (Q R) ((P Q) (P R)) ˇ Odvozovací pravidla: MP a substituce VÝ ROKOVÁ LOGIKA. Historické pozná mky. 60 Další odvozovací systémy: ¸ V roce 1947 zjednodušili Go¨tling a Rasiowa systém z Principia Mathematica do následující podoby: ˇ 1: (P P) P ˇ 2: P (P Q) ˇ 3: (Q R) ((P Q) (P R)) ˇ 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: (((( ) ( )) ) ) (( ) ( )) ˇ 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 Schro¨derovy monografie Algebra der Logik (1910) a monografii Principia Mathematica (Whitehead, Russel). Logika prvního řádu byla definována jako samostatný systém až v monografii Hilberta a Ackermanna Grundzu¨gen der theoretischen Logik (1928). PREDIKÁTOVÁ LOGIKA. Syntaxe. 62 PREDIKÁTOVÁ LOGIKA. Syntaxe. 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. PREDIKÁTOVÁ LOGIKA. Syntaxe. 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í přídá me speciá lní logický symbol = jehož sémantika bude definová na speciá lním způ sobem. PREDIKÁTOVÁ LOGIKA. Syntaxe. 63 PREDIKÁTOVÁ LOGIKA. Syntaxe. 63 Příklad 43. Jazyk teorie množin je jazykem s rovností, který obsahuje jeden prediká tový symbol arity 2. Jazyk teorie pologrup je jazykem s rovností, který obsahuje jeden funkční symbol ,," arity 2. PREDIKÁTOVÁ LOGIKA. Syntaxe. 63 Příklad 43. Jazyk teorie množin je jazykem s rovností, který obsahuje jeden prediká tový symbol 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 L tvoří 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 L. Je-li L jazyk s rovností, obsahuje abeceda speciá lní znak = pro rovnost. Logické spojky a . Symbol pro univerzá lní kvantifiká tor. Zá vorky ( a ). PREDIKÁTOVÁ LOGIKA. Syntaxe. 64 PREDIKÁTOVÁ LOGIKA. Syntaxe. 64 Definice 45. Termem jazyka L je slovo t nad abecedou prediká tové logiky pro jazyk L, pro které existuje vytvořující posloupnost slov t1, , tk, kde k 1, tk je t, a pro každé 1 i k má slovo ti jeden z ná sledujících tvarů : proměnná , f(ti1 , , tin ), kde 1 i1, , in < k, f je funkční symbol jazyka L, a n je arita f. Term je uzavřený, jestliže neobsahuje proměnné. PREDIKÁTOVÁ LOGIKA. Syntaxe. 64 Definice 45. Termem jazyka L je slovo t nad abecedou prediká tové logiky pro jazyk L, pro které existuje vytvořující posloupnost slov t1, , tk, kde k 1, tk je t, a pro každé 1 i k má slovo ti jeden z ná sledujících tvarů : proměnná , f(ti1 , , tin ), kde 1 i1, , in < k, f je funkční symbol jazyka L, 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 infixový zá pis. U funkčních (a prediká tových) symbolů arity nula budeme psá t c místo c(). PREDIKÁTOVÁ LOGIKA. Syntaxe. 64 Definice 45. Termem jazyka L je slovo t nad abecedou prediká tové logiky pro jazyk L, pro které existuje vytvořující posloupnost slov t1, , tk, kde k 1, tk je t, a pro každé 1 i k má slovo ti jeden z ná sledujících tvarů : proměnná , f(ti1 , , tin ), kde 1 i1, , in < k, f je funkční symbol jazyka L, 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 infixový 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) z je termem jazyka pologrup (v prefixové notaci ((x, y), z)) 0 + (S(0) + S(S(0))) je termem jazyka 0, S, +, kde 0, S a + jsou po řadě PREDIKÁTOVÁ LOGIKA. Syntaxe. 65 funkční symboly arity nula, jedna a dva. PREDIKÁTOVÁ LOGIKA. Syntaxe. 65 funkční symboly arity nula, jedna a dva. PREDIKÁTOVÁ LOGIKA. Syntaxe. 65 funkční symboly arity nula, jedna a dva. PREDIKÁTOVÁ LOGIKA. Syntaxe. 65 funkční symboly arity nula, jedna a dva. PREDIKÁTOVÁ LOGIKA. Syntaxe. 66 PREDIKÁTOVÁ LOGIKA. Syntaxe. 66 Definice 48. Formule prediká tového počtu jazyka L je slovo nad abecedou prediká tové logiky pro jazyk L, pro které existuje vytvořující posloupnost slov 1, , k, kde k 1, k je , a pro každé 1 i k má slovo i jeden z ná sledujících tvarů : P(t1, , tn), kde P je prediká tový symbol jazyka L arity n a t1, , tn jsou termy jazyka L. t1 = t2, je-li L jazyk s rovností a t1, t2 jsou termy jazyka L. j pro nějaké 1 j < i, (j j ) pro nějaká 1 j, j < i, x j, kde x je proměnná a 1 j < i. PREDIKÁTOVÁ LOGIKA. Syntaxe. 67 PREDIKÁTOVÁ LOGIKA. Syntaxe. 67 Poznámka 49. Ve zbytku předná šky budeme používat ná sledující ,,zkratky": x značí x značí značí ( ). značí ( ) ( ), kde symbol dá le ,,rozvineme" podle předchozího bodu. PREDIKÁTOVÁ LOGIKA. Syntaxe. 67 Poznámka 49. Ve zbytku předná šky budeme používat ná sledující ,,zkratky": x značí x značí značí ( ). značí ( ) ( ), kde symbol dá le ,,rozvineme" podle předchozího bodu. Příklady formulí: x P(x, y) x (P(x, x) Q(c)) x x (P(x, x) y x Q(x)) PREDIKÁTOVÁ LOGIKA. Syntaxe. 68 PREDIKÁTOVÁ LOGIKA. Syntaxe. 68 Definice 50. Každý výskyt proměnné ve formuli prediká tového počtu je bud' volný nebo vá zaný podle ná sledujícího induktivního předpisu: Ve formuli tvaru P(t1, , tn) 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 volný (resp. vá zaný), je odpovídající výskyt ve formulích , , rovněž volný (resp. vá zaný). Ve formuli x 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 , je odpovídající výskyt ve formuli x rovněž volný (resp. vá zaný). PREDIKÁTOVÁ LOGIKA. Syntaxe. 68 Definice 50. Každý výskyt proměnné ve formuli prediká tového počtu je bud' volný nebo vá zaný podle ná sledujícího induktivního předpisu: Ve formuli tvaru P(t1, , tn) 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 volný (resp. vá zaný), je odpovídající výskyt ve formulích , , rovněž volný (resp. vá zaný). Ve formuli x 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 , je odpovídající výskyt ve formuli x rovněž volný (resp. vá zaný). Příklady (volné výskyty jsou červené): x P(x, y) y P(x, y) x (P(x, y) y P(x, y)) PREDIKÁTOVÁ LOGIKA. Syntaxe. 69 PREDIKÁTOVÁ LOGIKA. Syntaxe. 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 (x1, , xn) značí, že všechny volné proměnné ve formuli jsou mezi x1, , xn (nemusí nutně platit, že každá z těchto proměnných je volná ve ). Univerzá lní uzá věr formule je formule tvaru x1 xn , kde x1, , xn jsou prá vě všechny volné proměnné formule . PREDIKÁTOVÁ LOGIKA. Substituce. 70 PREDIKÁTOVÁ LOGIKA. Substituce. 70 Definice 52. Term t je substituovatelný za proměnnou x ve formuli , 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 . Je-li t substituovatelný za x ve , značí zá pis (x/t) formuli, která vznikne nahrazením každého volného výskytu x ve termem t. PREDIKÁTOVÁ LOGIKA. Substituce. 70 Definice 52. Term t je substituovatelný za proměnnou x ve formuli , 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 . Je-li t substituovatelný za x ve , značí zá pis (x/t) formuli, která vznikne nahrazením každého volného výskytu x ve termem t. Příklady: Term y + 3 je substituovatelný za x ve formuli z x+y=z Term y + z není substituovatelný za x ve formuli z x+y=z (P(x, y) x P(x, y))(x/3) je formule P(3, y) x P(x, y) P(x, y)(x/y)(y/x) je formule P(x, x) PREDIKÁTOVÁ LOGIKA. Substituce. 71 PREDIKÁTOVÁ LOGIKA. Substituce. 71 Definice 53. Necht' je formule a t1, , tn termy, které jsou v uvedeném pořadí substituovatelné za proměnné x1, , xn ve (předpoklá dá me, že x1, , xn jsou rů zné). Symbol (x1/t1, , xn/tn) značí formuli, která vznikne ,,simultá nním nahrazením" každého volného výskytu xi termem ti pro každé 1 i n. Přesněji, (x1/t1, , xn/tn) je formule (x1/z1) (xn/zn)(z1/t1) (zn/tn), kde z1, , zn jsou (rů zné) proměnné, které se nevyskytují v t1, , tn ani mezi x1, , xn. PREDIKÁTOVÁ LOGIKA. Substituce. 71 Definice 53. Necht' je formule a t1, , tn termy, které jsou v uvedeném pořadí substituovatelné za proměnné x1, , xn ve (předpoklá dá me, že x1, , xn jsou rů zné). Symbol (x1/t1, , xn/tn) značí formuli, která vznikne ,,simultá nním nahrazením" každého volného výskytu xi termem ti pro každé 1 i n. Přesněji, (x1/t1, , xn/tn) je formule (x1/z1) (xn/zn)(z1/t1) (zn/tn), kde z1, , zn jsou (rů zné) proměnné, které se nevyskytují v t1, , tn ani mezi x1, , xn. Příklad: P(x, y)(x/y, y/x) je formule P(y, x) PREDIKÁTOVÁ LOGIKA. Realizace jazyka. 72 PREDIKÁTOVÁ LOGIKA. Realizace jazyka. 72 Definice 54. Realizace M jazyka L 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 fM : Mm M. Ohodnocení je zobrazení přiřazující proměnným prvky univerza M. PREDIKÁTOVÁ LOGIKA. Realizace jazyka. 73 PREDIKÁTOVÁ LOGIKA. Realizace jazyka. 73 Definice 55. Realizaci termu t při ohodnocení e v relizaci M, psá no tM [e] (případně jen t[e] je-li M jasné z kontextu), definujeme induktivně takto: x[e] = e(x) f(t1, , tm)[e] = fM(t1[e], , tm[e]) (pro m = 0 je na pravé staně uvedené definující rovnosti fM()). PREDIKÁTOVÁ LOGIKA. Realizace jazyka. 74 PREDIKÁTOVÁ LOGIKA. Realizace jazyka. 74 Definice 56 (A. Tarski). Bud' M realizace jazyka L, e ohodnocení a formule prediká tového počtu jazyka L. Terná rní vztah M |= [e] definujeme indukcí ke struktuře : M |= P(t1, , tm)[e] prá vě když (t1[e], , tm[e]) PM. Jestliže L je jazyk s rovností, definujeme M |= (t1 = t2)[e] prá vě když t1[e] a t2[e] jsou stejná individua. M |= [e] prá vě když není M |= [e]. M |= ( )[e] prá vě když M |= [e] nebo není M |= [e]. M |= x [e] prá vě když M |= [e(x/a)] pro každý prvek a univerza M. Jestliže M |= [e], říká me, že je pravdivá v M při ohodnocení e. Jestliže M |= [e] pro každé e, je pravdivá v M, psá no M |= . PREDIKÁTOVÁ LOGIKA. Realizace jazyka. 75 PREDIKÁTOVÁ LOGIKA. Realizace jazyka. 75 Příklad 57. Bud'L jazyk s jedním uná rním prediká tem P a M jeho realizace nad univerzem M = {a, b}, kde PM = {a}. Pak Platí M |= x (P(x) (P(x) P(x))) Neplatí M |= P(x) x P(x) Neplatí M |= (x P(x) x P(x)) x (P(x) P(x)) PREDIKÁTOVÁ LOGIKA. Teorie. 76 PREDIKÁTOVÁ LOGIKA. Teorie. 76 Definice 58. Bud' L jazyk (příp. jazyk s rovností). Teorie (s jazykem L) je soubor T formulí prediká tového počtu jazyka L. Prvky T se nazývají axiómy teorie T. Realizace M jazyka L je model teorie T, psá no M |= T, jestliže M |= pro každé z T. Teorie je splnitelná , jestliže má model. Je-li M realizace jazyka L, pak Th(M) označuje teorii tvořenou prá vě všemi uzavřenými formulemi, které jsou v M pravdivé. Formule je sémantickým dů sledkem teorie T, psá no T |= , jestliže je pravdivá v každém modelu teorie T. PREDIKÁTOVÁ LOGIKA. Teorie. 77 PREDIKÁTOVÁ LOGIKA. Teorie. 77 Příklad 59. Uvažme jazyk s rovností obsahující jeden biná rní funkční symbol "" a jednu konstantu 1. Necht'T je tvořena ná sledujícími formulemi: x y z x (y z) = (x y) z x (x 1 = x) (1 x = x) x y (x y = 1) (y x = 1) Pak formule x y (x y) = (y x) není sémantickým dů sledkem T, zatímco formule x (1 y) = (1 x) y ano. PREDIKÁTOVÁ LOGIKA. Odvozovací systém. 78 Schémata výrokových axiómů : P1: ( ) P2: ( ( )) (( ) ( )) P3: ( ) ( ) Schéma axiómu specifikace: P4: x (x/t), kde t je substituovatelný za x ve . Schéma axiómu distribuce: P5: (x ( )) ( x ), kde x nemá volný výskyt ve . Odvozovací pravidla: MP: Z a odvod' . (modus ponens) GEN: Z odvod' x . (generalizace) PREDIKÁTOVÁ LOGIKA. Odvozovací systém. 79 PREDIKÁTOVÁ LOGIKA. Odvozovací systém. 79 Je-li L jazyk s rovností, přídáme dále následující axiómy rovnosti: R1: x = x R2: (x1=y1 xn=yn P(x1, , xn)) P(y1, , yn), kde P je predikátový symbol arity n. R3: (x1=y1 xm=ym) (f(x1, , xm)=f(y1, , ym)), kde f je funkční symbol arity m. PREDIKÁTOVÁ LOGIKA. Odvozovací systém. 80 Definice 60. Bud' T teorie jazyka L. PREDIKÁTOVÁ LOGIKA. Odvozovací systém. 80 Definice 60. Bud' T teorie jazyka L. Dů kaz formule v teorii T je konečná posloupnost formulí 1, , k, kde k je a pro každé i, kde 1 i k, platí alespoň jedna z ná sledujících podmínek: i je prvek T; i je instancí jednoho ze schémat P1­P5; L je jazyk s rovností a i je instancí jednoho ze schémat R1­R3; i vznikne aplikací pravidla MP na formule m, n pro vhodné 1 m, n < i. i vznikne aplikací pravidla GEN na formuli m pro vhodné 1 m < i. PREDIKÁTOVÁ LOGIKA. Odvozovací systém. 81 PREDIKÁTOVÁ LOGIKA. Odvozovací systém. 81 Formule je dokazatelná v teorii T, psá no T , jestliže existuje dů kaz v T. Jestliže T pro prá zdné T, říká me že je dokazatelná a píšeme . Formule je vyvratitelná v teorii T, jestliže T Teorie T je sporná (též inkonzistentní), jestliže každá formule prediká tové logiky jazyka L je v T dokazatelná . Teorie je bezesporná (též konzistentní), jestliže není nekonzistentní. PREDIKÁTOVÁ LOGIKA. Dů kazy. 82 PREDIKÁTOVÁ LOGIKA. Dů kazy. 82 Poznámka 61 (Princip dosazení do tautologie výrokového počtu). Je-li tautologií L(, ), 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. PREDIKÁTOVÁ LOGIKA. Dů kazy. 82 Poznámka 61 (Princip dosazení do tautologie výrokového počtu). Je-li tautologií L(, ), 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í x . Platí ovšem {} x . Proto obecně neplatí, že T |= prá vě když T {} |= . PREDIKÁTOVÁ LOGIKA. Věta o dedukci. 83 PREDIKÁTOVÁ LOGIKA. Věta o dedukci. 83 Věta 63 (o dedukci). Necht'T je teorie jazyka L, uzavřená formule jazyka L a (libovolná ) formule jazyka L. Pak T prá vě když T {} . PREDIKÁTOVÁ LOGIKA. Věta o dedukci. 83 Věta 63 (o dedukci). Necht'T je teorie jazyka L, uzavřená formule jazyka L a (libovolná ) formule jazyka L. Pak T prá vě když T {} . Dů kaz. Dů kaz je velmi podobný dů kazu věty 35: ,,": Necht' 1, , k je dů kaz formule v T. Pak 1, , k, , je dů kaz formule v T {} (poslední formule vznikne aplikací MP na a k). PREDIKÁTOVÁ LOGIKA. Věta o dedukci. 83 Věta 63 (o dedukci). Necht'T je teorie jazyka L, uzavřená formule jazyka L a (libovolná ) formule jazyka L. Pak T prá vě když T {} . Dů kaz. Dů kaz je velmi podobný dů kazu věty 35: ,,": Necht' 1, , k je dů kaz formule v T. Pak 1, , k, , je dů kaz formule v T {} (poslední formule vznikne aplikací MP na a k). ,,": Necht' 1, , k je dů kaz v T {}. Metaindukcí k j dokážeme, že T j pro každé 1 j k. PREDIKÁTOVÁ LOGIKA. Věta o dedukci. 83 Věta 63 (o dedukci). Necht'T je teorie jazyka L, uzavřená formule jazyka L a (libovolná ) formule jazyka L. Pak T prá vě když T {} . Dů kaz. Dů kaz je velmi podobný dů kazu věty 35: ,,": Necht' 1, , k je dů kaz formule v T. Pak 1, , k, , je dů kaz formule v T {} (poslední formule vznikne aplikací MP na a k). ,,": Necht' 1, , k je dů kaz v T {}. Metaindukcí k j dokážeme, že T j pro každé 1 j k. j = 1. Je-li 1 instance axiómu nebo formule z T, platí T 1. K dů kazu 1 z T nyní připojíme formule 1 ( 1), 1. První formule je instancí P1, druhá aplikací MP na 1 a první formuli. Máme tedy dů kaz 1 v T. Je-li 1 formule , platí T 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 {}, postupujeme stejně jako výše (místo 1 použijeme j). PREDIKÁTOVÁ LOGIKA. Věta o dedukci. 84 Indukční krok: Je-li formule j instancí axiómu nebo prvek T {}, postupujeme stejně jako výše (místo 1 použijeme j). Je-li j výsledkem aplikace MP na m, n, kde 1 m, n < j, je n tvaru m j. Podle I.P. navíc platí T m a T (m j). Dů kazy m a (m j) v T nyní zřetězíme za sebe a připojíme následující formule: ( (m j)) (( m) ( j)) ( m) ( j) j První formule je instancí P2, další dvě vzniknou aplikací MP. Máme tedy dů kaz formule j v T. PREDIKÁTOVÁ LOGIKA. Věta o dedukci. 85 PREDIKÁTOVÁ LOGIKA. Věta o dedukci. 85 Je-li j výsledkem aplikace GEN na m, kde 1 m < j, je j tvaru x m. Podle I.P. platí T m. K tomuto dů kazu nyní stačí připojit formule x ( m) x ( m) ( x m) x m. První vznikne aplikací GEN, druhá je instancí P5, třetí vznikne aplikací MP. Dostaneme tak dů kaz formule j v T. PREDIKÁTOVÁ LOGIKA. Vlastnosti kvantifikace. 86 Lema 64. Pro každé formule a platí: 1. (x ( )) ( x ), pokud x není volná ve formuli ; 2. (x ( )) (x ), pokud x není volná ve formuli ; 3. (x ( )) ( x ), pokud x není volná ve formuli ; 4. (x ( )) (x ), pokud x není volná ve formuli . Dů kaz. Pozorování: (a) Jestliže a současně , pak . 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 a současně T , pak T . Stačí použít pozná mku 61 a tautologii (A C) ((C B) (A B)). PREDIKÁTOVÁ LOGIKA. Vlastnosti kvantifikace. 87 (c) Necht' (x), (x) jsou formule. Pak x ( ) x ( ), nebot' 1) x ( ) ( ) P4 2) ( ) ( ) výr. tautologie 3) x ( ) ( ) tranz. impl. na 1), 2) 4) x ( ) věta o dedukci 5) x ( ) x ( ) GEN 6) x ( ) x ( ) věta o dedukci Tvrzení 1.­4. ted' dokážeme za předpokladu, že (x) a (x). Obecná podoba vyplyne užitím věty konstantách (viz dále). PREDIKÁTOVÁ LOGIKA. Vlastnosti kvantifikace. 88 1. Platí (x ( )) ( x ), nebot' tato formule je instancí P5. Dů kaz opačné implikace vypadá takto: 1) x P4 2) (x ) (( x ) ( )) (A B) ((C A) (C B)) je tautologie, viz pozn. 61 3) ( x ) ( ) MP na 1), 2) 4) x věta o dedukci 5) x x ( ) GEN 6) ( x ) (x ( )) věta o dedukci PREDIKÁTOVÁ LOGIKA. Vlastnosti kvantifikace. 89 2. Nejprve ukážeme, že x ( ) (x ). 1) x ( ) ( x ) podle 1. 2) x ( ) x ( ) podle (c) 3) x ( )) ( x ) tranz. impl. na 2), 1) 4) ( x ) (x ) taut. (B A) (A B) 5) x ( ) (x ) tranz. impl. na 3), 4) 6) x ( ) (x ) reformulace PREDIKÁTOVÁ LOGIKA. Vlastnosti kvantifikace. 90 Nyní opačný směr (x ) x ( ): 1) ( x ) x ( ) podle 1. 2) (x ) ( x ) taut. (B A) (A B) 3) (x ) x ( ) tranz. impl. na 1), 2) 4) x x ( ) věta o dedukci 5) x P4 a MP 6) x (A B) (A B) a MP 7) x x ( ) GEN 8) (x ) x ( ) věta o dedukci PREDIKÁTOVÁ LOGIKA. Věta o korektnosti. 91 PREDIKÁTOVÁ LOGIKA. Věta o korektnosti. 91 Věta 65. Necht'T je teorie a formule jazyka teorie T. Jestliže T , pak T |= . PREDIKÁTOVÁ LOGIKA. Věta o korektnosti. 91 Věta 65. Necht'T je teorie a formule jazyka teorie T. Jestliže T , pak T |= . Dů kaz. Stačí ověřit následující tvrzení: Je-li 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 M model T a , formule jazyka teorie T, kde M |= a M |= , pak M |= . Je-li M model T a formule jazyka teorie T, kde M |= , pak M |= x . Metaindukcí vzhledem k i je pak již triviální ukázat, že je-li 1, , k dů kaz formule v T a M je model T, pak T |= i pro každé 1 i k. PREDIKÁTOVÁ LOGIKA. Věta o ú plnosti (ú vod). 92 Lema 66. Ná sledující tvrzení jsou ekvivalentní: 1. Pro každou teorii T a pro každou formuli jazyka teorie T platí, že jestliže T |= , pak T . 2. Každá bezesporná teorie má model. Dů kaz. (1. 2.) Bud' T bezesporná teorie. Pak existuje formule jazyka teorie T, která není v T dokazatelná (tj. T ). Obměnou 1. pak ale dostáváme, že není sémantickým dů sledkem T (tj. T |= ). To znamená, že existuje takový model T, kde není pravdivá . Zejména má tedy T model. PREDIKÁTOVÁ LOGIKA. Věta o ú plnosti (ú vod). 93 (2. 1.) Užitím 2. dokážeme obměnu 1. Necht' tedy T , a necht' je univerzální uzávěr . Ukážeme, že T {} je bezesporná; pak podle 2. má T {} model, tedy T |= . T {} je bezesporná: Předpokládejme naopak, že T {} je sporná. Pak 1) T {} T {} je sporná 2) T věta o dedukci 3) ( ) (A B) B je tautologie, viz pozn. 62 4) T MP na 2), 3) 5) T opakovaně P4 a MP Obdrželi jsme tedy spor s tím, že T . PREDIKÁTOVÁ LOGIKA. Věta o ú plnosti (ú vod). 94 PREDIKÁTOVÁ LOGIKA. Věta o ú plnosti (ú vod). 94 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á. PREDIKÁTOVÁ LOGIKA. Rozšíření teorie. 95 PREDIKÁTOVÁ LOGIKA. Rozšíření teorie. 95 Definice 67. Teorie S je rozšíření teorie T, jestliže jazyk teorie S obsahuje jazyk teorie T 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 jazyka 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 rozšířením S. PREDIKÁTOVÁ LOGIKA. Věta o konstantá ch. 96 Věta 68 (o konstantách). Necht'S je rozšíření T vzniklé obohacením jazyka teorie T o nové navzá jem rů zné konstanty c1, , ck (nové axiómy nepřidá vá me), a necht'x1, , xk jsou navzá jem rů zné proměnné. Pak pro každou formuli jazyka teorie T platí, že T prá vě když S (x1/c1, , xk/ck). Dů kaz. Jelikož c1, , ck jsou navzájem rů zné, stačí dokázat, že T právě když S (x/c). : K dů kazu v T připojíme formule x , x (x/c), (x/c) a obdržíme tak dů kaz formule (x/c) v S. : Necht' 1, , k je dů kaz (x/c) v S. Necht' y je proměnná, která se nevyskytuje v tomto dů kazu. Indukcí k i ukážeme, že pro každé 1 i k je 1(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 i instancí P1­P5 (příp. R1­R3), je také i(c/y) instancí téhož schématu. Je-li i axióm teorie T, pak se v i nevyskytuje c a formule i a i(c/y) jsou tedy totožné. Jestliže i vyplývá z j a m pomocí MP, je m tvaru j i a formule m(c/y) je tedy formulí j(c/y) i(c/y). Takže formule i(c/y) vyplývá z j(c/y) a m(c/y) pomocí MP. Jestliže i vyplývá z j pomocí GEN, je i tvaru x j. Stačí si uvědomit, že (x j)(c/y) je tatáž formule jako x (j(c/y)), nebot' x a y jsou rů zné. PREDIKÁTOVÁ LOGIKA. Věta o konstantá ch. 98 Ukázali jsme, že T (x/c)(c/y). Dále 1) T (x/y) (x/y) je totéž co (x/c)(c/y) 2) T y (x/y) GEN 3) y (x/y) ((x/y)(y/x)) P4 4) T (x/y)(y/x) MP na 2), 3) 5) T (x/y)(y/x) je totéž co PREDIKÁTOVÁ LOGIKA. Henkinovské a ú plné teorie. 99 Definice 69. Teorie T je henkinovská , jestliže pro každou formuli jazyka teorie T s jednou volnou proměnnou x existuje v jazyce teorie T konstanta c taková , že T x (x/c). Teorie T je ú plná , jestliže je bezesporná a pro každou uzavřenou formuli jejího jazyka platí bud' T nebo T . PREDIKÁTOVÁ LOGIKA. Henkinovské a ú plné teorie. 100 Věta 70 (o henkinovské konstantě). Bud' T teorie a (x) formule jejího jazyka. Je-li S rozšíření T, které vznikne přidá ním nové konstanty c a formule x (x/c), pak S je konzervativní rozšíření T. Dů kaz. Nejprve ukážeme, že pro libovolnou formuli (x) platí x y(x/y): 1) {y(x/y)} y(x/y) 2) {y(x/y)} (x/y)(y/x) P4 a MP 3) {y(x/y)} přepis 4) {y(x/y)} x GEN 5) y(x/y) x dedukce 6) x y(x/y) taut. (A B) (B A) a MP. PREDIKÁTOVÁ LOGIKA. Henkinovské a ú plné teorie. 101 Necht' R značí teorii vzniklou pouhým přidáním konstanty c k T. Necht' je formule jazyka teorie T taková, že S . Necht' y je proměnná, která se nevyskytuje ani ve , ani v . Platí: 1) S předpoklad 2) R (x (x/c)) S = R {x (x/c)} a dedukce 3) T (x (x/y)) věta o konstantách 4) T y((x (x/y)) ) GEN 5) T y(x (x/y)) lema 64 (2) a MP 6) (x y(x/y)) y(x (x/y)) lema 64 (3) 7) T (x y(x/y)) tranz. implikace 8) x y(x/y) dokázáno výše 9) T MP PREDIKÁTOVÁ LOGIKA. Henkinovské a ú plné teorie. 102 Věta 71 (o henkinovském rozšíření). Ke každé teorii existuje henkinovská teorie, která je jejím konzervativním rozšířením. Dů kaz. Bud' T (libovolná) teorie. Pro každé n 0 definujeme teorii Tn takto: T0 = T. Teorie Ti+1 vznikne z Ti tak, že pro každou formuli (x) jazyka teorie Ti přidáme novou konstantu c a formuli x (x/c). Metaindukcí vzhledem k n ukážeme, že Tn je konzervativní rozšíření T. Pro n = 0 není co dokazovat. V indukčním kroku si stačí uvědomit, že je-li Ti+1 , mů že být v dů kazu formule použito jen konečně mnoho axiómů 1, , k, které nepatří do Ti. Užitím věty o henkinovské konstantě k-krát po sobě dostáváme Ti , proto T podle I.P. Uvažme teorii S = n=0 Tn. Teorie S je konzervativní rozšíření T, nebot' každý dů kaz v S používá jen konečně mnoho axiómů a je tedy dů kazem v nějaké Tm. Teorie S je zjevně henkinovská. PREDIKÁTOVÁ LOGIKA. Henkinovské a ú plné teorie. 103 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. Bud' T teorie, a necht' je dobré uspořádání na množině všech uzavřených formulí jazyka teorie T. Pro každou uzavřenou formuli jazyka teorie T definujeme teorii T induktivně takto: Je-li nejmenší prvek v uspořádání , klademe T = T, Jinak T = T {} je-li T {} bezesporná; T {} jinak. PREDIKÁTOVÁ LOGIKA. Henkinovské a ú plné teorie. 104 Indukcí vzhledem k dokážeme, že každé T je bezesporné rozšíření T. Je-li nejmenší prvek v uspořádání , není co dokazovat. Indukční krok: Označme symbolem S teorii T. Teorie S je nutně bezesporná. Jinak S pro nějakou formuli . Jelikož tento dů kaz používá jen konečně mnoho axiómů teorie S, nutně existuje takové, že T obsahuje všechny použité axiómy. Proto T , což je spor s IP. Je-li T = S {}, je T bezesporná. Je-li T = S {}, je teorie S {} sporná. Pokud by byla sporná také teorie S {}, platilo by S {} a S {} , proto i S a S (užitím věty o dedukci). Z toho dostáváme S pro libovolné , nebot' (A A) ((A A) ( )) je výroková tautologie (použijeme 2x MP). Tedy i S je sporná, což je spor s předchozím bodem. PREDIKÁTOVÁ LOGIKA. Henkinovské a ú plné teorie. 105 Uvažme teorii U která vznikne sjednocením všech T. Zjevně U je rozšíření T a má stejný jazyk jako T. Pokud by U byla sporná, existoval by dů kaz v U. Tento dů kaz využívá pouze konečně mnoho axiómů U, proto je dokazatelná i v nějaké T, což je spor. PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 106 Definice 73. Bud' 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 fM, která uzavřeným termů m t1, , tn přiřadí uzavřený term f(t1, , tn); realizace prediká tového symbolu P arity m je prediká t PM definovaný takto: PM(t1, , tm) platí prá vě když T P(t1, , tm). PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 107 Věta 74 (o kanonické struktuře). Necht'T je ú plná henkinovské teorie, a necht'jazyk teorie T je jazykem bez rovnosti. Pak kanonická struktura teorie T je modelem T. Dů kaz. Necht' M je kanonická struktura teorie T. Ukážeme, že pro libovolnou formuli jazyka teorie T platí následující: Jestliže ^ je uzavřená instance formule , pak T ^ právě když M |= ^. Jelikož lze (bez ú jmy na obecnosti) předpokládat, že prvky T jsou uzavřené formule, plyne z výše uvedeného, že M je model T. Indukcí ke struktuře : P(t1, , tn). Bud' P(t 1, , t n) libovolná uzavřená instance. Podle definice kanonické struktury M |= P(t 1, , t n) právě když T P(t 1, , t n). PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 108 . Bud' ^ libovolná uzavřená instance. Jelikož ^ je uzavřená instance , podle IP platí T ^ právě když M |= ^. Dále T ^ právě když T ^ (T je bezesporná) právě když M |= ^ (IP) právě když M |= ^. . Každá uzavřená instance této formule je tvaru ^ ^, kde ^ je uzavřená instance a ^ je uzavřená instance . Necht' T ^ ^. Jelikož ^ je uzavřená formule a T je uplná, platí bud' T ^ nebo T ^. V prvém případě dále T ^ (MP) a užitím IP celkem dostáváme M |= ^ a M |= ^. Proto také M |= ^ ^. V druhém případě T ^ (T je bezesporná), proto M |= ^ (IP), tudíž M |= ^ ^. Necht' M |= ^ ^. Pak bud' M |= ^ nebo M |= ^. V prvém případě T ^ podle IP, tudíž T ^ nebot' T je ú plná. Proto T ^ ^ užitím tautologie A (A B) a MP. V druhém případě T ^, proto T ^ ^ užitím tautologie A (B A) a MP. PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 109 x . Bud' x libovolná uzavřená instance. Pak (x), jinak by x nebyla uzavřená. Necht' T x . Pak pro libovolný uzavřený term t platí T (x/t) (P4 a MP). Podle IP M |= (x/t). Jelikož tento argument funguje pro libovolný uzavřený term t, platí také M |= x . Necht' T x . Pak také T x (kdyby T x , dostaneme dále T (P4 a MP) a T (tautologie A A a MP), T x (GEN), spor). Jelikož T x , platí T x nebot' T je ú plná. Tedy T x . Jelikož T je henkinovská, platí T x (x/c). Tedy T (x/c) a proto T (x/c) nebot' T je bezesporná. Podle IP M |= (x/c), tedy M |= (x/c). Proto M |= x . PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 110 Věta 75. Necht'T je ú plná henkinovské teorie, a necht'jazyk teorie T je jazykem s rovností. Pak T má model. Dů kaz. Bud' 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). PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 111 Bud' M kanonická struktura teorie S, a necht' je realizace = v S (tj. t1 t2 právě když S t1 = t2). Dokážeme, že je nutně ekvivalence: reflexivita: S x=x (R1), S x x=x (GEN), S x x=x t=t (P4), S t=t (MP). Tedy t t. symetrie: necht' s t, tj. S s=t. Platí S (x1=y1 x2=y2) (x1=x2 y1=y2) (R2, = hraje i roli P). Užitím GEN, P4 a MP dostaneme S (s=t s=s) (s=s t=s). Užitím MP dostaneme S t=s. Tranzitivita: podobně. PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 112 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([t1], , [tn]) = [fM(t1, , tn)] Predikátový symbol P arity m je realizován takto: PO([t1], , [tm]) právě když PM(t1, , 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 O je [s] právě když S s=t. To znamená, že predikátový symbol = je v O realizován jako identita. PREDIKÁTOVÁ LOGIKA. Kanonická struktura. 113 Zbývá ukázat, že O je modelem S. Podobně jako ve větě 75 budeme chtít prokázat, že pro libovolnou formuli (x1, . . . , xn) jazyka teorie S platí: Jestliže t1, , tn jsou uzavřené termy jazyka teorie S, pak T (x1/t1, , xn/tn) právě když O |= (x1/[t1], , xn/[tn]). Jelikož S je henkinovská a ú plná, platí podle věty 75 T (x1/t1, , xn/tn) právě když M |= (x1/t1, , xn/tn) Stačí tedy ukázat, že M |= (x1/t1, , xn/tn) právě když O |= (x1/[t1], , xn/[tn]) To lze lehce provést indukcí ke struktuře . PREDIKÁTOVÁ LOGIKA. Věta o ú plnosti. 114 Kurt Go¨del (1906­1978) Věta 76 (o ú plnosti, Kurt Go¨del). Každá bezesporná teorie má model. Pro každou teorii T a každou formuli je- jího jazyka tedy platí, že jestliže T |= , pak T . Dů kaz. Jde o jednoduchý dů sledek předchozích vět. PREDIKÁTOVÁ LOGIKA. Věta o kompaktnosti. 115 Věta 77. Teorie T má model, prá vě když každá její podteorie s konečně mnoha axiómy (a s minimá lním jazykem, v němž jsou tyto axiómy formulovatelné) má model. Dů kaz. Směr ,," 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 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. Lo¨wenheimova-Skolemova věta.116 Poznámka 78. Z dů kazu věty 71 plyne, že každá bezesporná teorie s jazykem bez rovnosti má model kardinality max{|L|, 0} (při rozšíření teorie na henkinovskou bylo přidá no |L| 0 nových konstant). Toto pozorová ní neplatí pro teorie s jazykem s rovností (např. pro T = {x x=c}. Nicméně lze doká zat ná sledující: Věta 79. Necht'T je teorie a necht'pro každé n 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 N definujeme formuli n x1 xny x1=y xn=y a teorii Sn = T {1, , n}. Podle předpokladu věty má každá Sn model. Podle věty o kompaktnosti má proto model i teorie i=1 Sn. Tento model je nutně nekonečný a je i modelem teorie T. PREDIKÁTOVÁ LOGIKA. Lo¨wenheimova-Skolemova věta.117 Věta 80 (Lo¨wenheimova-Skolemova). Necht'T je teorie s jazykem L, která má nekonečný model. Necht' je nekonečný kardiná l takový, že |L|. Pak T má model mohutnosti . Dů kaz. Necht' M je nekonečný model T. Jazyk L rozšíříme o systém {ci | i < } nových konstant a k T přidáme axiómy {ci = cj | i, j < }. Obdržíme tak teorii T . Necht' K je konečná část T , a necht' c1, , 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 T je tedy splnitelná. Podle věty o kompaktnosti má tedy model i teorie T . Nosič tohoto model ale nutně obsahuje alespoň navzájem rů zných individuí. VĚTA 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 (N0, , +), 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ů Hilbertova programu formalizace matematiky mělo být vytvoření rekurzivní a ú plné teorie T jazyka aritmetiky. Slovem ,,ú plné" se myslí, že T právě když Th(N0, , +) (Tj. formule dokazatelné v T jsou právě formule pravdivé v (N0, , +)). 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 Go¨delových výsledků plyne, že taková teorie neexistuje. VĚTA O NEÚ PLNOSTI. Turingů 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). Turingů v stroj je matematickým mo- delem ,,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 pro- jevil až v druhé polovině 20. století. VĚTA O NEÚ PLNOSTI. Turingů v stroj (neformá lně). 120 Základní pojmy: Je-li konečná abeceda, značí symbol soubor všech konečných slov složených z prvků (prázdné slovo značíme symbolem ). Jazyk nad abecedou je podmnožina . 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. Turingů 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ě). 122 Definice 81. Turingů v stroj je devítice M = (Q, , , B, ˇ, , q0, Acc, Rej), kde Q je konečný soubor kontrolních stavů ; je konečná vstupní abeceda; je konečná pá sková abeceda (kde ); B je prá zdný znak; ˇ je znak konce pá sky; : Q × Q × × {L, R} je přechodová funkce, kde pro každé p Q platí (p, ˇ) = (q, ˇ, R) pro nějaké q Q; q0 Q je počá teční stav; Acc Q je množina akceptujících stavů ; Rej Q\Acc je množina zamítajících stavů . VĚTA O NEÚ PLNOSTI. Turingů v stroj (formá lně). 123 Konfigurace stroje M je konečná posloupnost symbolů tvaru ˇq, kde , a q Q. Akceptující resp. zamítající konfigurace je konfigurace tvaru ˇq kde q Acc resp. q Rej. 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 Conf M, která je pro koncové konfigurace definována jako identita a pro nekoncové konfigurace takto: step(XqY) = (XZr) jestliže (q, Y) = (r, Z, R) (rXZ) jestliže (q, Y) = (r, Z, L) step(Xq) = step(XqB) Slovo w je akceptované strojem M, jestliže existuje k N takové, že stepk (q0 ˇ w) je akceptující konfigurace. Jazyk akceptovaný strojem M, označovaný L(M), je soubor všech w , které jsou akceptované strojem M. VĚTA O NEÚ PLNOSTI. Turingů v stroj (formá lně). 124 Jazyk L je rekurzivně vyčíslitelný, jestliže L = L(M) pro nějaký Turingů v stroj M. Jazyk L je rekurzivní, jestliže L = L(M) pro nějaký Turingů v stroj M, který zastaví pro každé vstupní slovo. Jednoduché pozorování je, že jazyk L je rekurzivní právě když L i L jsou rekurzivně vyčíslitelné (kde L = \ 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) nad abecedou {0, 1}. Podobně každé vstupní slovo w stroje M lze jednoznačně zapsat jako slovo code(w) nad abecedou {0, 1}. Navíc mů žeme předpokládat, že každé slovo v {0, 1} je kódem nějakého Turingova 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 {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 bodu je 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ý. VĚTA O NEÚ PLNOSTI. Jazyk Accept. 125 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. Bud' 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 L(M ) právě když u#u L(M) Necht' v = code(M ). Platí wv L(M )? Ano. Pak v#v L(M), tj. Mv = M neakceptuje wv, spor. Ne. Pak v#v 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. VĚTA O NEÚ PLNOSTI. Peanova aritmetika. 126 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): x S(x) = 0 xy S(x)=S(y) x=y x x+0 = x xy x+S(y) = S(x+y) x x0 = 0 xy xS(y) = (xy) + x ((0) x ((x) (S(x)))) x (x), kde je formule s jednou volnou proměnnou x. VĚTA O NEÚ PLNOSTI. Peanova aritmetika. 127 Každou formuli jazyka aritmetiky je možné zapsat jako slovo nad abecedou {v, +, , 0, S, (, ), , , , =}. 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.) Systém všech formulí dokazatelných v Peanově aritmetice mů žeme chápat jako jazyk nad výše uvedenou abecedou. Označme tento jazyk Provable. Věta 83. Jazyk Provable je rekurzivně vyčíslitelný. Dů kaz věty 83 je technický, neopírá se ale o žádné hlubší pozorování. Příslušný Turingů v stroj jen systematicky generuje všechny možné dů kazy a akceptuje v případě, kdy nalezne dů kaz formule, která je zapsána jako vstupní slovo. Uvedený argument platí pro libovolnou ,,rozumnou" teorii. VĚTA O NEÚ PLNOSTI. Teorie Th(N0, , +). 128 Necht' Valid je jazyk nad abecedou {v, +, , 0, S, (, ), , , , =} obsahující zápisy všech formulí teorie Th(N0, , +). Naším cílem je dokázat, že Valid není rekurzivně vyčíslitelný jazyk, tj. Provable = Valid. Věta 84. 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í a to v takové konfiguraci, kdy je na pásce zápsáno slovo w nad abecedou {v, +, , 0, S, (, ), , , , =} takové, že v Accept právě když w 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. Teorie Th(N0, , +). 129 Stroj M nejprve ,,prověří" vstupní slovo: pokud není tvaru u#v, M smaže vstupní pásku a zapíše na ní (nějakou) nepravdivou formuli. Jinak M ,,nalezne" prvočíslo p, takové, že p > || (|Q| + 1), kde je pásková abeceda stroje Mu a Q soubor kontrolních stavů Mu. Pozorování: Jestliže zapisujeme čísla v soustavě o základu p, potřebuje p ,,číslic" [0], , [p-1]. Každé dvojici tvaru [X, q] a [X, -], kde X , q Q a - je nový symbol, lze tedy přiřadit jedinečnou ,,číslici". Dále nebudeme rozlišovat mezi symboly [X, q] (příp. [X, -]) a jim přiřazenými číslicemi. Každou konfiguraci stroje Mu pak lze přirozeně zapsat jako číslo v soustavě o základu p. Např. konfiguraci ˇXqYZBCC zapíšeme jako číslo [C, -] [C, -] [B, -] [Z, -] [Y, q] [X, -] [ˇ, -] Mu akceptuje slovo wv právě když existuje konečná posloupnost konfigurací 0, 1, , n s následujícími vlastnostmi: 0 je počáteční konfigurace q0 ˇ wv. i+1 = step(i) pro každé 0 i < n n je akceptující. VĚTA O NEÚ PLNOSTI. Teorie Th(N0, , +). 130 Bez ú jmy na obecnosti mů žeme předpokládat, že zápisy konfigurací 0, 1, , n mají stejnou délku, kterou označíme c. (Zápisy ,,krátkých" konfigurací lze totiž zprava doplnit ,,prázdným" znakem B; tím se předchozí podmínky neporuší, pouze zápis počáteční konfigurace mů že navíc obsahovat přidaná B.) Posloupnost konfigurací 0, 1, , n lze tedy opět zapsat jako číslo v soustavě o základu p. Zápis tohoto čísla vypadá takto: [n] [n-1] [0], kde [i] je zápis konfigurace i 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 soustavě o základu p 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 y ACOMP(y) a přejde do akceptujícího stavu. VĚTA O NEÚ PLNOSTI. Teorie Th(N0, , +). 131 Šestice ([a], [b], [c], [d], [e], [f]) symbolů p-ární soustavy je kompatibilní, jestliže existují konfigurace a stroje Mu takové, že a mají stejnou délku; = step(); existuje i takové, že v p-árním zápisu konfigurace (resp. ) se na místech i, i+1, i+2 vyskytují symboly [a], [b], [c] (resp. [d], [e], [f]). Necht' C je soubor všech kompatibilních šestic. Necht' [] a [ ] jsou zápisy konfigurací stroje Mu v p-ární soustavě, a necht' tyto zápisy mají stejnou délku c. Pak = step() právě když pro každé 1 i c - 2 platí, že trojice symbolů na pozicích i, i+1, i+2 v [] následovaná trojicí symbolů na pozicích i, i+1, i+2 v [ ] tvoří kompatibilní šestici. VĚTA O NEÚ PLNOSTI. Teorie Th(N0, , +). 132 Nyní sestrojíme několik formulí: ,,Číslo y je mocninou p." (Zde p je prvočíslo vypočtené výše.) POWERp(y) z((DIV(z, y) PRIME(z)) z=p) ,,V p-árním zápisu v se na logp(y)-tém místě zprava vyskutuje symbol [b]". (Za předpokladu, že y je mocnina p) DIGIT(v, y, b) u a (v=a+by+upy a