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í). 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: Pokud se mi stal úraz hlavy, ztratím práci. Pokud ztratím práci a rozvedu se, budu alkoholik. 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í Nejprve deklarujeme výroky, které budeme dále používat. Deklarací jsme vytvořili formální výroky 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 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 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 Důsledek formulujeme jako lemma pojmenované Zkuste si důkaz „krokovat“! Co se děje mezi klíčovými slovy 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: 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: Z nějakého důvodu nám přibyl jeden předpoklad: Potěšujícím koncem důkazu je, že po provedení posledního příkazu (taktiky) přehled zmizí a Coq vrací hlášku což znamená, že důkaz byl správně (korektně) proveden a my ho můžeme uložit příkazem 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. 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 Druh úsudku z minulého odstavce nyní zformalisujeme jako odvozovací pravidlo: označme si nějakou množinu výroků jako 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 Nyní budeme předpokládat, že námi zavedené výroky platí. Co znamená zápis Dokážeme tvrzení (lemma) s názvem 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 Nyní místo použití příkazu Lemma má stejný důkaz i stejný závěr, jen nyní obsahuje předpoklad platnosti výroků 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.Ukázkový příklad¶
Alt + šipka dolů
.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“.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í.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.rozvedu_se -> budu_alkoholik
?r_a
a dokážeme ho.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á.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
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
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.No more goals.
Qed
.Předpoklady a závěr¶
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ů.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
A
, B
a C
.(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
.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
.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í.Hypotheses
pro zavedení předpokladů tyto předpoklady zmíníme přímo ve znění našeho lemmatu: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.