====== Jazyk a sémantika predikátové logiky ======
===== Termy =====
[[wp>Term (logic)]]

Termy jsou:
  * Konstanty (0, 1, //π//, ...)
  * Proměnné (//x//, //y//, //z//, ...)
  * Funkční symboly (+, /, //f//, ...)
===== Formule =====
[[wp>Well-formed formula]]

Formule jsou termy a:
  * Predikétové symboly (<, >, =, ...) (pokud tam není nic víc, jsou to **[[wp>Atomic formula|atomické formule]]**)
  * Logické spojky a pomocné symboly (∧, ∨, (), ...)
  * Kvantifikátory (∃, ∀)
===== Realizace jazyka =====
[[wp>Interpretation (logic)]]

**Realizace** definuje konstanty, funkční symboly, predikátové symboly. Ne proměnné! Dostáváme tedy něco jako "předpis" který čeklá na dosazení za proměnné.

Když už dosadíme za proměnné, provádíme **ohodnocení proměnných**.
===== Pravdivost formulí =====
[[wp>Satisfiability]], [[wp>Validity]]

**Tautologie** je formule platná v každé realizaci, **kontradikce** obdobně.

Formule je **splnitelná**, pokud existuje nějaká realizace a ohodnocení proměnných ve kterém je platná.

Formule je **logicky platná v nějaké realizaci** pokud je úplně jedno jak ohodnotím proměnné a vždy to bude pravdivé.

Formule jsou **ekvivalentní** pokud pro libovolné realizace (ale pro obě formule stejné) a pro libovolné ohodnocení (opět stejné pro obě formule) dávají vždy stejné výsledky.