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

Výroková formule

Nechť P je neprázdná množina symbolů nazývaných atomické výrokové formule. Abecedou jazyka výrokové logiky L_P jsou prvky množiny P, symbol ¬ pro negaci a → pro implikaci. Výrokové formule jazyka L_P definujeme následovně:

1. Každá atomická výroková formule je též výroková formule.
2. Jestliže A je výroková formule, je i (¬A) výroková formule.
3. Jsou-li A, B výrokové formule, je i (A → B) výroková formule.
4. Formule vznikne konečným užitím 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)$
• implikace

Pravdivost

Pravdivostní ohodnocení atomických formulí je zobrazení v : P → {0,1}. Rozšíření w na výrokové formule definujeme takto:

1. w(A) = v(A) je-li A atomická formule
2. w(¬A) = 1 je-li w(A) = 0
3. w(¬A) = 0 je-li w(A) = 1
4. w(A → B) = 0 pokud w(A) = 1 a w(B) = 0
5. w(A → B) = 1 pokud w(A) = 0 nebo w(B) = 1

Odvozování

Hilbertův axiomatický systém

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

Odvozovací pravidlo

• (pravidlo Modus ponens) Jestliže A platí a A → 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.

Jestliže existuje důkaz výrokové formule $A$, říkáme o této formuli, že je dokazatelná.

Externí odkazy

• Obrázky, zvuky či videa k tématu výroková logika ve Wikimedia Commons
• Volně stažitelná skripta z předmětu Výroková a predikátová logika na MFF UK od Petra Štěpánka

Autoritní data: GND: 4136098-9 | PSH: 7100