Výroková logika

formální odvozovací systém, ve kterém atomické formule tvoří výrokové proměnné
(přesměrováno z Pravdivostní ohodnocení)
Na tento článek je přesměrováno heslo Výroková formule. Tento článek je o pojmu matematické logiky. Další významy jsou uvedeny na stránce Formule.
Na tento článek je přesměrováno heslo Výroková formule. Tento článek je o pojetí formule ve výrokové logice. O pojetí formule v predikátové logice pojednává článek Formule (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

Syntaxe

editovat

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

  1. Každá atomická výroková formule je též výroková formule.
  2. Jestliže   je výroková formule, je i   výroková formule.
  3. Jsou-li   výrokové formule, je i   výroková formule.
  4. 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:   pro  
  • Disjunkce:   pro  
  • Ekvivalence:   pro  
  • Exkluzivní disjunkce:   pro  
  • Tautologie:   pro  
  • Kontradikce:   pro  
  • NAND:   pro  
  • NOR:   pro  
  • Obrácená implikace:   pro  

Sémantika

editovat

Pravdivostní ohodnocení (též interpretace) atomických formulí je jakékoliv zobrazení  . Rozšíření   na výrokové formule definujeme induktivně takto:

  1.   je-li   atomická formule
  2.  
  3.  

Pokud pro formuli   a ohodnocení   platí, že  , říkáme, že formule   je v ohodnocení   pravdivá, což značíme též jako  . V opačném případě říkáme, že formule   je v ohodnocení   nepravdivá.

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

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

Odvozování

editovat

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

editovat

Pro jakékoliv formule   jsou následující formule axiomy:

  1.  
  2.  
  3.  

Odvozovací pravidlo

editovat

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

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

Úplnost

editovat

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

Externí odkazy

editovat