Výroková logika

V matematice a logice se pojmem výroková logika označuje formální odvozovací systém, ve kterém atomické formule tvoří výrokové proměnné (na rozdíl od predikátové logiky). Výroková logika je, stejně jako fuzzy logika, podoborem matematické logiky.

Výroková logika se skládá ze

syntaktických pravidel – určují, kdy je formule správně utvořená,
odvozovacích pravidel – určují, jak z jedněch formulí správně odvozovat další stále validní důsledkové formule,
(nejvýše spočetné) množiny axiomů a axiomatických schémat.

Syntaxe

Nechť $P$ je neprázdná množina symbolů nazývaných atomické výrokové formule (též výrokové proměnné). Abecedou jazyka výrokové logiky $L_{P}$ jsou prvky množiny $P$ , symbol $\neg$ pro negaci a $\Rightarrow$ pro implikaci. Výrokové formule jazyka $L_{P}$ definujeme následovně:

Každá atomická výroková formule je též výroková formule.
Jestliže $A$ je výroková formule, je i $\neg A$ výroková formule.
Jsou-li $A,B$ výrokové formule, je i $A\Rightarrow B$ výroková formule.
Formule vznikne konečným počtem užití pravidel 2 a 3.

Pro zkrácení zápisu dále používáme označení

Konjunkce: $A\land B$ pro $\neg (A\Rightarrow \neg B)$
Disjunkce: $A\vee B$ pro $\neg A\Rightarrow B$
Ekvivalence: $A\Leftrightarrow B$ pro $(A\Rightarrow B)\land (B\Rightarrow A)$
Exkluzivní disjunkce: $A\oplus B$ pro $\neg (A\Leftrightarrow B)$
Tautologie: $\top$ pro $A\Rightarrow A$
Kontradikce: $\bot$ pro $\neg (A\Rightarrow A)$
NAND: $A\uparrow B$ pro $\neg (A\land B)$
NOR: $A\downarrow B$ pro $\neg (A\vee B)$
Obrácená implikace: $A\Leftarrow B$ pro $B\Rightarrow A$

Sémantika

Pravdivostní ohodnocení (též interpretace) atomických formulí je jakékoliv zobrazení $v:P\to \{0,1\}$ . Rozšíření $w$ na výrokové formule definujeme induktivně takto:

$w(A)=v(A)$ je-li $A$ atomická formule
$w(\neg A)=1-w(A)$
$w(A\Rightarrow B)=\max\{w(\neg A),w(B)\}$

Pokud pro formuli $A$ a ohodnocení $w$ platí, že $w(A)=1$ , říkáme, že formule $A$ je v ohodnocení $w$ pravdivá, což značíme též jako $w\models A$ . V opačném případě říkáme, že formule $A$ je v ohodnocení $w$ nepravdivá.

O formuli $A$ říkáme, že je splnitelná, pokud existuje takové $w$ , že platí $w(A)=1$ (též značeno $w\models A$ ). V opačném případě o formuli $A$ říkáme, že je nesplnitelná.

O formuli $B$ říkáme, že je sémantickým důsledkem formule $A$ , značeno $A\models B$ pokud pro každé $w$ , takové že $w\models B$ platí i $w\models A$ . Tato relace je částečným uspořádáním výrokových formulí.

Odvozování

Pro výrokovou logiku můžeme definovat jednoduchý deduktivní dokazovací systém sestávající ze tří schémat pro tvorbu axiomů a jediného odvozovacího pravidla.

Hilbertův axiomatický systém

Pro jakékoliv formule $A,B,C$ jsou následující formule axiomy:

$A\Rightarrow (B\Rightarrow A)$
$(A\Rightarrow (B\Rightarrow C))\Rightarrow ((A\Rightarrow B)\Rightarrow (A\Rightarrow C))$
$(\neg B\Rightarrow \neg A)\Rightarrow (A\Rightarrow B)$

Odvozovací pravidlo

Stačí nám jediné pravidlo, tzv. Modus ponens: Jestliže $A$ platí a $A\Rightarrow B$ platí, pak $B$ platí.

Důkaz

Důkazem nazveme konečnou posloupnost $A_{1},\ldots ,A_{n}$ , jestliže pro každé $i\leq n$ je $A_{i}$ buď závěr odvozovacího pravidla, jehož předpoklady jsou mezi $A_{1}$ a $A_{i-1}$ , nebo axiom.