Formální systém predikátové logiky

FITwiki

Axiomy a odvozovací pravidla

Axiom

A → (B → A)

(A → (B → C)) → ((A → B) → (A → C))

(¬B → ¬A) → (A → B)

Modus ponens (pravidlo odloučení) A → B můžeme přepsat na A ⊢ B1) A dokazuje B .

Věta o dedukci je Modus ponens obráceně.

Pravidlo zobecnění znamená, že někam připíšeš ∀x

Axiom kvantifikátoru – ∀x(A ⇒ B) → (A ⇒ ∀xB)

Dokazatelnost

Důkaz je 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 ⊢ φ.

Model a důsledek teorie

Teorie v jazyce L je každá množina T formulí jazyka L. Prvky T se nazývají (vlastní) axiomy T. Jazyk L je množina znaků, pomocí nichž se vytvářejí formule T a odvozené formule.

Logika je potom odvozovací systém pro popis matematických vět.

Věty o úplnosti a kompaktnosti

Prenexní tvar formulí

Prenex normal form

Odstranění zbytečných kvantifikátorů2) ∀xB(y)

Zbavení se spojek kromě ∧, ∨ a ¬

Přejmenování proměnných

Přesun kvantifikátorů doleva (a odstranění neatomických negací)