El problema lógico del mal
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, completando la siguiente teoría
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
theory El_problema_logico_del_mal imports Main begin (* 1ª demostración *) 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 (* 2ª demostración *) lemma assumes "C ∧ Q ⟶ P" "¬C ⟶ ¬Op" "¬Q ⟶ M" "¬P" "E ⟶ Op ∧ ¬M" shows "¬E" using assms by blast end