===== Zadání =====
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.

===== Vypracování =====
**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).

==== Výroková logika ====

=== Syntaxe ===
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ů ∧, ∨, →.

=== Sémantika ===
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 //**F**//1, ···, //**F**//k pro uvedené výrokové funkce.
  * V definici vytvořující posloupnosti formule požadujeme, aby ψi bylo buď výrokovou proměnnou nebo tvaru //**F**//j(ψ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**//(//**F**//1, ···, //**F**//k) 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**//(//**F**//1, ···, //**F**//k) je plnohodnotný, jestliže pro každou výrokovou funkci F existuje formule φ systému //**L**//(//**F**//1, ···, //**F**//k) 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 //**l**//1 ∨ ··· ∨ //**l**//n, kde n ≥ 1 a každé //**l**//i 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á.

=== Lukasiewiczův odvozovací systém *L*(→, ¬) ===

Schémata axiomů:
  * A1: φ → (ψ → φ)
  * A2: (φ → (ψ → ξ)) → ( (φ → ψ) → (φ → ξ) )
  * A3: (¬φ → ¬ψ) → (ψ → φ)

Odvozovací pravidlo:
  * MP (modus ponens): Z φ a φ → ψ odvoď ψ.

== Důkazy ==
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 ⊢ ψ → φ.

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

== Úplnost ==
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 ====
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.

=== Syntaxe ===
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.

=== Sémantika ===
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.

=== Odvozovací systém ===
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.

=== Důkazy ===
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 ∪ {ψ} ⊢ φ.

== Korektnost ==
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.

== Úplnost ==
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 κ.

==== Gödelovy věty o neúplnosti ====
Alan Turing: Definoval pojem Turingova stroje a s jeho pomocí ukázal, že problém pravdivosti formulí prvního řádu je nerozhodnutelný.


===== Předměty =====
  * [[https://is.muni.cz/auth/predmet/fi/MA007|MA007 Matematická logika]]

===== Související otázky =====


~~DISCUSSION~~