Implikace

V této kapitole se budeme zabývat logickou spojkou implikace. Narozdíl od spojky konjunkce, která celkem přesně v přirozeném jazyce odpovídá spojce „a“, vysvětlit neformálně význam implikace je výrazně obtížnější. Pokud máme dva výroky A a B, pak výroku „A implikuje B“ občas bývá přiřazován význam „pokud A, pak B“. Takovéto chápání implikace je dobrým prvním přiblížením významu implikace, při hlubším zkoumání však neobstojí. My se spokojíme s vysvětlením implikace na základě toho, jak je obvykle používána v matematické praxi a rozebereme příklady jejího použití. Ukážeme také, jak se implikace dá chápat pohledem typovaného programovacího jazyka.

Syntax implikace

V matematické logice se implikace výroků A a B obvykle zapisuje šipkou jako A → B, případně dvojitou šipkou A ⇒ B. Podobně jako u konjunkce pro nás bude vhodnější nepoužívat speciální symboly. Implikaci A a B tedy budeme zapisovat jako A -> B - jednoduchou šipku zapisujeme pomlčkou a znakem „je větší než“.

Pravidla pro práci se spojkou konjunkce

I u implikace budeme potřebovat dvě pravidla, abychom s ní mohli pracovat a používat ji v důkazech. Pravidlo eliminace implikace má velmi snadné vysvětlení, pravidlo zavedení implikace je mírně složitější na pochopení, ale osvětlíme ho na několika příkladech. Eliminační pravidlo slouží k využití informace, která je uložena ve výroku tvaru A -> B, zaváděcí pravidlo nám říká, co musíme vědět, abychom mohli tvrdit, že výrok tvaru A -> B platí.

Jako první představíme pravidlo eliminace implikace.

Pravidlo eliminace implikace

Představme si, že z vyšetřování vraždy víme dvě fakta: 1. Vraždil muž. 2. Pokud vraždil muž, pak byl vrahem Ondřej.

Z těchto dvou fakt se dá usoudit, že vrahem byl Ondřej. Tento úsudek nám znovu přijde zcela triviální: závěr plyne z předpokladů čistě na základě struktury daných předpokladů. Tomuto druhu úsudku se občas v logice říká modus ponens. Mírně formálněji: když víme, že platí výrok A a že platí výrok A -> B, pak můžeme tvrdit, že platí i výrok B. Tedy víme, že B je důsledkem A a A -> B. Tím jsme eliminovali implikaci A -> B, využili jsme ji k „extrakci“ informace v ní uložené.

Tento způsob odvození nyní přesně zformulujeme. Umíme-li z množiny předpokladů Gamma odvodit A (symbolicky Gamma |- A ), a umíme-li navíc z Gamma odvodit A -> B, pak umíme z Gamma odvodit i B (symbolicky Gamma |- B ). Tento fakt zapisujeme jako odvozovací pravidlo:

Gamma |- A  Gamma |- A -> B
---------------------------
Gamma |- B

Toto pravidlo nazýváme eliminace implikace.

Pravidlo zavedení implikace

Pravidlo zavedení implikace je prvním pravidlem, ve kterém je pro nás nutné netriviálně pracovat s množinou předpokladů, které máme k disposici. To mírně ztěžuje jeho pochopení. Pokusíme se tedy nejprve vysvětlit jeho funkci neformálně.

Představte si, že jste naprogramovali program P, který se snaží řešit nějakou jednoduchou úlohu. Pochlubíte se s ním spolužákovi, necháte jej váš program vyzkoušet, a on se vám ozve zpět s následujícím tvrzením: „Když jsem vyzkoušel tvůj program P, havaroval na vstupu 15“. Jak se dá jeho tvrzení ověřit?

Tvrzení spolužáka je tvaru Spustím P se vstupem 15 -> P havaruje. Abychom ukázali (dokázali), že je pravdivé, stačí program P skutečně pustit se vstupem 15 a ověřit, zda havaruje. Tedy nám stačí dokázat tvrzení P havaruje s využitím předpokladu Spustím se vstupem 15.

Stejně tak můžeme uvažovat obráceně: když víme, že jsme P spustili se vstupem 15 a vidíme před sebou potemnělý monitor s chybovou hláškou (tedy důkaz výroku P havaruje), můžeme vyvodit platnost výroku Spustím P se vstupem 15 -> P havaruje. Tím jsme zavedli implikaci daných dvou výroků.

Předcházející příklad nám umožňuje formulovat toto pravidlo přesně. Umíme-li z množiny předpokladů Gamma s přidaným předpokladem A odvodit výrok B (to zapisujeme symbolicky jako Gamma, A |- B ), pak z množiny předpokladů Gamma umíme odvodit A -> B. Tento fakt zapisujeme jako odvozovací pravidlo:

Gamma, A |- B
---------------
Gamma |- A -> B

Toto pravidlo nazýváme zavedení implikace.

Všimněte si především toho, že v závěru daného pravidla se již výrok A nevyskytuje jako předpoklad. Vrátíme-li se k našemu intuitivnímu příkladu ze začátku, jakmile jsme již jednou vyzkoušeli, že na vstupu 15 program P havaruje, nemusíme to zkoušet dál, danou implikaci již víme i bez dalšího testování. (Tento příklad mírně nerealisticky předpokládá, že se P chová deterministicky.)

Práce s implikací v Coq

Na několika jednoduchých příkladech zase předvedeme, jak se s implikací dá pracovat v Coqu.

Zavedeme novou sekci, ve které do kontextu přidáme výroky A, B, C, o kterých se díky jejich zavedení můžeme začít vyjadřovat.

V prvním příkladu si předvedeme pravidlo eliminace implikace. Používáme ho příkazem (tzv. taktikou ) impl_elim. Našimi předpoklady jsou výroky A a A -> B, dokázat máme tvrzení B. Příkaz impl_elim ab vezme náš předpoklad A -> B a cíl B, a používá zpětné odvozování: když máme dokázat B a víme A -> B, stačí nám dokázat A a důkaz bude u konce. My však A také předpokládáme, a po použití impl_elim tedy stačí ještě použít příkaz assumption a důkaz je hotov.

Předcházející důkaz může vypadat na první pohled překvapivě; předvedeme ještě alternativní důkaz „dopředným způsobem“. V tomto důkazu si všímáme, že předpokládáme A i A -> B, a používáme příkaz impl_elim k přidání nového předpokladu. Syntax impl_elim ab in a as b funguje následovně: ab je označení důkazu implikace A -> B, a je označení důkazu výroku A, a b je označení, které chceme použít k označení vyvozeného závěru, důkazu výroku B.

V našem konkrétním příkladu tím získáme novou množinu předpokladů obsahující důkazy výroků A, A -> B i B. Jelikož máme dokázat B, stačí poukázat na to, že B již předpokládáme, příkazem assumption.

V dalším příkladu si ukážeme práci s pravidlem zavedení implikace. V Coqu toto pravidlo umožňuje použít příkaz intro.

Máme (bez dalších předpokladů) dokázat implikaci A -> A. Jako vždy u důkazu implikace můžeme předpokládat její předpoklad a pokusit se dokázat závěr. To jest, abychom dokázali |- A -> A, stačí nám důkaz A |- A. Tuto přeměnu cíle zajistí právě příkaz intro. Jelikož tento příkaz zavádí nový předpoklad, používáme parametr (zde a), abychom tento nový předpoklad pojmenovali. Jelikož je předpoklad i závěr implikace ze zadání totožný, máme tedy dokázat něco, co už předpokládáme: to svede assumption.

Dalším příklad (který popisuje „transitivitu“ implikace) dokážeme zase dvěma způsoby: „zpětným“ a „dopředným“. Porovnejte oba způsoby a promyslete, který způsob by vás napadl první, popř. který způsob vám přijde elegantnější.

Mírně složitější příklad ukazuje, jak lze pracovat s vnořenými implikacemi. Coq mírně zjednodušuje notaci asociováním vpravo: výrok A -> (B -> (C -> D)) zapisuje bez závorek jako A -> B -> C -> D.

Další příklady a úlohy

Zkuste samostatně vyřešit následující úlohy (dokažte zadaná tvrzení).

Za klíčové slovo Proof. začněte tvořit důkazový skript, a po úspěšné tvorbě důkazu nahraďte klíčové slovo Admitted. slovem Qed.