La paradoja del barbero
Demostrar 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 Lean:
1 2 3 4 5 6 7 8 |
import tactic variable (Hombre : Type) variable (afeita : Hombre → Hombre → Prop) example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := sorry |
[expand title=»Soluciones con Lean»]
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 |
import tactic variable (Hombre : Type) variable (afeita : Hombre → Hombre → Prop) -- 1ª demostración example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := begin intro h, cases h with b hb, specialize hb b, by_cases (afeita b b), { apply absurd h, exact hb.mp h, }, { apply h, exact hb.mpr h, }, end -- 2ª demostración example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := begin intro h, cases h with b hb, specialize hb b, by_cases (afeita b b), { exact (hb.mp h) h, }, { exact h (hb.mpr h), }, end -- 3ª demostración example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := begin intro h, cases h with b hb, specialize hb b, by itauto, end -- 4ª demostración example : ¬ (∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) := begin rintro ⟨b, hb⟩, exact (iff_not_self (afeita b b)).mp (hb b), end -- 5ª demostración example : ¬ (∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) := λ ⟨b, hb⟩, (iff_not_self (afeita b b)).mp (hb b) |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones 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 |
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 |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]