Se dice que la relación binaria \(R\) es

• reflexiva si \((∀x)R(x, x)\)
• circular si \((∀x, y, z)[R(x, y) ∧ R(y, z) ⟶ R(z, x)]\)
• simétrica si \((∀x, y)[R(x, y) ⟶ R(y, x)]\)

Demostrar que las relaciones reflexivas y circulares son simétricas. Para ello, completar la siguiente teoría de Isabelle/HOL:

theory Las_reflexivas_circulares_son_simetricas
imports Main
begin

lemma
  assumes "∀x. R(x, x)"
          "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
  oops

end

Read more…

Decidir si es cierto que

"Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las Chinas. Por consiguiente, Carlos no afeita a nadie."

Se usará la siguiente simbolización:

• A(x,y) para x afeita a y
• C(x) para x es un habitante de Las Chinas
• c para Carlos

El problema consiste en completar la siguiente teoría de Isabelle/HOL:

theory El_problema_del_barbero
imports Main
begin

lemma
  assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
  oops

end

Read more…

Decidir si es cierto que

"Existe una persona tal que si dicha persona se infecta, entonces todas las personas se infectan."

El problema consiste en completar la siguiente teoría de Isabelle/HOL:

theory El_problema_de_los_infectados
imports Main

begin

lemma "∃x. (I x ⟶ (∀y. I y))"
  by sorry

end

en la que se ha usado I(x) para representar que la persona x está infectada.

Read more…

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.

Read more…

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…

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…

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…

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…