Demostrar con Lean4 la paradoja del barbero; es decir, que no existe un hombre que afeite a todos los que no se afeitan a sí mismo y sólo a los que no se afeitan a sí mismo.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable (Hombre : Type) variable (afeita : Hombre → Hombre → Prop) example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := by sorry |
Decidir si es cierto que
Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las Chinas. Por consiguiente, Carlos no afeita a nadie.
Se usará la siguiente simbolización:
El problema consiste en completar la siguiente teoría de Isabelle/HOL:
|
1 2 3 4 5 6 7 8 9 10 |
theory El_problema_del_barbero imports Main begin lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" oops end |
|
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 |
theory El_problema_del_barbero imports Main begin ― ‹La demostración automática es› lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" using assms by auto ― ‹La demostración estructurada es› lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" proof - have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) .. have "A(c,c)" proof (rule ccontr) assume "¬A(c,c)" with assms(2) have "C(c) ∧ ¬A(c,c)" .. with 1 have "A(c,c)" .. with ‹¬A(c,c)› show False .. qed have "¬A(c,c)" proof - have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› .. then show "¬A(c,c)" .. qed then show "¬(∃x. A(c,x))" using ‹A(c,c)› .. qed ― ‹La demostración detallada es› lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" proof - have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE) have "A(c,c)" proof (rule ccontr) assume "¬A(c,c)" with assms(2) have "C(c) ∧ ¬A(c,c)" by (rule conjI) with 1 have "A(c,c)" by (rule iffD2) with ‹¬A(c,c)› show False by (rule notE) qed have "¬A(c,c)" proof - have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› by (rule iffD1) then show "¬A(c,c)" by (rule conjunct2) qed then show "¬(∃x. A(c,x))" using ‹A(c,c)› by (rule notE) qed end |
Decidir si es cierto que
Existe una persona tal que si dicha persona se infecta, entonces todas las personas se infectan.
En la formalización se usará I(x) para representar que la persona x está infectada. El problema consiste en completar la siguiente teoría de Isabelle/HOL:
|
1 2 3 4 5 6 7 8 |
theory Infectados imports Main begin lemma "∃x. (I x ⟶ (∀y. I y))" by simp end |
|
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 Infectados imports Main begin (* 1ª solución (automática) *) lemma "∃x. (I x ⟶ (∀y. I y))" by simp (* 2ª solución (estructurada) *) lemma "∃x. (I x ⟶ (∀y. I y))" proof - have "¬ (∀y. I y) ∨ (∀y. I y)" .. then show "∃x. (I x ⟶ (∀y. I y))" proof assume "¬ (∀y. I y)" then have "∃y. ¬(I y)" by simp then obtain a where "¬ I a" .. then have "I a ⟶ (∀y. I y)" by simp then show "∃x. (I x ⟶ (∀y. I y))" .. next assume "∀y. I y" then show "∃x. (I x ⟶ (∀y. I y))" by simp qed qed (* 3ª solución (detallada con lemas auxiliares) *) lemma aux1: assumes "¬ (∀y. I y)" shows "∃y. ¬(I y)" proof (rule ccontr) assume "∄y. ¬ I y" have "∀y. I y" proof fix a show "I a" proof (rule ccontr) assume "¬ I a" then have "∃y. ¬ I y" by (rule exI) with ‹∄y. ¬ I 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. (I x ⟶ (∀y. I y))" proof - have "¬ (∀y. I y) ∨ (∀y. I y)" .. then show "∃x. (I x ⟶ (∀y. I y))" proof assume "¬ (∀y. I y)" then have "∃y. ¬(I y)" by (rule aux1) then obtain a where "¬ I a" by (rule exE) then have "I a ⟶ (∀y. I y)" by (rule aux2) then show "∃x. (I x ⟶ (∀y. I y))" by (rule exI) next assume "∀y. I y" then show "∃x. (I x ⟶ (∀y. I y))" by (rule aux4) qed qed end |
En el libro de Raymond Smullyan ¿La dama o el tigre? (en inglés, The lady or the tiger? se plantea el siguiente problema
Un rey somete a un prisionero a la siguiente prueba: lo enfrenta a dos
puertas, de las que el prisionero debe elegir una, y entrar la habitación correspondiente. Se informa al prisionero que en cada una de las habitaciones puede haber un tigre o una dama. Como es natural, el prisionero debe elegir la puerta que le lleva a la dama (entre otras cosas, para no ser devorado por el tigre). Para ayudarle, en cada puerta hay un letrero. El de la puerta 1 dice «en esta habitación hay una dama y en la otra un tigre» y el de la puerta 2 dice «en una de estas habitaciones hay una dama y en una de estas habitaciones hay un tigre».Sabiendo que uno de los carteles dice la verdad y el otro no, demostrar que la dama se encuentra en la segunda habitación.
Para la formalización del problema se usarán los siguientes símbolos
|
1 2 3 4 5 6 7 8 9 10 11 12 |
theory La_dama_o_el_tigre imports Main begin lemma assumes "c1 ⟷ dp ∧ ts" "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)" "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)" shows "ds" oops end |
Demostrar con Isabelle/HOL que el argumento anterior es correcto.
|
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 |
theory La_dama_o_el_tigre imports Main begin (* 1ª demostración *) lemma assumes "c1 ⟷ dp ∧ ts" "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)" "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)" shows "ds" oops using assms by auto (* 2ª demostración *) lemma assumes "c1 ⟷ dp ∧ ts" "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)" "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)" shows "ds" proof - note ‹(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)› then show "ds" proof assume "c1 ∧ ¬ c2" then have "c1" .. with ‹c1 ⟷ dp ∧ ts› have "dp ∧ ts" .. then have "(dp ∧ ts) ∨ (ds ∧ tp)" .. with assms(2) have "c2" .. have "¬ c2" using ‹c1 ∧ ¬ c2› .. then show "ds" using ‹c2› .. next assume "c2 ∧ ¬ c1" then have "c2" .. with assms(2) have "(dp ∧ ts) ∨ (ds ∧ tp)" .. then show "ds" proof assume "dp ∧ ts" with assms(1) have c1 .. have "¬ c1" using ‹c2 ∧ ¬ c1› .. then show ds using ‹c1› .. next assume "ds ∧ tp" then show ds .. qed qed qed (* 3ª demostración *) lemma assumes "c1 ⟷ dp ∧ ts" "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)" "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)" shows "ds" proof - note ‹(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)› then show "ds" proof (rule disjE) assume "c1 ∧ ¬ c2" then have "c1" by (rule conjunct1) with ‹c1 ⟷ dp ∧ ts› have "dp ∧ ts" by (rule iffD1) then have "(dp ∧ ts) ∨ (ds ∧ tp)" by (rule disjI1) with assms(2) have "c2" by (rule iffD2) have "¬ c2" using ‹c1 ∧ ¬ c2› by (rule conjunct2) then show "ds" using ‹c2› by (rule notE) next assume "c2 ∧ ¬ c1" then have "c2" by (rule conjunct1) with assms(2) have "(dp ∧ ts) ∨ (ds ∧ tp)" by (rule iffD1) then show "ds" proof (rule disjE) assume "dp ∧ ts" with assms(1) have c1 by (rule iffD2) have "¬ c1" using ‹c2 ∧ ¬ c1› by (rule conjunct2) then show ds using ‹c1› by (rule notE) next assume "ds ∧ tp" then show ds by (rule conjunct1) qed qed qed end |
El problema lógico del mal intenta demostrar la inconsistencia lógica entre la existencia de una entidad omnipotente, omnibenevolente y omnisciente y la existencia del mal. Se ha atribuido al filósofo griego Epicuro la formulación original del problema del mal y este argumento puede esquematizarse como sigue:
Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo haría. Si Dios fuera incapaz de evitar el mal, no sería omnipotente; si no quisiera evitar el mal sería malévolo. Dios no evita el mal. Si Dios existe, es omnipotente y no es malévolo. Luego, Dios no existe.
Demostrar con Isabelle/HOL la corrección del argumento
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
theory El_problema_logico_del_mal imports Main begin lemma assumes "C ∧ Q ⟶ P" "¬C ⟶ ¬Op" "¬Q ⟶ M" "¬P" "E ⟶ Op ∧ ¬M" shows "¬E" oops end |
donde se han usado los siguientes símbolos
|
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 |
theory El_problema_logico_del_mal imports Main begin lemma notnotI: "P ⟹ ¬¬P" by simp lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" by simp lemma assumes "C ∧ Q ⟶ P" "¬C ⟶ ¬Op" "¬Q ⟶ M" "¬P" "E ⟶ Op ∧ ¬M" shows "¬E" proof (rule notI) assume "E" with ‹E ⟶ Op ∧ ¬M› have "Op ∧ ¬M" by (rule mp) then have "Op" by (rule conjunct1) then have "¬¬Op" by (rule notnotI) with ‹¬C ⟶ ¬Op› have "¬¬C" by (rule mt) then have "C" by (rule notnotD) moreover have "¬M" using ‹Op ∧ ¬M› by (rule conjunct2) with ‹¬Q ⟶ M› have "¬¬Q" by (rule mt) then have "Q" by (rule notnotD) ultimately have "C ∧ Q" by (rule conjI) with ‹C ∧ Q ⟶ P› have "P" by (rule mp) with ‹¬P› show False by (rule notE) qed end |
Demostrar el Praeclarum theorema de Leibniz:
|
1 2 3 4 5 6 7 8 |
theory Praeclarum_theorema imports Main begin lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))" oops end |
|
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 |
theory Praeclarum_theorema imports Main begin (* 1ª demostración: automática *) lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))" by simp (* 2ª demostración: aplicativa *) lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))" apply (rule impI) apply (rule impI) apply (erule conjE)+ apply (rule conjI) apply (erule mp) apply assumption apply (erule mp) apply assumption done (* 3ª demostración: estructurada *) lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))" proof assume "(p ⟶ q) ∧ (r ⟶ s)" show "(p ∧ r) ⟶ (q ∧ s)" proof assume "p ∧ r" show "q ∧ s" proof have "p ⟶ q" using ‹(p ⟶ q) ∧ (r ⟶ s)› .. moreover have "p" using ‹p ∧ r› .. ultimately show "q" .. next have "r ⟶ s" using ‹(p ⟶ q) ∧ (r ⟶ s)› .. moreover have "r" using ‹p ∧ r› .. ultimately show "s" .. qed qed qed (* 4ª demostración: detallada *) lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))" proof (rule impI) assume "(p ⟶ q) ∧ (r ⟶ s)" show "(p ∧ r) ⟶ (q ∧ s)" proof (rule impI) assume "p ∧ r" show "q ∧ s" proof (rule conjI) have "p ⟶ q" using ‹(p ⟶ q) ∧ (r ⟶ s)› by (rule conjunct1) moreover have "p" using ‹p ∧ r› by (rule conjunct1) ultimately show "q" by (rule mp) next have "r ⟶ s" using ‹(p ⟶ q) ∧ (r ⟶ s)› by (rule conjunct2) moreover have "r" using ‹p ∧ r› by (rule conjunct2) ultimately show "s" by (rule mp) qed qed qed end |
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.
|
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 |
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