====== Formální systém predikátové logiky ======
[[http://wiki.fituska.eu/index.php/Form%C3%A1ln%C3%AD_syst%C3%A9m_predik%C3%A1tov%C3%A9_logiky|FITwiki]]
===== Axiomy a odvozovací pravidla =====
[[wp>Axiom]]
  - //A// → (//B// → //A//)
  - (//A// → (//B// → //C//)) → %%((%%//A// → //B//) → (//A// → //C//%%))%%
  - (¬//B// → ¬//A//) → (//A// → //B//)
  * **[[wp>Modus ponens]]** (pravidlo odloučení) //A// → //B// můžeme přepsat na //A// ⊢ //B//((//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 =====
**[[wp>Formal proof|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 =====
**[[wp>Theory (mathematical logic)|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í =====
[[wp>Prenex normal form]]
  - Odstranění zbytečných kvantifikátorů((∀//xB//(//y//%%)%%))
  - Zbavení se spojek kromě ∧, ∨ a ¬
  - Přejmenování proměnných
  - Přesun kvantifikátorů doleva (a odstranění neatomických negací)