Demostrar con Lean4 e Isabelle/HOL que
Si \(s ⊆ t\), entonces \(s ∩ u ⊆ t ∩ u\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} variable (s t u : Set α) example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by sorry
y la siguiente teoría de Isabelle/HOL:
theory Propiedad_de_monotonia_de_la_interseccion imports Main begin lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" oops end
Se dice que la relación binaria \(R\) es
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
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:
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
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 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
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
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
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
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 \]
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
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.