Demostrar con Lean4 y con Isabelle/HOL que \[ (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (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 : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union_2
imports Main
begin

lemma "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)"
oops

end

Read more…

Demostrar con Lean4 y con Isabelle/HOL que \[ (s \setminus t) \setminus u ⊆ s \setminus (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 : (s \ t) \ u ⊆ s \ (t ∪ u) :=
by sorry

y la la siguiente teoría de Isabelle/HOL:

theory Diferencia_de_diferencia_de_conjuntos
imports Main
begin

lemma "(s - t) - u ⊆ s - (t ∪ u)"
oops

Read more…

Demostrar con Lean4 y con Isabelle/HOL que \[s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ 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 :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union
imports Main
begin

lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)"
oops

end

Read more…

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

Read more…

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…