Konjunkce

V této kapitole se budeme zabývat logickou spojkou konjunkce. Je to spojka přibližně odpovídající spoje „a“ v přirozeném jazyce, a práce s ní je v přirozené dedukci velmi intuitivní. Konjunkce umožňuje spojit dva výroky A a B do složeného výroku, jehož význam je „A a B platí současně“. Uvidíme, že pravidla pro práci s konjunkcí věrně kopírují způsob, jakým se spojkou „a“ obvykle pracujeme.

Syntax konjunkce

V matematické logice se konjunkce výroků A a B obvykle zapisuje stříškou jako A ∧ B. Pro naše účely je vhodné používat syntax bez speciálního symbolu, aby bylo snazší ji rychle zapsat. Konjunkci A a B tedy budeme značit A /\ B - stříšku zapisujeme dopředným a zpětným lomítkem.

Pravidla pro práci se spojkou konjunkce

Téměř u všech spojek, které zavedeme, budeme potřebovat zavést i dvě pravidla pro práci s nimi: pravidlo zavedení dané spojky a pravidlo eliminace dané spojky. Pravidlo zavedení nám říká, co vše musíme vědět, abychom byli přesvědčeni o platnosti výroku, ve kterém se daná spojka vyskytuje. Pravidlo eliminace nám dává návod, jak využít platnost výroku využívajícího danou spojku k odvození dalších tvrzení.

V případě konjunkce je velmi snadné pravidla zavedení a eliminace vyslovit a pochopit.

Pravidlo zavedení konjunkce

Nejprve neformálně: když víme, že prší, a když navíc víme, že je mlha, tak můžeme naše dvě znalosti spojit do jedné (větší) znalosti „prší a je mlha“. Tak se spojka „a“ v přirozeném jazyce používá: skládá několik tvrzení dohromady. Mírně formálněji: když víme, že platí výrok A a víme, že platí výrok B, pak můžeme začít tvrdit, že platí výrok A /\ B. Tím jsme zavedli konjunkci výroků A a B.

Nyní už můžeme naše odvozovací pravidlo vyslovit přesně: umíme-li z množiny předpokladů Gamma odvodit A (to zapisujeme symbolicky jako Gamma |- A), a umíme-li z Gamma odvodit i B (symbolicky Gamma |- B), pak z množiny předpokladů Gamma umíme odvodit i A /\ B. Tento fakt zapisujeme jako odvozovací pravidlo:

Gamma |- A  Gamma |- B
----------------------
Gamma |- A /\ B

Toto pravidlo nazýváme zavedení konjunkce.

Pravidlo eliminace konjunkce

Znovu zmíníme nejprve neformální příklad: když víme, že sněží a fouká, tak speciálně víme, že sněží. Tento úsudek nám přijde zcela trivální. Proč tomu tak je? Protože přesně takto se spojka „a“ v našem jazyce chová: když víme více věcí dohromady, tak jistě víme i každou z daných věcí zvlášť. Mírně formálněji: když víme, že platí výrok A /\ B, pak můžeme tvrdit, že platí i výrok A. (A samozřejmě také můžeme tvrdit, že platí i výrok B.) Tím jsme eliminovali konjunkci A /\ B, využili jsme ji k „extrakci“ informace v ní uložené.

Jak přesně formulovat toto odvozovací pravidlo? Umíme-li z množiny předpokladů Gamma odvodit A /\ B (symbolicky Gamma |- A /\ B), pak umíme z Gamma odvodit i A (symbolicky Gamma |- A). A podobně umíme z Gamma |- A /\ B odvodit i Gamma |- B. Tento fakt zapisujeme jako dvě odvozovací pravidla:

Gamma |- A /\ B
---------------
Gamma |- A

Gamma |- A /\ B
---------------
Gamma |- B

Tato dvě pravidla nazýváme eliminace konjunkce.

Práce s konjunkcí v Coq

Nyní si ukážeme několik jednoduchých příkladů, na kterých předvedeme, jak se s konjunkcí dá pracovat v Coqu.

Nejprve zavedeme novou sekci, ve které do kontextu přidáme výroky A, B, C, D. Připomeňme: zavedením těchto výroků netvrdíme, že platí! Pouze se o nich díky zavedení můžeme začít vyjadřovat. Podobně v přirozeném jazyce můžeme vyřknout výrok „Prší.“, aniž by byl pravdivý.

Section priklady_konjunkce. Set Printing Parentheses. Context (A B C D : Prop).

V Coqu pravidlo zavedení konjunkce používáme příkazem split. Když máme za cíl dokázat A /\ B, rozdělí se nám cíl na dva podcíle: v jednom budeme muset dokázat A a ve druhém B.

V následujícím příkladu máme dokázat právě A /\ B (výrok za dvojtečkou), a naše předpoklady jsou A a B. Značením a : A uvádíme, že výrok A platí, a důkaz jeho platnosti označujeme jako a. Podobně b je důkazem platnosti B.

Lemma konj_priklad_1 (a : A) (b : B) : A /\ B. Proof. split. - assumption. - assumption. Qed.

V obou podcílech jsme měli dokázat něco, co jsme předpokládali: použili jsme tedy příkaz assumption. Všimněte si, že jednotlivé podcíle označujeme značkou -, aby byl důkazový skript přehlednější.

V dalším příkladu máme za cíl dokázat B z předpokladu (A /\ B) /\ C. Zde bude zjevně potřeba eliminovat konjunkci, kterou předpokládáme. Důkaz dané konjunkce označen jako d; eliminace se provádí příkazem destruct d. Tím se změní naše množina předpokladů: místo jednoho předpokladu tvaru (A /\ B) /\ C budeme mít k disposici dva předpoklady: jeden tvaru A /\ B, a jeden tvaru C. Všimněte si, že jsme skutečně „eliminovali“ spojku konjunkce. Příkazu destruct d jsme přidali nepovinný argument as [ab c], který slouží k tomu, abychom označili důkazy nově vzniklých předpokladů A /\ B a C. Jejich pojmenování (ab a c) je čistě na nás.

Lemma konj_priklad_2 (d : (A /\ B) /\ C) : B. Proof. destruct d as [ab c]. destruct ab as [a b]. assumption. Qed.

Ve třetím příkladu budeme potřebovat jak pravidlo zavedení, tak pravidlo eliminace. Naším cílem je dokázat, že spojka konjunkce je „významově komutativní“: výroky A /\ B a B /\ A sice nejsou totožné, ale mají „stejný význam“: z prvního lze dokázat druhý, a naopak z druhého lze dokázat první. My provedeme jen jeden směr důkazu, druhý můžete zkusit sami formulovat a dokázat (nicméně důkaz je v podstatě totožný).

Lemma konj_priklad_3 (ab : A /\ B) : B /\ A. Proof. destruct ab as [a b]. split. - assumption. - assumption. Qed.

Čtvrtý příklad už není konceptuálně obtížnější. Pouze zde již máme dva složitější předpoklady a máme dokázat složitější závěr.

Lemma konj_priklad_4 (ba : B /\ A) (c : C) : A /\ (C /\ B). Proof. destruct ba as [b a]. split. - assumption. - split. + assumption. + assumption. Qed. End priklady_konjunkce.

Nyní jste již vybaveni vším, co potřebujete k důkazům tvrzení týkajících se čistě spojky konjunkce.

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.

Section ulohy_konjunkce. Context (A B C D E : Prop). Lemma konj_uloha_1 (ab : A /\ B) (cde: (C /\ D) /\ E) : (A /\ D) /\ E. Proof. Admitted. Lemma konj_uloha_2 (abc: A /\ (B /\ C)) : (C /\ A) /\ B. Proof. Admitted. End ulohy_konjunkce.