Celebración del día mundial de la lógica
Decidir si es cierto que
Existe una Universidad tal que si en dicha Universidad se celebra el Día Mundial de la Lógica (DML), entonces en todas las Universidades se celebra el DML.
En la formalización usar C(x) para representar que en la Universidad x se celebra el DML.
Soluciones
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 |
theory Celebracion_del_DML imports Main begin (* 1ª solución (automática) *) lemma "∃x. (C x ⟶ (∀y. C y))" by simp (* 2ª solución (estructurada) *) lemma "∃x. (C x ⟶ (∀y. C y))" proof - have "¬ (∀y. C y) ∨ (∀y. C y)" .. then show "∃x. (C x ⟶ (∀y. C y))" proof assume "¬ (∀y. C y)" then have "∃y. ¬(C y)" by simp then obtain a where "¬ C a" .. then have "C a ⟶ (∀y. C y)" by simp then show "∃x. (C x ⟶ (∀y. C y))" .. next assume "∀y. C y" then show "∃x. (C x ⟶ (∀y. C y))" by simp qed qed (* 3ª solución (detallada con lemas auxiliares) *) lemma aux1: assumes "¬ (∀y. C y)" shows "∃y. ¬(C y)" proof (rule ccontr) assume "∄y. ¬ C y" have "∀y. C y" proof fix a show "C a" proof (rule ccontr) assume "¬ C a" then have "∃y. ¬ C y" by (rule exI) with ‹∄y. ¬ C y› show False by (rule notE) qed qed with assms show False by (rule notE) qed lemma aux2: assumes "¬P" shows "P ⟶ Q" proof assume "P" with assms show "Q" by (rule notE) qed lemma aux3: assumes "∄x. P x" shows "∀x. ¬ P x" proof fix a show "¬ P a" proof assume "P a" then have "∃x. P x" by (rule exI) with assms show False by (rule notE) qed qed lemma aux4: assumes "Q" shows "∃x. (P x ⟶ Q)" proof (rule ccontr) assume "∄x. (P x ⟶ Q)" then have "∀x. ¬ (P x ⟶ Q)" by (rule aux3) then have "¬ (P a ⟶ Q)" by (rule allE) moreover have "P a ⟶ Q" proof assume "P a" show "Q" using assms by this qed ultimately show False by (rule notE) qed lemma "∃x. (C x ⟶ (∀y. C y))" proof - have "¬ (∀y. C y) ∨ (∀y. C y)" .. then show "∃x. (C x ⟶ (∀y. C y))" proof assume "¬ (∀y. C y)" then have "∃y. ¬(C y)" by (rule aux1) then obtain a where "¬ C a" by (rule exE) then have "C a ⟶ (∀y. C y)" by (rule aux2) then show "∃x. (C x ⟶ (∀y. C y))" by (rule exI) next assume "∀y. C y" then show "∃x. (C x ⟶ (∀y. C y))" by (rule aux4) qed qed end |
Nota
- Se pueden añadir otras soluciones en los comentarios.
- El código se debe escribir entre una línea con <pre lang=»isar»> y otra con </pre>
Pensamiento
Si así fue, así pudo ser; si así fuera, así podría ser; pero como no es, no es. Eso es lógica.
Lewis Carroll
