AP4, IN4 Výroková logika
Zadání
IN(syntax, sémantika, odvozovací systém výrokové logiky, důkazy ve výrokové logice, pravdivost a dokazatelnost logických formulí)
AP(syntax, sémantika, odvozovací systém výrokové logiky, důkazy ve výrokové logice, pravdivost a dokazatelnost logických formulí, rezoluce)
Vypracování
Logika
Logika se zabývá problematikou správnosti usuzování (vztah vyplývání). Na usuzování však logiku zajímají pouze vybrané aspekty. Usuzování chápeme jako určitý myšlenkový proces. Psychologické aspekty tohoto procesu však logika zcela opomíjí, stejně jako jeho obsahovou stránku. Zabývá se především analýzou formální stavby úsudků jako základních jednotek usuzování. Úsudkem rozumíme takový myšlenkový postup, kterým dospíváme od nějakých tvrzení, která nazýváme předpoklady (premisy), k jinému tvrzení, které nazýváme závěr (důsledek). Při studiu úsudků logiku zajímá pouze jejich forma, nikoliv konkrétní obsah. Proto úsudkem je z hlediska logiky schéma tvaru:
A1, A2, …, An / B,
kde výrazy A1, A2, …, An reprezentují nějaká tvrzení a výraz B tvrzení, které je závěrem. Je-li úsudek daného tvaru platný (z pravdivých premis vždy získáme pravdivý závěr), říkáme, že závěr B vyplývá z premis A1, A2, …, An (A1, A2, …, An implikuje B [2]).[1]
Logika je schopna (svými prostředky) kontrolovat správnost pouze u deduktivních úsudků. Porovnejte následující dva úsudky:
všichni lidé jsou smrtelní, Sokrates je člověk;
tudíž Sokrates je smrtelný
a
slunce doposud vyšlo každý den;
tudíž (asi) vyjde i zítra.[1]
První z nich je běžný příklad deduktivního úsudku, který je považován za platný. Druhý úsudek je považován za deduktivně neplatný — je to pravděpodobnostní úsudek.
Rozdíl mezi deduktivními a pravděpodobnostními úsudky je mj. v tom, že u platného deduktivního úsudku je pravdivost závěru zaručena pravdivostí premis, kdežto u pravděpodobnostního úsudku pravdivost premis nezaručuje jistou pravdivost závěru, pouze jeho pravděpodobnost (v uvedeném úsudku je tato pravděpodobnost jistě vysoká). [1]
Logika poskytuje nástroj pro budování (vědeckých) teorií (teorie grup, modální logiky). Například výpočtová logika umožňuje automatizaci důkazů a programování v jazyce Prolog (logické programování). [2]
Klasifikace logik
Nejobecnější klasifikací usuzování vůbec je rozdělení na:
Mentální (neformální) – usuzování všeobecně („selský rozum”), to co je poznatelné
Formální – to co je poznané a definované, metody odvozování.
Rozlišujeme dvouhodnotovou a vícehodnotovou logiku podle toho, zda připouštíme k ohodnocení tvrzení právě dvě pravdivostní hodnoty, tj. „pravda“ a “nepravda“, nebo více než dvě pravdivostní hodnoty.
Dále rozlišujeme logiku extenzionální a intensionální především podle toho, jakých spojek se užívá pro vytvoření složených tvrzení. U extenzionální pravdivost formule závisí jen na pravdivosti jejich složek („ne“, „a“, „nebo“), naopak u intensionální („možná“, „věřím“…).
Logika, která je dvouhodnotová a extenzionální se nazývá klasická logika. Dělí se dále podle detailnosti analýzy na logiku výrokovou a predikátovou.
Klasická logika
„Nebude-li pršet nezmoknem“ . Více viz. níže.
Predikátová logika
1. řádu: „Není pravda, že všichni lidé jsou spokojení.“
2. řádu: „Existuje vlastnost, kterou mají všichni lidé.“
[1] a [2]
Žádný jazyk nelze systematicky vybudovat pouze pomocí jeho vlastních výrazových prostředků. K tomuto účelu vždy potřebujeme další jazyk (vyšší expresivní úrovně), v němž pak také můžeme formulovat výpovědi o výrazech toho nového jazyka. Jazyk který budujeme, nazveme objektový jazyk a jazyk, ve kterém hovoříme o objektovém jazyce, nazveme metajazyk. Nerozlišování objektového jazyka a metajazyka vede ke vzniku tzv. sémantických paradoxů. Např. paradox lháře: „Tato věta je nepravdivá“.[1]
Výroková logika
Výroková logika je teorií logických spojek chápaných jako pravdivostní funkce. [1] Zabývá se způsoby tvoření výroků pomocí spojek a vztahy mezi pravdivostí různých výroků. [2]
Nezabývá se smyslem výroků, jelikož má extenzionální charakter. Výroková logika zkoumá uvedené jevy prostřednictvím umělého jazyka používajícího výrokových symbolů, logických spojek a závorek. Jelikož sémantika tohoto jazyka je extenzionální, lze si představit, že výroková logika uznává pouze dva výroky: jeden, který reprezentuje všechny pravdivé výroky a druhý, který reprezentuje ty nepravdivé. [1]
Syntax
Výroková logika rozlišuje na syntaktické úrovni dva typy výroků — jednoduché (elementální) a složené:
Výrok je tvrzení nebo jazykový výraz, o jehož (ne)pravdivosti lze uvažovat.[1]
Jednoduchý výrok je výrok, který neobsahuje žádnou logickou spojku.
Složený výrok je výrok, který obsahuje alespoň jednu logickou spojku.[2]
Příklady:
Výroky:
Výrazy, které nejsou výroky:
Kolik je hodin?
2 + 3
napiš úkoly a ukliď
[2]
Pravdivostní spojky (funkce)
Pravdivostní hodnota složeného výroku je jednoznačně určena pravdivostními hodnotami složek. Uvažujeme-li n-ární spojku, pak tato spojka je funkcí, která přiřazuje n-tici pravdivostních hodnot určitou pravdivostní hodnotu. Počet pravdivostních hodnot je konečný, jsou dvě (pravda, nepravda).[1]
Každou n-ární spojku (jako pravdivostní funkci) lze zadat tabulkou o 2n řádcích, tzv. pravdivostní tabulkou.[1]
Počet vzájemně různých n-árních spojek je [1].
Nulární výrokové spojky
Nulární pravdivostní funkce (nezávisí na žádném argumentu) jsou konstanty odpovídající pravdivostním hodnotám 0,1. [2]
Unární (jednoargumentové) výrokové spojky
p | | F1 | F2 | F3 | F4 |
1 | | 1 | 1 | 0 | 0 |
0 | | 1 | 0 | 1 | 0 |
F1: unární verum,
F2: unární projekce p,
F3: negace p (ozn. ¬p);jediná netriviální unární funkce,
F4: unární falsum.
[1],[2]
Binární výrokové spojky
Přehled nejpoužívanějších spojek:
p | q | | | | | | F5 | F6 | F7 |
1 | 1 | | 1 | 1 | 1 | 1 | 0 | 0 | 0 |
1 | 0 | | 1 | 0 | 0 | 0 | 1 | 1 | 0 |
0 | 1 | | 1 | 0 | 1 | 0 | 1 | 1 | 0 |
0 | 0 | | 0 | 0 | 1 | 1 | 1 | 0 | 1 |
— disjunkce (alternativa; a nebo; OR)
— konjunkce (a zároveň; AND)
— implikace (jestliže p, pak q; předpoklad důsledek)
— ekvivalence (právě tehdy,když;iff - if and only if)
F5 — Shefferova funkce (negace konjunkce;NAND;„… je neslučitelné s …“)
F6 — nonekvivalence (spojka nebo ve vylučovacím smyslu;„buď …,anebo …“;XOR - eXclusive OR)
F7 — Nicodova (Peirceova) funkce (negace disjunkce;NOR;„ani …, ani …“)
Spojky
jsou komutativní (hodnota funkce nezávisí na pořadí argumentů).
Běžně se používá infixový zápis
.
je komutativní,
není komutativní.
[1],[2]
Symbolický jazyk výrokové logiky
Jazyk výrokové logiky má tuto abecedu a gramatiku:
[1]
Symboly A a B z bodů 2 a 3 této induktivní definice jsou výrazy metajazyka. Nepatří tedy do jazyka výrokové logiky, ale označují jeho libovolné výrazy (správně utvořené formule). Závorky lze vynechat, pokud odstraněním nedojde k nejednoznačnostem.[1]
Reprezentace výroků v přirozeném jazyce
Věta:„Pokud rychle napíšeš úkoly a venku bude hezky, půjdeme na procházku nebo pojedeme na koupaliště.“
p — „rychle napíšeš úkoly“
r — „venku bude hezky“
s — „půjdeme na procházku“
t — „pojedeme na koupaliště“
Výsledná reprezentace v symbolickém jazyce je:
Převod z přirozeného jazyka do symbolického jazyka výrokové logiky nemusí být vždy jednoznačný.
[2]
Sémantika
Pravdivostní ohodnocení (interpretace) je funkce přiřazující všem atomickým formulím dané úvahy pravdivostní hodnoty (tj. každému výrokovému symbolu přiřadí 0 nebo 1).
Valuace je rozšíření interpretace z atomických na všechny formule dle tabulky pro výrokové spojky.
Interpretace I splňuje formuli A (formule je pravdivá v I, resp. odpovídající valuace I'(A) = 1), pokud
A je výrokový symbol a I(A) = 1
A je
a
I nesplňuje
B, resp.
I'(B) = 0
A je tvaru
a
I splňuje
B i
C, resp.
I'(B) = I'(C) = 1
A je tvaru
a
I splňuje
B nebo
C, resp.
I'(B) = 1 nebo
I'(C) = 1
A je tvaru
a
I nesplňuje
B nebo splňuje
C, resp.
I'(B) = 0 nebo
I'(C) = 1
A je tvaru
a
I splňuje
B i
C nebo
I nesplňuje
B i
C, resp.
I'(B) =
I'(C)
[2]
Formule A se nazývá
tautologie, je-li splňována každou interpretací. Např.
Formule A se nazývá
kontradikce, jestliže není splňována žádnou interpretací. Např.
Říkáme, že
formule A je splnitelná, je-li splňována aspoň jednou interpretací
I, kterou pak nazýváme
model formule A.
Množina formulí T je
splnitelná, jestliže existuje ohodnocení
I takové, že každá formule
A ∈ T je splňována
I. Tuto interpretaci pak nazýváme
model množiny T.
Říkáme, že formule
A logicky vyplývá (na základě výrokové logiky) z množiny T a tuto skutečnost označíme
(případně T ∴ A), jestliže pro každý model
I množiny T je formule
A interpretací
I splňována.
Tautologií je nekonečně mnoho.[2]
Ke zjištění pravdivosti formulí pro všechny možné interpretace používáme
tabulkovou metodu.
[2]
Zásady:
Vyhodnocení probíhá po složkách (podformulích) dané formule (výrok. symboly, negace, …, celá formule).
Zápis pravdivostní hodnoty provedeme v řádku s příslušnou interpretací pod vyhodnocovanou spojkou (výr. symbol).[2]
Odvozovací systém výrokové logiky
Na rozdíl od vyhodnocování (interpretace, resp. valuace) logických formulí na základě atomických formulí (výrokových symbolů) klademe na formální systém výr. logiky požadavek na dokazování výr. formulí. Tj. zjištění, zda-li pravdivost dané formule vyplývá z pravdivostí jiných formulí.
Formálním systémem výrokové logiky se rozumí
jazyk výrokové logiky a
deduktivní soustava, která je tvořena odvozovacími pravidly a případně axiomy. Za
axiomy (výchozí tvrzení přijímaná bez důkazu) volíme vhodná schémata tautologií,
odvozovací pravidlo chápeme jako operace na formulích umožňující konstrukce důkazů a stačí jediné - pravidlo
modus ponens. Po tomto pravidle požadujeme korektnost, to znamená, aby z pravdivých premis byl odvozen pravdivý závěr.
Formální systémy jsou postaveny výhradně na syntaktické bázi, jazyk logiky neinterpretujeme, provádíme s ním pouze syntaktické manipulace — důkazy.[2]
Formální systémy lze rozdělit na:
axiomatické (méně pravidel)
předpokladové (méně axiomů) — např. Gentzenovský systém (kalkul sekventů), jediný axiom (
). Důkaz sekventu je strom, v jehož kořeni je dokazovaný sekvent, v listech axiomy a každý uzel (závěr) se svými přímými následovníky (předpoklady) představuje instanci některého z pravidel systému.
Požadované vlastnosti formálních systémů:
korektnost (bezespornost): je dána výběrem axiomů a odvozovacích pravidel; systém je korektní, nelze-li v něm zároveň odvodit tvrzení i jeho negaci. Ve sporném systému lze odvodit cokoliv. Vyžadována vždy.
úplnost: připojením neodvoditelné věty k úplnému systému se tento stane sporným. Nevyžadována vždy – úplné jsou pouze velmi jednoduché teorie.
rozhodnutelnost: existence algoritmu pro ověření dokazatelnosti libovolné formule. V axiom. systémech podmíněna úplností; zpravidla splněna pouze pro určité třídy formulí.
nezávislost axiomů: nezávislý axiom nelze odvodit z ostatních axiomů;závislý axiom může být vypuštěn z dané soustavy axiomů.
[1] a [2]
Modus ponens (MP)
MP je základní a nejdůležitější odvozovací pravidlo. Jeho tvar:
MP říká, že když máme formule A a A ⇒ B pak z toho vyplývá platnost B.
Důkazy ve výrokové logice
Důkaz je v daném systému konečná posloupnost správně utvořených formulí (kroků důkazu), z nichž každá je buď axiómem nebo byla odvozena aplikací některého pravidla odvození na některé předcházející správně utvořené formule.
Určitá
formule je dokazatelná v daném systému tehdy a jen tehdy, když v tomto systému existuje důkaz, jehož je tato formule členem. (
).
Teorém je v systému S formule, která je dokazatelná v systému S.[3]
Pravdivost logické formule je dána sémantikou této formule. Kdežto,
dokazatelnost (odvoditelnost) logické formule je posuzována syntaxí. Říkáme, že formule je dokazatelná, pokud k této formuli existuje důkaz. Těchto důkazů je nekonečně mnoho.
Rezoluce
Rezoluce je
formální systém výrokové logiky vhodný pro
strojové dokazování (Prolog) a je založena na vyvracení — dokazuje se nesplnitelnost formulí.
Rezoluce pracuje s formulemi v KNF
1), notace je však jiná:
klauzule je konečná množina literálů (chápána jako jejich disjunkce). Je pravdivá, pokud alespoň jeden prvek je pravdivý. Prázdná klauzule □ je vždy nepravdivá — neobsahuje žádný pravdivý prvek. Příklad klauzule
dříve značeno
.
formule je (ne nutně konečná) množina klauzulí (chápána jako jejich konjunkce, tedy KNF). Je pravdivá, je-li každý její prvek pravdivý. Prázdná formule ∅ je vždy pravdivá — neobsahuje žádný nepravdivý prvek. Příklad formule
dříve značeno
.
rezoluční pravidlo: nechť
jsou klauzule, jejich rezolventou je
. Rezoluční pravidlo zachovává splnitelnost, tj. libovolná valuace splňující C
1 a C
2 splňuje i C.
rezoluční důkaz klauzule C z formule S je konečná posloupnost klauzulí C
1,C
2,…,C
n, kde C
n = C a každé C
i je buď prvkem S, nebo rezolventou klauzulí C
j, C
k pro j,k < i. Existuje-li tento důkaz, je C rezolučně dokazatelná z S (píšeme
). Odvození □ z S je vyvrácením S.
[2]
Přehlednější reprezentací rezolučních důkazů jsou stromy.
Strom rezolučního důkazu C z S je binární strom T s vlastnostmi:
Příklad: strom důkazu
Obecné schéma důkazu, formule A je log. důsledkem množiny formulí T:
vytvoříme konjunkci T' všech prvků z T,
formuli T' ∧ ¬A převedeme do KNF a
ukážeme KNF(T' ∧ ¬A)
□.
Výhody pro strojové zpracování:
systematické hledání důkazu
práce s jednoduchou datovou strukturou
jediné odvozovací pravidlo
Problém: Strategie generování rezolvent — prohledávaný prostor může být příliš veliký. Omezení prohledávaného prostoru (zjemnění rezoluce):
Doposud [2].
Lineární rezoluce –- jde o posloupnost dvojic , … , takovou, že a
a všechny
jsou z S anebo nějaké
, kde
každé
,
je rezolventou
a
(vstupní klauzule S, boční
a střední
)
Lineární vstupní rezoluce (LI) množiny je lineární vyvrácení S, které začíná klauzulí G, a bočními klauzulemi jsou jen klauzule z P.
je úplná jen pro Hornovy klauzule
2)
LD rezoluce –- už máme uspořádané klauzule a při rezoluci vkládáme dovnitř. LD rezoluční vyvrácení je postupnost , … , uspořádaných klauzulí taková, že □, a každé , je rezolventou uspořádaných klauzulí a
[4]
Předměty
IB101 Úvod do logiky a logického programování
Použitá literatura
[1] Štěpán, Jan, Klasická logika. Olomouc, Univerzita Palackého v Olomouci 2001.
[2] Popelínský, L., Mráková, E., Úvod do logiky a logického programování, slídy, červen 2008, dostupné na: http://www.fi.muni.cz/~popel/lectures/bak_logika/
[3] Raclavský, J., Výroková logika, červen 2008, dostupne na http://www.phil.muni.cz/fil/logika/vl.php
[4] Vypracování otázek Elena Halická - http://www.fi.muni.cz/~xhalic1/statnice/vypracovaneIM.doc
Kam dál?
Vypracuje
Erik Zitterbart, ICQ: 172319825. eriksson (zavinac) mail.muni.cz
Z mé strany 99%. Rád dopracuji případné komentáře a opravy. Vypracování je poněkud delší.
Otázku si přečetl pan doc. RNDr. Lubomír Popelínský a rámcově prošel. Jeho podněty pro doplnění textu, opravy nesrovnalostí a odstranění matoucích či k otázce se nevztahujících textů byly do otázky zaneseny. Tato kontrola je jen rámcová, stále se může stát, že v otázce zůstala zapomenutá chybka či nesrovnalost, vyučující za toto nenese odpovědnost, berte tuto rámcovou kontrolu jako formu pomoci od vyučujících pro studenty.