{"id":212,"date":"2020-03-05T00:35:19","date_gmt":"2020-03-04T22:35:19","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=212"},"modified":"2021-08-21T12:55:18","modified_gmt":"2021-08-21T10:55:18","slug":"el-problema-logico-del-mal","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/el-problema-logico-del-mal\/","title":{"rendered":"El problema l\u00f3gico del mal"},"content":{"rendered":"

El problema l\u00f3gico\u200b del mal<\/a> intenta demostrar la inconsistencia l\u00f3gica entre la existencia de una entidad omnipotente, omnibenevolente y omnisciente y la existencia del mal. Se ha atribuido al fil\u00f3sofo griego Epicuro la formulaci\u00f3n original del problema del mal y este argumento puede esquematizarse como sigue:<\/p>\n

\nSi Dios fuera capaz de evitar el mal y quisiera hacerlo, lo har\u00eda. Si Dios fuera incapaz de evitar el mal, no ser\u00eda omnipotente; si no quisiera evitar el mal ser\u00eda mal\u00e9volo. Dios no evita el mal. Si Dios existe, es omnipotente y no es mal\u00e9volo. Luego, Dios no existe.\n<\/p><\/blockquote>\n

Demostrar con Isabelle\/HOL la correcci\u00f3n del argumento<\/p>\n

\ntheory El_problema_logico_del_mal\nimports Main\nbegin\n\nlemma\n  assumes \"C \u2227 Q \u27f6 P\"\n          \"\u00acC \u27f6 \u00acOp\"\n          \"\u00acQ \u27f6 M\"\n          \"\u00acP\"\n          \"E \u27f6 Op \u2227 \u00acM\"\n  shows  \"\u00acE\"\n  oops\nend\n<\/pre>\n
donde se han usado los siguientes s\u00edmbolos<\/p>\n
    \n
  • C:  Dios es capaz de evitar el mal.<\/li>\n
  • Q:  Dios quiere evitar el mal.<\/li>\n
  • Op: Dios es omnipotente.<\/li>\n
  • M:  Dios es mal\u00e9volo.<\/li>\n
  • P:  Dios evita el mal.<\/li>\n
  • E:  Dios existe.<\/li>\n<\/ul>\n
    Soluciones con Isabelle\/HOL<\/h4>\n
    \ntheory El_problema_logico_del_mal\nimports Main\nbegin\n\nlemma notnotI: \"P \u27f9 \u00ac\u00acP\"\n  by simp\n\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\n  by simp\n\nlemma\n  assumes \"C \u2227 Q \u27f6 P\"\n          \"\u00acC \u27f6 \u00acOp\"\n          \"\u00acQ \u27f6 M\"\n          \"\u00acP\"\n          \"E \u27f6 Op \u2227 \u00acM\"\n  shows  \"\u00acE\"\nproof (rule notI)\n  assume \"E\"\n  with \u2039E \u27f6 Op \u2227 \u00acM\u203a have \"Op \u2227 \u00acM\" by (rule mp)\n  then have \"Op\" by (rule conjunct1)\n  then have \"\u00ac\u00acOp\" by (rule notnotI)\n  with \u2039\u00acC \u27f6 \u00acOp\u203a have \"\u00ac\u00acC\" by (rule mt)\n  then have \"C\" by (rule notnotD)\n  moreover\n  have \"\u00acM\" using \u2039Op \u2227 \u00acM\u203a by (rule conjunct2)\n  with \u2039\u00acQ \u27f6 M\u203a have \"\u00ac\u00acQ\" by (rule mt)\n  then have \"Q\" by (rule notnotD)\n  ultimately have \"C \u2227 Q\" by (rule conjI)\n  with \u2039C \u2227 Q \u27f6 P\u203a have \"P\" by (rule mp)\n  with \u2039\u00acP\u203a show False by (rule notE)\nqed\n\nend\n<\/pre>\n
    Otras soluciones<\/h4>\n
      \n
    • Se pueden escribir otras soluciones en los comentarios.\n
    • El c\u00f3digo se debe escribir entre una l\u00ednea con <pre lang="isar"> y otra con <\/pre>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"
      El problema l\u00f3gico\u200b del mal intenta demostrar la inconsistencia l\u00f3gica entre la existencia de una entidad omnipotente, omnibenevolente y omnisciente y la existencia del mal. Se ha atribuido al fil\u00f3sofo griego Epicuro la formulaci\u00f3n 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\u00eda. Si Dios fuera incapaz de evitar el mal, no ser\u00eda omnipotente; si no quisiera evitar el mal ser\u00eda mal\u00e9volo. Dios no evita el mal. Si Dios existe, es omnipotente y no es mal\u00e9volo. Luego, Dios no existe. Demostrar con Isabelle\/HOL la correcci\u00f3n del argumento theory El_problema_logico_del_mal imports Main begin lemma assumes \u00abC \u2227 Q \u27f6 P\u00bb \u00ab\u00acC \u27f6 \u00acOp\u00bb \u00ab\u00acQ \u27f6 M\u00bb \u00ab\u00acP\u00bb \u00abE \u27f6 Op…<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[103],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/212"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=212"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/212\/revisions"}],"predecessor-version":[{"id":270,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/212\/revisions\/270"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=212"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=212"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=212"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}