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>

José A. Alonso

5 Comentarios

theory El_problema_logico_del_mal
imports Main
begin

lemma notnotI: "P ⟹ ¬¬P"
  by simp

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
  by simp

lemma ejercicio_57:
  "⟦¬(C ∧ Q)⟧ ⟹ ¬C ∨ ¬Q"
  apply (rule ccontr)
  apply (erule notE)
  apply (rule conjI)
   apply (rule ccontr)
   apply (erule notE)
   apply (rule disjI1)
   apply assumption
  apply (rule ccontr)
  apply (erule notE)
  apply (rule disjI2)
  apply assumption
  done

lemma enrniecar:
  "¬Op ⟹ ¬(Op ∧ ¬M)"
  apply (rule ccontr)
  apply (drule notnotD)
  apply (erule conjE)
  apply (erule notE)
  apply assumption
  done

lemma enrniecar2:
  "M ⟹ ¬(Op ∧ ¬M)"
  apply (rule ccontr)
  apply (drule notnotD)
  apply (erule conjE)
  apply (erule notE)
  apply assumption
  done

lemma
  assumes "C ∧ Q ⟶ P" 
    "¬C ⟶ ¬Op" 
    "¬Q ⟶ M" 
    "¬P"
    "E ⟶ Op ∧ ¬M"
  shows  "¬E"
proof - 
  have "¬(C ∧ Q)" using ‹C ∧ Q ⟶ P› ‹¬P› by (rule mt)
  have "¬C∨¬Q" using ‹¬(C ∧ Q)› by (rule ejercicio_57)
  show "¬E"
  proof (rule disjE)
    show "¬C ∨ ¬Q" using ‹¬C ∨ ¬Q›by this
  next
    assume "¬C"
    have "¬Op" using ‹¬C ⟶ ¬Op› ‹¬C› by (rule mp)
    then have "¬(Op ∧ ¬M)" by (rule enrniecar)
    show "¬E" using ‹E ⟶ Op ∧ ¬M› ‹¬(Op ∧ ¬M)› by (rule mt)
  next
    assume "¬Q"
    have "M" using ‹¬Q ⟶ M› ‹¬Q› by (rule mp) 
    then have "¬(Op ∧ ¬M)" by (rule enrniecar2)
    show "¬E" using ‹E ⟶ Op ∧ ¬M› ‹¬(Op ∧ ¬M)› by (rule mt)
  qed
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 ejercicio_57:

"⟦¬(C ∧ Q)⟧ ⟹ ¬C ∨ ¬Q"

apply (rule ccontr)

apply (erule notE)

apply (rule conjI)

apply (rule ccontr)

apply (erule notE)

apply (rule disjI1)

apply assumption

apply (rule ccontr)

apply (erule notE)

apply (rule disjI2)

apply assumption

done

lemma enrniecar:

"¬Op ⟹ ¬(Op ∧ ¬M)"

apply (rule ccontr)

apply (drule notnotD)

apply (erule conjE)

apply (erule notE)

apply assumption

done

lemma enrniecar2:

"M ⟹ ¬(Op ∧ ¬M)"

apply (rule ccontr)

apply (drule notnotD)

apply (erule conjE)

apply (erule notE)

apply assumption

done

lemma

assumes "C ∧ Q ⟶ P"

"¬C ⟶ ¬Op"

"¬Q ⟶ M"

"¬P"

"E ⟶ Op ∧ ¬M"

shows "¬E"

proof -

have "¬(C ∧ Q)" using ‹C ∧ Q ⟶ P› ‹¬P› by (rule mt)

have "¬C∨¬Q" using ‹¬(C ∧ Q)› by (rule ejercicio_57)

show "¬E"

proof (rule disjE)

show "¬C ∨ ¬Q" using ‹¬C ∨ ¬Q›by this

assume "¬C"

have "¬Op" using ‹¬C ⟶ ¬Op› ‹¬C› by (rule mp)

then have "¬(Op ∧ ¬M)" by (rule enrniecar)

show "¬E" using ‹E ⟶ Op ∧ ¬M› ‹¬(Op ∧ ¬M)› by (rule mt)

assume "¬Q"

have "M" using ‹¬Q ⟶ M› ‹¬Q› by (rule mp)

then have "¬(Op ∧ ¬M)" by (rule enrniecar2)

show "¬E" using ‹E ⟶ Op ∧ ¬M› ‹¬(Op ∧ ¬M)› by (rule mt)

qed

end

Responder

lemma
  assumes "C ∧ Q ⟶ P" 
    "¬C ⟶ ¬Op" 
    "¬Q ⟶ M" 
    "¬P"  
    "E ⟶ Op ∧ ¬M"
  shows  "¬E"
proof (rule notI)
  assume "E"
  have "Op ∧ ¬M" using assms(5) `E` by (rule mp)
  then have "Op" by (rule conjunct1)
  then have "¬¬Op" by (rule notnotI)
  have "¬¬C" using assms(2) `¬¬Op` by (rule mt)
  then have "C" by (rule notnotD) 
  have "¬M" using `Op ∧ ¬M` by (rule conjunct2)
  have "¬¬Q" using assms(3) `¬M` by (rule mt)
  then have "Q" by (rule notnotD)
  have "C ∧ Q" using `C` `Q` by (rule conjI)
  have "P" using assms(1) `C ∧ Q` by (rule mp)
  show "False" using assms(4) `P` by (rule notE)
qed

lemma

assumes "C ∧ Q ⟶ P"

"¬C ⟶ ¬Op"

"¬Q ⟶ M"

"¬P"

"E ⟶ Op ∧ ¬M"

shows "¬E"

proof (rule notI)

assume "E"

have "Op ∧ ¬M" using assms(5) `E` by (rule mp)

then have "Op" by (rule conjunct1)

then have "¬¬Op" by (rule notnotI)

have "¬¬C" using assms(2) `¬¬Op` by (rule mt)

then have "C" by (rule notnotD)

have "¬M" using `Op ∧ ¬M` by (rule conjunct2)

have "¬¬Q" using assms(3) `¬M` by (rule mt)

then have "Q" by (rule notnotD)

have "C ∧ Q" using `C` `Q` by (rule conjI)

have "P" using assms(1) `C ∧ Q` by (rule mp)

show "False" using assms(4) `P` by (rule notE)

qed

Responder

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 assms(5) have  "Op ∧ ¬M"  by (rule mp)
  hence "Op" by (rule conjunct1)
  hence "¬¬Op" by (rule notnotI) 
  with assms(2) have "¬¬C" by (rule mt)
  hence "C" by (rule notnotD)
  have "¬M" using ‹Op ∧ ¬M› by (rule conjunct2)
  with assms(3) have "¬¬Q" by (rule mt)
  hence "Q" by (rule notnotD)
  with ‹C›  have "C∧Q" by (rule conjI)
  with assms(1) have "P" by (rule mp)
  with assms(4) show False by (rule notE)
qed

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 assms(5) have "Op ∧ ¬M" by (rule mp)

hence "Op" by (rule conjunct1)

hence "¬¬Op" by (rule notnotI)

with assms(2) have "¬¬C" by (rule mt)

hence "C" by (rule notnotD)

have "¬M" using ‹Op ∧ ¬M› by (rule conjunct2)

with assms(3) have "¬¬Q" by (rule mt)

hence "Q" by (rule notnotD)

with ‹C› have "C∧Q" by (rule conjI)

with assms(1) have "P" by (rule mp)

with assms(4) show False by (rule notE)

qed

Responder

lemma
  assumes "C ∧ Q ⟶ P" 
    "¬C ⟶ ¬Op" 
    "¬Q ⟶ M" 
    "¬P"  
    "E ⟶ Op ∧ ¬M"
  shows  "¬E"
proof (rule notI)
  assume "E"
  have "Op ∧ ¬M" using assms(5) `E`  by (rule mp)
  have "Op" using `Op ∧ ¬M` by (rule conjunct1)
  have "¬¬Op" using `Op` by (rule notnotI)
  have "¬¬C" using assms(2) `¬¬Op` by (rule mt)
  have "C" using `¬¬C` by (rule notnotD)
  have "¬M" using `Op ∧ ¬M` by (rule conjunct2)
  have "¬¬Q" using assms(3) `¬M` by (rule mt)
  have "Q" using `¬¬Q` by (rule notnotD)
  have "C ∧ Q" using `C` `Q` by (rule conjI)
  have "P" using assms(1) `C ∧ Q` by (rule mp)
  show False using assms(4) `P` by (rule notE)
qed

lemma

assumes "C ∧ Q ⟶ P"

"¬C ⟶ ¬Op"

"¬Q ⟶ M"

"¬P"

"E ⟶ Op ∧ ¬M"

shows "¬E"

proof (rule notI)

assume "E"

have "Op ∧ ¬M" using assms(5) `E` by (rule mp)

have "Op" using `Op ∧ ¬M` by (rule conjunct1)

have "¬¬Op" using `Op` by (rule notnotI)

have "¬¬C" using assms(2) `¬¬Op` by (rule mt)

have "C" using `¬¬C` by (rule notnotD)

have "¬M" using `Op ∧ ¬M` by (rule conjunct2)

have "¬¬Q" using assms(3) `¬M` by (rule mt)

have "Q" using `¬¬Q` by (rule notnotD)

have "C ∧ Q" using `C` `Q` by (rule conjI)

have "P" using assms(1) `C ∧ Q` by (rule mp)

show False using assms(4) `P` by (rule notE)

qed

Responder

Usando Lean 4

open Classical

theorem of_not_not [Decidable p] : ¬ ¬ p → p :=
  fun hnn ↦ byContradiction (fun hn ↦ absurd hn hnn)

-- a : Dios es capaz de evitar el mal
-- b : Dios quiere evitar el mal
-- c : Dios evita el mal
-- d : Dios es omnipotente
-- e : Dios es malévolo
-- f : Dios existe

theorem god_exists_1 (a b c d e f : Prop)
    (h1 : (a ∧ b) → c)
    (h2 : ¬ a → ¬ d)
    (h3 : ¬ b → e)
    (h4 : ¬ c)
    (h5 : f → (d ∧ ¬ e))
 : ¬f := by
  intro h
  have h6 := h5 h
  have h7 := And.left h6
  have h8 := And.right h6
  have h9 := mt h3 h8
  have h10 := mt h2 (not_not_intro h7)
  have h11 := of_not_not h10
  have h12 := of_not_not h9
  have h13 := And.intro h11 h12
  have h14 := h1 h13
  apply absurd h14 h4

open Classical

theorem of_not_not [Decidable p] : ¬ ¬ p → p :=

fun hnn ↦ byContradiction (fun hn ↦ absurd hn hnn)

-- a : Dios es capaz de evitar el mal

-- b : Dios quiere evitar el mal

-- c : Dios evita el mal

-- d : Dios es omnipotente

-- e : Dios es malévolo

-- f : Dios existe

theorem god_exists_1 (a b c d e f : Prop)

(h1 : (a ∧ b) → c)

(h2 : ¬ a → ¬ d)

(h3 : ¬ b → e)

(h4 : ¬ c)

(h5 : f → (d ∧ ¬ e))

: ¬f := by

intro h

have h6 := h5 h

have h7 := And.left h6

have h8 := And.right h6

have h9 := mt h3 h8

have h10 := mt h2 (not_not_intro h7)

have h11 := of_not_not h10

have h12 := of_not_not h9

have h13 := And.intro h11 h12

have h14 := h1 h13

apply absurd h14 h4

Responder

Soluciones con Isabelle/HOL

Otras soluciones

Share this:

5 Comentarios

Escribe un comentarioCancel reply