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

1
Q

Jak lze definovat Axiomy predikátové logiky

A

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(¬φ))

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
2
Q

Axiom kvantifikátoru

A

(∀x(φ→ψ))→(φ→(∀xψ)), x nemá volný výskyt v φ

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
3
Q

Axiom substituce

A

• (∀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))

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
4
Q

Axiomy rovnosti (je-li L jazyk s rovností)

A
  • 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)
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
5
Q

Gödelova věta o úplnosti predikátové logiky, Věta o kompaktnosti pro predikátovou logiku, důsledek teorie

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
6
Q

Skolemizace, Skolemova normální forma

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

Důkaz

A

libovolná posloupnost formulí jazyka L, každá formule je buď axiom nebo ji lze odvodit z některých předchozích formulí.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

Formule φ je dokazatelná z předpokladů T

A

jestliže existuje důkaz z předpokladů T. Píšeme T⊢φ.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

Věta o korektnosti, uzávěr formule, věta o úzávěru

A

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,φ⊢ψ.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly