Calculemus

Las reflexivas circulares son simétricas

PorJosé A. Alonso 8 abril 202021 agosto 2021

Se dice que la relación binaria R es

reflexiva si ∀x. R(x, x)
circular si ∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)
simétrica si ∀x y. R(x, y) ⟶ R(y, x)

Demostrar que las relaciones reflexivas y circulares son simétricas. Para ello, completar la siguiente teoría de Isabelle/HOL:

theory Las_reflexivas_circulares_son_simetricas
imports Main
begin

lemma
  assumes "∀x. R(x, x)"
          "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
  oops

end

theory Las_reflexivas_circulares_son_simetricas

imports Main

begin

lemma

assumes "∀x. R(x, x)"

"∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"

shows "∀x y. R(x, y) ⟶ R(y, x)"

oops

end

Soluciones con Isabelle/HOL

theory Las_reflexivas_circulares_son_simetricas
imports Main
begin

(* 1ª demostración: automática *)
lemma
  assumes "∀x. R(x, x)"
          "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
  using assms
  by blast

(* 2ª demostración: estructurada *)
lemma
  assumes "∀x. R(x, x)"
          "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
proof (rule allI)+
  fix a b
  show "R (a, b) ⟶ R (b, a)"
  proof (rule impI)
    assume "R(a, b)"
    have "R(b, b)"
      using assms(1) by (rule allE)
    with `R(a, b)` have "R(a, b) ∧ R(b, b)"
      by (rule conjI)
    have  "∀y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)"
      using assms(2) by (rule allE)
    then have "∀z. R(a, b) ∧ R(b, z) ⟶R(z, a)"
      by (rule allE)
    then have "R(a, b) ∧ R(b, b) ⟶R(b, a)"
      by (rule allE)
    then show "R(b, a)" using `R(a, b) ∧ R(b, b)`
      by (rule mp)
  qed
qed

(* 3º demostración: detallada *)
lemma
  assumes "∀x. R(x, x)"
          "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
proof (rule allI)+
  fix a b
  show "R (a, b) ⟶ R (b, a)"
  proof (rule impI)
    assume "R(a , b)"
    have "R(b, b)" using assms(1) ..
    with `R(a, b)` have "R(a, b) ∧ R(b, b)" ..
    have  "∀y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)" using assms(2) ..
    then have "∀z. R(a, b) ∧ R(b, z) ⟶R(z, a)" ..
    then have "R(a, b) ∧ R(b, b) ⟶R(b, a)" ..
    then show "R(b, a)" using `R(a, b) ∧ R(b, b)` ..
  qed
qed

end

theory Las_reflexivas_circulares_son_simetricas

imports Main

begin

(* 1ª demostración: automática *)

lemma

assumes "∀x. R(x, x)"

"∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"

shows "∀x y. R(x, y) ⟶ R(y, x)"

using assms

by blast

(* 2ª demostración: estructurada *)

lemma

assumes "∀x. R(x, x)"

"∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"

shows "∀x y. R(x, y) ⟶ R(y, x)"

proof (rule allI)+

fix a b

show "R (a, b) ⟶ R (b, a)"

proof (rule impI)

assume "R(a, b)"

have "R(b, b)"

using assms(1) by (rule allE)

with `R(a, b)` have "R(a, b) ∧ R(b, b)"

by (rule conjI)

have "∀y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)"

using assms(2) by (rule allE)

then have "∀z. R(a, b) ∧ R(b, z) ⟶R(z, a)"

by (rule allE)

then have "R(a, b) ∧ R(b, b) ⟶R(b, a)"

by (rule allE)

then show "R(b, a)" using `R(a, b) ∧ R(b, b)`

by (rule mp)

qed

(* 3º demostración: detallada *)

lemma

assumes "∀x. R(x, x)"

"∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"

shows "∀x y. R(x, y) ⟶ R(y, x)"

proof (rule allI)+

fix a b

show "R (a, b) ⟶ R (b, a)"

proof (rule impI)

assume "R(a , b)"

have "R(b, b)" using assms(1) ..

with `R(a, b)` have "R(a, b) ∧ R(b, b)" ..

have "∀y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)" using assms(2) ..

then have "∀z. R(a, b) ∧ R(b, z) ⟶R(z, a)" ..

then have "R(a, b) ∧ R(b, b) ⟶R(b, a)" ..

then show "R(b, a)" using `R(a, b) ∧ R(b, b)` ..

qed

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

El problema del barbero

PorJosé A. Alonso 31 marzo 202021 agosto 2021

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:

A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos

El problema consiste en completar la siguiente teoría de Isabelle/HOL:

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

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

Soluciones con Isabelle/HOL

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

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

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

El problema de los infectados

PorJosé A. Alonso 19 marzo 202021 agosto 2021

Decidir si es cierto que

Existe una persona tal que si dicha persona, 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:

Soluciones con Isabelle/HOL

theory Infectados
imports Main
begin

lemma "∃x. (I x ⟶ (∀y. I y))"
  by simp

end

theory Infectados

imports Main

begin

lemma "∃x. (I x ⟶ (∀y. I y))"

by simp

end

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

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))" ..

assume "∀y. I y"

then show "∃x. (I x ⟶ (∀y. I y))" by simp

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

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

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)

assume "∀y. I y"

then show "∃x. (I x ⟶ (∀y. I y))" by (rule aux4)

qed

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

La dama o el tigre

PorJosé A. Alonso 12 marzo 202021 agosto 2021

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, 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

c1 que representa el contenido del cartel de la puerta 1,
c2 que representa el contenido del cartel de la puerta 2 ,
dp que representa hay una dama en la primera habitación,
tp que representa hay un tigre en la primera habitación,
ds que representa hay una dama en la segunda habitación y
ts que representa hay un tigre en la segunda habitación.

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

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.

Soluciones con Isabelle/HOL

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

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› ..

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› ..

assume "ds ∧ tp"

then show ds ..

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)

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)

assume "ds ∧ tp"

then show ds by (rule conjunct1)

qed

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

El problema lógico del mal

PorJosé A. Alonso 5 marzo 202021 agosto 2021

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

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

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

C: Dios es capaz de evitar el mal.
Q: Dios quiere evitar el mal.
Op: Dios es omnipotente.
M: Dios es malévolo.
P: Dios evita el mal.
E: Dios existe.

Soluciones con Isabelle/HOL

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

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

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>