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 V matematické logice se konjunkce výroků 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. 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 Nyní už můžeme naše odvozovací pravidlo vyslovit přesně: umíme-li z množiny předpokladů Toto pravidlo nazýváme zavedení 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 Jak přesně formulovat toto odvozovací pravidlo? Umíme-li z množiny předpokladů Tato dvě pravidla nazýváme eliminace konjunkce. 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 V Coqu pravidlo zavedení konjunkce používáme příkazem V následujícím příkladu máme dokázat právě V obou podcílech jsme měli dokázat něco, co jsme předpokládali: použili jsme tedy příkaz V dalším příkladu máme za cíl dokázat 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 Č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. Nyní jste již vybaveni vším, co potřebujete k důkazům tvrzení týkajících se čistě spojky konjunkce. Zkuste samostatně vyřešit následující úlohy (dokažte zadaná tvrzení). Za klíčové slovo 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¶
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¶
Pravidlo zavedení konjunkce¶
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
.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
Pravidlo eliminace konjunkce¶
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é.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
Práce s konjunkcí v Coq¶
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ý.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
.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
.assumption
. Všimněte si, že jednotlivé podcíle označujeme značkou -
, aby byl důkazový skript přehlednější.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.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ý).Další příklady a úlohy¶
Proof.
začněte tvořit důkazový skript, a po úspěšné tvorbě důkazu nahraďte klíčové slovo Admitted.
slovem Qed.