Calculemus

La dama o el tigre

PorJosé A. Alonso 12 marzo 202021 agosto 2021

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, 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 la formalización del problema se usarán 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.

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

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

Demostrar con Isabelle/HOL que el argumento anterior es correcto.

Soluciones con Isabelle/HOL

theory La_dama_o_el_tigre
imports Main
begin

(* 1ª demostración *)
lemma
  assumes "c1 ⟷ dp ∧ ts"
          "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)"
          "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)"
  shows   "ds"
  oops
  using assms
  by auto

(* 2ª demostración *)
lemma
  assumes "c1 ⟷ dp ∧ ts"
    "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)"
    "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)"
  shows "ds"
proof -
  note ‹(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)›
  then show "ds"
  proof
    assume "c1 ∧ ¬ c2"
    then have "c1" ..
    with ‹c1 ⟷ dp ∧ ts› have "dp ∧ ts" ..
    then have "(dp ∧ ts) ∨ (ds ∧ tp)" ..
    with assms(2) have "c2" ..
    have "¬ c2" using ‹c1 ∧ ¬ c2› ..
    then show "ds" using ‹c2› ..
  next
    assume "c2 ∧ ¬ c1"
    then have "c2" ..
    with assms(2) have "(dp ∧ ts) ∨ (ds ∧ tp)" ..
    then show "ds"
    proof
      assume "dp ∧ ts"
      with assms(1) have c1 ..
      have "¬ c1" using ‹c2 ∧ ¬ c1› ..
      then show ds using ‹c1› ..
    next
      assume "ds ∧ tp"
      then show ds ..
    qed
  qed
qed

(* 3ª demostración *)
lemma
  assumes "c1 ⟷ dp ∧ ts"
    "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)"
    "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)"
  shows "ds"
proof -
  note ‹(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)›
  then show "ds"
  proof (rule disjE)
    assume "c1 ∧ ¬ c2"
    then have "c1" by (rule conjunct1)
    with ‹c1 ⟷ dp ∧ ts› have "dp ∧ ts" by (rule iffD1)
    then have "(dp ∧ ts) ∨ (ds ∧ tp)" by (rule disjI1)
    with assms(2) have "c2" by (rule iffD2)
    have "¬ c2" using ‹c1 ∧ ¬ c2› by (rule conjunct2)
    then show "ds" using ‹c2› by (rule notE)
  next
    assume "c2 ∧ ¬ c1"
    then have "c2" by (rule conjunct1)
    with assms(2) have "(dp ∧ ts) ∨ (ds ∧ tp)" by (rule iffD1)
    then show "ds"
    proof (rule disjE)
      assume "dp ∧ ts"
      with assms(1) have c1 by (rule iffD2)
      have "¬ c1" using ‹c2 ∧ ¬ c1› by (rule conjunct2)
      then show ds using ‹c1› by (rule notE)
    next
      assume "ds ∧ tp"
      then show ds by (rule conjunct1)
    qed
  qed
qed

end

theory La_dama_o_el_tigre

imports Main

begin

(* 1ª demostración *)

lemma

assumes "c1 ⟷ dp ∧ ts"

"c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)"

"(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)"

shows "ds"

oops

using assms

by auto

(* 2ª demostración *)

lemma

assumes "c1 ⟷ dp ∧ ts"

"c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)"

"(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)"

shows "ds"

proof -

note ‹(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)›

then show "ds"

proof

assume "c1 ∧ ¬ c2"

then have "c1" ..

with ‹c1 ⟷ dp ∧ ts› have "dp ∧ ts" ..

then have "(dp ∧ ts) ∨ (ds ∧ tp)" ..

with assms(2) have "c2" ..

have "¬ c2" using ‹c1 ∧ ¬ c2› ..

then show "ds" using ‹c2› ..

assume "c2 ∧ ¬ c1"

then have "c2" ..

with assms(2) have "(dp ∧ ts) ∨ (ds ∧ tp)" ..

then show "ds"

proof

assume "dp ∧ ts"

with assms(1) have c1 ..

have "¬ c1" using ‹c2 ∧ ¬ c1› ..

then show ds using ‹c1› ..

assume "ds ∧ tp"

then show ds ..

qed

(* 3ª demostración *)

lemma

assumes "c1 ⟷ dp ∧ ts"

"c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)"

"(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)"

shows "ds"

proof -

note ‹(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)›

then show "ds"

proof (rule disjE)

assume "c1 ∧ ¬ c2"

then have "c1" by (rule conjunct1)

with ‹c1 ⟷ dp ∧ ts› have "dp ∧ ts" by (rule iffD1)

then have "(dp ∧ ts) ∨ (ds ∧ tp)" by (rule disjI1)

with assms(2) have "c2" by (rule iffD2)

have "¬ c2" using ‹c1 ∧ ¬ c2› by (rule conjunct2)

then show "ds" using ‹c2› by (rule notE)

assume "c2 ∧ ¬ c1"

then have "c2" by (rule conjunct1)

with assms(2) have "(dp ∧ ts) ∨ (ds ∧ tp)" by (rule iffD1)

then show "ds"

proof (rule disjE)

assume "dp ∧ ts"

with assms(1) have c1 by (rule iffD2)

have "¬ c1" using ‹c2 ∧ ¬ c1› by (rule conjunct2)

then show ds using ‹c1› by (rule notE)

assume "ds ∧ tp"

then show ds by (rule conjunct1)

qed

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

El problema lógico del mal

PorJosé A. Alonso 5 marzo 202021 agosto 2021

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

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

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 con Isabelle/HOL

theory El_problema_logico_del_mal
imports Main
begin

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

end

theory El_problema_logico_del_mal

imports Main

begin

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

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

Praeclarum theorema

PorJosé A. Alonso 24 febrero 202021 agosto 2021

Demostrar el Praeclarum theorema de Leibniz:

theory Praeclarum_theorema
imports Main
begin

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

end

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: automática *)
lemma "(p ⟶ q) ∧ (r ⟶ s) ⟶ ((p ∧ r) ⟶ (q ∧ s))"
  by simp

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

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

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

end

theory Praeclarum_theorema

imports Main

begin

(* 1ª demostración: automática *)

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

by simp

(* 2ª demostración: aplicativa *)

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

apply (rule impI)

apply (erule conjE)+

apply (rule conjI)

apply (erule mp)

apply assumption

apply (erule mp)

apply assumption

done

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

have "r ⟶ s" using ‹(p ⟶ q) ∧ (r ⟶ s)› ..

moreover have "r" using ‹p ∧ r› ..

ultimately show "s" ..

qed

(* 4ª 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)

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

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

Teorema de Nicómaco

PorJosé A. Alonso 30 enero 202021 agosto 2021

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³ + 2³ + ... + n³ = (1 + 2 + ... + n)²

1	1³ + 2³ + ... + n³ = (1 + 2 + ... + n)²

Soluciones con Isabelle/HOL

theory Teorema_de_Nicomaco
imports Main
begin

(* (suma n) es la suma de los primeros números naturales. *)
fun suma :: "nat ⇒ nat" where
  "suma 0 = 0"
| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)
fun sumaCubos :: "nat ⇒ nat" where
  "sumaCubos 0 = 0"
| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* Fórmula para la suma *)
lemma "2 * suma n = n^2 + n"
proof (induct n)
  show "2 * suma 0 = 0^2 + 0" by simp
next
  fix n
  assume "2 * suma n = n^2 + n"
  then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"
    by simp
  also have "… = (Suc n)^2 + Suc n"
    by (simp add: power2_eq_square)
  finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"
    by this
qed

(* Demostración automática de la propiedad anterior *)
lemma formula_suma:
  "2 * suma n = n^2 + n"
  by (induct n) (auto simp add: power2_eq_square)

lemma "4 * sumaCubos n = (n^2 + n)^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0^2 + 0)^2"
    by simp
next
  fix n
  assume "4 * sumaCubos n = (n^2 + n)^2"
  then have "4 * sumaCubos (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3"
    by simp
  then show "4 * sumaCubos (Suc n) = ((Suc n)^2 + Suc n)^2"
  by (simp add: algebra_simps
                power2_eq_square
                power3_eq_cube )
qed

(* Demostración automática de la propiedad anterior *)
lemma formula_sumaCubos:
  "4 * sumaCubos n = (n^2 + n)^2"
  by (induct n) (auto simp add: algebra_simps
                                power2_eq_square
                                power3_eq_cube)

(* Lema auxiliar *)
lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"
  by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)
theorem teorema_de_Nicomaco:
  "sumaCubos n = (suma n)^2"
  by (simp only: formula_suma formula_sumaCubos aux)

end

theory Teorema_de_Nicomaco

imports Main

begin

(* (suma n) es la suma de los primeros números naturales. *)

fun suma :: "nat ⇒ nat" where

"suma 0 = 0"

| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)

fun sumaCubos :: "nat ⇒ nat" where

"sumaCubos 0 = 0"

| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* Fórmula para la suma *)

lemma "2 * suma n = n^2 + n"

proof (induct n)

show "2 * suma 0 = 0^2 + 0" by simp

fix n

assume "2 * suma n = n^2 + n"

then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"

by simp

also have "… = (Suc n)^2 + Suc n"

by (simp add: power2_eq_square)

finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"

by this

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_suma:

"2 * suma n = n^2 + n"

by (induct n) (auto simp add: power2_eq_square)

lemma "4 * sumaCubos n = (n^2 + n)^2"

proof (induct n)

show "4 * sumaCubos 0 = (0^2 + 0)^2"

by simp

fix n

assume "4 * sumaCubos n = (n^2 + n)^2"

then have "4 * sumaCubos (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3"

by simp

then show "4 * sumaCubos (Suc n) = ((Suc n)^2 + Suc n)^2"

by (simp add: algebra_simps

power2_eq_square

power3_eq_cube )

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_sumaCubos:

"4 * sumaCubos n = (n^2 + n)^2"

by (induct n) (auto simp add: algebra_simps

power2_eq_square

power3_eq_cube)

(* Lema auxiliar *)

lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"

by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)

theorem teorema_de_Nicomaco:

"sumaCubos n = (suma n)^2"

by (simp only: formula_suma formula_sumaCubos aux)

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

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

PorJosé A. Alonso 24 enero 202021 agosto 2021

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

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

sorry

Soluciones con Isabelle/HOL

theory reto

imports Main
begin

(* 1ª solución *)

lemma "∀(f :: bool ⇒ bool). f (f (f b)) = f b"
  by smt

(* 2ª solución *)

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

(* 3ª solución *)

lemma
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  by (cases b; cases "f True"; cases "f False"; simp)

(* 4ª solución *)

lemma
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
proof (cases "f True"; cases "f False"; cases b)
  assume "f True" "f False" "b"
  then have "f b = True" by simp
  then show "f (f (f b)) = f b" using ‹f True› by simp 
next
  assume "f True" "f False" "¬ b"
  then have "f b = True" by simp
  then show "f (f (f b)) = f b" using ‹f True› ‹f False› ‹¬ b› by simp 
next
  assume "f True" "¬ f False" "b"
  then have "f b = True" by simp
  then show "f (f (f b)) = f b" using ‹f True› ‹¬ f False› ‹b› by simp 
next
  assume "f True" "¬ f False" "¬ b"
  then have "f b = False" by simp
  then show "f (f (f b)) = f b" using ‹f True› ‹¬ f False› ‹¬ b› by simp 
next 
  assume "¬ f True" "f False" "b"
  then have "f b = False" by simp
  then show "f (f (f b)) = f b" using ‹¬ f True› ‹f False› ‹b› by simp 
next
  assume "¬ f True" "f False" "¬ b"
  then have "f b = True" by simp
  then show "f (f (f b)) = f b" using ‹¬ f True› ‹f False› ‹¬ b› by simp 
next
  assume "¬ f True" "¬ f False" "b"
  then have "f b = False" by simp
  then show "f (f (f b)) = f b" using ‹¬ f True› ‹¬ f False› ‹b› by simp 
next
  assume "¬ f True" "¬ f False" "¬ b"
  then have "f b = False" by simp
  then show "f (f (f b)) = f b" using ‹¬ f True› ‹¬ f False› ‹¬b› by simp 
qed

(* 5ª solución *)

lemma
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
proof (cases "f True"; cases "f False"; cases b)
  assume "f True" "f False" "b"
  have "f (f (f b)) = f (f (f True))" using ‹b› by simp
  also have "… = f (f True)" using ‹f True› by simp
  also have "… = f True" using ‹f True› by simp
  also have "… = f b" using ‹b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "f True" "f False" "¬ b"
  have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp
  also have "… = f (f True)" using ‹f False› by simp
  also have "… = f True" using ‹f True› by simp
  also have "… = f False" using ‹f True› ‹f False› by simp
  also have "… = f b" using ‹¬ b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "f True" "¬ f False" "b"
  have "f (f (f b)) = f (f (f True))" using ‹b› by simp
  also have "… = f (f True)" using ‹f True› by simp
  also have "… = f True" using ‹f True› by simp
  also have "… = f b" using ‹b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "f True" "¬ f False" "¬ b"
  have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp
  also have "… = f (f False)" using ‹¬ f False› by simp
  also have "… = f False" using ‹¬ f False› by simp
  also have "… = f b" using ‹¬ b› by simp
  finally show "f (f (f b)) = f b" by this 
next 
  assume "¬ f True" "f False" "b"
  have "f (f (f b)) = f (f (f True))" using ‹b› by simp
  also have "… = f (f False)" using ‹¬ f True› by simp
  also have "… = f True" using ‹f False› by simp
  also have "… = f b" using ‹b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "¬ f True" "f False" "¬ b"
  have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp
  also have "… = f (f True)" using ‹f False› by simp
  also have "… = f False" using ‹¬ f True› by simp
  also have "… = f b" using ‹¬ b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "¬ f True" "¬ f False" "b"
  have "f (f (f b)) = f (f (f True))" using ‹b› by simp
  also have "… = f (f False)" using ‹¬ f True› by simp
  also have "… = f False" using ‹¬ f False› by simp
  also have "… = False" using ‹¬ f False› by simp
  also have "… = f True" using ‹¬ f True› by simp
  also have "… = f b" using ‹b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "¬ f True" "¬ f False" "¬ b"
  have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp
  also have "… = f (f False)" using ‹¬ f False› by simp
  also have "… = f False" using ‹¬ f False› by simp
  also have "… = f b" using ‹¬ b› by simp
  finally show "f (f (f b)) = f b" by this 
qed

(* 6ª solución *)

theorem
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b" 
proof (cases b)
  assume b: b
  show ?thesis
  proof (cases "f True")
    assume ft: "f True"
    show ?thesis
      using b ft by auto
  next
    assume ft: "¬ f True"
    show ?thesis
    proof (cases "f False")
      assume ff: "f False"
      show ?thesis
        using b ft ff by auto
    next
      assume ff: "¬ f False"
      show ?thesis
        using b ft ff by auto
    qed
  qed
next
  assume b: "¬ b"
  show ?thesis
  proof (cases "f True")
    assume ft: "f True"
    show ?thesis
    proof (cases "f False")
      assume ff: "f False"
      show ?thesis
        using b ft ff by auto
    next
      assume ff: "¬ f False"
      show ?thesis
        using b ft ff by auto
    qed
  next
    assume ft: "¬ f True"
    show ?thesis
    proof (cases "f False")
      assume ff: "f False"
      show ?thesis
        using b ft ff by auto
    next
      assume ff: "¬ f False"
      show ?thesis
        using b ft ff by auto
    qed
  qed
qed

(* 7ª solución *)

theorem
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  by (cases b "f True" "f False"
      rule: bool.exhaust [ case_product bool.exhaust
                         , case_product bool.exhaust])
    auto

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

theory reto

imports Main

begin

(* 1ª solución *)

lemma "∀(f :: bool ⇒ bool). f (f (f b)) = f b"

by smt

(* 2ª solución *)

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

by smt

(* 3ª solución *)

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

by (cases b; cases "f True"; cases "f False"; simp)

(* 4ª solución *)

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

proof (cases "f True"; cases "f False"; cases b)

assume "f True" "f False" "b"

then have "f b = True" by simp

then show "f (f (f b)) = f b" using ‹f True› by simp

assume "f True" "f False" "¬ b"

then have "f b = True" by simp

then show "f (f (f b)) = f b" using ‹f True› ‹f False› ‹¬ b› by simp

assume "f True" "¬ f False" "b"

then have "f b = True" by simp

then show "f (f (f b)) = f b" using ‹f True› ‹¬ f False› ‹b› by simp

assume "f True" "¬ f False" "¬ b"

then have "f b = False" by simp

then show "f (f (f b)) = f b" using ‹f True› ‹¬ f False› ‹¬ b› by simp

assume "¬ f True" "f False" "b"

then have "f b = False" by simp

then show "f (f (f b)) = f b" using ‹¬ f True› ‹f False› ‹b› by simp

assume "¬ f True" "f False" "¬ b"

then have "f b = True" by simp

then show "f (f (f b)) = f b" using ‹¬ f True› ‹f False› ‹¬ b› by simp

assume "¬ f True" "¬ f False" "b"

then have "f b = False" by simp

then show "f (f (f b)) = f b" using ‹¬ f True› ‹¬ f False› ‹b› by simp

assume "¬ f True" "¬ f False" "¬ b"

then have "f b = False" by simp

then show "f (f (f b)) = f b" using ‹¬ f True› ‹¬ f False› ‹¬b› by simp

qed

(* 5ª solución *)

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

proof (cases "f True"; cases "f False"; cases b)

assume "f True" "f False" "b"

have "f (f (f b)) = f (f (f True))" using ‹b› by simp

also have "… = f (f True)" using ‹f True› by simp

also have "… = f True" using ‹f True› by simp

also have "… = f b" using ‹b› by simp

finally show "f (f (f b)) = f b" by this

assume "f True" "f False" "¬ b"

have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp

also have "… = f (f True)" using ‹f False› by simp

also have "… = f True" using ‹f True› by simp

also have "… = f False" using ‹f True› ‹f False› by simp

also have "… = f b" using ‹¬ b› by simp

finally show "f (f (f b)) = f b" by this

assume "f True" "¬ f False" "b"

have "f (f (f b)) = f (f (f True))" using ‹b› by simp

also have "… = f (f True)" using ‹f True› by simp

also have "… = f True" using ‹f True› by simp

also have "… = f b" using ‹b› by simp

finally show "f (f (f b)) = f b" by this

assume "f True" "¬ f False" "¬ b"

have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp

also have "… = f (f False)" using ‹¬ f False› by simp

also have "… = f False" using ‹¬ f False› by simp

also have "… = f b" using ‹¬ b› by simp

finally show "f (f (f b)) = f b" by this

assume "¬ f True" "f False" "b"

have "f (f (f b)) = f (f (f True))" using ‹b› by simp

also have "… = f (f False)" using ‹¬ f True› by simp

also have "… = f True" using ‹f False› by simp

also have "… = f b" using ‹b› by simp

finally show "f (f (f b)) = f b" by this

assume "¬ f True" "f False" "¬ b"

have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp

also have "… = f (f True)" using ‹f False› by simp

also have "… = f False" using ‹¬ f True› by simp

also have "… = f b" using ‹¬ b› by simp

finally show "f (f (f b)) = f b" by this

assume "¬ f True" "¬ f False" "b"

have "f (f (f b)) = f (f (f True))" using ‹b› by simp

also have "… = f (f False)" using ‹¬ f True› by simp

also have "… = f False" using ‹¬ f False› by simp

also have "… = False" using ‹¬ f False› by simp

also have "… = f True" using ‹¬ f True› by simp

also have "… = f b" using ‹b› by simp

finally show "f (f (f b)) = f b" by this

assume "¬ f True" "¬ f False" "¬ b"

have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp

also have "… = f (f False)" using ‹¬ f False› by simp

also have "… = f False" using ‹¬ f False› by simp

also have "… = f b" using ‹¬ b› by simp

finally show "f (f (f b)) = f b" by this

qed

(* 6ª solución *)

theorem

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

proof (cases b)

assume b: b

show ?thesis

proof (cases "f True")

assume ft: "f True"

show ?thesis

using b ft by auto

assume ft: "¬ f True"

show ?thesis

proof (cases "f False")

assume ff: "f False"

show ?thesis

using b ft ff by auto

assume ff: "¬ f False"

show ?thesis

using b ft ff by auto

qed

assume b: "¬ b"

show ?thesis

proof (cases "f True")

assume ft: "f True"

show ?thesis

proof (cases "f False")

assume ff: "f False"

show ?thesis

using b ft ff by auto

assume ff: "¬ f False"

show ?thesis

using b ft ff by auto

qed

assume ft: "¬ f True"

show ?thesis

proof (cases "f False")

assume ff: "f False"

show ?thesis

using b ft ff by auto

assume ff: "¬ f False"

show ?thesis

using b ft ff by auto

qed

(* 7ª solución *)

theorem

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

by (cases b "f True" "f False"

rule: bool.exhaust [ case_product bool.exhaust

, case_product bool.exhaust])

auto

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

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

PorJosé A. Alonso 14 enero 202021 agosto 2021

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.

Soluciones

theory Celebracion_del_DML
imports Main

begin

(* 1ª solución (automática) *)
lemma "∃x. (C x ⟶ (∀y. C y))"
  by simp

(* 2ª solución (estructurada) *)
lemma "∃x. (C x ⟶ (∀y. C y))"
proof -
  have "¬ (∀y. C y) ∨ (∀y. C y)" ..
  then show "∃x. (C x ⟶ (∀y. C y))"
  proof 
    assume "¬ (∀y. C y)"
    then have "∃y. ¬(C y)" by simp
    then obtain a where "¬ C a" ..
    then have "C a ⟶ (∀y. C y)" by simp
    then show "∃x. (C x ⟶ (∀y. C y))" ..
  next
    assume "∀y. C y"
    then show "∃x. (C x ⟶ (∀y. C y))" by simp
  qed
qed

(* 3ª solución (detallada con lemas auxiliares) *)

lemma aux1:
  assumes "¬ (∀y. C y)"
  shows "∃y. ¬(C y)"
proof (rule ccontr)
  assume "∄y. ¬ C y"
  have "∀y. C y"
  proof 
    fix a
    show "C a"
    proof (rule ccontr)
      assume "¬ C a"
      then have "∃y. ¬ C y" by (rule exI)
      with ‹∄y. ¬ C y› show False by (rule notE)
    qed 
  qed
  with assms show False by (rule notE)
qed

lemma aux2:
  assumes "¬P"
  shows   "P ⟶ Q"
proof
  assume "P"
  with assms show "Q" by (rule notE)
qed

lemma aux3:
  assumes "∄x. P x"
  shows   "∀x. ¬ P x"
proof
  fix a
  show "¬ P a"
  proof 
    assume "P a"
    then have "∃x. P x" by (rule exI)
    with assms show False by (rule notE)
  qed 
qed

lemma aux4:
  assumes "Q"
  shows   "∃x. (P x ⟶ Q)"
proof (rule ccontr)
  assume "∄x. (P x ⟶ Q)"
  then have "∀x. ¬ (P x ⟶ Q)" by (rule aux3)
  then have "¬ (P a ⟶ Q)" by (rule allE)
  moreover
  have "P a ⟶ Q"
  proof
    assume "P a"
    show "Q" using assms by this
  qed
  ultimately show False by (rule notE)
qed

lemma "∃x. (C x ⟶ (∀y. C y))"
proof -
  have "¬ (∀y. C y) ∨ (∀y. C y)" ..
  then show "∃x. (C x ⟶ (∀y. C y))"
  proof 
    assume "¬ (∀y. C y)"
    then have "∃y. ¬(C y)" by (rule aux1)
    then obtain a where "¬ C a" by (rule exE)
    then have "C a ⟶ (∀y. C y)" by (rule aux2)
    then show "∃x. (C x ⟶ (∀y. C y))" by (rule exI)
  next
    assume "∀y. C y"
    then show "∃x. (C x ⟶ (∀y. C y))" by (rule aux4)
  qed
qed

end

100

theory Celebracion_del_DML

imports Main

begin

(* 1ª solución (automática) *)

lemma "∃x. (C x ⟶ (∀y. C y))"

by simp

(* 2ª solución (estructurada) *)

lemma "∃x. (C x ⟶ (∀y. C y))"

proof -

have "¬ (∀y. C y) ∨ (∀y. C y)" ..

then show "∃x. (C x ⟶ (∀y. C y))"

proof

assume "¬ (∀y. C y)"

then have "∃y. ¬(C y)" by simp

then obtain a where "¬ C a" ..

then have "C a ⟶ (∀y. C y)" by simp

then show "∃x. (C x ⟶ (∀y. C y))" ..

assume "∀y. C y"

then show "∃x. (C x ⟶ (∀y. C y))" by simp

qed

(* 3ª solución (detallada con lemas auxiliares) *)

lemma aux1:

assumes "¬ (∀y. C y)"

shows "∃y. ¬(C y)"

proof (rule ccontr)

assume "∄y. ¬ C y"

have "∀y. C y"

proof

fix a

show "C a"

proof (rule ccontr)

assume "¬ C a"

then have "∃y. ¬ C y" by (rule exI)

with ‹∄y. ¬ C y› show False by (rule notE)

qed

with assms show False by (rule notE)

qed

lemma aux2:

assumes "¬P"

shows "P ⟶ Q"

proof

assume "P"

with assms show "Q" by (rule notE)

qed

lemma aux3:

assumes "∄x. P x"

shows "∀x. ¬ P x"

proof

fix a

show "¬ P a"

proof

assume "P a"

then have "∃x. P x" by (rule exI)

with assms show False by (rule notE)

qed

lemma aux4:

assumes "Q"

shows "∃x. (P x ⟶ Q)"

proof (rule ccontr)

assume "∄x. (P x ⟶ Q)"

then have "∀x. ¬ (P x ⟶ Q)" by (rule aux3)

then have "¬ (P a ⟶ Q)" by (rule allE)

moreover

have "P a ⟶ Q"

proof

assume "P a"

show "Q" using assms by this

qed

ultimately show False by (rule notE)

qed

lemma "∃x. (C x ⟶ (∀y. C y))"

proof -

have "¬ (∀y. C y) ∨ (∀y. C y)" ..

then show "∃x. (C x ⟶ (∀y. C y))"

proof

assume "¬ (∀y. C y)"

then have "∃y. ¬(C y)" by (rule aux1)

then obtain a where "¬ C a" by (rule exE)

then have "C a ⟶ (∀y. C y)" by (rule aux2)

then show "∃x. (C x ⟶ (∀y. C y))" by (rule exI)

assume "∀y. C y"

then show "∃x. (C x ⟶ (∀y. C y))" by (rule aux4)

qed

end

Nota

Se pueden añadir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang=»isar»> y otra con </pre>

Pensamiento

Si así fue, así pudo ser; si así fuera, así podría ser; pero como no es, no es. Eso es lógica.

Lewis Carroll

Día mundial de la lógica y Calculemus

PorJosé A. Alonso 14 enero 202021 agosto 2021

El Consejo Ejecutivo de la UNESCO ha proclamado el 14 de enero 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

Lógica matemática y fundamentos (de 3º del Grado en Matemáticas) y
Razonamiento automático del Máster el Lógica, Computación e Inteligencia Artificial.

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>