Matematická logika. Výroková a predikátová logika, syntaxe, sémantika. Odvozovací systémy, formální důkazy. Korektnost a úplnost odvozovacích systémů. Gödelovy věty o neúplnosti.

Upozornění: bez nároku na úplnost a korektnost. Podle hesla „lepší něco než nic“. Ale snaha byla o co nejlepší výsledek.
Poznámka: asi nejnáročnější otázka (a u komise vděčná). Doporučuji jí věnovat dostatečný čas (měsíc+?) a projít si poznámky ve slajdech (a možno i důkazy).

Abecedu výrokové logiky tvoří:
a) spočetně mnoho znaků pro výrokové proměnné: A, B, C, … b) logické spojky ∧, ∨, →, ¬
c) závorky (, )

Formule výrokové logiky je slovo φ nad abecedou, pro které existuje konečná vytvořující posloupnost slov ψ1, ···, ψk, kde k ≥ 1, ψk je φ, a pro každé 1 ≤ i ≤ k má slovo ψi jeden z následujících tvarů:
a) výroková proměnná,
b) ¬ψj pro nějaké 1 ≤ j < i,
c) (ψj ◦ ψj) pro nějaká 1 ≤ j, j < i, kde ◦ je jeden ze symbolů ∧, ∨, →.

Pravdivostní ohodnocení (valuace) je zobrazení v, které každé výrokové proměnné přiřadí hodnotu 0 nebo 1.

(Indukcí k délce vytvořující posloupnosti lze každou valuaci v jednoznačně rozšířit na všechny výrokové formule.)

Výroková formule φ je:

• pravdivá při valuaci v, pokud v(φ) = 1;
• splnitelná, jestliže existuje valuace v taková, že v(φ) = 1;
• tautologie (také (logicky) pravdivá), jestliže v(φ) = 1 pro každou valuaci v.

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

Formule φ a ψ jsou ekvivalentní, psáno φ ≈ ψ, právě když pro každou valuaci v platí, že v(φ) = v(ψ).

Formule φ je tautologickým důsledkem souboru formulí T, psáno T ⊨ φ, jestliže v(φ) = 1 pro každou valuaci v takovou, že v(ψ) = 1 pro každou formuli ψ ze souboru T. Jestliže T ⊨ φ pro prázdný soubor T, píšeme krátce ⊨ φ.

Výroková funkce je funkce F: {0, 1}^n → {0, 1}, kde n ≥ 1. (například spojka)

Nechť F1, ···, Fk je konečný soubor výrokových funkcí. Definujeme formální logický systém L(F1 , ···, Fk), kde:

• Abeceda je tvořena znaky pro výrokové promenné, závorkami a znaky F1, ···, Fk pro uvedené výrokové funkce.
• V definici vytvořující posloupnosti formule požadujeme, aby ψi bylo buď výrokovou proměnnou nebo tvaru Fj(ψj1, ···, ψjn), kde 1 ≤ j1, ···, jn < i a n je arita Fj.
• Valuace rozšíříme z výrokových proměnných na formule předpisem v(F(ψ1, ···, ψn)) = F(v(ψ1), ···, v(ψn))

[pomocná definice k plnohodnotnosti]
Nechť φ je formule L(F1, ···, Fk) a nechť X1, ···, Xn je vzestupně uspořádaná posloupnost (vzhledem k lib. pevné lin. usp. ⊑) všech výrokových proměnných, které se ve φ vyskytují. Formule φ jednoznačně určuje výrokovou funkci Fφ: {0, 1}^n → {0, 1} danou předpisem Fφ(u) = v_u(φ), kde v_u je valuace definovaná takto: v_u(Xi) = u(i) pro každé 1 ≤ i ≤ n; = 0 pro ostatní proměnné „Xi“

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

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

Literál je formule tvaru X nebo ¬X, kde X je výroková promenná;
Klauzule je formule tvaru l1 ∨ ··· ∨ ln, kde n ≥ 1 a každé li je literál. (Duální s ∧.)

Nechť T je soubor formulí výrokové logiky. T je splnitelný, právě když každá konečná část T je splnitelná.

Schémata axiomů:

• A1: φ → (ψ → φ)
• A2: (φ → (ψ → ξ)) → ( (φ → ψ) → (φ → ξ) )
• A3: (¬φ → ¬ψ) → (ψ → φ)

Odvozovací pravidlo:

• MP (modus ponens): Z φ a φ → ψ odvoď ψ.

Buď T soubor formulí.
Důkaz formule ψ z předpokladu T je konečná posloupnost formulí φ1, ···, φk, kde φk je ψ a pro každé φi, kde 1 ≤ i ≤ k, platí alespoň jedna z následujících podmínek:

• φi je prvek T;
• φi je instancí jednoho ze schémat A1–A3;
• φi vznikne aplikací pravidla MP na formule φm, φn pro vhodné 1 ≤ m, n < i.

Formule ψ je dokazatelná z předpokladu T, psáno T ⊢ ψ, jestliže existuje důkaz ψ z předpokladu T. Jestliže T ⊢ ψ pro prázdné T, říkáme, že ψ je dokazatelná a píšeme ⊢ ψ.

Dedukce: Nechť φ, ψ jsou formule a T soubor formulí. Pak T ∪ {ψ} ⊢ φ právě když T ⊢ ψ → φ.

Necht’ φ je formule a T soubor formulí. Jestliže T ⊢ φ, pak T ⊨ φ.

Nechť v je valuace a φ formule. Jestliže v(φ) = 1, označuje symbol φ^v formuli φ. Jinak φ^v označuje formuli ¬φ.

Churchovo Lemma: Nechť v je valuace, φ formule, a {X1, ···, Xk} konečný soubor výrokových proměnných, kde všechny proměnné vyskytující se ve φ jsou mezi {X1, ···, Xk}. Pak {X1^v, ···, Xk^v} ⊢ φ^v.

Nechť φ je formule a T soubor formulí. Jestliže T ⊨ φ, pak T ⊢ φ.

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

Jazyk (stejně jako jazyk s rovností) je systém predikátových symbolů a funkčních symbolů, kde u každého symbolu je dána jeho četnost (arita), která je nezáporným celým číslem.

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

• Znaky pro proměnné x, y, z, …, kterých je spočetně mnoho.
• Mimologické symboly, tj. predikátové a funkční symboly jazyka L.
• Je-li L jazyk s rovností, obsahuje abeceda speciální znak = pro rovnost.
• Logické spojky → a ¬.
• Symbol ∀ pro univerzální kvantifikátor.
• Závorky ( a ).

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

• proměnná,
• f(ti1, ···, tin), kde 1 ≤ i1, ···, in < k, f je funkční symbol jazyka L, a n je arita f.

Term je uzavřený, jestliže neobsahuje proměnné.

Formule predikátového počtu jazyka L je slovo φ nad abecedou predikátové logiky pro jazyk L, pro které existuje vytvořující posloupnost slov ψ1, ···, ψk, kde k ≥ 1, ψk je φ a pro každé 1 ≤ i ≤ k má slovo ψi jeden z následujících tvarů:

• P(t1, ···, tn), kde P je predikátový symbol jazyka L arity n a t1, ···, tn jsou termy jazyka L.
• t1 = t2, je-li L jazyk s rovností a t1, t2 jsou termy jazyka L.
• ¬ψj pro nějaké 1 ≤ j < i,
• (ψj → ψj') pro nějaká 1 ≤ j, j' < i,
• ∀x ψj , kde x je proměnná a 1 ≤ j < i.

Každý výskyt proměnné ve formuli predikátového počtu je buď volný, nebo vázaný podle následujícího induktivního předpisu:

• Ve formuli tvaru P(t1, ···, tn) jsou všechny výskyty proměnných volné.
• Výrokové spojky nemění charakter výskytu proměnných, tj. je-li daný výskyt proměnné ve formuli ψ volný (resp. vázaný), je odpovídající výskyt ve formulích ¬ψ, φ → ψ, ψ → φ rovněž volný (resp. vázaný).
• Ve formuli ∀x ψ je každý výskyt proměnné x (včetně výskytu za kvantifikátorem) vázaný; byl-li výskyt proměnné ruzné od x volný (resp. vázaný) ve formuli ψ, je odpovídající výskyt ve formuli ∀x ψ rovněž volný (resp. vázaný).

Proměnná se nazývá volnou (resp. vázanou) ve formuli, má-li v ní volný (resp. vázaný) výskyt.
Formule je otevřená, jestliže v ní žádná proměnná nemá vázaný výskyt.
Formule je uzavřená (také sentence), jestliže v ní žádná proměnná nemá volný výskyt.
Zápis φ(x1, ···, xn) značí, že všechny volné proměnné ve formuli φ jsou mezi x1, ···, xn (nemusí nutně platit, že každá z těchto proměnných je volná ve φ).
Univerzální uzávěr formule φ je formule tvaru ∀x1 ··· ∀xn φ, kde x1, ···, xn jsou právě všechny volné proměnné formule φ.

Term t je substituovatelný za proměnnou x ve formuli φ, jestliže žádný výskyt proměnné v termu t se nestane vázaným po provedení substituce termu t za každý volný výskyt proměnné x ve formuli φ. Je-li t substituovatelný za x ve φ, značí zápis φ(x/t) formuli, která vznikne nahrazením každého volného výskytu x ve φ termem t.
φ(x1/t1, ···, xn/tn) = φ(x1/z1) ··· (xn/zn)(z1/t1) ··· (zn/tn), kde z1, ··· , zn jsou (ruzné) proměnné, které se nevyskytují v t1, ···, tn ani mezi x1, ···, xn.

Realizace M jazyka L je zadána

• neprázdným souborem M, nazývaným univerzem (případně nosičem). Prvky univerza nazýváme individui.
• přiřazením, které každému n-árnímu predikátovému symbolu P přiřadí n-ární relaci P_M na M.
• přiřazením, které každému m-árnímu funkčnímu symbolu přiřadí funkci f_M : M^m → M.

Ohodnocení je zobrazení přiřazující proměnným prvky univerza M.

Realizaci termu *t* při ohodnocení *e* v realizaci M, psáno t^M [e] (případně jen t[e], je-li M jasné z kontextu), definujeme induktivně takto:

• x[e] = e(x)
• f(t1, ···, tm)[e] = f_M (t1[e], ···, tm[e])

(pro m = 0 je na pravé straně uvedené definující rovnosti f_M (∅)).

Tarski: Buď M realizace L, e ohodnocení a φ formule predikátového počtu jazyka L. Ternární vztah M ⊨ φ[e] definujeme indukcí ke struktuře φ:

• M ⊨ P(t1, ···, tm)[e] právě když (t1[e], ···, tm[e]) ∈ P_M.
• Jestliže L je jazyk s rovností, definujeme M ⊨ (t1 = t2)[e] právě když t1[e] a t2[e] jsou stejná individua.
• M ⊨ ¬ψ[e] právě když není M ⊨ ψ[e].
• M ⊨ (ψ → ξ)[e] právě když M ⊨ ξ[e], nebo není M ⊨ ψ[e].
• M ⊨ ∀x ψ[e] právě když M ⊨ ψ[e(x/a)] pro každý prvek *a* univerza M.

Jestliže M ⊨ φ[e], říkáme, že φ je pravdivá v M při ohodnocení e.
Jestliže M ⊨ φ[e] pro každé e, je φ pravdivá v M, psáno M ⊨ φ.

Buď L jazyk (příp. jazyk s rovností).

• Teorie (s jazykem L) je soubor T formulí predikátového počtu jazyka L. Prvky T se nazývají axiómy teorie T.
• Realizace M jazyka L je model teorie T, psáno M ⊨ T, jestliže M ⊨ φ pro každé φ z T.
• Teorie je splnitelná, jestliže má model.
• Je-li M realizace jazyka L, pak Th(M) označuje teorii tvořenou právě všemi uzavřenými formulemi, které jsou v M pravdivé.
• Formule φ je sémantickým důsledkem teorie T, psáno T ⊨ φ, jestliže φ je pravdivá v každém modelu teorie T.

Schémata výrokových axiómů:

• P1: φ → (ψ → φ)
• P2: (φ → (ψ → ξ)) → ( (φ → ψ) → (φ → ξ) )
• P3: (¬φ → ¬ψ) → (ψ → φ)

Schéma axiómu specifikace:

• P4: ∀x φ → φ(x/t), kde t je substituovatelný za x ve φ.

Schéma axiómu distribuce:

• P5: (∀x (φ → ψ)) → (φ → ∀x ψ), kde x nemá volný výskyt ve φ.

Odvozovací pravidla:

• MP: Z φ a φ → ψ odvod’ ψ. (modus ponens)
• GEN: Z φ odvod’ ∀x φ. (generalizace)

Je-li L jazyk s rovností, přidáme dále následující axiómy rovnosti:

• R1: x = x
• R2: (x1 = y1 ∧ ··· ∧ xn = yn ∧ P(x1, ···, xn)) → P(y1, ···, yn), kde P je predikátový symbol arity n.
• R3: (x1 = y1 ∧ ··· ∧ xm = ym) → (f(x1, ···, xm) = f(y1, ···, ym)), kde f je funkční symbol arity m.

Buď T teorie jazyka L. Dukaz formule ψ v teorii T je konečná posloupnost formulí φ1, ···, φk, kde φk je ψ a pro každé φi, kde 1 ≤ i ≤ k, platí alespoň jedna z následujících podmínek:

• φi je prvek T;
• φi je instancí jednoho ze schémat P1–P5;
• L je jazyk s rovností a φi je instancí jednoho ze schémat R1–R3;
• φi vznikne aplikací MP na formule φm, φn pro vhodné 1 ≤ m, n < i;
• φi vznikne aplikací GEN na formuli φm pro vhodné 1 ≤ m < i.

Buď T teorie jazyka L.

• Formule ψ je dokazatelná v teorii T, psáno T ⊢ ψ, jestliže existuje důkaz ψ v T. Jestliže T ⊢ ψ pro prázdné T, říkáme, že ψ je dokazatelná a píšeme ⊢ ψ.
• Formule ψ je vyvratitelná v teorii T, jestliže T ⊢ ¬ψ.
• Teorie T je sporná (též nekonzistentní), jestliže každá formule predikátové logiky jazyka L je v T dokazatelná.
• Teorie je bezesporná (též konzistentní), jestliže není sporná.

Dedukce: Nechť T je teorie jazyka L, ψ uzavřená formule jazyka L a φ (libovolná) formule jazyka L. Pak T ⊢ ψ → φ právě když T ∪ {ψ} ⊢ φ.

Nechť T je teorie a φ formule jazyka teorie T. Jestliže T ⊢ φ, pak T ⊨ φ.

Následující tvrzení jsou ekvivalentní:

• Pro každou teorii T a pro každou formuli φ jazyka teorie T platí, že jestliže T ⊨ φ, pak T ⊢ φ.
• Každá bezesporná teorie má model.

Teorie S je rozšíření teorie T, jestliže jazyk teorie S obsahuje jazyk teorie T a v teorii S jsou dokazatelné všechny axiómy teorie T.
Rozšíření S teorie T se nazývá konzervativní, jestliže každá formule jazyka teorie T, která je dokazatelná v S, je dokazatelná i v T.
Teorie S a T jsou ekvivalentní, jestliže S je rozšířením T a současně T je rozšířením S.

Věta o konstantách: Nechť S je rozšíření T vzniklé obohacením jazyka teorie T o nové navzájem různé konstanty c1, ···, ck (nové axiómy nepřidáváme), a nechť x1, ···, xk jsou navzájem různé proměnné. Pak pro každou formuli φ jazyka teorie T platí, že T ⊢ φ právě když S ⊢ φ(x1/c1, ···, xk/ck).

Teorie T je henkinovská, jestliže pro každou formuli φ jazyka teorie T s jednou volnou proměnnou x existuje v jazyce teorie T konstanta c taková, že T ⊢ ∃x φ → φ(x/c).

Teorie T je úplná, jestliže je bezesporná a pro každou uzavřenou formuli φ jejího jazyka platí buď T ⊢ φ nebo T ⊢ ¬φ.

Buď T teorie a φ(x) formule jejího jazyka. Je-li S rozšíření T, které vznikne přidáním nové konstanty c_φ a formule ∃x φ → φ(x/c_φ), pak S je konzervativní rozšíření T.

Ke každé teorii existuje henkinovská teorie, která je jejím konzervativním rozšířením.

Věta o zúplňování teorií: Ke každé bezesporné teorii existuje její rozšíření se stejným jazykem, které je úplnou teorií.

Kanonická struktura: Buď T teorie, kde jazyk teorie T obsahuje alespoň jednu konstantu. Kanonická struktura teorie T je realizace M jazyka teorie T, kde:

• univerzum M je tvořeno všemi uzavřenými termy jazyka teorie T;
• realizace funkčního symbolu *f* arity *n* je funkce f_M , která uzavřeným termům t1, ···, tn přiřadí uzavřený term f(t1, ···, tn);
• realizace predikátového symbolu *P* arity *m* je predikát P_M definovaný takto: P_M (t1, ···, tm) platí právě když T ⊢ P(t1, ···, tm).

Věta o kanonické struktuře: Nechť T je úplná henkinovská teorie a nechť jazyk teorie T je jazykem bez rovnosti. Pak kanonická struktura teorie T je modelem T.

Nechť T je úplná henkinovská teorie a nechť jazyk teorie T je jazykem s rovností. Pak T má model.

Každá bezesporná teorie má model. Pro každou teorii T a každou formuli jejího jazyka tedy platí, že jestliže T ⊨ φ, pak T ⊢ φ.

Věta o kompaktnosti: Teorie T má model, právě když každá její podteorie s konečně mnoha axiómy (a s minimálním jazykem, v němž jsou tyto axiómy formulovatelné) má model.

= Löwenheimova-Skolemova věta =
Nechť T je teorie a nechť pro každé n ∈ N existuje model teorie T, jehož nosič má mohutnost alespoň *n*. Pak T má nekonečný model.

L-S V.: Nechť T je teorie s jazykem L, která má nekonečný model. Nechť κ je nekonečný kardinál takový, že κ ≥ |L|. Pak T má model mohutnosti κ.

Alan Turing: Definoval pojem Turingova stroje a s jeho pomocí ukázal, že problém pravdivosti formulí prvního řádu je nerozhodnutelný.

• MA007 Matematická logika