Matematická logika logika Aristotelova · 2015. 5. 31. · Matematická logika Antonín Kuceraˇ...

Matematickálogika

Antonín Kucera

Úvod

AristotelovalogikaLogický ctverec

Sylogismy

Booleovaalgebra logikyDva zákl. problémy

Rešení 1. problému


Výroková logikaSyntaxe

Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost

PredikátoválogikaSyntaxe

Sémantika

Odvozovací systém

Veta o úplnosti

Veta oneúplnostiTuringuv stroj

Dukaz vety oneúplnosti

Gödeluv dukaz

2. veta o neúplnosti

29. zárí 2009 1/147

Matematická logikaMateriály ke kurzu MA007

Poslední modifikace: 29. zárí 2009

Antonín Kucerahttp://www.fi.muni.cz/usr/kucera/teaching.html

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 2/147

Logika.

Buh

Lidské uvažování

Logika

Logika (z reckého λoγoς)zkoumá zpusob vyvozovánízáveru z predpokladu.

V bežné reci se ,,logikou‘‘oznacuje myšlenková cesta,která vedla k daným záverum.

Logika nezkoumá lidské myšlení(psychologie) ani obecné hranicelidského poznání (epistemologie).

,,Muže všemohoucí Buh stvoritkámen, který sám nedokážeuzvednout?‘‘

http://www.fi.muni.cz/usr/kucera/teaching.html

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 3/147

Logika. Neformální, formální, matematická.

Neformální logika studuje problematiku správné argumentacev prirozeném jazyce.

Formální logika definuje a studuje abstraktní odvozovací pravidla (tj.,,formy úsudku‘‘), jejichž platnost nezávisí na významu pojmu, kterév nich vystupují.

Pojmem matematická logika se obvykle myslí dve ruzné oblastivýzkumu:

aplikace poznatku z oblasti formální logiky na matematiku (napr.snaha ,,vnorit‘‘ matematiku do logiky ve forme konecného systémuaxiomu a odvozovacích pravidel);

aplikace matematických struktur a technik ve formální logice(napr. teorie modelu, teorie dukazu, apod.)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 4/147

Aristotelova logika.

Aristoteles (384-322 pr. Kr.)

Považován za zakladatele formálnílogiky.

Zavedl a prozkoumal pojemsylogismu.

Aristoteles zkoumal taképravdivostní módy a položil takzáklady modální logiky.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 5/147

Aristotelova logika. Logický ctverec.

I O

A ENecht’ S a P jsou neprázdnévlastnosti. Aristoteles rozlišujenásledující základní kategorickátvrzení:

A ,,všechna S jsou P‘‘

E ,,žádná S nejsou P‘‘

I ,,nekterá S jsou P‘‘

O ,,nekterá S nejsou P‘‘

Mnemonika: AffIrmo—nEgO(tvrdím—popírám)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 6/147

Aristotelova logika. Logický ctverec. (2)

I O

A E

A a O jsou kontradiktorická, tj. nemohou být soucasne pravdivá anisoucasne nepravdivá. I a E jsou rovnež kontradiktorická.

A a E jsou kontrární, tj. mohou být soucasne nepravdivá ale nesoucasne pravdivá.

I a O jsou subkontrární, tj. mohou být soucasne pravdivá ale nesoucasne nepravdivá.

I je subalterní (podrízené) A , tj. I je pravdivé jestliže A je pravdivé, asoucasne A je nepravdivé jestliže I je nepravdivé. Podobne O jesubalterní E.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 7/147

Aristotelova logika. Sylogismy.

Sylogismy jsou jednoduché úsudky tvaru

Hlavní premisaVedlejší premisa∴ Záver

Obe premisy i záver jsou kategorická tvrzení tvaru A , E, I, Oobsahující dohromady práve tri vlastnosti S, M, P, kde

hlavní premisa obsahuje P a M;vedlejší premisa obsahuje S a M;záver je tvaru S z P.

Lze tedy rozlišit následující ctyri formy sylogismu:

I: M x PS y M∴ S z P

II: P x MS y M∴ S z P

III: M x PM y S∴ S z P

IV: P x MM y S∴ S z P

Celkem tedy existuje 4 · 43 = 256 sylogismu.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 8/147

Aristotelova logika. Sylogismy. (2)

Jen 24 sylogismu je platných:

,,Barbara, Celarent, Darii, Ferioque priorisCesare, Camestres, Festino, Baroco secundaeTertia grande sonans recitat Darapti, FelaptonDisamis, Datisi, Bocardo, Ferison. QuartaeSunt Bamalip, Calames, Dimatis, Fesapo, Fresison.‘‘

Forma I: AAA, EAE, AII, EIO (Barbara, Celarent, Darii,Ferioque), AAI, EAO (subalterní módy);

Forma II: EAE, AEE, EIO, AOO, (Cesare, Camestres, Festino,Baroco), AEO, EAO (subalterní módy);

Forma III: AAI, EAO, IAI, AII, OAO, EIO (Darapti, Felapton,Disamis, Datisi, Bocardo, Ferison);

Forma IV: AAI, AEE, IAI, EAO, EIO (Bamalip, Calemes, Dimatis,Fesapo, Fresison), AEO (subalterní mód).

O (ne)platnosti sylogismu se lze snadno presvedcit pomocíVennových diagramu (John Venn, 1834–1923).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 9/147

Aristotelova logika. Platnost sylogismu.

S P

A(všechna S jsou P)

S P

E(žádná S nejsou P)

S P

I(nekterá S jsou P)

S P

O(nekterá S nejsou P)

šedé oblasti jsou prázdné;

symbol ,,•‘‘ oznacuje neprázdné oblasti;

bílé oblasti mohou být prázdné i neprázdné.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 10/147

Aristotelova logika. Platnost sylogismu. (2)

Uvažme nyní napr. 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 MNekterá S jsou M∴ Nekterá S nejsou P

S P

M

S P

M

Druhý diagram podává protipríklad, sylogismus platný není.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 11/147

Aristotelova logika. Platnost sylogismu. (3)

Rozeberme ješte AAI sylogismus tretí formy (Darapti):

Všechna M jsou PVšechna M jsou S∴ Nekterá S jsou P

?

S P

M

Tento sylogismus je v Aristotelove logice považován za platný. Je všaktreba použít predpoklad, že každá vlastnost je neprázdná. Tentopredpoklad ale prináší jisté problémy:

Všechny sklenené hory jsou sklenené.Všechny sklenené hory jsou hory.∴ Nekteré hory jsou sklenené.

Hlavní i vedlejší premisa jsou na intuitivní úrovni pravdivá tvrzení, závervšak nikoliv.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 12/147

Booleova ,,algebra logiky‘‘.

George Boole (1815–1864)

Aplikoval algebraické techniky priformalizaci procesu odvozování.Nalezl souvislost mezi algebrou asylogismy.

Booleova ,,algebra logiky‘‘ sechová podobne jako algebra císel.Násobení odpovídá logické spojce,,a soucasne‘‘, scítání logickéspojce ,,nebo‘‘, apod. (Odtudpocházejí pojmy ,,logický soucin‘‘ a,,logický soucet‘‘.).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 13/147

Algebra logiky. Motivacní príklad.

Uvažme následující sylogismus:

Všechna S jsou MŽádná M nejsou P∴ Žádná S nejsou P

Pokud vlastnosti identifikujeme se soubory objektu univerza, pro kteréplatí, mužeme uvedený sylogismus prepsat na

S ⊆ M

M ∩ P = 0

∴ S ∩ P = 0a dále na

S ∩M′ = 0 (1)

M ∩ P = 0 (2)

∴ S ∩ P = 0 (3)

Pokusme se nyní ,,odvodit‘‘ (3) z (1) a (2):

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 14/147

Algebra logiky. Motivacní príklad. (2)

Z toho, že S ∩M′ = 0 a 0 ∩ X = 0 pro libovolné X dostáváme

(S ∩M′) ∩ P = 0 (4)

Podobne 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) prepsat na

(S ∩ P) ∩ (M′ ∪M) = 0 (8)

Jelikož X ∪ X ′ = 1 a X ∩ 1 = X pro libovolné X , dostáváme z (8)

S ∩ P = 0

což bylo dokázat.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 15/147


V predchozím príkladu jsme k dokázání sylogismu použili symbolickoumanipulaci 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 ′ = 1X ∩ X = X X ∩ X ′ = 0X ∪ Y = Y ∪ X X ′′ = XX ∩ Y = Y ∩ X X ∪ 1 = 1

X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z X ∩ 1 = XX ∩ (Y ∩ Z) = (X ∩ Y) ∩ Z X ∪ 0 = XX ∩ (X ∪ Y) = X X ∩ 0 = 0X ∪ (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)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 16/147


Tyto identity definují algebraickou strukturu, které se pozdeji zacaloríkat Booleva algebra (prípadne Booleuv svaz).

V puvodní Booleove notaci se

místo X ∩ Y píše X .Y (prípadne 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í císelnou podobu a Boole sám sepokoušel prevést další císelné konstrukce (napr. delení, ale i Tayloruvrozvoj) do své ,,algebry logiky‘‘. Tyto úvahy však již byly zcela mylné.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 17/147

Algebra logiky. Dva základní problémy.

Podle Boolea je každý sylogismus možné zapsat ve tvaru

F1(P,M,A) = 0

F2(S ,M,B) = 0

∴ F(S ,P,C) = 0

kde F1(P,M,A), F2(S ,M,B), F(S ,P,C) jsou vhodné výrazyvytvorené ze symbolu 0, 1, ∪, ∩, ′ a symbolu v závorkách.

Symboly A , B, C plní roli ,,blíže neurcených vlastností‘‘ pri prepisukategorických tvrzení I a O . Napr. ,,nekterá S jsou P‘‘ Boole vyjádrilpomocí rovnosti S ∩ A = P ∩ A , tj. (S ∩ A) ∩ (P ∩ A)′ = 0, kde A jeblíže neurcená vlastnost. Tento postup není zcela korektní.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 18/147

Algebra logiky. Dva základní problémy. (2)

Boole uvážil obecnejší ú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í

zjistit, zda je daný úsudek pravdivý;

nalézt nejobecnejší záver (F) pro dané predpoklady (F1,. . . ,Fk ).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 19/147

Algebra logiky. Booleova metoda.

Definice 1

Necht’ ~A = A1, . . . ,An. ~A-konstituent je výraz tvaru `1 ∩ · · · ∩ `n, kde ì je bud’ Ainebo A ′i .

Veta 2

Pro každé F(X1, · · · ,Xn) platí

F(X1, · · · ,Xn) =⋃

~v∈{0,1}nF(~v) ∩ `1(~v) ∩ · · · ∩ `n(~v)

kde ì(~v) je bud’ Xi nebo X ′i podle toho, zda je ~vi rovno 1 nebo 0.

Prí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)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 20/147

Algebra logiky. Rešení 1. problému.

Veta 4

Úsudek

F1(A1, . . . ,Am,B1, . . . ,Bn) = 0

...

Fk (A1, . . . ,Am,B1, . . . ,Bn) = 0

∴ F(B1, . . . ,Bn) = 0

je platný, práve když každý ~A , ~B-konstituent výrazu F je~A , ~B-konstituentem nekterého Fi .

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 21/147

Algebra logiky. Rešení 1. problému. (2)

Príklad 5

Uvažme opet sylogismus

S ∩M′ = 0M ∩ P = 0

∴ S ∩ P = 0

Pak ~A = M a ~B = S ,P. Uvažme ~A , ~B-konstituenty jednotlivých výrazu:

S ∩M′ : M′ ∩ S ∩ P, M′ ∩ S ∩ P ′

M ∩ P : M ∩ S ∩ P, M ∩ S ′ ∩ P

S ∩ P : M ∩ S ∩ P, M′ ∩ S ∩ P

Podle vety 4 je tento úsudek pravdivý.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 22/147

Algebra logiky. Rešení 2. problému.

Necht’ ~A = A1, . . . ,Am, ~B = B1, . . . ,Bn. Uvažme predpoklady tvaru

F1(~A , ~B) = 0, · · · ,Fk (~A , ~B) = 0

Cílem je nalézt nejobecnejší záver tvaru F(~B) = 0. Oznacme

E(~A , ~B) = F1(~A , ~B) ∪ · · · ∪ Fk (~A , ~B)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 23/147

Algebra logiky. Rešení 2. problému. (2)

Veta 6

Nejobecnejší záver F(~B) = 0, který plyne z E(~A , ~B) = 0, je tvaru

F(~B) =⋂

~v∈{0,1}m

E(~v , ~B)

Príklad 7

Nejobecnejší záver F(S ,P) plynoucí z predpokladu S ∩M′ = 0 aM ∩ P = 0 je tvaru

F(S ,P) = ((S ∩ 0′) ∪ (0 ∩ P)) ∩ ((S ∩ 1′) ∪ (1 ∩ P))

= S ∩ P

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 24/147

Výstavba formálních logických systému.

Potrebujeme znát jisté pojmy a umet myslet (metaúroven).

Musí být napr. jasné, co myslíme symbolem, konecnouposloupností, atd.

Metapojmy a formální pojmy se bohužel casto ,,znací‘‘ stejne. Tímvzniká (nesprávný) dojem, že formální pojmy jsou definoványpomocí ,,sebe sama‘‘ (typickým príkladem je dukaz nebomnožina).

Co všechno si lze na metaúrovni dovolit? (potenciální vs. aktuálnínekonecno).

Základní kroky:

Vymezení užívaných symbolu (abeceda).

Syntaxe formulí.

Sémantika (zde se objeví pojem pravdivost).

Odvozovací systém (zde se objeví pojem dokazatelnost).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 25/147

Výroková logika. Syntaxe.

Definice 8

Abecedu výrokové logiky tvorí následující symboly:

znaky pro výrokové promenné A ,B ,C , . . . , kterých je spocetnemnoho;

logické spojky ∧, ∨,→, ¬

závorky ( a )

Definice 9

Formule výrokové logiky je slovo ϕ nad abecedou výrokové logiky, prokteré existuje vytvorující posloupnost, tj. konecná posloupnost slovψ1, · · · , ψk , kde k ≥ 1, ψk je ϕ, a pro každé 1 ≤ i ≤ k má slovo ψi jedenz následujících tvaru:

výroková promenná,

¬ψj pro nejaké 1 ≤ j < i,

(ψj ◦ ψj′) pro nejaká 1 ≤ j, j′ < i, kde ◦ je jeden ze symbolu ∧, ∨,→.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 26/147

Výroková logika. Syntaxe. (2)

Poznámka 10

V dalším textu budeme casto vynechávat v zápisech formulí vnejšízávorky. Napr. místo (A ∨ ¬B) budeme psát A ∨ ¬B. Po zavedenísémantiky výrokové logiky budeme casto vynechávat i další dvojicezávorek v prípade, kdy vzniklá syntaktická nejednoznacnost nepovedek sémantické nejednoznacnosti.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 27/147

Výroková logika. Sémantika.

Definice 11

Pravdivostní ohodnocení (valuace) je zobrazení v, které každé výrokovépromenné priradí hodnotu 0 nebo 1.

Metamatematickou indukcí k délce vytvorující posloupnosti lze každouvaluaci v jednoznacne rozšírit 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 soucasne v(ψ2) = 0;

1 jinak.

v(ψ1 → ψ2) =

0 jestliže v(ψ1) = 1 a soucasne v(ψ2) = 0;

1 jinak.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 28/147

Výroková logika. Sémantika. (2)

Definice 12

Výroková formule ϕ je

pravdivá (resp. nepravdivá) pri 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ždouvaluaci v.

Soubor T výrokových formulí je splnitelný, jestliže existuje valuace vtaková, že v(ϕ) = 1 pro každé ϕ z T.

Formule ϕ a ψ jsou ekvivalentní, psáno ϕ ≈ ψ, práve když pro každouvaluaci v platí, že v(ϕ) = v(ψ).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 29/147


Príklad 13

Formule A ∨ B je pravdivá pri valuaci v1, kde v1(A) = v1(B) = 1, anepravdivá pri valuaci v2, kde v2(A) = 0. Jde tedy o splnitelnouformuli, která není tautologií.

Pro každou formuli ϕ platí, že ϕ je tautologie práve když ¬ϕ nenísplnitelná.

Necht’ ϕ, ψ, ξ jsou výrokové formule. Pak:

ϕ ∧ ψ ≈ ψ ∧ ϕϕ ∧ (ψ ∧ ξ) ≈ (ϕ ∧ ψ) ∧ ξϕ ∧ (ψ ∨ ξ) ≈ (ϕ ∧ ψ) ∨ (ϕ ∧ ξ)¬(ϕ ∧ ψ) ≈ ¬ϕ ∨ ¬ψ¬¬ϕ ≈ ϕ

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 30/147


Poznámka 14

,,Identity‘‘ z posledního bodu príkladu 13 umožnují dále zprehlednit zápisformulí. Napr. místo (A ∨ B) ∨ C mužeme (nejednoznacne) psátA ∨ B ∨ C. Tato nejednoznacnost nevede k problémum, nebot’ príslušnédefinice a tvrzení ,,fungují‘‘ pro libovolné možné uzávorkování.

Poznámka 15

V teorii výpocetní 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 16

Formule ϕ je tautologickým dusledkem souboru formulí T, psáno T |= ϕ,jestliže v(ϕ) = 1 pro každou valuaci v takovou, že v(ψ) = 1 pro každouformuli ψ ze souboru T. Jestliže T |= ϕ pro prázdný soubor T, píšemekrátce |= ϕ.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 31/147

Výroková logika. Pravdivostní tabulky.

Nekdy se sémantika výrokových spojek definuje ,,predem‘‘ pomocípravdivostních tabulek:

X Y X ∧ Y0 0 00 1 01 0 01 1 1

X Y X ∨ Y0 0 00 1 11 0 11 1 1

X Y X → Y0 0 10 1 11 0 01 1 1

X ¬X0 11 0

Pojmy ,,pravdivostní tabulka‘‘ a ,,výroková spojka‘‘ je možné dále zobecnita uvážit formální logické systémy budované na obecnejším základu:

Definice 17

Výroková funkce je funkce F : {0,1}n → {0,1}, kde n ≥ 1.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 32/147

Výroková logika. Systém L(F1, · · · ,Fk ).

Definice 18

Necht’ F1, · · · ,Fk je konecný soubor výrokových funkcí. Definujemeformální logický systém L(F1, · · · ,Fk ), kde

Abeceda je tvorena znaky pro výrokové promenné, závorkami a znakyF1, · · · ,Fk pro uvedené výrokové funkce.

V definici vytvorující posloupnosti formule (viz definice 9) požadujeme,aby ψi bylo bud’ výrokovou promennou nebo tvaru Fj(ψj1 , · · · , ψjn ), kde1 ≤ j1, · · · , jn < i a n je arita Fj .

Valuace rozšíríme z výrokových promenných na formule predpisemv(F (ψ1, · · · , ψn)) = F(v(ψ1), · · · , v(ψn))

Poznámka 19

Ve smyslu definice 18 je dosud uvažovaný systém výrokové logikysystémem L(∧,∨,→,¬). Dríve zavedené sémantické pojmy (splnitelnost,pravdivost, atd.) se opírají pouze o pojem valuace a ,,fungují‘‘ tedyv libovolném systému L(F1, · · · ,Fk ).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 33/147

Výroková logika. Systém L(F1, · · · ,Fk ). (2)

Pro úcely následující definice zvolme libovolné (ale dále pevné) lineárníusporádání v na souboru všech výrokových promenných.

Definice 20

Necht’ ϕ je formule L(F1, · · · ,Fk ) a necht’ X1, · · · ,Xn je vzestupneusporádaná posloupnost (vzhledem k v) všech výrokových promenných,které se ve ϕ vyskytují. Formule ϕ jednoznacne urcuje výrokovou funkciFϕ : {0,1}n → {0,1} danou predpisem Fϕ(~u) = v~u(ϕ), kde v~u je valuacedefinovaná takto:

v~u(Xi) = ~u(i) pro každé 1 ≤ i ≤ n,

v~u(Y) = 0 pro ostatní Y.

Definice 21

Systém L(F1, · · · ,Fk ) je plnohodnotný, jestliže pro každou výrokovoufunkci F existuje formule ϕ systému L(F1, · · · ,Fk ) taková, že F = Fϕ.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 34/147

Výroková logika. Plnohodnotnost.

Veta 22

Systém L(∧,∨,¬) je plnohodnotný.

Dukaz. 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) ∧ · · · ∧ `n(ui)

kde `j(ui) je bud’ Xj nebo ¬Xj podle toho, zda ui(j) = 1 nebo ui(j) = 0.Nyní se lehce overí, že F = Fϕ. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 35/147

Výroková logika. Plnohodnotnost. (2)

Uvažme následující výrokové funkce:

X Y X f Y0 0 10 1 01 0 01 1 0

X Y X | Y0 0 10 1 11 0 11 1 0

X Y Z �(X ,Y ,Z)

0 0 0 10 0 1 00 1 0 10 1 1 01 0 0 11 0 1 01 1 0 01 1 1 0

Funkce f se nazývá Schröderuv operátor. Platí ϕ f ψ ≈ ¬(ϕ ∨ ψ).

Funkce | se nazývá Shefferuv operátor. Platí ϕ | ψ ≈ ¬(ϕ ∧ ψ).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 36/147

Výroková logika. Plnohodnotnost. (3)

Následující systémy výrokové logiky jsou plnohodnotné:

L(∧,∨,¬) Veta 22.

L(∧,¬) ϕ ∨ ψ ≈ ¬(¬ϕ ∧ ¬ψ)

L(∨,¬) ϕ ∧ ψ ≈ ¬(¬ϕ ∨ ¬ψ)

L(→,¬) ϕ ∨ ψ ≈ ¬ϕ→ ψ

L(f) ¬ϕ ≈ ϕ f ϕ, ϕ ∨ ψ ≈ (ϕ f ψ) f (ϕ f ψ)

L(|) ¬ϕ ≈ ϕ | ϕ, ϕ ∧ ψ ≈ (ϕ | ψ) | (ϕ | ψ)

L(�) ¬ϕ ≈ �(ϕ,ϕ, ϕ),ϕ→ ψ ≈ �(ϕ,�(ϕ,ϕ, ϕ),�(ϕ,ψ,�(ϕ,ϕ, ϕ)))

Následující systémy plnohodnotné nejsou:

L(∧), L(∨), L(→), L(¬), atd.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 37/147

Výroková logika. Shefferovské spojky.

Definice 23

Výroková funkce F je Shefferovská jestliže L(F) je plnohodnotný systém.

Veta 24

Necht’ S(n) znací pocet všech Shefferovských funkcí arity n ≥ 1. PakS(n) = 2(2n−1

−1)(2(2n−1−1)− 1). (Pro n = 1,2,3,4,5, . . . dostáváme

postupne 0,2,56,16256,1073709056, . . . )

Jelikož limn→∞S(n)

22n = 1/4, je (pro velká n) zhruba ctvrtina ze všechvýrokových funkcí arity n Shefferovská.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 38/147

Výroková logika. Shefferovské spojky. (2)

Poznámka 25

Výsledky o Shefferovských funkcích nalézají uplatnení pri výrobelogických obvodu; na ,,podkladové desce‘‘ se napr. vytvorí hustá sít’binárních |-hradel. Obvody ruzné funkce se pak realizují jejich vhodnýmpropojením.

Integrovaný obvod 4011 CMOS se ctyrmi |-hradly.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 39/147

Výroková logika. Normální formy.

Definice 26

Literál je formule tvaru X nebo ¬X, kde X je výroková promenná;

Klauzule je formule tvaru `1 ∨ · · · ∨ `n, kde n ≥ 1 a každé ì je literál.

Duální klauzule je formule tvaru `1 ∧ · · · ∧ `n, kde n ≥ 1 a každé ì jeliterál.

Formule v konjunktivním normálním tvaru (CNF) je formule tvaruC1 ∧ · · · ∧ Cm, kde m ≥ 1 a každé Ci je klauzule.

Formule v disjunktivním normálním tvaru je formule tvaruC1 ∨ · · · ∨ Cm, kde m ≥ 1 a každé Ci je duální klauzule.

Okamžitým dusledkem vety 22 je následující:

Veta 27

Pro každou formuli ϕ existuje ekvivalentní formule v disjunktivnímnormálním tvaru.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 40/147

Výroková logika. Normální formy. (2)

Veta 28

Pro každou formuli ϕ existuje ekvivalentní formule v konjunktivnímnormálním tvaru.

Dukaz. Podle Vety 27 existuje k ϕ ekvivalentní formule v disjunktivnímnormálním tvaru, tj. ϕ ≈

∨ni=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 soucasne v CNF.

Indukcní 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)

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 41/147

Výroková logika. Normální formy. (3)

Prí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í urcena jednoznacne až na poradí klauzulí a literálu.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 42/147

Výroková logika. Veta o kompaktnosti.

Veta 30 (o kompaktnosti)

Necht’ T je soubor formulí výrokové logiky. T je splnitelný práve kdyžkaždá konecná cást T je splnitelná.

Dukaz. Smer ,,⇒‘‘ je triviální. Dokážeme ,,⇐‘‘. Zavedeme pomocnýpojem: soubor V výrokových formulí je dobrý, jestliže každý konecnýpodsoubor V je splnitelný. Necht’ ψ1, ψ2, . . . je posloupnost všech formulívýrokové logiky. Metamatematickou indukcí definujeme pro každé i ≥ 1dobrý 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.

Alespon jeden ze souboru Si ∪ {ψi} a Si ∪ {¬ψi} musí být dobrý; jinakexistují konecné V1 ⊆ Si ∪ {ψi} a V2 ⊆ Si ∪ {¬ψi}, které nejsousplnitelné. Jestliže V1 ⊆ Si nebo V2 ⊆ Si , máme ihned spor s tím, žeSi je dobrý; jinak V1 ∪ V2 obsahuje ψi i ¬ψi , proto i(V1 ∪ V2) r {ψi ,¬ψi} ⊆ Si je nesplnitelný, spor.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 43/147

Výroková logika. Veta o kompaktnosti. (2)

Necht’ S =⋃∞

i=1 Si . Dokážeme, že S má následující vlastnosti:

S obsahuje ϕ práve když S neobsahuje ¬ϕ.S nutne obsahuje ϕ nebo ¬ϕ. Jestliže S obsahuje ϕ i ¬ϕ, existuje Si

obsahující ϕ i ¬ϕ; tedy {ϕ,¬ϕ} je nesplnitelný podsoubor Si , spor.

S obsahuje ϕ ∧ ψ práve když S obsahuje ϕ i ψ;

S obsahuje ϕ ∨ ψ práve když S obsahuje ϕ nebo ψ;

S obsahuje ϕ→ ψ práve když S neobsahuje ϕ nebo obsahuje ψ.

Bud’ v valuace definovaná takto: v(A) = 1 práve když A patrí do S.Indukcí k délce vytvorující posloupnosti se nyní snadno overí (s využitímvýše uvedených vlastností S), že:

S obsahuje ϕ práve když v(ϕ) = 1.

Tedy S (a proto i T ) je splnitelný. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 44/147


Užitím vety 30 lze snadno dokázat radu dalších tvrzení.

Graf G je dvojice (U,H), kde U je nejvýše spocetný soubor uzlu a H jeareflexivní 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 funkcef : U → {1, · · · , k } taková, že f(u) , f(v) pro každé (u, v) ∈ H.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 45/147


Veta 31

Graf G = (U,H) je k -obarvitelný práve když každý konecný podgraf G jek -obarvitelný.

Dukaz. Necht’ Bu,i je výroková promenná pro každý uzel u a každé1 ≤ i ≤ k . Bud’ T soubor tvorený 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áve když soubor T je splnitelný.

Každý konecný podgraf G je k -obarvitelný práve když každý konecnýpodsoubor T je splnitelný.

Nyní stací aplikovat vetu 30. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 46/147

Výroková logika. Systém L(→,¬).

V této cásti se soustredíme na L(→,¬). Uvažme následující odvozovacísystém pro L(→,¬) (Lukasiewicz, 1928):Schémata axiómu:

A1: ϕ→ (ψ→ ϕ)

A2: (ϕ→ (ψ→ ξ))→ ((ϕ→ ψ)→ (ϕ→ ξ))

A3: (¬ϕ→ ¬ψ)→ (ψ→ ϕ)

Odvozovací pravidlo:

MP: Z ϕ a ϕ→ ψ odvod’ ψ. (modus ponens)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 47/147

Výroková logika. Systém L(→,¬). (2)

Definice 32

Bud’ T soubor formulí.

Dukaz formule ψ z predpokladu T je konecná posloupnost formulíϕ1, · · · , ϕk , kde ϕk je ψ a pro každé ϕi , kde 1 ≤ i ≤ k , platí alesponjedna 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 predpokladu T, psáno T ` ψ, jestližeexistuje dukaz ψ z predpokladu T. Jestliže T ` ψ pro prázdné T,ríkáme že ψ je dokazatelná a píšeme ` ψ.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 48/147


Príklad 33

Pro libovolnou formuli ϕ platí ` ϕ→ ϕ.

Dukaz. Následující posloupnost formulí je dukazem ϕ→ ϕ.

1) (ϕ→ ((ϕ→ ϕ)→ ϕ))→ ((ϕ→ (ϕ→ ϕ))→ (ϕ→ ϕ)) A22) ϕ→ ((ϕ→ ϕ)→ ϕ) A13) (ϕ→ (ϕ→ ϕ))→ (ϕ→ ϕ) MP na 2),1)4) ϕ→ (ϕ→ ϕ) A15) ϕ→ ϕ MP na 4),3)

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 49/147


Príklad 34

Pro libovolné formule ϕ, ψ platí {ϕ,¬ϕ} ` ψ.

Dukaz. Následující posloupnost formulí je dukazem ψ z {ϕ,¬ϕ}:

1) ¬ϕ→ (¬ψ→ ¬ϕ) A12) ¬ϕ predpoklad3) ¬ψ→ ¬ϕ MP na 2),1)4) (¬ψ→ ¬ϕ)→ (ϕ→ ψ) A35) ϕ→ ψ MP na 3),4)6) ϕ predpoklad7) ψ MP na 6),5)

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 50/147

Výroková logika. Veta o dedukci.

Veta 35 (o dedukci)

Necht’ ϕ, ψ jsou formule a T soubor formulí. Pak T ∪ {ψ} ` ϕ práve kdyžT ` ψ→ ϕ.

Dukaz.,,⇐‘‘: Necht’ ξ1, · · · , ξk je dukaz formule ψ→ ϕ z predpokladu T . Pakξ1, · · · , ξk , ψ, ϕ je dukaz formule ϕ z predpokladu T ∪ {ψ} (posledníformule vznikne aplikací MP na ψ a ξk ).,,⇒‘‘: Necht’ ξ1, · · · , ξk je dukaz ϕ z predpokladu T ∪ {ψ}. Metaindukcí k jdokáž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 dukazu ξ1 z T nyní pripojíme formule ξ1 → (ψ→ ξ1), ψ→ ξ1. Prvníformule je instancí A1, druhá aplikací MP na ξ1 a první formuli. Mámetedy dukaz ψ→ ξ1 z T .Je-li ξ1 formule ψ, platí T ` ψ→ ψ podle príkladu 33.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 51/147

Výroková logika. Veta o dedukci. (2)

Indukcní krok: Je-li formule ξj instancí axiómu nebo prvek T ∪ {ψ},postupujeme stejne 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).Dukazy ψ→ ξm a ψ→ (ξm → ξj) z T nyní zretezíme za sebe apripojíme následující formule:

(ψ→ (ξm → ξj))→ ((ψ→ ξm)→ (ψ→ ξj))

(ψ→ ξm)→ (ψ→ ξj)

ψ→ ξj

První formule je instancí A2, další dve vzniknou aplikací MP. Mámetedy dukaz formule ψ→ ξj z T .

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 52/147

Výroková logika. Veta o korektnosti.

Veta 36 (o korektnosti)

Necht’ ϕ je formule a T soubor formulí. Jestliže T ` ϕ, pak T |= ϕ.

Dukaz. Necht’ ξ1, · · · , ξk je dukaz ϕ z T . Indukcí vzhledem k jdokážeme, že T |= ξj pro každé 1 ≤ j ≤ k . (Stací overit, že každáinstance A1–A3 je tautologie, a že jestliže T |= ψ a T |= ψ→ ξ, pak takéT |= ξ). �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 53/147

Výroková logika. Veta o úplnosti.

Lema 37

Necht’ ϕ, ψ jsou formule. Pak

(a) ` ¬ϕ→ (ϕ→ ψ)

(b) ` ¬¬ϕ→ ϕ

(c) ` ϕ→ ¬¬ϕ

(d) ` (ϕ→ ψ)→ (¬ψ→ ¬ϕ)

(e) ` ϕ→ (¬ψ→ ¬(ϕ→ ψ))

(f) ` (ϕ→ ψ)→ ((¬ϕ→ ψ)→ ψ)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 54/147

Výroková logika. Veta o úplnosti. (2)

Dukaz.

(a): Podle príkladu 34 platí {ϕ,¬ϕ} ` ψ, proto ` ¬ϕ→ (ϕ→ ψ)opakovaným užitím vety o dedukci.

(b): Platí

1) ` ¬¬ϕ→ (¬ϕ→ ¬¬¬ϕ) podle (a)2) {¬¬ϕ} ` ¬ϕ→ ¬¬¬ϕ veta o dedukci3) ` (¬ϕ→ ¬¬¬ϕ)→ (¬¬ϕ→ ϕ) A34) {¬¬ϕ} ` ¬¬ϕ→ ϕ MP na 2),3)5) {¬¬ϕ} ` ϕ veta o dedukci6) ` ¬¬ϕ→ ϕ veta o dedukci

(c): Platí

1) ` ¬¬¬ϕ→ ¬ϕ podle (b)2) ` (¬¬¬ϕ→ ¬ϕ)→ (ϕ→ ¬¬ϕ) A33) ` ϕ→ ¬¬ϕ MP na 1),2)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 55/147


(d): Platí

1) {ϕ→ ψ} ` ϕ→ ψ2) {¬¬ϕ} ` ϕ podle (b) a vety o dedukci3) {ϕ→ ψ,¬¬ϕ} ` ψ MP na 2),1)4) ` ψ→ ¬¬ψ podle (c)5) {ϕ→ ψ,¬¬ϕ} ` ¬¬ψ MP na 3),4)6) {ϕ→ ψ} ` ¬¬ϕ→ ¬¬ψ veta o dedukci7) ` (¬¬ϕ→ ¬¬ψ)→ (¬ψ→ ¬ϕ) A38) {ϕ→ ψ} ` ¬ψ→ ¬ϕ MP na 6),7)9) ` (ϕ→ ψ)→ (¬ψ→ ¬ϕ) veta o dedukci

(e): Platí

1) {ϕ,ϕ→ ψ} ` ψ2) {ϕ} ` (ϕ→ ψ)→ ψ veta o dedukci3) ` ((ϕ→ ψ)→ ψ)→ (¬ψ→ ¬(ϕ→ ψ)) podle (d)4) {ϕ} ` ¬ψ→ ¬(ϕ→ ψ) MP na 2),3)5) ` ϕ→ (¬ψ→ ¬(ϕ→ ψ)) veta o dedukci

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 56/147


(f): Platí

1) ` (ϕ→ ψ)→ (¬ψ→ ¬ϕ)) podle (d)2) {ϕ→ ψ,¬ψ} ` ¬ϕ 2x MP na 1)3) {ϕ→ ψ,¬ψ,¬ϕ→ ψ} ` ψ MP na 2),¬ϕ→ ψ4) {ϕ→ ψ,¬ϕ→ ψ} ` ¬ψ→ ψ veta o dedukci5) ` ¬ψ→ (¬ψ→ ¬(¬ψ→ ψ)) podle (e)6) {¬ψ} ` ¬(¬ψ→ ψ) 2x veta o dedukci7) ` ¬ψ→ ¬(¬ψ→ ψ) veta o dedukci8) ` (¬ψ→ ¬(¬ψ→ ψ))→ ((¬ψ→ ψ)→ ψ) A39) ` (¬ψ→ ψ)→ ψ MP na 7),8)

10) {ϕ→ ψ,¬ϕ→ ψ} ` ψ MP na 4),9)11) ` (ϕ→ ψ)→ ((¬ϕ→ ψ)→ ψ) 2x veta o dedukci

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 57/147


Definice 38

Necht’ v je valuace a ϕ formule. Jestliže v(ϕ) = 1, oznacuje symbol ϕv

formuli ϕ. Jinak ϕv oznacuje formuli ¬ϕ.

Lema 39 (A. Church)

Necht’ v je valuace, ϕ formule, a {X1, · · · ,Xk } konecný soubor výrokovýchpromenných, kde všechny promenné vyskytující se ve ϕ jsou mezi{X1, · · · ,Xk }. Pak {X v

1 , · · · ,Xvk } ` ϕ

v .

Dukaz. Indukcí k délce vytvorující posloupnosti pro ϕ.

Je-li ϕ = X , pak X je mezi {X1, · · · ,Xk } a tedy {X v1 , · · · ,X

vk } ` X v .

Je-li ϕ = ¬ψ, kde {X v1 , · · · ,X

vk } ` ψ

v , rozlišíme dve možnosti:

v(ψ) = 0. Pak ψv = ¬ψ a ϕv = ¬ψ, není co dokazovat.

v(ψ) = 1. Pak ψv = ψ a ϕv = ¬¬ψ. Podle lematu 37 (c) platí` ψ→ ¬¬ψ, proto {X v

1 , · · · ,Xvk } ` ¬¬ψ užitím MP.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 58/147


Je-li ϕ = ψ→ ξ, kde {X v1 , · · · ,X

vk } ` ψ

v a {X v1 , · · · ,X

vk } ` ξ

v rozlišímenásledující možnosti:

v(ψ→ ξ) = 1. Máme tedy dokázat, že {X v1 , · · · ,X

vk } ` ψ→ ξ.

Jestliže v(ψ) = 0, platí {X v1 , · · · ,X

vk } ` ¬ψ. Podle lematu 37 (a)

dále platí ` ¬ψ→ (ψ→ ξ), proto {X v1 , · · · ,X

vk } ` ψ→ ξ užitím MP.

Jestliže v(ξ) = 1, platí {X v1 , · · · ,X

vk } ` ξ. Podle A1 platí

` ξ→ (ψ→ ξ), proto {X v1 , · · · ,X

vk } ` ψ→ ξ užitím MP.

v(ψ→ ξ) = 0. Pak {X v1 , · · · ,X

vk } ` ψ a {X v

1 , · · · ,Xvk } ` ¬ξ. Máme

dokázat, že {X v1 , · · · ,X

vk } ` ¬(ψ→ ξ). Podle lematu 37 (e) platí

` ψ→ (¬ξ→ ¬(ψ→ ξ)), proto {X v1 , · · · ,X

vk } ` ¬(ψ→ ξ)

opakovaným užitím MP.�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 59/147


Veta 40 (o úplnosti)

Necht’ ϕ je formule a T soubor formulí. Jestliže T |= ϕ, pak T ` ϕ.

Dukaz. Nejprve uvážíme prípad, kdy T je prázdný soubor. Necht’ ϕ jetautologie a X1, · · · ,Xk všechny výrokové promenné, které se ve ϕvyskytují.

Podle Churchova lematu platí {X v1 , · · · ,X

vk } ` ϕ pro libovolné v.

Ukážeme, že všechny X vi lze postupne ,,eliminovat‘‘, až dostaneme

dukaz ϕ z prázdného souboru formulí.

Predpokládejme, že pro dané 0 ≤ n < k jsme již prokázali, že

{X v1 , · · · ,X

vn ,X

vn+1} ` ϕ

pro libovolné v. Dokážeme, že pak také {Xu1 , · · · ,X

un } ` ϕ pro libovolné u.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 60/147


Bud’ tedy u libovolná valuace. Necht’ u1, u2 jsou valuace definovanétakto:

u1(Xn+1) = 1, u2(Xn+1) = 0

pro každé Y , Xn+1 platí u1(Y) = u2(Y) = u(Y).

Platí

1) {Xu1 , · · · ,X

un ,Xn+1} ` ϕ predpoklad pro v = u1

2) {Xu1 , · · · ,X

un ,¬Xn+1} ` ϕ predpoklad pro v = u2

3) {Xu1 , · · · ,X

un } ` Xn+1 → ϕ veta o dedukci na 1)

4) {Xu1 , · · · ,X

un } ` ¬Xn+1 → ϕ veta o dedukci na 2)

5) ` (Xn+1 → ϕ)→ ((¬Xn+1 → ϕ)→ ϕ) podle lematu 37 (f)6) {Xu

1 , · · · ,Xun } ` ϕ 2x MP na 5) s využitím 3),4)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 61/147


Nyní uvážíme obecný prípad. Bud’ T libovolný soubor formulí a ϕ formuletaková, že T |= ϕ. Podle vety o kompaktnosti existuje konecný soubor{ψ1, · · · , ψn} formulí z T takový, že {ψ1, · · · , ψn} |= ϕ. Lehce se overí, že

|= ψ1 → (ψ2 → (ψ3 → · · · (ψn → ϕ) · · · )

Podle predchozího bodu tedy platí

` ψ1 → (ψ2 → (ψ3 → · · · (ψn → ϕ) · · · )

Po n aplikacích vety o dedukci dostáváme {ψ1, · · · , ψn} ` ϕ, tedy takéT ` ϕ. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 62/147

Výroková logika. Historické poznámky.

Výroková logika nebyla rozvíjena samostatne, ale jako soucástsložitejších formálních systému.

Gottlob Frege (1848–1925) položil základy predikátové logiky a zavedl,,moderní‘‘ odvozovací systém. ,,Výrokový fragment‘‘ tohoto systémuvypadá 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 vedeckou komunitou ignorovány zhruba 20 let.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 63/147

Výroková logika. Historické poznámky. (2)

Giuseppe Peano (1858-1932) doporucil na mezinárodnímmatematickém kongresu v Paríži (rok 1900) mladému BertranduRussellovi (1872-1970) studovat Fregeho práce. Russell v roce 1901objevil inkonzistenci ve Fregeho systému (Russelluv paradox),soucasne plne docenil Fregeho myšlenky. V letech 1910-1913 bylapublikována trídílná Principia Mathematica (autori Whitehead,Russell). Tato monografie mela hluboký vliv na vývoj logiky vnásledujících desetiletích. Venována byla Fregemu. Pro fragmentvý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))


Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 64/147


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))


Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 65/147


Ve stejném roce publikoval Henry Sheffer následující axiomatickýsystém založený na Shefferove 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‘‘

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))


V roce 1927 navrhl John von Neumann (1903-1957) aplikovatsubstituci pouze na axiómy. Vznikly systémy založené na schématechaxiómu.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 66/147


Jan Lukasiewicz (1878–1956) prezentoval svuj odvozovací systém(použitý v prednášce) v roce 1928.

Další odvozovací systémy:

V roce 1947 zjednodušili Götling a Rasiowa systém z PrincipiaMathematica do následující podoby:

1: (P ∨ P)→ P

2: P → (P ∨Q)

3: (Q → R)→ ((P ∨Q)→ (P ∨ R))


V roce 1953 prezentoval Meredith systém s jediným schématem ajediným odvozovacím pravidlem:

Schéma axiómu: ((((ϕ→ ψ)→ (¬%→ ¬ξ))→ %)→ γ)→((γ→ ϕ)→ (ξ→ ϕ))

Odvozovací pravidlo: MP

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 67/147

Predikátová logika. Vznik a vývoj.

Predikátová logika (také logika prvního rádu) se opírá o pojemvlastnosti (tj. predikátu). Umožnuje formulovat tvrzení o vlastnostechobjektu s využitím kvantifikátoru.

Napr. Aristotelova logika je z dnešního pohledu fragmentempredikátové logiky.

Formule prvního rádu byly soucástí Fregeho systému, pozdeji seobjevily ve 3. dílu Schröderovy monografie Algebra der Logik (1910) amonografii Principia Mathematica (Whitehead, Russel).

Logika prvního rádu byla definována jako samostatný systém ažv monografii Hilberta a Ackermanna Grundzügen der theoretischenLogik (1928).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 68/147

Predikátová logika. Syntaxe.

Definice 41

Jazyk (stejne jako jazyk s rovností) je systém predikátových symbolu afunkcních symbolu, kde u každého symbolu je dána jeho cetnost (arita),která je nezáporným celým císlem.

Poznámka 42

Predikáty arity nula v jistém smyslu odpovídají výrokovýmpromenným, funkcní symboly arity nula jsou symboly pro konstanty.

Predikátovým a funkcním symbolum se také ríká mimologickésymboly. Jazyk je tedy plne urcen mimologickými symboly.

Rozdíl mezi jazykem a jazykem s rovností se projeví v tom, že dopredikátové logiky pro jazyk s rovností prídáme speciální logickýsymbol = jehož sémantika bude definována speciálním zpusobem.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 69/147

Predikátová logika. Syntaxe. (2)

Príklad 43

Jazyk teorie množin je jazykem s rovností, který obsahuje jedenpredikátový symbol ∈ arity 2.

Jazyk teorie pologrup je jazykem s rovností, který obsahuje jedenfunkcní symbol ,,·‘‘ arity 2.

Definice 44

Abecedu predikátové logiky pro jazyk L tvorí následující symboly:

Znaky pro promenné x , y , z, . . . , kterých je spocetne mnoho

Mimologické symboly, tj. predikátové a funkcní symboly jazyka L.

Je-li L jazyk s rovností, obsahuje abeceda speciální znak = prorovnost.

Logické spojky→ a ¬.

Symbol ∀ pro univerzální kvantifikátor.

Závorky ( a ).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 70/147


Definice 45

Termem jazyka L je slovo t nad abecedou predikátové logiky pro jazykL, pro které existuje vytvorující posloupnost slov t1, · · · , tk , kde k ≥ 1, tkje t , a pro každé 1 ≤ i ≤ k má slovo ti jeden z následujících tvaru:

promenná,

f(ti1 , · · · , tin ), kde 1 ≤ i1, · · · , in < k , f je funkcní symbol jazyka L, a n jearita f .

Term je uzavrený, jestliže neobsahuje promenné.

Poznámka 46

U binárních funkcních symbolu (a pozdeji také predikátu) dovolíme provetší citelnost infixový zápis. U funkcních (a predikátových) symbolu aritynula budeme psát c místo c().

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 71/147


Prí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 porade funkcní symboly arity nula, jedna a dva.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 72/147


Definice 48

Formule predikátového poctu jazyka L je slovo ϕ nad abecedoupredikátové logiky pro jazyk L, pro které existuje vytvorující posloupnostslov ψ1, · · · , ψk , kde k ≥ 1, ψk je ϕ, a pro každé 1 ≤ i ≤ k má slovo ψi

jeden z následujících tvaru:

P(t1, · · · , tn), kde P je predikátový symbol jazyka L arity n a t1, · · · , tnjsou termy jazyka L.

t1 = t2, je-li L jazyk s rovností a t1, t2 jsou termy jazyka L.

¬ψj pro nejaké 1 ≤ j < i,

(ψj → ψj′) pro nejaká 1 ≤ j, j′ < i,

∀x ψj , kde x je promenná a 1 ≤ j < i.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 73/147


Poznámka 49

Ve zbytku prednášky budeme používat následující ,,zkratky‘‘:

∃x ϕ znací ¬∀x ¬ϕ

ϕ ∨ ψ znací ¬ϕ→ ψ

ϕ ∧ ψ znací ¬(ϕ→ ¬ψ).

ϕ↔ ψ znací (ϕ→ ψ) ∧ (ψ→ ϕ), kde symbol ∧ dále ,,rozvineme‘‘podle predchozího bodu.

Príklady formulí:

∀x P(x , y) ∧ ∃x (P(x , x) ∨Q(c))

∀x ∃x (P(x , x) ∨ ∀y ∀x Q(x))

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 74/147


Definice 50

Každý výskyt promenné ve formuli predikátového poctu je bud’ volnýnebo vázaný podle následujícího induktivního predpisu:

Ve formuli tvaru P(t1, · · · , tn) jsou všechny výskyty promenných volné.

Výrokové spojky nemení charakter výskytu promenných, tj. je-li danývýskyt promenné ve formuli ψ volný (resp. vázaný), je odpovídajícívýskyt ve formulích ¬ψ, ϕ→ ψ, ψ→ ϕ rovnež volný (resp. vázaný).

Ve formuli ∀x ψ je každý výskyt promenné x (vcetne výskytu zakvantifikátorem) vázaný; byl-li výskyt promenné ruzné od x volný(resp. vázaný) ve formuli ψ, je odpovídající výskyt ve formuli ∀x ψrovnež volný (resp. vázaný).

Príklady (volné výskyty jsou cervené):

∀x P(x , y) ∨ ∀y P(x , y)

∀x (P(x , y) ∨ ∀y P(x , y))

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 75/147


Definice 51

Promenná se nazývá volnou (resp. vázanou) ve formuli, má-li v nívolný (resp. vázaný) výskyt.

Formule je otevrená, jestliže v ní žádná promenná nemá vázanývýskyt.

Formule je uzavrená (také sentence), jestliže v ní žádná promennánemá volný výskyt.

Zápis ϕ(x1, · · · , xn) znací, že všechny volné promenné ve formuli ϕjsou mezi x1, · · · , xn (nemusí nutne platit, že každá z techtopromenných je volná ve ϕ).

Univerzální uzáver formule ϕ je formule tvaru ∀ x1 · · · ∀ xn ϕ, kdex1, · · · , xn jsou práve všechny volné promenné formule ϕ.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 76/147

Predikátová logika. Substituce.

Definice 52

Term t je substituovatelný za promennou x ve formuli ϕ, jestliže žádnývýskyt promenné v termu t se nestane vázaným po provedení substitucetermu t za každý volný výskyt promenné x ve formuli ϕ. Je-li tsubstituovatelný za x ve ϕ, znací zápis ϕ(x/t) formuli, která vzniknenahrazením každého volného výskytu x ve ϕ termem t.

Prí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)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 77/147

Predikátová logika. Substituce. (2)

Definice 53

Necht’ ϕ je formule a t1, · · · , tn termy, které jsou v uvedeném poradísubstituovatelné za promenné x1, · · · , xn ve ϕ (predpokládáme, žex1, · · · , xn jsou ruzné). Symbol ϕ(x1/t1, · · · , xn/tn) znací formuli, kterávznikne ,,simultánním nahrazením‘‘ každého volného výskytu xi termem tipro každé 1 ≤ i ≤ n. Presneji, ϕ(x1/t1, · · · , xn/tn) je formuleϕ(x1/z1) · · · (xn/zn)(z1/t1) · · · (zn/tn), kde z1, · · · , zn jsou (ruzné)promenné, které se nevyskytují v t1, · · · , tn ani mezi x1, · · · , xn.

Príklad:

P(x , y)(x/y , y/x) je formule P(y , x)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 78/147

Predikátová logika. Realizace jazyka.

Definice 54

RealizaceM jazyka L je zadána

neprázdným souborem M, nazývaným univerzem (prípadne nosicem).Prvky univerza nazýváme individui.

prirazením, které každému n-árnímu predikátovému symbolu P priradín-ární relaci PM na M

prirazením, které každému m-árnímu funkcnímu symbolu priradífunkci fM : Mm

→ M.

Ohodnocení je zobrazení prirazující promenným prvky univerza M.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 79/147

Predikátová logika. Realizace jazyka. (2)

Definice 55

Realizaci termu t pri ohodnocení e v relizaciM, psáno tM[e] (prípadnejen t [e] je-liM jasné z kontextu), definujeme induktivne takto:

x[e] = e(x)

f(t1, · · · , tm)[e] = fM(t1[e], · · · , tm[e])(pro m = 0 je na pravé strane uvedené definující rovnosti fM(∅)).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 80/147


Definice 56 (A. Tarski)

Bud’M realizace L, e ohodnocení a ϕ formule predikátového poctujazyka L. Ternární vztahM |= ϕ[e] definujeme indukcí ke strukture ϕ:

M |= P(t1, · · · , tm)[e] práve když (t1[e], · · · , tm[e]) ∈ PM.

Jestliže L je jazyk s rovností, definujemeM |= (t1 = t2)[e] práve kdyžt1[e] a t2[e] jsou stejná individua.

M |= ¬ψ[e] práve když neníM |= ψ[e].

M |= (ψ→ ξ)[e] práve kdyžM |= ξ[e] nebo neníM |= ψ[e].

M |= ∀x ψ[e] práve kdyžM |= ψ[e(x/a)] pro každý prvek auniverza M.

JestližeM |= ϕ[e], ríkáme, že ϕ je pravdivá vM pri ohodnocení e.JestližeM |= ϕ[e] pro každé e, je ϕ pravdivá vM, psánoM |= ϕ.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 81/147


Príklad 57

Bud’ L jazyk s jedním unárním predikátem P aM jeho realizace naduniverzem 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))

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 82/147

Predikátová logika. Teorie.

Definice 58

Bud’ L jazyk (príp. jazyk s rovností).

Teorie (s jazykem L) je soubor T formulí predikátového poctujazyka L. Prvky T se nazývají axiómy teorie T.

RealizaceM jazyka L je model teorie T, psánoM |= T, jestližeM |= ϕ pro každé ϕ z T.

Teorie je splnitelná, jestliže má model.

Je-liM realizace jazyka L, pak Th(M) oznacuje teorii tvorenou právevšemi uzavrenými formulemi, které jsou vM pravdivé.

Formule ϕ je sémantickým dusledkem teorie T, psáno T |= ϕ, jestližeϕ je pravdivá v každém modelu teorie T.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 83/147

Predikátová logika. Teorie. (2)

Príklad 59

Uvažme jazyk s rovností obsahující jeden binární funkcní symbol “·” ajednu konstantu 1. Necht’ T je tvorena 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 dusledkem T ,zatímco formule x · (1 · y) = (1 · x) · y ano.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 84/147

Predikátová logika. Odvozovací systém.

Schémata výrokových axiómu:

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)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 85/147

Predikátová logika. Odvozovací systém. (2)

Je-li L jazyk s rovností, prí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 funkcní symbol arity m.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 86/147


Definice 60

Bud’ T teorie jazyka L. Dukaz formule ψ v teorii T je konecnáposloupnost formulí ϕ1, · · · , ϕk , kde ϕk je ψ a pro každé ϕi , kde1 ≤ i ≤ k , platí alespon 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í MP na formule ϕm, ϕn pro vhodné 1 ≤ m,n < i.

ϕi vznikne aplikací GEN na formuli ϕm pro vhodné 1 ≤ m < i.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 87/147


Definice 61

Bud’ T teorie jazyka L.

Formule ψ je dokazatelná v teorii T, psáno T ` ψ, jestliže existujedukaz ψ v T. Jestliže T ` ψ pro prázdné T, ríkáme že ψ jedokazatelná a píšeme ` ψ.

Formule ψ je vyvratitelná v teorii T, jestliže T ` ¬ψ

Teorie T je sporná (též inkonzistentní), jestliže každá formulepredikátové logiky jazyka L je v T dokazatelná.

Teorie je bezesporná (též konzistentní), jestliže není nekonzistentní.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 88/147

Predikátová logika. Dukazy.

Poznámka 62 (Princip dosazení do tautologie výrokového poctu)

Je-li ϕ tautologií L(¬,→), ve které nahradíme výrokové promennéformulemi predikátové logiky tak, že daná výroková promenná jenahrazena 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 63 (Neplatnost ,,obecné‘‘ vety o dedukci)

Za predpokladu korektnosti odvozovacího systému pro predikátovoulogiku neplatí ` ϕ→ ∀x ϕ. Platí ovšem {ϕ} ` ∀x ϕ. Proto obecne neplatí,že T |= ϕ→ ψ práve když T ∪ {ϕ} |= ψ.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 89/147

Predikátová logika. Veta o dedukci.

Veta 64 (o dedukci)

Necht’ T je teorie jazyka L, ψ uzavrená formule jazyka L a ϕ (libovolná)formule jazyka L. Pak T ` ψ→ ϕ práve když T ∪ {ψ} ` ϕ.

Dukaz. Dukaz je velmi podobný dukazu vety 35:,,⇒‘‘: Necht’ ξ1, · · · , ξk je dukaz formule ψ→ ϕ v T . Pak ξ1, · · · , ξk , ψ, ϕ jedukaz ϕ v T ∪ {ψ} (poslední formule vznikne aplikací MP na ψ a ξk ).,,⇐‘‘: Necht’ ξ1, · · · , ξk je dukaz ϕ 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 dukazu ξ1 z T nyní pripojíme formule ξ1 → (ψ→ ξ1), ψ→ ξ1. Prvníformule je instancí P1, druhá aplikací MP na ξ1 a první formuli. Mámetedy dukaz ψ→ ξ1 v T . Je-li ξ1 formule ψ, platí T ` ψ→ ψ podlepríkladu 33 a poznámky 62.

Indukcní krok: Je-li formule ξj instancí axiómu nebo prvek T ∪ {ψ},postupujeme stejne jako výše (místo ξ1 použijeme ξj).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 90/147

Predikátová logika. Veta o dedukci. (2)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 aT ` ψ→ (ξm → ξj). Dukazy ψ→ ξm a ψ→ (ξm → ξj) v T nynízretezíme za sebe a pripojíme následující formule:

(ψ→ (ξm → ξj))→ ((ψ→ ξm)→ (ψ→ ξj))

(ψ→ ξm)→ (ψ→ ξj)

ψ→ ξj

První formule je instancí P2, další dve vzniknou aplikací MP.Máme tedy dukaz formule ψ→ ξj v T .

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 dukazu nyní stacípripojit formule

∀x (ψ→ ξm)

∀x (ψ→ ξm)→ (ψ→ ∀x ξm)

ψ→ ∀x ξm.

První vznikne aplikací GEN, druhá je instancí P5, tretí vznikneaplikací MP. Dostaneme tak dukaz formule ψ→ ξj v T . �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 91/147

Predikátová logika. Kvantifikace.

Lema 65

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 ψ.

Dukaz. Pozorování:

(a) Jestliže ` ϕ→ ψ a soucasne ` ψ→ ϕ, pak ` ϕ↔ ψ. To plyne z toho,že (A → B)→ ((B → A)→ (A ↔ B)) je výroková tautologie (vizpoznámka 62).

(b) (tranzitivita implikace). Jestliže T ` ϕ→ ξ a soucasne T ` ξ→ ψ, pakT ` ϕ→ ψ. Stací použít poznámku 62 a tautologii(A → C)→ ((C → B)→ (A → B)).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 92/147

Predikátová logika. Kvantifikace. (2)

(c) Necht’ ϕ(x), ψ(x) jsou formule. Pak ` ∀x (ϕ→ ψ)→ ∀x (¬ψ→ ¬ϕ),nebot’

1) ` ∀x (ϕ→ ψ)→ (ϕ→ ψ) P42) ` (ϕ→ ψ)→ (¬ψ→ ¬ϕ) výr. tautologie3) ` ∀x (ϕ→ ψ)→ (¬ψ→ ¬ϕ) tranz. impl. na 1), 2)4) ∀x (ϕ→ ψ) ` ¬ψ→ ¬ϕ veta o dedukci5) ∀x (ϕ→ ψ) ` ∀x (¬ψ→ ¬ϕ) GEN6) ` ∀x (ϕ→ ψ)→ ∀x (¬ψ→ ¬ϕ) veta o dedukci

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 93/147

Predikátová logika. Kvantifikace. (3)

Tvrzení 1.–4. ted’ dokážeme za predpokladu, že ϕ(x) a ψ(x). Obecnápodoba vyplyne užitím vety konstantách (viz dále).

1 Platí ` (∀x (ϕ→ ψ))→ (ϕ→ ∀x ψ), nebot’ tato formule jeinstancí P5. Dukaz opacné implikace vypadá takto:

1) ` ∀x ψ→ ψ P42) ` (∀x ψ→ ψ)→ ((ϕ→ ∀x ψ)→ (ϕ→ ψ)) (A → B)→ ((C → A)→ (C → B))

je tautologie, viz pozn. 623) ` (ϕ→ ∀x ψ)→ (ϕ→ ψ) MP na 1),2)4) ϕ→ ∀x ψ ` ϕ→ ψ veta o dedukci5) ϕ→ ∀x ψ ` ∀x (ϕ→ ψ) GEN6) ` (ϕ→ ∀x ψ)→ (∀x (ϕ→ ψ)) veta o dedukci

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 94/147

Predikátová logika. Kvantifikace. (4)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

Nyní opacný smer ` (∃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 (¬ψ→ ¬ϕ) veta o dedukci5) ∃x ϕ→ ψ ` ¬ψ→ ¬ϕ P4 a MP6) ∃x ϕ→ ψ ` ϕ→ ψ (¬A → ¬B)→ (A → B) a MP7) ∃x ϕ→ ψ ` ∀x (ϕ→ ψ) GEN8) ` (∃x ϕ→ ψ)→ ∀x (ϕ→ ψ) veta o dedukci

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 95/147

Predikátová logika. Veta o korektnosti.

Veta 66

Necht’ T je teorie a ϕ formule jazyka teorie T. Jestliže T ` ϕ, pak T |= ϕ.

Dukaz. Stací overit následující tvrzení:

Je-li ψ instancí jednoho ze schémat P1–P5 (príp. také R1–R3, pokudjazyk teorie T je jazyk s rovností) a M je model T , pakM |= ψ.

Je-liM model T a ψ, ξ formule jazyka teorie T , kdeM |= ψ aM |= ψ→ ξ, pakM |= ξ.

Je-liM model T a ψ formule jazyka teorie T , kdeM |= ψ, pakM |= ∀x ψ.

Metaindukcí vzhledem k i je pak již triviální ukázat, že je-li ψ1, · · · , ψk

dukaz formule ϕ v T aM je model T , pak T |= ψi pro každé 1 ≤ i ≤ k . �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 96/147

Predikátová logika. Úplnost (úvod).

Lema 67

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.

Dukaz.

(1.⇒ 2.) Bud’ T bezesporná teorie. Pak existuje formule ϕ jazyka teorieT , která není v T dokazatelná (tj. T 0 ϕ). Obmenou 1. pak aledostáváme, že ϕ není sémantickým dusledkem T (tj. T 6|= ϕ). Toznamená, že existuje takový model T , kde není pravdivá ϕ. Zejménamá tedy T model.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 97/147

Predikátová logika. Úplnost (úvod). (2)

(2.⇒ 1.) Užitím 2. dokážeme obmenu 1. Necht’ tedy T 0 ϕ, a necht’ ϕ jeuniverzální uzáver ϕ. Ukážeme, že T ∪ {¬ϕ} je bezesporná; pakpodle 2. má T ∪ {¬ϕ} model, tedy T 6|= ϕ.T ∪ {¬ϕ} je bezesporná: Predpokládejme naopak, že T ∪ {¬ϕ} jesporná. Pak

1) T ∪ {¬ϕ} ` ϕ T ∪ {¬ϕ} je sporná2) T ` ¬ϕ→ ϕ veta o dedukci3) ` (¬ϕ→ ϕ)→ ϕ (¬A → A)→ A je tautologie, viz pozn. 624) T ` ϕ MP na 2),3)5) T ` ϕ opakovane P4 a MP

Obdrželi jsme tedy spor s tím, že T 0 ϕ.�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 98/147

Predikátová logika. Úplnost (úvod). (3)

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 . Tatostruktura obecne není modelem T . Ukážeme, že pokud T vyhovujedalším podmínkám (je henkinovská a úplná), pak kanonická strukturaje modelem T .

Ukážeme, že každou bezespornou teorii je možné vhodnýmzpusobem rozšírit tak, aby byla henkinovská a úplná.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 99/147

Predikátová logika. Rozšírení teorie.

Definice 68

Teorie S je rozšírení teorie T, jestliže jazyk teorie S obsahuje jazykteorie T a v teorii S jsou dokazatelné všechny axiómy teorie T.

Rozšírení S teorie T se nazývá konzervativní, jestliže každá formulejazyka teorie T, která je dokazatelná v S, je dokazatelná i v T.

Teorie S a T jsou ekvivalentní, jestliže S je rozšírením T a soucasneT je rozšírením S.

Príklad 69

Teorie komutativních grup je nekonzervativní rozšírení teorie grup.

Teorie grup je nekonzervativní rozšírení teorie monoidu (tvrzení∀x ∃y x · y = 1 nelze dokázat v teorii monoidu).

Gödel-Bernaysova teorie tríd je konzervativním rozšírenímZermelo-Fraenkelovy teorie množin.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 100/147

Predikátová logika. Veta o konstantách.

Veta 70 (o konstantách)

Necht’ S je rozšírení T vzniklé obohacením jazyka teorie T o novénavzájem ruzné konstanty c1, · · · , ck (nové axiómy nepridáváme), anecht’ x1, · · · , xk jsou navzájem ruzné promenné. Pak pro každou formuliϕ jazyka teorie T platí, že T ` ϕ práve když S ` ϕ(x1/c1, · · · , xk/ck ).

Dukaz. Jelikož c1, · · · , ck jsou navzájem ruzné, stací dokázat, že T ` ϕpráve když S ` ϕ(x/c).⇒: K dukazu ϕ v T pripojíme formule ∀x ϕ, ∀x ϕ→ ϕ(x/c), ϕ(x/c) aobdržíme tak dukaz formule ϕ(x/c) v S.⇐: Necht’ ψ1, · · · , ψk je dukaz ϕ(x/c) v S. Necht’ y je promenná, která senevyskytuje v tomto dukazu. Indukcí k i ukážeme, že pro každé 1 ≤ i ≤ kje ψ1(c/y), · · · , ψi(c/y) dukaz v T . Rozlišíme tyto možnosti:

Je-li ψi instancí P1–P5 (prí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é.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 101/147

Predikátová logika. Veta o konstantách. (2)

Jestliže ψi vyplývá z ψj a ψm pomocí MP, je ψm tvaru ψj → ψi aformule ψ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 . Stací siuvedomit, že (∀x ψj)(c/y) je tatáž formule jako ∀x (ψj(c/y)), nebot’ xa y jsou ruzné.

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) GEN3) ` ∀y ϕ(x/y)→ (ϕ(x/y)(y/x)) P44) T ` ϕ(x/y)(y/x) MP na 2),3)5) T ` ϕ ϕ(x/y)(y/x) je totéž co ϕ

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 102/147

Predikátová logika. Henkinovské teorie.

Definice 71

Teorie T je henkinovská, jestliže pro každou formuli ϕ jazyka teorie Ts jednou volnou promennou x existuje v jazyce teorie T konstanta ctaková, že T ` ∃x ϕ→ ϕ(x/c).

Teorie T je úplná, jestliže je bezesporná a pro každou uzavrenouformuli ϕ jejího jazyka platí bud’ T ` ϕ nebo T ` ¬ϕ.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 103/147

Predikátová logika. Henkinovské teorie. (2)

Veta 72 (o henkinovské konstante)

Bud’ T teorie a ϕ(x) formule jejího jazyka. Je-li S rozšírení T, kterévznikne pridáním nové konstanty cϕ a formule ∃x ϕ→ ϕ(x/cϕ), pak S jekonzervativní rozšírení T.

Dukaz. 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 MP3) {∀y¬ξ(x/y)} ` ¬ξ prepis4) {∀y¬ξ(x/y)} ` ∀x¬ξ GEN5) ` ∀y¬ξ(x/y)→ ∀x¬ξ dedukce6) ` ∃xξ→ ∃yξ(x/y) taut. (A → B)→ (¬B → ¬A) a MP.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 104/147


Necht’ R znací teorii vzniklou pouhým pridáním konstanty cϕ k T . Necht’ψ je formule jazyka teorie T taková, že S ` ψ. Necht’ y je promenná,která se nevyskytuje ani ve ϕ, ani v ψ. Platí:

1) S ` ψ predpoklad2) R ` (∃xϕ→ ϕ(x/cϕ))→ ψ S = R ∪ {∃xϕ→ ϕ(x/cϕ)}

a dedukce3) T ` (∃xϕ→ ϕ(x/y))→ ψ veta o konstantách4) T ` ∀y((∃xϕ→ ϕ(x/y))→ ψ) GEN5) T ` ∃y(∃xϕ→ ϕ(x/y))→ ψ lema 65 (2) a MP6) ` (∃xϕ→ ∃yϕ(x/y))→ ∃y(∃xϕ→ ϕ(x/y)) lema 65 (3)7) T ` (∃xϕ→ ∃yϕ(x/y))→ ψ tranz. implikace8) ` ∃xϕ→ ∃yϕ(x/y) dokázáno výše9) T ` ψ MP

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 105/147


Veta 73 (o henkinovském rozšírení)

Ke každé teorii existuje henkinovská teorie, která je jejím konzervativnímrozšírením.

Dukaz. Bud’ T 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) jazykateorie Ti pridáme novou konstantu cϕ a formuli ∃xϕ→ ϕ(x/cϕ).

Metaindukcí vzhledem k n ukážeme, že Tn je konzervativní rozšírení T .

Pro n = 0 není co dokazovat. V indukcním kroku si stací uvedomit, žeje-li Ti+1 ` ψ, muže být v dukazu formule ψ použito jen konecnemnoho axiómu ξ1, · · · , ξk , které nepatrí do Ti . Užitím vety ohenkinovské konstante k -krát po sobe dostáváme Ti ` ψ, proto T ` ψpodle I.P.

Uvažme teorii S =⋃∞

n=0 Tn. Teorie S je konzervativní rozšírení T , nebot’každý dukaz v S používá jen konecne mnoho axiómu a je tedy dukazemv nejaké Tm. Teorie S je zjevne henkinovská. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 106/147


V následující vete využíváme Zornovo lema, které ríká následující:

Necht’ (A ,≤) je usporádaná množina. Jestliže pro každýspocetný retez a0 ≤ a1 ≤ a2 · · · existuje v A horní závora, pak(A ,≤) má maximální prvek.

Zornovo lema je ekvivalentní s axiomem výberu.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 107/147


Veta 74 (o zúplnování teorií)

Ke každé bezesporné teorii existuje její rozšírení se stejným jazykem,které je úplnou teorií.

Dukaz. Uvažme usporádanou množinu (T ,⊆), kde T je soubor všechbezesporných teorií obsahujících T . Každý spocetný retezecT0 ⊆ T1 ⊆ T2 · · · má v (T ,⊆) horní závoru

⋃∞

i=0 Ti . Zde je treba overit, že⋃∞

i=0 Ti je skutecne bezesporná teorie (a tedy prvek T ): pokud by tatoteorie byla sporná, existuje v ní dukaz kontradikce. Tento dukaz alepoužívá jen konecne mnoho axiómu, proto je dukazem i v nejaké Ti , tedyTi je sporná, spor.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 108/147


Podle Zornova lematu tedy existuje maximální bezesporná teorieUobsahující T . Dokážeme, žeU je úplná. Pokud není, existuje uzavrenáformula ϕ taková, žeU 0 ϕ a soucasneU 0 ¬ϕ. Zejména tedyϕ,¬ϕ <U. Z maximalityU plyne, že teorieU ∪ {ϕ} iU ∪ {¬ϕ} jsousporné, platí tedyU ∪ {ϕ} ` ¬ϕ aU ∪ {¬ϕ} ` ϕ. Proto takéU ` ϕ→ ¬ϕaU ` ¬ϕ→ ϕ (užitím vety o dedukci). Z toho dostávámeU ` ψ ∧ ¬ψpro libovolné ψ, nebot’ (A → ¬A)→ ((¬A → A)→ (ψ ∧ ¬ψ)) jevýroková tautologie (použijeme 2x MP). TedyU je sporná, spor.Pokud je jazyk teorie T konecný nebo spocetný, lze se použití Zornovalematu snadno vyhnout. Dokazovaná veta pak žádnou formu axiómuvýberu nevyužívá. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 109/147

Predikátová logika. Kanonická struktura.

Definice 75

Bud’ T teorie, kde jazyk teorie T obsahuje alespon jednu konstantu.Kanonická struktura teorie T je realizaceM jazyka teorie T, kde

univerzum M je tvoreno všemi uzavrenými termy jazyka teorie T;

relizace funkcního symbolu f arity n je funkce fM , která uzavrenýmtermum t1, · · · , tn priradí uzavrený term f(t1, · · · , tn);

realizace predikátového symbolu P arity m je predikát PM definovanýtakto: PM(t1, · · · , tm) platí práve když T ` P(t1, · · · , tm).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 110/147

Predikátová logika. Kanonická struktura. (2)Veta 76 (o kanonické strukture)

Necht’ T je úplná henkinovská teorie, a necht’ jazyk teorie T je jazykembez rovnosti. Pak kanonická struktura teorie T je modelem T.

Dukaz. Necht’M je kanonická struktura teorie T . Ukážeme, že prolibovolnou formuli ϕ jazyka teorie T platí následující:

Jestliže ϕ je uzavrená instance formule ϕ, pak T ` ϕ práve kdyžM |= ϕ.

Jelikož lze (bez újmy na obecnosti) predpokládat, že prvky T jsouuzavrené formule, plyne z výše uvedeného, žeM je model T .Indukcí ke strukture ϕ:

ϕ ≡ P(t1, · · · , tn). Bud’ P(t ′1, · · · , t′

n) libovolná uzavrená instance. Podledefinice kanonické strukturyM |= P(t ′1, · · · , t

′

n) práve kdyžT ` P(t ′1, · · · , t

′

n).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 111/147

Predikátová logika. Kanonická struktura. (3)

ϕ ≡ ¬ψ. Bud’ ¬ψ libovolná uzavrená instance. Jelikož ψ je uzavrenáinstance ψ, podle IP platí T ` ψ práve kdyžM |= ψ. Dále T ` ¬ψpráve když T 0 ψ (T je bezesporná) práve kdyžM 6|= ψ (IP) právekdyžM |= ¬ψ.

ϕ ≡ ψ→ ξ. Každá uzavrená instance této formule je tvaru ψ→ ξ, kdeψ je uzavrená instance ψ a ξ je uzavrená instance ξ.

Necht’ T ` ψ→ ξ. Jelikož ψ je uzavrená formule a T je uplná, platíbud’ T ` ψ nebo T ` ¬ψ. V prvém prípade dále T ` ξ (MP) aužitím IP celkem dostávámeM |= ψ aM |= ξ. Proto takéM |= ψ→ ξ. V druhém prípade T 0 ψ (T je bezesporná), protoM 6|= ψ (IP), tudížM |= ψ→ ξ.

Necht’M |= ψ→ ξ. Pak bud’M 6|= ψ neboM |= ξ. V prvémprípade T 0 ψ podle IP, tudíž T ` ¬ψ nebot’ T je úplná. ProtoT ` ψ→ ξ užitím tautologie ¬A → (A → B) a MP. V druhémprípade T ` ξ, proto T ` ψ→ ξ užitím tautologie A → (B → A) aMP.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 112/147


ϕ ≡ ∀x ψ. Bud’ ∀x ψ libovolná uzavrená instance. Pak ψ(x), jinak by∀x ψ nebyla uzavrená.

Necht’ T ` ∀x ψ. Pak pro libovolný uzavrený term t platí T ` ψ(x/t)(P4 a MP). Podle IPM |= ψ(x/t). Jelikož tento argument fungujepro libovolný uzavrený term t , platí takéM |= ∀x ψ.

Necht’ T 0 ∀x ψ. Pak také T 0 ∀x ¬¬ψ (kdyby T ` ∀x ¬¬ψ,dostaneme dále T ` ¬¬ψ (P4 a MP) a T ` ψ (tautologie ¬¬A → Aa MP), T ` ∀x ψ (GEN), spor).Jelikož T 0 ∀x¬¬ψ, platí T ` ¬∀x¬¬ψ nebot’ T je úplná. TedyT ` ∃x¬ψ. Jelikož T je henkinovská, platí T ` ∃x¬ψ→ ¬ψ(x/c).Tedy T ` ¬ψ(x/c) a proto T 0 ψ(x/c) nebot’ T je bezesporná.Podle IPM 6|= ψ(x/c), tedyM |= ¬ψ(x/c). ProtoM 6|= ∀xψ.

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 113/147


Veta 77

Necht’ T je úplná henkinovské teorie, a necht’ jazyk teorie T je jazykem srovností. Pak T má model.

Dukaz. Bud’ S teorie (s jazykem bez rovnosti), která vzniknerozšírením T o nový binární predikátový symbol = a axiomy R1–R3.Symbol = v teorii S je tedy mimologický a muže být realizován ,,jakkoliv‘‘.Axiomy R1–R3 jsou v S ,,normální‘‘ axiómy. Stací nám ukázat, že S mátakový model, kde = je realizován jako identita. Takový model pak jistebude i modelem T (kde = je chápáno jako logický symbol).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 114/147


Bud’M kanonická struktura teorie S, a necht’ ∼ je realizace = v S (tj.t1 ∼ t2 práve když S ` t1 = t2). Dokážeme, že ∼ je nutne 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ímGEN, P4 a MP dostaneme S ` (s=t ∧ s=s)→ (s=s → t=s). UžitímMP dostaneme S ` t=s.

Tranzitivita: podobne.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 115/147


Nyní již mužeme definovat strukturu O pro jazyk teorie S:

Nosicem O jsou trídy rozkladu nosiceM podle ∼.

Funkcní 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áve když PM(t1, · · · , tm)

Korektnost této definice (tj. nezávislost na volbe reprezentantu) sedokáže pomocí R1–R3 podobným stylem jako výše. Snadno se overí, žerealizací uzavreného termu t ve strukture O je [s] práve když S ` s=t . Toznamená, že predikátový symbol = je v O realizován jako identita.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 116/147


Zbývá ukázat, že O je modelem S. Podobne jako ve vete 76 budemechtít prokázat, že pro libovolnou formuli ϕ(x1, . . . , xn) jazyka teorie S platí:

Jestliže t1, · · · , tn jsou uzavrené termy jazyka teorie S, pakT ` ϕ(x1/t1, · · · , xn/tn) práve když O |= ϕ(x1/[t1], · · · , xn/[tn]).

Jelikož S je henkinovská a úplná, platí podle vety 76

T ` ϕ(x1/t1, · · · , xn/tn) práve kdyžM |= ϕ(x1/t1, · · · , xn/tn)

Stací tedy ukázat, že

M |= ϕ(x1/t1, · · · , xn/tn) práve když O |= ϕ(x1/[t1], · · · , xn/[tn])

To lze lehce provést indukcí ke strukture ϕ. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 117/147

Predikátová logika. Veta o úplnosti.

Kurt Gödel (1906–1978)

Veta 78 (o úplnosti, Kurt Gödel)

Každá bezesporná teorie má model.Pro každou teorii T a každou formulijejího jazyka tedy platí, že jestližeT |= ϕ, pak T ` ϕ.

Dukaz. Jde o jednoduchýdusledek predchozích vet. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 118/147

Predikátová logika. Veta o kompaktnosti.

Veta 79

Teorie T má model, práve když každá její podteorie s konecne mnohaaxiómy (a s minimálním jazykem, v nemž jsou tyto axiómyformulovatelné) má model.

Dukaz. Smer ,,⇒‘‘ je triviální. Pro opacnou implikaci stací ukázat, že Tje bezesporná (pak T má model podle vety o úplnosti). Kdyby T bylasporná, existoval by dukaz formule ψ ∧ ¬ψ v T . Tento dukaz je konecný,využívá tedy jen konecne mnoho axiómu T , které tvorí spornoupodteorii T , spor. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 119/147

Predikátová logika.Löwenheimova-Skolemova veta.

Poznámka 80

Z dukazu vety 73 plyne, že každá bezesporná teorie s jazykem bezrovnosti má model kardinality max{|L|,ℵ0} (pri rozšírení teorie nahenkinovskou bylo pridáno |L| · ℵ0 nových konstant). Toto pozorováníneplatí pro teorie s jazykem s rovností (napr. pro T = {∀x x=c}).Nicméne lze dokázat následující:

Veta 81

Necht’ T je teorie a necht’ pro každé n ∈N existuje model teorie T jehožnosic má mohutnost alespon n. Pak T má nekonecný model.

Dukaz. Je-li jazyk teorie T jazykem bez rovnosti, plyne tvrzení ihnedz poznámky 80. Jinak pro každé n ∈N definujeme formuliϕn ≡ ∀x1 · · · ∀xn∃y x1,y ∧ · · · ∧ xn,y a teorii Sn = T ∪ {ϕ1, · · · , ϕn}. Podlepredpokladu vety má každá Sn model. Podle vety o kompaktnosti máproto model i teorie

⋃∞

i=1 Sn. Tento model je nutne nekonecný a je imodelem teorie T . �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 120/147

Predikátová logika.Löwenheimova-Skolemova veta. (2)

Veta 82 (Löwenheimova-Skolemova)

Necht’ T je teorie s jazykem L, která má nekonecný model. Necht’ κ jenekonecný kardinál takový, že κ ≥ |L|. Pak T má model mohutnosti κ.

Dukaz. Necht’M je nekonecný model T . Jazyk L rozšíríme o systém{ci | i < κ} nových konstant a k T pridáme axiómy {ci , cj | i, j < κ}.Obdržíme tak teorii T ′. Necht’ K je konecná cást T ′, a necht’ c1, · · · , cn

jsou všechny nove pridané konstanty, které se vyskytují ve formulíchteorie K (takových konstant je jen konecne mnoho). Pokud tyto konstantyrealizujeme navzájem ruznými prvky nosiceM, obdržíme model teorieK . Každá konecná cást T ′ je tedy splnitelná. Podle vety o kompaktnostimá tedy model i teorie T ′. Nosic tohoto model ale nutne obsahujealespon κ navzájem ruzných individuí. �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 121/147

Veta o neúplnosti. Úvod.

Jazyk aritmetiky je jazyk s rovností obsahující konstantu 0, unárnífunkcní symbol S a dva binární funkcní symboly ∗ a +.

Význacnou realizací jazyka aritmetiky je (N0, ∗,+), kde univerzem jesoubor všech nezáporných celých císel, 0 je realizováno jako nula, Sjako funkce následníka, ∗ jako násobení, + jako scítání. (Relacnípredikáty jako <,≤ lze snadno definovat.)

Jedním ze základních kroku Hilbertova programu formalizacematematiky melo být vytvorení rekurzivní a úplné teorie T jazykaaritmetiky.

Slovem ,,úplné‘‘ se myslí, že T ` ϕ práve když ϕ ∈ Th(N0, ∗,+) (Tj.formule dokazatelné v T jsou práve formule pravdivé v (N0, ∗,+)).

Slovo ,,rekurzívní‘‘ intuitivne znamená, že musí být ,,mechanickyoveritelné‘‘, zda daná posloupnost symbolu je ci není dukazem v T(možných formalizací tohoto pojmu je více).

Z Gödelových výsledku plyne, že taková teorie neexistuje.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 122/147

Veta o neúplnosti. Turinguv stroj.

Alan Turing (1912–1954)

Definoval pojem Turingovastroje a s jeho pomocí ukázal,že problém pravdivosti formulíprvního rádu je nerozhodnutelný.

Považován za zakladateleinformatiky (jako vedy).

Turinguv stroj je matematickýmmodelem ,,hloupéhoodvozovace‘‘, který má k dispozicipapír, tužku a gumu, a kterýsi pamatuje konecne mnohoschémat axiómu.

Význam Turingova stroje cobymodelu reálných výpocetníchzarízení se projevil až v druhépolovine 20. století.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 123/147

Veta o neúplnosti. Turinguv stroj. (2)Je-li Σ konecná abeceda, znací symbol Σ∗ soubor všech konecnýchslov složených z prvku Σ (prázdné slovo znacíme symbolem ε). Délkuslova w znacíme len(w). Pro každé 1 ≤ i ≤ len(w) znací symbol w(i)i-tý znak slova w (zleva). Jazyk nad abecedou Σ je podmnožina Σ∗.Turinguv stroj je matematický model výpocetního zarízení, které jevybaveno konecne-stavovou rídící jednotkou (,,hlava odvozovace‘‘),jednosmerne nekonecnou pracovní páskou (,,papír‘‘), actecí/zápisovou hlavou (,,tužka/guma‘‘).Na zacátku výpoctu je na pásce zapsáno konecné vstupní slovo,hlava je na nejlevejší pozici, a stavová jednotka je v pocátecním stavu.Stroj na základe svého momentálního kontrolního stavu a symbolupod ctecí hlavou provede ,,výpocetní krok‘‘, tj. zmení svuj kontrolnístav, nahradí symbol pod ctecí hlavou jiným symbolem, a posunectecí hlavu vlevo nebo vpravo.Výpocet se zastaví, pokud stroj dojde do konfigurace, jejíž kontrolnístav je akceptující nebo zamítající. Pro nekterá slova muže stroj takénezastavit (cyklit).Vstupní slovo je akceptované, jestliže stroj po konecne mnoha krocíchdojde do akceptující konfigurace. Soubor všech vstupních slov, kterástroj akceptuje, tvorí jazyk akceptovaný daným strojem.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 124/147

Veta o neúplnosti. Turinguv stroj. (3)

Definice 83

Turinguv stroj je devítice M = (Q ,Σ,Γ,�,B,q0,qa ,qr , δ), kde

Q je konecný soubor kontrolních stavu;

Σ je konecná vstupní abeceda;

Γ je konecná pásková abeceda (kde Σ ⊆ Γ a Q ∩ Γ = ∅);

� ∈ Γ je prázdný znak;

B ∈ Γ je levý konec pásky;

q0,qa ,qr ∈ Q je po rade pocátecní, akceptující a zamítající stav(q0,qa ,qr jsou navzájem ruzné).

δ : Q × Γ→ Q × Γ × {L ,R} je prechodová funkce, kde

pro každé p ∈ Q platí δ(p,B) = (q,B,R) pro nejaké q ∈ Q;

δ(qa , c) = (qa , c,R) pro každé c ∈ Γ;

δ(qr , c) = (qr , c,R) pro každé c ∈ Γ.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 125/147

Veta o neúplnosti. Turinguv stroj. (4)

Konfigurace stroje M je konecné slovo uqv, kde u, v ∈ Γ∗ a q ∈ Q .

Pocátecní konfigurace pro slovo w ∈ Σ∗ je konfigurace q0Bw.

Krok výpoctu je binární relace 7→ na množine konfigurací definovanátakto:

Jestliže δ(q,a) = (p,b ,L), pak ucqav 7→ upcbv pro každéu, v ∈ Γ∗ a c ∈ Γ.

Jestliže δ(q,a) = (p,b ,R), pak uqav 7→ ubpv ′ pro každé u, v ∈ Γ∗,kde v ′ = v pokud v je neprázdné, jinak v ′ = �.

7→ obsahuje jen to, co lze odvodit pomocí predchozích dvoupravidel.

Slovo w ∈ Σ∗ je akceptované strojem M, jestliže q0Bw 7→∗ uqav pronejaké u, v ∈ Γ∗.

Jazyk akceptovaný strojemM, oznacovaný L(M), je soubor všechw ∈ Σ∗, které jsou akceptované strojemM.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 126/147

Veta o neúplnosti. Vlastnosti jazyku.

Jazyk L ⊆ Σ∗ je rekurzivne vycíslitelný, jestliže L = L(M) pro nejakýTuringuv stroj M. Jazyk L ⊆ Σ∗ je rekurzivní, jestliže L = L(M) pronejaký Turinguv stroj M, který zastaví pro každé vstupní slovo.Jednoduché pozorování je, že jazyk L ⊆ Σ∗ je rekurzivní práve když Li L jsou rekurzivne vycíslitelné (kde L = Σ∗ \ L ).

Uvažme soubor všech Turingových stroju se vstupní abecedou {0,1}.Bez újmy na obecnosti lze predpokládat, že kontrolní stavy a symbolypáskové abecedy každého takového stroje jsou prvky nejaké fixníspocetné množiny. Pak každý Turinguv stroj M se vstupní abecedou{0,1} lze jednoznacne zapsat jako slovo code(M) ∈ {0,1}∗. Navíc lzepredpokládat, že každé u ∈ {0,1}∗ je kódem nejakého stroje Mu sevstupní abecedou {0,1}.

Uvažme jazyk Accept = {u ∈ {0,1}∗ | Mu akceptuje u}.

Lze snadno (i když technicky) dokázat, že Accept je rekurzívnevycíslitelný (lze zkonstruovat stroj U, který pro dané vstupní slovou ∈ {0,1}∗ ,,simuluje‘‘ výpocet stroje Mu na slove u).

Ukážeme, že Accept není rekurzívní. Podle jednoho z predchozíchbodu pak jazyk Accept není rekurzivne vycíslitelný.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 127/147

Veta o neúplnosti. Jazyk Accept .

Veta 84

Jazyk Accept není rekuzivní.

Dukaz. Predpokládejme, že Accept je rekurzivní. Pak také Accept jerekurzivní, tj. existuje Turinguv stroj M se vstupní abecedou {0,1}, kterýzastaví pro každé vstupní slovo a L(M) = Accept. Necht’ v = code(M).Platí v ∈ L(M)?

Ano. Pak v < L(Mv ) = L(M), spor.

Ne. Pak v ∈ L(Mv ) = L(M), spor.

Z predpokladu existence stroje M se nám podarilo odvodit spor. Stroj Mtedy neexistuje. �

Poznámka 85

V dukazu predchozí vety se objevuje urcitá forma autoreference (stroj Mzkoumá ,,sám sebe‘‘ tak, že analyzuje svuj vlastní kód). Každý známýdukaz vety o neúplnosti se o nejakou formu autoreference opírá.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 128/147

Veta o neúplnosti. Peanova aritmetika.

Jedním z pokusu o vytvorení rekurzivní a úplné teorie aritmetiky bylnásledující systém nazývaný Peanova aritmetika (seznam Peanovýchaxiómu bývá v literature uváden v ruzných podobách):

∀x S(x) , 0

∀x∀y S(x)=S(y)→ x=y

∀x x+0 = x

∀x∀y x+S(y) = S(x+y)

∀x x∗0 = 0

∀x∀y x∗S(y) = (x∗y) + x

(ϕ(0) ∧ ∀x (ϕ(x)→ ϕ(S(x))))→ ∀x ϕ(x), kde ϕ je formule s jednouvolnou promennou x.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 129/147

Veta o neúplnosti. Peanova aritmetika. (2)

Každou formuli jazyka aritmetiky je možné zapsat jako slovo nadabecedou {v ,+, ∗,0,S , (, ),∀,→,¬,=,#}. Ruzné promennézapisujeme jako retezce složené z v ruzné délky (napr. místo x , y , zmužeme psát v , vv , vvv apod.).

Podobne mužeme i každou konecnou posloupnost formulí zapsat jakoslovo nad výše uvedenou abecedou, kde symbol # použijeme prooddelení jednotlivých formulí.

Definice 86

Teorie T jazyka aritmetiky je rekurzivní, jestliže jazyk tvorený zápisyvšech dukazu v T je rekurzivní.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 130/147

Veta o neúplnosti. Peanova aritmetika. (3)

Lze snadno (i když technicky) dokázat, že napr. Peanovy axiómy tvorírekurzivní teorii. Definici rekurzivity teorie lze samozrejme rozšírit i nateorie nad jinými jazyky. Rekurzivní teorie odpovídají (na intuitivní úrovni)práve teoriím, které umožnují ,,mechanické odvozování‘‘. Triviálnípozorování o rekurzivních teoriích podává následující veta.

Veta 87

Necht’ T je rekurzivní teorie jazyka aritmetiky. Pak jazyk tvorený všemiformulemi dokazatelnými v T je rekurzivne vycíslitelný.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 131/147

Veta o neúplnosti. Jazyk Valid.

Necht’ Valid resp. Provable jsou jazyky nad abecedou{v ,+, ∗,0,S , (, ),∀,→,¬,=} obsahující zápisy všech formulí jazykaPeanovy aritmetiky, které jsou pravdivé v realizaci (N0, ∗,+) resp.dokazatelné ze systému axiomu Peanovy aritmetiky.

Zjevne Provable ⊆ Valid, nebot’ Peanova aritmetika je korektní.

Naším cílem je ukázat, že tato inkluze je vlastní, tj. že existují formulepravdivé v (N0, ∗,+), které nejsou z Peanových axiómu dokazatelné.

Jelikož jazyk Provable je podle vety 87 rekurzivne vycislitelný, stacíukázat, že Valid není rekurzivne vycislitelný (je videt, že pakProvable , Valid i pro libovolnou jinou rekurzivní teorii aritmetiky).

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 132/147

Veta o neúplnosti. Gödeluv predikát β.

Z hlediska dukazu vety o neúplnosti je jednou z podstatných vlastnostíprirozených císel jejich schopnost ,,kódovat‘‘ libovolne dlouhé konecnéposloupnosti prirozených císel.

Definujeme 4-ární predikát β na nezáporných celých císlechpredpisem

β(a,b , i, x) ⇐⇒ x = a mod (1 + b(1 + i))

Bud’ S nekonecná posloupnost nezáporných celých císel, a,b ∈N0.Rekneme, že S splnuje β (pro dané a a b), jestliže pro každé i ∈N0

platí β(a,b , i,S(i)).

Pro každé a,b ∈N0 existuje jediná posloupnost splnující β; tou jeposloupnost Sa,b daná predpisem Sa,b (i) = a mod(1 + b(1 + i)).

Predikát β je vyjádritelný v jazyce aritmetiky, nebot’ x = a mod b lzenapsat jakoa ≥ 0 ∧ b ≥ 0 ∧ ∃k

(k ≥ 0 ∧ k ∗b ≤ a ∧ (k +1)∗b > a ∧ x = a−(k ∗b)

)

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 133/147

Veta o neúplnosti. Gödeluv predikát β. (2)Veta 88

Pro každou konecnou posloupnost n0, · · · ,nk nezáporných celých císelexistují n,m ∈N0 taková, že nj = Sn,m(j) pro každé 0 ≤ j ≤ k . Toznamená, že pro každé 0 ≤ j ≤ k platí β(n,m, j, x) ⇐⇒ x = nj .

Dukaz. (osnova)

Necht’ m = (max{k ,n0, · · · ,nk })! Císla pi = 1 + m(1 + i), kde0 ≤ i ≤ k , jsou navzájem nesoudelná a ni < pi pro každé 0 ≤ i ≤ k .

Dále pro každé 0 ≤ i ≤ k definujeme

ci = p0 · · · · · pk/pi

Nyní pro každé 0 ≤ i ≤ k existuje presne jedno di , 0 ≤ di ≤ pi , takové,že (ci · di) mod pi = 1

Definujeme

n =

k∑i=0

ci · di · ni

Pro každé 0 ≤ i ≤ k platí ni = n mod pi , což je tvrzení vety.�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 134/147

Veta o neúplnosti. Dukaz.

Veta 89

Jazyk Valid není rekurzivne vycíslitelný.

Dukaz. Ukážeme, že existuje Turinguv stroj M, který pro každé vstupníslovo u nad abecedou {0,1} zastaví v konfiguraci, kdy je na páscezápsáno slovo w nad abecedou {v ,+, ∗,0,S , (, ),∀,→,¬,=} takové, žev ∈ Accept práve když w ∈ Valid. Pokud by tedy jazyk Valid bylakceptovaný nejakým strojem M′, stacilo by ,,napojit stroje M a M′ zasebe‘‘ a dostali bychom stroj akceptující jazyk Accept, což je spor.Stroj M pro dané vstupní slovo u ∈ {0,1}∗ ,,vypocítá‘‘ formuli jazykaaritmetiky, která ríká ,,není pravda, že stroj Mu akceptuje slovo u‘‘.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 135/147

Veta o neúplnosti. Dukaz. (2)

Pozorování: Necht’ γ0 · · ·γd je zápis iniciální konfigurace stroje Mu proslovo u. Stroj Mu akceptuje slovo u práve když existují `, c ∈N0 a retezecS nad abecedou Γu ∪Qu ∪ {#} tvaru α0#α1# · · ·α`# tak, že platí:

d < c;

délka αi je c − 1 pro každé 0 ≤ i ≤ ` ;

α0 je zápisem iniciální konfigurace Mu pro slovo u, doplneným zpravaznakem � na délku c−1;

αi 7→ αi+1 pro každé 0 ≤ i < `;

v retezci α` se vyskytuje akceptující stav stroje Mu.

Cílem našeho dalšího úsilí je ,,zakódovat‘‘ podmínku z predchozíhopozorování jako formuli jazyka aritmetiky. Klícovým obratem je použitíGödelova predikátu β, pomocí kterého vyjádríme existenci retezce S.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 136/147


Pri kódování požadavku ,,αi 7→ αi+1 pro každé 0 ≤ i < `‘‘ se uplatnínásledující pozorování: existuje soubor C(Mu) kompatibilních šestictvorený (nekterými) šesticemi znaku nad abecedou Γu ∪Qu ∪ {#} takový,že pro každou konfiguraci α délky c−1, každé slovo γ nad abecedouΓu ∪Qu ∪ {#} délky c−1, a každý znak s této abecedy platí následující:

α 7→ γ a s = # práve když pro každé 0 ≤ i ≤ c−3 tvorí trojiceznaku od pozice i ve slove α# následovaná trojicí znaku odpozice i ve slove γs kompatibilní šestici (pozice ve slovechcíslujeme od 0).

Soubor kompatibilních šestic lze pro každý Turinguv stroj sestrojitalgoritmicky na základe jeho prechodové funkce. Stroj M tedy dokáževypocítat soubor C(Mu) kompatibilních šestic stroje Mu.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 137/147


Každému a ∈ Γu ∪Qu ∪ {#} pridelíme jedinecné prirozené císlo [a].Podmínku z predchozího pozorování pak zapíšeme jako

∃` ∃c ∃m ∃n(d < c ∧ INIT(m,n, c) ∧COMP(m,n, c, `) ∧ ACC(m,n, c, `)

)kde jednotlivé podformule vyjadrují následující:

,,Posloupnost Sm,n zacíná zápisem iniciálním konfiguraceMu proslovo u, doplneným zprava znakem � na délku c−1. Pak následujeznak #‘‘.

INIT(m,n, c) ≡

d∧i=0

β(m,n, i, [γi ]) ∧

∀i(d < i ≤ c−2 → β(m,n, i, [�])

)∧ β(m,n, c−1, [#])

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 138/147


,,V posloupnosti Sm,n tvorí odpovídající trojice znaku v sousedníchkonfiguracích kompatibilní šestice‘‘.

COMP(m,n, c, `) ≡ ∀i ∀j((i < ` ∧ j ≤ c−3)→ MATCH(m,n, i · c + j, c)

)kde MATCH(m,n, k , c) je formule∨

(a,b ,c,d,e,f)∈C(Mu)

TRIO(m,n, k , [a], [b], [c]) ∧ TRIO(m,n, k+c, [d], [e], [f ])

aTRIO(m,n,p, x , y , z) ≡ β(m,n,p, x)∧β(m,n,p+1, y)∧β(m,n,p+2, z)

,,Poslední konfigurace je akceptující‘‘. (Predpokládejme, že akceptujícístav stroje Mu je q.)

ACC(m,n, c, `) ≡ ∃i (i < c ∧ β(m,n, c · ` + i, [q]))

�

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 139/147

Veta o neúplnosti. Gödeluv dukaz.

Triviálním dusledkem vety 87 a vety 89 je následující:

Veta 90 (o neúplnosti)

Neexistuje žádná rekurzivní teorie jazyka aritmetiky, ve které jsoudokazatelné práve všechny formule pravdivé v realizaci (N0,+, ∗).Specielne pro každou korektní rekurzivní teorii T (tj. takovou teorii, kteráumožnuje dokázat pouze formule pravdivé v (N0,+, ∗)) nutne existujeformule platná v (N0,+, ∗), která není v T dokazatelná.

Veta 90 bývá v literature také oznacována jako první veta o neúplnosti.Puvodní Gödelova formulace této vety (a zejména její dukaz) vypadáodlišne. Klícové obraty v Gödelove konstrukci si nyní naznacíme. V tétocásti se slovem ,,formule‘‘ myslí formule jazyka aritmetiky.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 140/147

Veta o neúplnosti. Gödeluv dukaz. (2)

Necht’ PA znací teorii Peanovy aritmetiky, a necht’ N znací realizaci(N0,+, ∗) jazyka aritmetiky. Formule jsou konecná slova nad abecedou{v ,+, ∗,0,S , (, ),∀,→,¬,=} a lze je tedy kódovat císly stejným zpusobemjako konfigurace Turingových stroju. Pro každou formuli ϕ oznacímesymbolem dϕe císlo, které je jejím kódem.

Lema 91 (Gödelovo lema o pevném bode)

Pro každou formuli ψ(x) existuje uzavrená formule τ taková, žePA ` τ↔ ψ(dτe). (Formule τ ríká ,,ψ platí pro muj kód‘‘.)

Dukaz. (osnova) Pro libovolnou fixní promennou x0 lze sestrojit formuliSUBST(x , y , z), která ríká následující:

,,Císlo z je kódem formule, kterou získáme substitucí promenné x0 zakonstantu s hodnotou x ve formuli s kódem y.‘‘

Napr. SUBST(5, dϕ(x0)e,413) je pravdivá práve když dϕ(5)e = 413.Konstrukce formule SUBST(x , y , z) je technická; lze použít podobnýprístup jako pri konstrukci formule ACOMP v dukazu vety 89.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 141/147


Nyní definujeme

σ(x) ≡ ∀y (SUBST(x , x , y)→ ψ(y))

τ ≡ σ(dσ(x0)e)

Overme, že τ má požadovanou vlastnost:

τ ≡ σ(dσ(x0)e) ≡ ∀y (SUBST(dσ(x0)e, dσ(x0)e, y)→ ψ(y))

N |= ∀y (SUBST(dσ(x0)e, dσ(x0)e, y)→ ψ(y)) práve kdyžN |= ∀y (y = dσ(dσ(x0)e)e → ψ(y))

∀y (y = dσ(dσ(x0)e)e → ψ(y)) ≡ ∀y (y = dτe → ψ(y))

N |= ∀y (y = dτe → ψ(y)) práve když N |= ψ(dτe)

Predchozí argument se opírá o sémantickou ekvivalenci jistých formulí;ekvivalence techto formulí je ale ve skutecnosti dokazatelná v PA . Napr.

PA ` (∀y (y = dτe → ψ(y)))↔ ψ(dτe)

což je treba v posledním bodu. Proto PA ` τ↔ ψ(dτe). �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 142/147


Veta 92 (1. veta o neúplnosti, Gödelova)

Lze sestrojit uzavrenou formuli %, která je pravdivá v N , ale nenídokazatelná v PA.

Dukaz. (osnova) Ukáže se, že i dukazy (tj. konecné posloupnostiformulí) je možné kódovat císly, a že existuje formule PROOF(x , y), kteráríká, že x je kódem dukazu (v PA ) pro formuli s kódem y. Dokazatelnostv PA lze pak zapsat formulí

PROVABLE(y) ≡ ∃x PROOF(x , y)

Pak pro každou uzavrenou formuli ϕ platí

PA ` ϕ práve když N |= PROVABLE(dϕe)

Dále lze ukázat

PA ` ϕ práve když PA ` PROVABLE(dϕe)

Smer ,,⇐‘‘ plyne ihned z korektnosti PA (indukcí se snadno ukáže, žejestliže PA ` ϕ, pak N |= ϕ). Opacný smer je výrazne pracnejší.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 143/147


Nyní stací aplikovat lema 91 na formuli ¬PROVABLE(x). Dostaneme taksentenci % takovou, že platí

PA ` %↔ ¬PROVABLE(d%e)

Formule % tedy ríká ,,já nejsem dokazatelná‘‘, pricemž toto tvrzení je v PAdokazatelné. Z korektnosti PA dostáváme, že

N |= %↔ ¬PROVABLE(d%e)

Pak ale musí platit N |= %; kdyby totiž N |= ¬%, dostanemeN |= PROVABLE(d%e), proto PA ` % a tedy N |= %, spor.Jelikož N |= %, platí N |= ¬PROVABLE(d%e), tedy N 6|= PROVABLE(d%e),proto PA 0 %.Formule % je tedy pravdivá v N , ale není dokazatelná v PA . �

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 144/147

Veta o neúplnosti. Tvrzení o PA v PA .

Pozorování:

Dukaz vety 92 se opírá o možnost vyjádrit jistá metatvrzení oformulích aritmetiky a teorii PA jako formule aritmetiky. Typicky lzetakto vyjádrit tvrzení, která se týkají dokazatelnosti.

Metatvrzení ,,PA ` ϕ‘‘ lze vyjádrit formulí PROVABLE(dϕe).Dokonce platí PA ` ϕ práve když PA ` PROVABLE(dϕe).

I metatvrzení ,,PA ` ϕ práve když PA ` PROVABLE(dϕe)‘‘ lzevyjádrit v PA pomocí formule

PROVABLE(dϕe)↔ PROVABLE(dPROVABLE(dϕe)e)

I tato formule je v PA dokazatelná.

Bezespornost teorie PA lze vyjádrit formulíCONSIS ≡ ¬PROVABLE(dξ ∧ ¬ξe), kde ξ je (nejaká) formule.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 145/147

Veta o neúplnosti. Tvrzení o PA v PA . (2)

Jsou ale i metatvrzení o formulích aritmetiky, která jako formulearitmetiky výjádrit nelze. Typicky se jedná o tvrzení týkající sepravdivosti.

Tvrzení ,,N |= ϕ‘‘ jako formuli aritmetiky vyjádrit nelze:Predpokládejme naopak, že existuje formule TRUE(x) taková, žeN |= ϕ práve když N |= TRUE(dϕe). Pak podle lematu 91 existujesentence τ taková, že N |= τ práve když N |= ¬TRUE(dτe).Ovšem podle výše uvedeného platí N |= τ práve kdyžN |= TRUE(dτe), což je spor.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 146/147

Veta o neúplnosti. 2. veta o neúplnosti.

Úvahy o vyjádritelnosti nekterých vlastností teorie PA formulemiaritmetiky hrají klícovou roli v dukazu následujícího tvrzení:

Veta 93 (2. veta o neúplnosti, Gödelova)

Je-li PA bezesporná, pak CONSIS není v PA dokazatelná. (Jinými slovy:v ,,dostatecne silné‘‘ teorii lze dokázat její vlastní bezespornost jen vprípade, že je tato teorie sporná.)

Dukaz. (osnova) Necht’ % je formule zkonstruovaná v dukazu vety 92(která o sobe ríká, že je nedokazatelná). Uvažme následujícímetatvrzení:

,,Jestliže PA ` %, pak platí PA ` PROVABLE(d%e) a soucasnePA ` ¬PROVABLE(d%e)‘‘

Toto tvrzení je nejen pravdivé, ale lze ho vyjádrit formulí aritmetiky, kteráje navíc dokazatelná v PA :

PA ` PROVABLE(d%e)→(PROVABLE(dPROVABLE(d%e)e)∧PROVABLE(d¬PROVABLE(d%e)e))

Proto platí také PA ` PROVABLE(d%e)→ ¬CONSIS.

Matematickálogika

Antonín Kucera

Úvod


Sylogismy





Sémantika

Plnohodnotnost

Kompaktnost

Systém L(→,¬)

Korektnost

Úplnost


Sémantika

Odvozovací systém

Veta o úplnosti



Gödeluv dukaz


29. zárí 2009 147/147

Veta o neúplnosti. 2. veta o neúplnosti. (2)

Obmenou uvedeného tvrzení dostáváme

PA ` CONSIS → ¬PROVABLE(d%e)

Kdyby PA ` CONSIS, platilo by také PA ` ¬PROVABLE(d%e) (aplikacíMP). Už dríve jsme ale ukázali (viz dukaz vety 92), že

PA ` %↔ ¬PROVABLE(d%e)

Další aplikací MP tedy dostáváme PA ` %. Výše jsme ale ukázali, žepredpoklad PA ` % implikuje, že PA je sporná. Celkem tedy dostáváme,že predpoklad PA ` CONSIS implikuje, že PA je sporná. �

Na intuitivní úrovni: druhá veta o neúplnosti ríká, že bezespornost,,dostatecne silné‘‘ teorie (napr. teorie množin) nelze v této teorii dokázat.Jediná možnost je použít metaargumenty, tj. zduvodnit bezespornostdané teorie pomocí teorie ,,vyšší‘‘. Ani bezespornost této vyšší teorienení ovšem možno prokázat v ní samé. Na nejaké úrovni nám prostenezbývá, než v bezespornost uverit, resp. ji predpokládat. Gödelovyvýsledky o neúplnosti mají tedy i svuj epistemologický význam.

Date post:	20-Jan-2021
Category:	Documents
Upload:	others
View:	19 times
Download:	0 times

Matematická logika logika Aristotelova · 2015. 5. 31. · Matematická logika Antonín Kuceraˇ...

Documents