Skip to main content

El problema lógico del mal

Lógica proposicional

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.

Read more…

Praeclarum theorema

Proposicional

Demostrar con Isabelle/HOL el Praeclarum theorema de Leibniz: \[ (p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s)) \]

Para ello, completar la siguiente teoría

theory Praeclarum_theorema
imports Main
begin

lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
  oops

end

Soluciones con Isabelle/HOL

theory Praeclarum_theorema
imports Main
begin

(* 1ª 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

(* 2ª 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

(* 3ª 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

(* 4ª demostración: automática *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
  by simp

end

Teorema de Nicómaco

Inducción

Demostrar el teorema de Nicómaco que afirma que la suma de los cubos de los \(n\) primeros números naturales es igual que el cuadrado de la suma de los \(n\) primeros números naturales; es decir, para todo número natural n se tiene que \[ 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2 \]

Read more…

Reto f(f(f(b))) = f(b)

Razonamiento ecuacional

El problema de hoy está basado en el reto Daily Challenge #168 que se planteó ayer. El reto consiste en demostrar que si f es una función de los booleanos en los booleanos, entonces para todo b se verifica que f (f (f b)) = f b.

Concretamente, el reto consiste en completar la siguiente demostración

lemma
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  sorry

Read more…

Celebración del día mundial de la lógica

Lógica de primer orden

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.

Read more…

Día mundial de la lógica

Misceláneas

El Consejo Ejecutivo de la UNESCO ha proclamado el 14 de enero como Día mundial de la jógica.

Día mundial de la lógica

La fecha del 14 de enero se ha eligido para rendir homenaje a dos grandes lógicos del siglo XX: Kurt Gödel (que falleció el 14 de enero de 1978) y Alfred Tarski (que nació el 14 de enero de 1901).

Uniéndose a dicha celebración, hoy (14 de enero de 2020) comienza la andadura de este blog cuyo principal objetivo es servir de complemento a las asignaturas de

El plan es proponer cada semana un ejercicio de forma que los alumnos pueden escribir las soluciones en los comentarios utilizando Isabelle/HOL en la demostración.

El código se escribe entre una línea con <pre lang="isar"> y otra con </pre>