Demostrar con Lean4 la paradoja del barbero; es decir, que no existe un hombre que afeite a todos los que no se afeitan a sí mismo y sólo a los que no se afeitan a sí mismo.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable (Hombre : Type) variable (afeita : Hombre → Hombre → Prop) example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := by sorry
Demostrar con Lean4 que si \((∃x)¬P(x)\), entonces \(¬(∀x)P(x)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := by sorry
Demostrar con Lean4 que si \(¬(∀x)P(x)\), entonces \((∃x)¬P(x)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := by sorry
Demostrar con Lean4 que si \((∀x)¬P(x)\), entonces \(¬(∃x)P(x)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by sorry
Demostrar con Lean4 que si \(¬(∃x)P(x)\), entonces \((∀x)¬P(x)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by sorry
Demostrar con Lean4 que si \((∀ε > 0)[x ≤ ε]\), entonces \(x ≤ 0\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (x : ℝ) example (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by sorry
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
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.