Výroková logika

Z Wikipedie, otevřené encyklopedie

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

[editovat] 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. Nic jiného není výroková formule.

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

• konjunkce: pro
• disjunkce: pro
• ekvivalence: pro

[editovat] 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

[editovat] Odvozování

[editovat] Axiomy

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

[editovat] Odvozovací pravidlo

• (pravidlo Modus Ponens) Jestliže A platí a A → B platí, pak B platí.

[editovat] Důkaz

Důkazem nazveme konečnou posloupnost A₁,…,A_n, jestliže pro každé i menší nebo rovné než n je A_i buď závěr odvozovacího pravidla, jehož předpoklady jsou mezi A₁ a A_i-1, nebo axiom.

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

[editovat] Externí odkazy

• Volně stažitelná skripta z předmětu Výroková a predikátová logika na MFF UK od Petra Štěpánka