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
Nechť P {\displaystyle P} jazyka výrokové logiky L P {\displaystyle L_{P}} jsou prvky množiny P {\displaystyle P} , symbol ¬ {\displaystyle \neg } pro negaci a ⇒ {\displaystyle \Rightarrow } pro implikaci. Výrokové formule jazyka L P {\displaystyle L_{P}} definujeme následovně:
je neprázdná množina symbolů nazývaných atomické výrokové formule (též výrokové proměnné). AbecedouPro zkrácení zápisu dále používáme označení
Pravdivostní ohodnocení (též interpretace) atomických formulí je jakékoliv zobrazení v : P → { 0 , 1 } {\displaystyle v:P\to \{0,1\}} . Rozšíření w {\displaystyle w} na výrokové formule definujeme induktivně takto:
Pokud pro formuli A {\displaystyle A}
a ohodnocení w {\displaystyle w} platí, že w ( A ) = 1 {\displaystyle w(A)=1} , říkáme, že formule A {\displaystyle A} je v ohodnocení w {\displaystyle w} pravdivá, což značíme též jako w ⊨ A {\displaystyle w\models A} . V opačném případě říkáme, že formule A {\displaystyle A} je v ohodnocení w {\displaystyle w} nepravdivá.O formuli A {\displaystyle A} splnitelná, pokud existuje takové w {\displaystyle w} , že platí w ( A ) = 1 {\displaystyle w(A)=1} (též značeno w ⊨ A {\displaystyle w\models A} ). V opačném případě o formuli A {\displaystyle A} říkáme, že je nesplnitelná.
říkáme, že jeO formuli B {\displaystyle B} sémantickým důsledkem formule A {\displaystyle A} , značeno A ⊨ B {\displaystyle A\models B} pokud pro každé w {\displaystyle w} , takové že w ⊨ B {\displaystyle w\models B} platí i w ⊨ A {\displaystyle w\models A} . Tato relace je částečným uspořádáním výrokových formulí.
říkáme, že jePro 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.
Pro jakékoliv formule A , B , C {\displaystyle A,B,C}
jsou následující formule axiomy:Stačí nám jediné pravidlo, tzv. Modus ponens: Jestliže A {\displaystyle A} platí a A ⇒ B {\displaystyle A\Rightarrow B} platí, pak B {\displaystyle B} platí.
Důkazem nazveme konečnou posloupnost A 1 , … , A n {\displaystyle A_{1},\ldots ,A_{n}}
, jestliže pro každé i ≤ n {\displaystyle i\leq n} je A i {\displaystyle A_{i}} buď závěr odvozovacího pravidla, jehož předpoklady jsou mezi A 1 {\displaystyle A_{1}} a A i − 1 {\displaystyle A_{i-1}} , nebo axiom.Jestliže existuje důkaz výrokové formule A {\displaystyle A}
, říkáme o této formuli, že je dokazatelná.Výroková logika je úplná a konzistentní v tom smyslu, že dokazatelné formule jsou právě ty, které jsou pravdivé v každém ohodnocení.