V´ yrokov´ a logika – dokazatelnost Ke zjiˇstˇen´ı, zda formule s´emanticky plyne z dan´e teorie (mnoˇziny formul´ı), m´ame k dispozici tabulkovou metodu. Velikost tabulky vˇsak roste exponenci´alnˇe vzhledem k poˇctu v´ yrokov´ ych symbol˚ u ve formuli. Jiˇz pro relativnˇe mal´ y poˇcet v´ yrokov´ ych symbol˚ u je tedy tabulkov´a metoda ne´ unosn´a. Nab´ız´ı se ot´azka, jestli nen´ı moˇzn´e o s´emantick´em vypl´ yv´an´ı rozhodnout i jinak.
Dokazatelnost (syntaktick´ e vypl´ yv´ an´ı) Dokazatelnost formalizuje intuitivnˇe ch´apan´e pojet´ı d˚ ukazu a je zaloˇzena na manipulaci s formulemi na syntaktick´e u ´rovni. Na rozd´ıl od s´emantick´eho vypl´ yv´an´ı nijak nepracuje s pojmem pravdivost formul´ı. Z´akladn´ı pojmy: • axiomov´a sch´emata, kter´a formalizuj´ı z´akladn´ı vlastnosti a vz´ajemn´ y vztah logick´ ych spojek: ϕ ⇒ (ψ ⇒ ϕ) (ϕ ⇒ (ψ ⇒ χ)) ⇒ ((ϕ ⇒ ψ) ⇒ (ϕ ⇒ χ)) (¬ψ ⇒ ¬ϕ) ⇒ (ϕ ⇒ ψ)
(A1) (A2) (A3)
Jak´akoli formule, kter´a je ve tvaru (A1)–(A3), se naz´ yv´a axiom VL. Jin´ ymi slovy, nahrazen´ım symbol˚ u ϕ, ψ a χ v axiomov´ ych sch´ematech libovoln´ ymi formulemi z´ısk´ame axiom VL. Je vˇsak nutn´e nahrazovat konzistentnˇe – tedy kaˇzd´ y v´ yskyt ϕ nahrad´ıme stejnou formul´ı atd. • pravidlo odlouˇcen´ı (modus ponens, MP): ϕ, ϕ ⇒ ψ ψ Tedy z formul´ı ϕ a ϕ ⇒ ψ m˚ uˇzeme odvodit (odlouˇcit) ψ. • d˚ ukaz formule ϕ z teorie (mnoˇziny formul´ı) T je koneˇcn´a posloupnost formul´ı ϕ1 , . . . , ϕn , kde ϕn = ϕ a kaˇzd´a ϕi (1 ≤ i ≤ n) – je axiomem VL, nebo – je formule z T , nebo – vznikla z pˇredchoz´ıch formul´ı pouˇzit´ım pravidla odlouˇcen´ı, tedy existuj´ı indexy j, k < i tak, ˇze ϕk je ve tvaru ϕj ⇒ ϕi . 1
Pˇr´ıklad pouˇzit´ı pravidla odlouˇcen´ı: Uvaˇzujme posloupnost formul´ı ϕ1 , . . . , ϕj ⇒ ϕi , . . . , ϕj , . . . , ϕm | {z } ϕk
Tuto posloupnost m˚ uˇzeme rozˇs´ıˇrit o formuli ϕi , jelikoˇz existuj´ı formule ϕj , ϕk , pro kter´e plat´ı j, k < i a ϕk je ve tvaru ϕj ⇒ ϕi . Pouˇzit´ım pravidla odlouˇcen´ı tedy dostaneme posloupnost ϕ1 , . . . , ϕj ⇒ ϕi , . . . , ϕj , . . . , ϕm , ϕi Formule ϕ je dokazateln´a z T (T ` ϕ), pokud existuje d˚ ukaz ϕ z T . Pokud plat´ı ` ϕ, potom ˇr´ık´ame, ˇze ϕ je dokazateln´a (z pr´azdn´eho syst´emu pˇredpoklad˚ u).
Z´ akladn´ı principy Pˇri dokazov´an´ı lze vyuˇz´ıt n´asleduj´ıc´ı vlastnosti dokazatelnosti ` (d˚ ukazy viz pˇredn´aˇska): • Pro kaˇzdou teorii T a libovoln´e formule ϕ, ψ plat´ı: Jestliˇze T ` ϕ a T ` ϕ ⇒ ψ, potom T ` ψ. • Pro libovolnou formuli ϕ plat´ı: `ϕ⇒ϕ • (Monotonie dokazatelnosti, MD) Necht’ jsou T, S libovoln´e teorie a ϕ, ψ jsou formule. Potom plat´ı: Pokud T ` ϕ a pro kaˇzdou ψ ∈ T plat´ı S ` ψ, potom S ` ϕ. Jednoduch´ y pˇr´ıklad uˇzit´ı: – Pˇredpokl´adejme, ˇze pro nˇejakou teorii T a nˇejakou formuli ϕ m´ame T ` ϕ, potom z monotonie dokazatelnosti ihned dost´av´ame, ˇze T, χ ` ϕ pro libovolnou formuli χ. Zd˚ uvodnˇen´ı: teorie S je v tomto pˇr´ıpadˇe S = T ∪ {χ} a evidentnˇe pro libovolnou ψ ∈ T existuje d˚ ukaz z T , t´ım sp´ıˇse bude existovat d˚ ukaz z S = T ∪ {χ}, tedy m´ame S ` ψ. Pˇredpoklady vˇety jsou splnˇeny, proto m˚ uˇzeme usoudit S ` ϕ. 2
• (Vˇeta o dedukci, VoD) Pro kaˇzdou teorii T a libovoln´e formule ϕ, ψ plat´ı: T ` ϕ ⇒ ψ pr´avˇe kdyˇz T, ϕ ` ψ • (Tranzitivita implikace, TI) Pro kaˇzdou teorii T a libovoln´e formule ϕ, ψ, χ plat´ı: Jestliˇze T ` ϕ ⇒ ψ a T ` ψ ⇒ χ, potom T ` ϕ ⇒ χ.
D˚ ukazy tvrzen´ı (a` ), (b` ) a (c` ) Tvrzen´ı (a` ) Pro libovoln´e formule ϕ, ψ plat´ı: ` ¬ϕ ⇒ (ϕ ⇒ ψ) D˚ ukaz (a` ) Necht’ jsou ϕ, ψ libovoln´e formule. Potom 1. 2. 3.
` ¬ϕ ⇒ (¬ψ ⇒ ¬ϕ) ` (¬ψ ⇒ ¬ϕ) ⇒ (ϕ ⇒ ψ) ` ¬ϕ ⇒ (ϕ ⇒ ψ)
(A1) (A3) (TI) z krok˚ u 1. a 2.
Vysvˇ etlen´ı d˚ ukazu (a` ) Jelikoˇz jsme pˇredpokl´adali, ˇze ϕ a ψ jsou formule, potom z definice jsou formulemi i ¬ϕ a ¬ψ. Evidentnˇe i ¬ϕ ⇒ (¬ψ ⇒ ¬ϕ) je formule. Nav´ıc je tato formule ve tvaru axiomov´eho sch´ematu (A1), jedn´a se tedy o axiom VL. Obdobnˇe pak pro formuli z druh´eho kroku, jeˇz je ve tvaru axiomov´eho sch´ematu (A3). Nenechte se zm´ast, ˇze se v definici axiomov´ ych sch´emat vyskytuj´ı symboly ϕ, ψ atd. Jedn´a se o z´astupn´e symboly, kter´e pom´ahaj´ı zn´azornit strukturu axiomov´eho sch´ematu. Nam´ısto tˇechto symbol˚ u si m˚ uˇzete pˇredstavit napˇr. symboly A, B, atd. Pokud za kaˇzd´ y takov´ y symbol dosad´ıme libovolnou formuli (za stejn´ y symbol stejnou formuli), dostaneme axiom VL.
3
N´asleduj´ıc´ı diagram zn´azorˇ nuje, jak byl vytvoˇren axiom, kter´ y se vyskytuje v prvn´ım kroku d˚ ukazu. Axiomov´e sch´ema 1 Axiom VL
A ⇒ (B ⇒ A) ↓ ↓ ↓ ¬ϕ ⇒ (¬ψ ⇒ ¬ϕ)
Vˇsimnˇete si, ˇze za symbol A byla na obou m´ıstech dosazena stejn´a formule ¬ϕ, za symbol B potom ¬ψ. Stejn´ ym zp˚ usobem obdrˇz´ıme axiom ve druh´em kroku, pouze vyuˇzijeme axiomov´e sch´ema 3: Axiomov´e sch´ema 3 (¬B ⇒ ¬A) ⇒ (A ⇒ B) ↓ ↓ ↓ ↓ Axiom VL (¬ψ ⇒ ¬ϕ) ⇒ (ϕ ⇒ ψ) Nyn´ı jsme za symbol A dosadili formuli ϕ a za symbol B formuli ψ. Tˇret´ı krok d˚ ukazu kombinuje pˇredchoz´ı dva kroky uˇzit´ım tranzitivity implikace. Tranzitivita implikace ˇr´ık´a, ˇze pro kaˇzdou teorii T a libovoln´e formule ϕ0 , ψ 0 , χ0 plat´ı1 : Jestliˇze T ` ϕ0 ⇒ ψ 0 a T ` ψ 0 ⇒ χ0 , potom T ` ϕ0 ⇒ χ0 . V naˇsem konkr´etn´ım pˇr´ıpadu m´ame T = ∅, ϕ0 = ¬ϕ, ψ 0 = (¬ψ ⇒ ¬ϕ), χ0 = (ϕ ⇒ ψ) a tedy jestliˇze ` ¬ϕ ⇒ (¬ψ ⇒ ¬ϕ) a
` (¬ψ ⇒ ¬ϕ) ⇒ (ϕ ⇒ ψ)
potom plat´ı ` ¬ϕ ⇒ (ϕ ⇒ ψ) Z krok˚ u 1. a 2. ale vid´ıme, ˇze plat´ı jak ` ¬ϕ ⇒ (¬ψ ⇒ ¬ϕ), tak i ` (¬ψ ⇒ ¬ϕ) ⇒ (ϕ ⇒ ψ). Takˇze m˚ uˇzeme z tranzitivity implikace usoudit, ˇze ` ¬ϕ ⇒ (ϕ ⇒ ψ), coˇz jsme chtˇeli dok´azat. Nav´ıc jsme pˇredpokl´adali, ˇze ϕ a ψ jsou libovoln´e formule, ˇcehoˇz vz´apˇet´ı vyuˇzijeme pˇri d˚ ukazu tvrzen´ı (b` ).
1
Formule byly pˇreznaˇceny, aby nekolidovaly s formulemi, kter´e se vyskytuj´ı v d˚ ukazu.
4
Tvrzen´ı (b` ) Pro libovolnou formuli ϕ plat´ı: ` ¬¬ϕ ⇒ ϕ D˚ ukaz (b` ) Necht’ je ϕ libovoln´a formule. Potom 1. 2. 3. 4. 5. 6. 7.
` ¬¬ϕ ⇒ (¬ϕ ⇒ ¬¬¬ϕ) ¬¬ϕ ` ¬ϕ ⇒ ¬¬¬ϕ ` (¬ϕ ⇒ ¬¬¬ϕ) ⇒ (¬¬ϕ ⇒ ϕ) ¬¬ϕ ` (¬ϕ ⇒ ¬¬¬ϕ) ⇒ (¬¬ϕ ⇒ ϕ) ¬¬ϕ ` ¬¬ϕ ⇒ ϕ ¬¬ϕ ` ϕ ` ¬¬ϕ ⇒ ϕ
(a` ) (VoD) (A3) (MD) (MP) (VoD) (VoD)
z 1. kroku z z z z
3. 2. 5. 6.
kroku a 4. kroku kroku kroku
Vysvˇ etlen´ı d˚ ukazu (b` ) Jelikoˇz je princip podobn´ y, rozebereme jen nˇekter´e kroky. K prvn´ımu kroku: Z (a` ) v´ıme, ˇze pro libovoln´e formule ϕ0 , ψ 0 plat´ı ` ¬ϕ0 ⇒ (ϕ0 ⇒ ψ 0 ) Fakt z 1. kroku z´ısk´ame, pokud poloˇz´ıme ϕ0 = ¬ϕ a ψ 0 = ¬¬¬ϕ. V 5. kroku jsme zjistili, ˇze ¬¬ϕ ` ¬¬ϕ ⇒ ϕ. Jin´ ymi slovy, z teorie {¬¬ϕ} je dokazateln´a formule ¬¬ϕ ⇒ ϕ. V 6. kroku vyuˇzijeme vˇetu o dedukci na 5. krok: obohat´ıme teorii z 5. kroku, tj. teorii {¬¬ϕ}, o formuli ¬¬ϕ a z takto obohacen´e teorie je potom podle vˇety o dedukci dokazateln´a formule ϕ. Nicm´enˇe teorie je mnoˇzina formul´ı, obohacen´a teorie je tedy ve tvaru {¬¬ϕ} ∪ {¬¬ϕ} = {¬¬ϕ}. Odtud je jiˇz zˇrejm´ y 6. krok.
5
Tvrzen´ı (c` ) Pro libovolnou formuli ϕ plat´ı: ` ϕ ⇒ ¬¬ϕ D˚ ukaz (c` ) Necht’ je ϕ libovoln´a formule. Potom 1. 2. 3.
` ¬¬¬ϕ ⇒ ¬ϕ ` (¬¬¬ϕ ⇒ ¬ϕ) ⇒ (ϕ ⇒ ¬¬ϕ) ` ϕ ⇒ ¬¬ϕ
6
(b` ) (A3) (MP) z 1. a 2. kroku
