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

FITwiki

Axiom

1. A → (B → A)
2. (A → (B → C)) → ((A → B) → (A → C))
3. (¬B → ¬A) → (A → B)

• Modus ponens (pravidlo odloučení) A → B můžeme přepsat na A ⊢ 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)

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

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.

Prenex normal form

1. Odstranění zbytečných kvantifikátorů²⁾
2. Zbavení se spojek kromě ∧, ∨ a ¬
3. Přejmenování proměnných
4. Přesun kvantifikátorů doleva (a odstranění neatomických negací)