1 (*:maxLineLen=80:*) 2 (* Vodite racuna kada preuzimate fajl da skinete thy, a ne htm - njega mozete 3 koristiti samo za brz pregled zato sto je laksi za online citanje *) 4 5 section ‹ Classical propositional logic › 6 7 theory Cas6_vezbe_resenja 8 imports Main 9 10 begin 11 12 subsection ‹Podsećanje sa predavanja› 13 14 subsubsection ‹Pravilo ccontr› 15 16 text‹Do sada su svi dokazi bili u okviru intuicionističke logike. Za rad sa 17 negacijom koristili smo dva pravila: 18 pravilo eliminacije negacije @{text notE}: @{text "⟦¬ P; P⟧ ⟹ R"}, 19 i pravilo uvođenja negacije @{text notI}: @{text "(P ⟹ False) ⟹ ¬ P"}.› 20 21 text‹Kada se radi u okvirima klasične logike, imamo mogućnost da koristimo i 22 pravilo @{text ccontr}: @{text "(¬ P ⟹ False) ⟹ P"}. Odnosno možemo da 23 izvodimo i dokaze uz pomoć kontradikcije, \emph{ccontr} označava 24 \emph{classical contradiction}.› 25 26 thm notE 27 thm notI 28 thm ccontr 29 30 31 lemma "¬ (A ∧ B) ⟶ ¬ A ∨ ¬ B" 32 apply (rule impI) 33 ― ‹primena pravila ccontr će prebaciti zaključak u negativnom obliku u premise, 34 i pokušaće da dokaze kontradikciju, odnosno False› 35 apply (rule ccontr) ―‹često se nad disjunkcijom u zaključku primenjuje ovo pravilo› 36 ― ‹kada imamo dve premise na koje možemo primeniti isto pravilo, možemo da biramo 37 da li ćemo primeniti na prvu ili drugu pretpostavku, međutim ovde nam odgovara 38 da ostavimo ovakvu primenu (bez back), zato što je bolje sa desne strane imati 39 konjunkciju nego disjunkciju; 40 Napomena: pogledajte šta se dešava kada stavite back› 41 apply (erule notE) 42 apply (rule conjI) 43 ―‹sada dokazujemo prvi podcilj› 44 apply (rule ccontr) 45 apply (erule notE) ― ‹ovde nam odgovara da imamo disjunkciju sa desne strane 46 zato što se jednostavno eliminiše› 47 apply (rule disjI1) 48 apply assumption 49 ―‹sada dokazujemo drugi podcilj› 50 apply (rule ccontr) 51 apply (erule notE) 52 apply (rule disjI2) 53 apply assumption 54 done 55 56 text‹Dokaz ove iste leme u Isar-u: › 57 58 lemma "¬ (A ∧ B) ⟶ ¬ A ∨ ¬ B" 59 proof 60 ― ‹isto kao da smo napisali @{text "proof (rule impI)"}, ali ovde će i sam Isabelle 61 primeniti pravilo impI pa nije neophodno da stoji i nakon toga ide assume Levo show Desno› 62 assume "¬ (A ∧ B)" 63 show "¬ A ∨ ¬ B" ― ‹ovo je naš cilj C › 64 proof (rule ccontr) 65 ― ‹obratite pažnju: ako ne napišemo ništa (pogledajte šta se dešava ako se samo 66 napiše @{text proof}), Isabelle će ovaj cilj transformisati u prvi disjunkt, što 67 nije ono što želimo - nije korektno, tako da moramo paziti i eksplicitno navesti 68 koje pravilo želimo da bude primenjeno› 69 70 ― ‹da bi dokazali cilj C na osnovu pravila ccontr, dovoljno je da pokažemo da 71 @{text "¬ C ⟹ False"}, pa nakon toga sledi @{text "assume ¬ C ... show False"} blok › 72 assume "¬ (¬ A ∨ ¬ B)" 73 have "A ∧ B" ― ‹među korak koji prvo dokazujemo › 74 proof 75 ― ‹sada nam odgovara da bude samo proof, bez crtice, jer Isabelle sam deli 76 ovaj cilj na dva cilja › 77 show "A" 78 proof (rule ccontr) 79 ― ‹slično kao gore, da bi dokazali A korišćenjem pravila ccontr, dovoljno je da 80 pokažemo @{text "¬ A ⟹ False"} odnosno sledi @{text "assume ¬ A ... show False"} blok › 81 assume "¬ A" 82 then have "¬ A ∨ ¬ B" 83 by (rule disjI1) 84 then show "False" 85 using ‹¬ (¬ A ∨ ¬B)› ― ‹sve do sada uvedene pretpostavke mogu se koristiti, 86 ali moraju biti navedene svojim vrednostima, između `...` › 87 by auto 88 qed 89 next 90 show "B" 91 proof (rule ccontr) 92 assume "¬ B" 93 then have "¬ A ∨ ¬ B" 94 by (rule disjI2) 95 then show "False" 96 using ‹¬ (¬ A ∨ ¬B)› 97 by auto 98 qed 99 qed 100 then show False 101 using `¬ (A ∧ B)` 102 by auto 103 qed 104 qed 105 106 subsubsection ‹ Pravilo classical › 107 108 text‹ Princip klasične logike se oslikava kroz pravilo 109 @{text classical}: @{text "(¬ P ⟹ P) ⟹ P"}. Postoji nekoliko ekvivalentnih 110 varijanti ovog pravila ali je ovaj oblik najpogodniji za upotrebu zato što ne menja 111 traženi zaključak teoreme. Ovo pravilo podrazumeva da u dokazu teoreme uvek možemo 112 pretpostaviti negaciju zaključka teoreme.› 113 114 thm classical 115 116 lemma "P ∨ ¬ P" 117 apply (rule classical) ―‹da bi smo dokazali A moramo da prvo dokažemo @{text "¬ A ⇒ A"}› 118 apply (rule disjI1) ―‹dovoljno je da dokažemo jednu od dve disjunkcije, a kako je sve simetricno, biramo da dokažemo P › 119 apply (rule classical) ―‹na postojeće pretpostavke dodajemo @{text "¬ P"} i pokušavamo da dokažemo P› 120 apply (erule notE) ―‹notE znači da treba da dokažemo pozitivan oblik iz preostalih pretpostavki› 121 apply (rule disjI2) 122 apply assumption 123 done 124 125 lemma "P ∨ ¬ P" 126 proof (rule classical) 127 ―‹ovde ne smemo ostaviti bez crtice, zato što Isabelle transformiše disjunkciju 128 u prvi disjunkt - u ovom trenutku to nam ne odgovara i ne možemo to dokazati 129 zato što još uvek nemamo nikakve pretpostavke; 130 nećemo ni sa crticom, već ćemo odmah reći koje pravilo želimo da se primeni› 131 assume "¬ (P ∨ ¬ P)" 132 show "P ∨ ¬ P" 133 proof 134 ―‹sada ćemo ostaviti bez crtice, zato što nam odgovara da primeni podrazumevano pravilo, 135 tj. disjI1› 136 show "P" 137 proof (rule classical) 138 assume "¬ P" 139 from this have "P ∨ ¬ P" by auto 140 from this `¬ (P ∨ ¬ P)` have False by auto 141 from this show "P" by auto 142 qed 143 qed 144 qed 145 146 subsection ‹Dodatni primeri› 147 148 text‹U klasičnoj logici, dokazati naredna tvrđenja:› 149 150 lemma "¬ ¬ A ⟶ A" 151 apply (rule impI) 152 ― ‹apply (erule notE) ne možemo primeniti ovo pravilo zato što ono očekuje da iz 153 @{text "¬ P"} i @{text P} možemo da izvedemo bilo šta. @{text "¬ P"} je ovde 154 @{text "¬ ¬ A"}, što znači da je @{text P} u stvari @{text "¬ A"}, i zato ono 155 postaje preostali cilj› 156 apply (rule ccontr) 157 apply (erule notE) 158 apply assumption 159 done 160 161 lemma "(¬ B ⟶ ¬ A) ⟶ (A ⟶ B)" 162 apply (rule impI) 163 apply (rule impI) 164 apply (rule ccontr) ― ‹prebacuje zaključak sa desna na levo i pokušavamo da 165 izvedemo kontradikciju› 166 apply (erule impE) 167 apply assumption 168 apply (erule notE) ― ‹eliminacija negacije, ali treba da je primenimo na drugu 169 negaciju, ne na @{text "¬ B"}, već na @{text "¬ A"}› 170 back 171 apply assumption 172 done 173 174 lemma "(A ⟶ B) ⟶ (¬ A ∨ B)" 175 apply (rule impI) 176 apply (rule ccontr) 177 apply (erule impE) 178 apply (rule ccontr) 179 apply (erule notE) 180 apply (rule disjI1) 181 apply assumption 182 apply (erule notE) 183 apply (rule disjI2) 184 apply assumption 185 done 186 187 lemma "(¬ P ⟶ Q) ⟷ (¬ Q ⟶ P)" 188 apply (rule iffI) ―‹dobijamo dva cilja; sada prvo razbijamo implikaciju sa desne 189 strane u prvom cilju › 190 apply (rule impI) ―‹sada prebacujemo zaključak na levu stranu i desno dobijamo False › 191 apply (rule ccontr) ―‹ovo nam odgovara zato što se sada @{text "¬ P"} dodaje među 192 pretpostavke, a već se pojavljuje kao leva strana implikacije › 193 apply (erule impE) 194 apply (assumption) 195 apply (erule notE) 196 apply assumption ―‹sada smo zatvorili prvi cilj, pa slično sa drugim ciljom› 197 apply (rule impI) 198 apply (rule ccontr) ―‹slično kao u prethodnoj primeni, odgovara nam da @{text "¬ Q"} 199 prebacimo u pretpostavke jer se već pojavljuje kao leva strana implikacije› 200 apply (erule impE) 201 apply assumption 202 apply (erule notE) 203 apply assumption 204 done 205 206 207 lemma "(¬ P ⟶ Q) ⟷ (¬ Q ⟶ P)" 208 apply (rule iffI) 209 apply (rule impI) 210 apply (rule ccontr) 211 apply (erule impE) 212 apply assumption 213 apply (erule notE) 214 apply assumption 215 apply (rule impI) 216 apply (rule ccontr) 217 apply (erule impE) 218 apply assumption 219 apply (erule notE) 220 apply assumption 221 done 222 223 text‹Pirsov zakon. Tipičan ne-intuicionistički primer koji će sigurno zahtevati 224 neki oblik klasične kontradikcije.› 225 226 lemma "((P ⟶ Q) ⟶ P) ⟶ P" 227 apply (rule impI) 228 apply (rule ccontr) ―‹primena klasične kontradikcije, dodajemo negirani zaključak 229 kao novu premisu i pokušavamo da izvedemo kontradikciju› 230 apply (erule impE) 231 apply (rule impI) 232 apply (erule notE) 233 apply assumption 234 apply (erule notE) 235 apply assumption 236 done 237 238 text‹Dokaz u Isar-u:› 239 240 lemma 241 assumes "(P ⟶ Q) ⟶ P" 242 shows "P" 243 proof (rule ccontr) ―‹dodajemo negaciju zaključka u premise i pokušavamo da izvedemo 244 kontradikciju› 245 assume "¬ P" 246 ―‹dodajemo međukorak› 247 have "P ⟶ Q" 248 proof 249 assume "P" 250 from this `¬ P` show "Q" by auto 251 qed 252 from this assms have "P" by auto 253 from this `¬ P` show False by auto 254 qed 255 256 text ‹Malo komplikovaniji primeri › 257 258 text ‹ 259 \begin{exmp} 260 Ako je relacija R simetricna, tranzitivna i ako za svako x postoji y koje je sa njim u 261 relaciji, onda je relacija R i refleksivna. 262 \end{exmp} 263 › 264 265 text‹Prvo je potrebno uvesti definicije pojmova koji se javljaju u postavci ovog zadatka:› 266 267 definition 268 "reflexive R ⟷ (∀ x. R x x)" 269 270 definition 271 "transitive R ⟷ (∀ x y z. R x y ∧ R y z ⟶ R x z)" 272 273 definition 274 "symmetric R ⟷ (∀ x y. R x y ⟷ R y x)" 275 276 lemma "symmetric R ∧ transitive R ∧ (∀ x. ∃ y. R x y) ⟶ reflexive R" 277 unfolding symmetric_def transitive_def reflexive_def 278 ―‹prvo primenjujemo unfolding da bismo radili nad samim formulama› 279 apply (rule impI) 280 apply (erule conjE) 281 apply (erule conjE) 282 apply (rule allI) ―‹uvodimo fiksirano ali proizvoljno x› 283 ―‹sada hoćemo da razbijemo treću premisu, da bismo dosli do exists› 284 apply (erule_tac x = "x" in allE) back back 285 apply (erule exE) ―‹uvodimo fiksirano y› 286 ―‹sada skidamo univerzalni kvantifikator za već dobijeno x› 287 apply (erule_tac x = "x" in allE) 288 apply (erule_tac x = "x" in allE) 289 ―‹sada treba da vodimo računa da nam je primarni kvantifikator po y, i odgovara 290 nam da ostane y (naspram x, pogledajte šta bi se dobilo na taj način)› 291 apply (erule_tac x = "y" in allE) 292 apply (erule_tac x = "y" in allE) 293 ―‹sada biramo sa čim ćemo da zamenimo z, odgovara nam x (pogledajte šta bi se 294 dobilo kada biste napisali y)› 295 apply (erule_tac x = "x" in allE) 296 ―‹sada radimo na uobičajeni nacin, nakon što smo sve unifikovali kako treba› 297 apply (erule impE) 298 apply (rule conjI) 299 apply assumption 300 apply (erule iffE) 301 apply (erule impE) 302 apply assumption 303 apply assumption 304 apply assumption 305 done 306 307 308 lemma 309 shows "(nA ⟷ bA ∨ bB) ∧ (nB ⟷ ¬ bA) ∧ ((nA ∧ nB) ∨ (¬ nA ∧ ¬ nB)) ⟶ ¬ bA ∧ bB" 310 apply (rule impI) ― ‹prvo razbijamo što više možemo levu stranu, da ne bismo prvo 311 razbili desnu pa onda dva puta ponavljali isti postupak za obe grane› 312 apply (erule conjE) 313 apply (erule conjE) 314 ―‹sada razbijamo disjunkciju i dobijamo dva podcilja› 315 apply (erule disjE) 316 apply (erule conjE) ―‹pokušavamo sa prvom ekvivalencijom› 317 apply (erule iffE) ―‹pokušavamo sa prvom ekvivalencijom› 318 ―‹napomena: ako se negde zaglavite u dokazu, možete se vratiti na ovakva mesta i sa 319 back pokušati sa primenom istog pravila na neku drugu pretpostavku› 320 apply (erule impE) 321 apply assumption 322 apply (erule iffE) 323 apply (erule impE) ―‹pokušavamo sa prvom implikacijom› 324 apply assumption 325 apply (erule impE) 326 apply assumption 327 apply (rule conjI) 328 apply assumption 329 apply (erule disjE) 330 apply (erule notE) 331 apply assumption 332 apply assumption 333 ―‹sada dokazujemo drugi podcilj› 334 apply (erule conjE) 335 apply (erule iffE) 336 apply (erule iffE) ―‹ako pokušamo da razbijemo prvu implikaciju dobijemo da treba 337 da dokažemo @{text nA}, a u pretpostavkama već imamo @{text "¬ nA"}, 338 pa je bolje da razbijemo drugu implikaciju› 339 ―‹sada pokušavamo da razbijemo drugu implikaciju› 340 apply (erule impE) back 341 apply (rule ccontr) ―‹sada primenjujemo pravilo ccontr; kada imamo disjunkciju u 342 zaključku, češto je ovo zgodno pravilo› 343 ―‹ako probamo da razbijemo prvu implikaciju, dobijamo @{text nA}, slično kao gore to 344 nam ne koristi› 345 ―‹ako probamo da razbijemo drugu implikaciju, dobijamo @{text nB}, slično kao malopre 346 to nam ne koristi jer u premisama imamo @{text "¬ nB"}; 347 pa pokušavamo sa trećom › 348 ―‹sada pokušavamo da razbijemo treću implikaciju› 349 apply (erule impE) back back 350 apply (rule notI) 351 ―‹sada pokušavamo da razbijemo prvu negaciju i vidimo da nam traži @{text nA} a to 352 ne možemo da dokažemo, pa pokušavamo sa drugom negacijom i dodajemo back; 353 sada vidimo da treba da dokažemo @{text nB}, što takođe ne možemo da uradimo 354 pa dodajemo još jedno back› 355 ―‹sada pokušavamo da razbijemo treću negaciju› 356 apply (erule notE) back back ―‹ovo je sada lako dokazati› 357 apply (rule disjI1) 358 apply assumption ―‹sada pokušavamo da razbijemo drugu negaciju, da bi izvukli 359 kontradikciju iz @{text "¬ nB"} i @{text nB}› 360 apply (erule notE) back 361 apply assumption 362 apply (erule notE) 363 apply assumption 364 done 365 end