La paradoja del barbero
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:
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable (Hombre : Type) variable (afeita : Hombre → Hombre → Prop) example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que
\[ ¬((∃ x)(∀ y)[\text{afeita}(x,y) ↔ ¬\text{afeita}(y,y)]) \]
Para ello, supongamos que
\[ (∃ x)(∀ y)[\text{afeita}(x,y) ↔ ¬\text{afeita}(y,y)] \tag{1} \]
y tenemos que llegar a una contradicción.
Sea \(b\) un elemento que verifica (1); es decir,
\[ (∀ y)[\text{afeita}(b,y) ↔ ¬\text{afeita}(y,y)] \]
Entonces,
\[ \text{afeita}(b,b) ↔ ¬\text{afeita}(b,b) \]
que es una contradicción.
2. Demostraciones con Lean4
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 |
import Mathlib.Tactic variable (Hombre : Type) variable (afeita : Hombre → Hombre → Prop) -- 1ª demostración -- =============== example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := by intro h -- h : ∃ x, ∀ (y : Hombre), afeita x y ↔ ¬afeita y y -- ⊢ False cases' h with b hb -- b : Hombre -- hb : ∀ (y : Hombre), afeita b y ↔ ¬afeita y y specialize hb b -- hb : afeita b b ↔ ¬afeita b b by_cases (afeita b b) . -- h : afeita b b apply absurd h -- ⊢ ¬afeita b b exact hb.mp h . -- h : ¬afeita b b apply h -- ⊢ afeita b b exact hb.mpr h -- 2ª demostración -- =============== example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := by intro h -- h : ∃ x, ∀ (y : Hombre), afeita x y ↔ ¬afeita y y -- ⊢ False cases' h with b hb -- b : Hombre -- hb : ∀ (y : Hombre), afeita b y ↔ ¬afeita y y specialize hb b -- hb : afeita b b ↔ ¬afeita b b by_cases (afeita b b) . -- h : afeita b b exact (hb.mp h) h . -- h : ¬afeita b b exact h (hb.mpr h) -- 3ª demostración -- =============== example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := by intro h -- h : ∃ x, ∀ (y : Hombre), afeita x y ↔ ¬afeita y y -- ⊢ False cases' h with b hb -- b : Hombre -- hb : ∀ (y : Hombre), afeita b y ↔ ¬afeita y y exact iff_not_self (hb b) -- 4ª demostración -- =============== example : ¬ (∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) := by rintro ⟨b, hb⟩ -- b : Hombre -- hb : ∀ (y : Hombre), afeita b y ↔ ¬afeita y y -- ⊢ False exact iff_not_self (hb b) -- 5ª demostración -- =============== example : ¬ (∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) := fun ⟨b, hb⟩ ↦ iff_not_self (hb b) -- Lemas usados -- ============ -- variable (p q : Prop) -- #check (absurd : p → (¬p → q)) -- #check (iff_not_self : ¬(p ↔ ¬p)) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 |
theory La_paradoja_del_barbero imports Main begin (* 1ª demostración *) lemma "¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)" proof (rule notI) assume "∃ x. ∀ y. afeita x y ⟷ ¬ afeita y y" then obtain b where "∀ y. afeita b y ⟷ ¬ afeita y y" by (rule exE) then have h : "afeita b b ⟷ ¬ afeita b b" by (rule allE) show False proof (cases "afeita b b") assume "afeita b b" then have "¬ afeita b b" using h by (rule rev_iffD1) then show False using ‹afeita b b› by (rule notE) next assume "¬ afeita b b" then have "afeita b b" using h by (rule rev_iffD2) with ‹¬ afeita b b› show False by (rule notE) qed qed (* 2ª demostración *) lemma "¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)" proof assume "∃ x. ∀ y. afeita x y ⟷ ¬ afeita y y" then obtain b where "∀ y. afeita b y ⟷ ¬ afeita y y" by (rule exE) then have h : "afeita b b ⟷ ¬ afeita b b" by (rule allE) then show False by simp qed (* 3ª demostración *) lemma "¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)" by auto end |