Výroky, předpoklady, závěry

Hlavním cílem této učebnice je představit praktickým způsobem důkazový systém nazvaný přirozená dedukce v takzvané (intuicionistické) výrokové logice. Co tento cíl znamená prakticky? Naučíte se dokazovat jednoduchá logická tvrzení: rozhodovat, zda vyplývají z předpokladů, které máte k disposici.

Nejsnazší způsob přiblížení toho, co vás učebnice naučí, je ukázat příklad toho, co budete umět po jejím pročtení (a po zpracování všech úloh k procvičení).

Ukázkový příklad

Vyzkoušíme si odvození jednoduchého důsledku ve výrokové logice.

Představme si, že následující tři tvrzení bereme jako fakta:

  1. Pokud se mi stal úraz hlavy, ztratím práci.

  2. Pokud ztratím práci a rozvedu se, budu alkoholik.

  3. Stal se mi úraz hlavy.

Plyne z těchto třech tvrzení následující tvrzení? - Pokud se rozvedu, budu alkoholik.

Ukážeme, že ano. Využijeme k tomu důkazový asistent Coq, který vás bude celou učebnicí doprovázet. Coq spustíte tlačítkem „power“, které byste měli vidět v pravém horním rohu učebnice, „krokovat“ příkazy můžete pomocí Alt + šipka dolů.

Nejprve deklarujeme výroky, které budeme dále používat.

Deklarací jsme vytvořili formální výroky Uraz_hlavy, Ztratim_praci, Rozvedu_se a Budu_alkoholik, což jsou takzvané atomické výroky, z nichž budeme skládat výroky složitější. Představujeme si, že námi deklarované výroky representují výroky v přirozeném jazyce, a to „stal se mi úraz hlavy“, „ztratím práci“, „rozvedu se“, a „budu alkoholik“.

díky tomu, že jsme výroky deklarovali, s nimi teď můžeme dál pracovat. Pozor! Deklarací výše jsme netvrdili, že dané výroky platí či jsou pravdivé. Srovnejte s přirozenou komunikací: mohu vyřknout například větu „Prší.“, a je to výrok v přirozeném jazyce, ať už ve skutečnosti prší, či nikoli.

Pokud např. chceme skutečně tvrdit, že jsem utrpěl úraz hlavy, musíme platnost tohoto výroku dosvědčit (zde spíše předpokládat) tím, že ho zavedeme jako hypotézu u : Uraz_hlavy. Zde Uraz_hlavy je výrok representující výrok „stal se mi úraz hlavy“, a u je označení důkazu ( dosvědčení ), že daný výrok skutečně platí.

Zavedeme nyní ještě dva předpoklady („hypotheses“) representující složené výroky z bodů 1. a 2. výše:

Zatím není třeba, abyste rozuměli syntaxi, kterou používáme. Zápis u_z : Uraz_hlavy -> Ztratim_praci zde nicméně znamená, že u_z je označení pro důkaz (náš předpoklad), že „pokud se mi stal úraz hlavy, ztratím práci“. Zápis zr_a : (Ztratim_praci /\ Rozvedu_se) -> Budu_alkoholik značí, že předpokládáme další tvrzení, a to složený výrok „pokud ztratím práci a rozvedu se, budu alkoholik“. Atomické výroky skládáme pomocí takzvaných logických spojek.

Nyní tedy předpokládáme všechna tři tvrzení, která jsme formulovali jako předpoklady v našem úvodním příkladu. Plyne z těchto předpokladů závěr, že pokud se rozvedu, budu alkoholik? To jest, lze vyvodit z výše zavedených „hypotéz“ důsledek rozvedu_se -> budu_alkoholik?

Důsledek formulujeme jako lemma pojmenované r_a a dokážeme ho.

Zkuste si důkaz „krokovat“!

Co se děje mezi klíčovými slovy Proof a Qed? Používáme takzvané taktiky, příkazy v Coqu, které (zjednodušeně řečeno) odpovídají logickým odvozovacím pravidlům, krokům důkazu, ze kterých se celý důkaz nakonec skládá.

Po celou dobu důkazu máte k disposici interaktivní přehled, v němž je vidět, co máte právě dokazovat, a jaké předpoklady zrovna můžete používat. Tedy například na začátku důkazu přehled vypadá přibližně takto:

Uraz_hlavy, Ztratim_praci, Rozvedu_se, Budu_alkoholik : Prop
u : Uraz_hlavy
u_z : Uraz_hlavy -> Ztratim_praci
zr_a : Ztratim_praci /\ Rozvedu_se -> Budu_alkoholik
______________________________________(1/1)
Rozvedu_se -> Budu_alkoholik

Přehled přesně odpovídá naší úloze: deklarovali jsme čtyři atomické výroky zmíněné v prvním řádku, v dalších třech řádcích vidíme naše tři předpoklady, a pod dlouhou vodorovnou čarou vidíme to, co máme dokázat: takzvaný cíl.

Už po dvou krocích důkazu však vypadá náš přehled jinak:

Uraz_hlavy, Ztratim_praci, Rozvedu_se, Budu_alkoholik : Prop
u : Uraz_hlavy
u_z : Uraz_hlavy -> Ztratim_praci
zr_a : Ztratim_praci /\ Rozvedu_se -> Budu_alkoholik
r : Rozvedu_se
______________________________________(1/1)
Ztratim_praci /\ Rozvedu_se

Z nějakého důvodu nám přibyl jeden předpoklad: r : Rozvedu_se. Také se změnil náš cíl: máme dokázat (složený) výrok „ztratím práci a rozvedu se“ (pouze formálně zapsán). Proč přibyl zrovna daný předpoklad a proč máme dokazovat zrovna daný cíl? V této učebnici si klademe za úkol přesně tyto otázky vysvětlit a zodpovědět.

Potěšujícím koncem důkazu je, že po provedení posledního příkazu (taktiky) přehled zmizí a Coq vrací hlášku

No more goals.

což znamená, že důkaz byl správně (korektně) proveden a my ho můžeme uložit příkazem Qed.

Díky důkazovému asistentu jsme získali jistotu, že pokud jsme naši původní úlohu správně formalisovali, pak si o tom, že daný závěr vyplývá z našich předpokladů, můžeme být jisti.

Co nám ukázkový příklad osvětluje? Budeme se snažit tvořit formální důkazy: vyvozovat závěry z předpokladů. Důkaz v Coq budujeme interaktivně tak, že se snažíme splnit cíl, a cíl postupně měníme (zjednodušujeme) taktikami. Tvrzení, která předpokládáme a dokazujeme, tvoříme z atomických výroků pomocí logických spojek. Význam a chování jednotlivých logických spojek si vysvětlíme v následujících kapitolách.

Předpoklady a závěr

Jelikož nyní ještě logické spojky používat neumíme, vysvětlíme prozatím pouze jednu nejjednodušší formu logického úsudku.

Řekněme, že jsme přesvědčeni o třech výrocích, např. „prší“, „je mlhavo“, „je tma“. Co vše z těchto výroků můžeme vyvodit? Přinejmenším můžeme vyvodit to, co předpokládáme, tedy každý z daných třech výroků, například „prší“. Formálně budeme takovýto úsudek značit jako prší, je mlhavo, je tma |- prší. Znak |- je symbolem logického důsledku: před něj doleva píšeme množinu předpokladů, se kterými pracujeme, za něj doprava píšeme důsledek daných předpokladů.

Druh úsudku z minulého odstavce nyní zformalisujeme jako odvozovací pravidlo: označme si nějakou množinu výroků jako Gamma. Dále budeme používat značení Gamma, A pro množinu výroků Gamma, do které jsme přidali ještě výrok A. Z množiny předpokladů Gamma, A lze odvodit výrok A, jelikož tento výrok již předpokládáme. Tomuto pravidlu se říká pravidlo předpokladu a je značeno následovně:

-------------
Gamma, A |- A

Vodorovné čáře v odvozovacím pravidlu říkáme odvozovací čára. Nad ní jsou zapsány podmínky, za kterých lze pravidlo použít (tedy naše pravidlo nemá žádné podmínky), a pod ní je napsáno, co lze díky odvozovacímu pravidlu odvodit.

Předvedeme si nyní na příkladu užití pravidla předpokladu v Coqu. Příklad nutně nemůže být příliš zajímavý, protože samotné pravidlo předpokladu neumožňuje tvořit zajímavé a složité důkazy. Je to pouze základní stavební kámen, který budeme v dalších kapitolách pravidelně využívat.

Deklarujeme výroky A, B a C.

Nyní budeme předpokládat, že námi zavedené výroky platí.

Co znamená zápis (a : A)? Symbolem a zde označujeme důkaz toho, že A pro nás nyní platí, a podobně tomu je u b a c.

Dokážeme tvrzení (lemma) s názvem z_A_B_C_plyne_A, jehož závěrem je B. Důkaz v Coqu začínáme příkazem Proof., končíme ho příkazem Qed., a pravidlo předpokladu v Coqu používáme příkazem assumption.

Jelikož jsme závěr lemmatu skutečně předpokládali, je náš důkaz korektní a Coq nehlásí problém.

Předvedeme ještě alternativní způsob zápisu našeho příkladu, který bude obvyklejší v následujících kapitolách.

Znovu zavedeme výroky A, B a C. Obor platnosti zavedení výroků (jejich scope ) je pouze uvnitř sekce, zavedení výroků A, B, C z minulé sekce zde tedy již neplatí.

Nyní místo použití příkazu Hypotheses pro zavedení předpokladů tyto předpoklady zmíníme přímo ve znění našeho lemmatu:

Lemma má stejný důkaz i stejný závěr, jen nyní obsahuje předpoklad platnosti výroků A, B a C, důkazy těchto třech výroků postupně označujeme jako a, b a c. Předpoklady píšeme za název lemmatu, a oddělujeme je od závěru dvojtečkou.

Nyní jste již připraveni na opravdový začátek: studium logických spojek a jejich chování. V dalších kapitolách probereme spojky konjunkce, implikace, disjunkce a negace, a uvidíme, jak jejich využití umožňuje formulovat výrazně složitější a zajímavější důkazy.