2 - Formální systém predikátové logiky (axiomy a odvozovací pravidla, dokazatelnost, model a důsledek teorie, věty o úplnosti a kompaktnosti, prenexní tvar formulí) Flashcards
Jak lze definovat Axiomy predikátové logiky
Axiomy lze definovat pouze za použití spojek ¬ a → a kvantifikátoru ∀. Přepis existenčního kvantifikátoru na univerzální ∃xφ je logicky ekvivalentní formule ¬(∀x(¬φ))
Axiom kvantifikátoru
(∀x(φ→ψ))→(φ→(∀xψ)), x nemá volný výskyt v φ
Axiom substituce
• (∀xφ)→φ_x [t], kde t je term substituovatelný za proměnnou x
○ Říkáme, že term t je substituovatelný za proměnnou x do formule φ, jestliže x není volná v žádné podformuli tvaru (∀y)ψ, kde proměnná y má výskyt v termu t.
§ Například následující substituce neplatí:(∀x(¬∀y(x=y)))→(¬∀y(y=y))
○ Tedy, pokud náš term t obsahuje proměnnou y, která je v místě substituce vázaná, musí tam být i x vázaná.
• Substituovatelná proměnná x je taková, že žádný její volný výskyt neleží v oboru kvantifikátoru proměnné y, která je obsažená v substituovaném termu. Např. term S(y) není substituovatelný za term x ve formuli x→∃y(x=S(y))
Axiomy rovnosti (je-li L jazyk s rovností)
- x=x je axiom (x je proměnná)
- x_1=y_1→(x_2=y_2→(…(x_n=y_n→(f(x_1,…,x_n )=f(y_1,…,y_n ))…))) je axiom (f je funkční symbol četnosti n)
- x_1=y_1→(x_2=y_2→(…(x_n=y_n→(p(x_1,…,x_n )=p(y_1,…,y_n ))…))) je axiom (p je predikátový symbol četnosti n)
Gödelova věta o úplnosti predikátové logiky, Věta o kompaktnosti pro predikátovou logiku, důsledek teorie
Formule φ je dokazatelná v teorii T, právě když φ platí v každém modelu T.
Větou o úplnosti se obvykle nazývá následující ekvivalence. Implikace zleva doprava se někdy nazývá věta o korektnosti.
teorie = množina formulí (speciální axiomy teorie) + axiomy dané logiky
model teorie = realizace jazyka ve které jsou všechny formule dané teorie splněné (pro jakékoliv ohodnocení predikátových proměnných)
důsledek teorie = formule dokazatelna z/v teorie
Godelova věta o úplnosti: teorie dokazuje formuli, pokud ta formule platí v každým modelu té teorie
Věta o kompaktnosti pro predikátovou logiku: Pokud každá konečná podteorie teorie T má model, pak teorie T má model
Skolemizace, Skolemova normální forma
Skolemizace je převod formulí na formule bez existenčních kvantifikátorů v jazyce, který je rozšířen o tzv. Skolemovy funkce; zachovává splnitelnost.
Skolemova normální forma je prenexová normální forma pouze s univerzálními kvantifikátory.
Ideí je transformace formule (∀x_1)…(∀x_n)(∃y)(P(x_1,…,x_n,y)) na formuli (∀x_1 )…(∀x_n )P(x_1,…,f(x_1,…,x_n ))
• podmínku na existenci y můžeme chápat jako podmínku na existenci zobrazení f (tzv. výběrové funkce), která pro konkrétní hodnoty x_1,…,x_n konstruuje požadované y=f(x_1,…,x_n).
Například mějme čísla s + : ∀x∃y :x+y=0 převedeme na ∀x :x+f(x)=0, kde interpretace funkce f je, že vrátí opačné číslo k číslu x (unární operátor mínus).
Důkaz
libovolná posloupnost formulí jazyka L, každá formule je buď axiom nebo ji lze odvodit z některých předchozích formulí.
Formule φ je dokazatelná z předpokladů T
jestliže existuje důkaz z předpokladů T. Píšeme T⊢φ.
Věta o korektnosti, uzávěr formule, věta o úzávěru
Věta o korektnosti: Libovolná formule jazyka L dokazatelná v predikátové logice 1. řádu je logicky platnou formulí, tj. je splněna v každé realizaci jazyka L.
Pravidlo ∀: Je-li ⊢φ→ψ a proměnná x nemá volný výskyt ve φ, pak ⊢φ→(∀xψ).
Pravidlo ∃: Je-li ⊢φ→ψ a proměnná x nemá volný výskyt ve ψ, pak ⊢(∃xφ)→ψ.
Uzávěr formule: Jsou-li x1,…,xn všechny volné proměnné ve formuli φ, pak formuli ∀x_1…∀x_n φ nazveme uzávěrem formule φ.
Věta o uzávěru: Je-li T množina formulí, je-li φ^′ uzávěr formule φ, pak T⊢φ právě když T⊢φ^′.
Distribuce kvantifikátorů: Je-li ⊢φ→ψ, potom ⊢(∀xφ)→(∀xψ), ⊢(∃xφ)→(∃xψ).
Věta o dedukci: Nechť T je množina formulí jazyka L, nechť φ je uzavřená formule, ψ je libovolná formule jazyka L. Potom T⊢φ→ψ právě tehdy, když T,φ⊢ψ.
