Demostrar con Lean4 que \[ (P → Q) ↔ ¬P ∨ Q \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable (P Q : Prop)

example
  : (P → Q) ↔ ¬P ∨ Q :=
by sorry

Leer más…

Demostrar con Lean4 que \[ ¬¬P → P \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable (P : Prop)

example : ¬¬P → P :=
by sorry

Leer más…

Demostrar con Lean4 que \(P → ¬¬P\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable (P : Prop)

example
  (h : P)
  : ¬¬P :=
by sorry

Leer más…

Demostrar con Lean4 que \(¬¬P → P\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable (P : Prop)

example
  (h : ¬¬P)
  : P :=
by sorry

Leer más…

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, de las que el prisionero debe elegir una, y entrar la 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 ello, completar la siguiente teoría

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

donde se han usado 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.

Leer más…

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.

Leer más…