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á formuleEditovat
Nechť P je neprázdná množina symbolů nazývaných atomické výrokové formule. Abecedou jazyka výrokové logiky LP jsou prvky množiny P, symbol ¬ pro negaci a → pro implikaci. Výrokové formule jazyka LP definujeme následovně:
- Každá atomická výroková formule je též výroková formule.
- Jestliže A je výroková formule, je i (¬A) výroková formule.
- Jsou-li A, B výrokové formule, je i (A → B) výroková formule.
- 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: pro
- disjunkce: pro
- ekvivalence: pro
- implikace
PravdivostEditovat
Pravdivostní ohodnocení atomických formulí je zobrazení v : P → {0,1}. Rozšíření w na výrokové formule definujeme takto:
- w(A) = v(A) je-li A atomická formule
- w(¬A) = 1 je-li w(A) = 0
- w(¬A) = 0 je-li w(A) = 1
- w(A → B) = 0 pokud w(A) = 1 a w(B) = 0
- w(A → B) = 1 pokud w(A) = 0 nebo w(B) = 1
OdvozováníEditovat
Hilbertův axiomatický systémEditovat
- A → (B → A)
- (A → (B → C)) → ((A → B) → (A → C))
- (¬B → ¬A) → (A → B)
Odvozovací pravidloEditovat
- (pravidlo Modus ponens) Jestliže A platí a A → B platí, pak B platí.
DůkazEditovat
Důkazem nazveme konečnou posloupnost , jestliže pro každé je buď závěr odvozovacího pravidla, jehož předpoklady jsou mezi a , nebo axiom.
Jestliže existuje důkaz výrokové formule , říkáme o této formuli, že je dokazatelná.
Externí odkazyEditovat
- 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