El problema del barbero

PorJosé A. Alonso 31 marzo 202021 agosto 2021

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

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

Soluciones con Isabelle/HOL

theory El_problema_del_barbero
imports Main
begin

― ‹La demostración automática es›
lemma
  assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
  using assms
  by auto

― ‹La demostración estructurada es›
lemma
  assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
proof -
  have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) ..
  have "A(c,c)"
  proof (rule ccontr)
    assume "¬A(c,c)"
    with assms(2) have "C(c) ∧ ¬A(c,c)" ..
    with 1 have "A(c,c)" ..
    with ‹¬A(c,c)› show False ..
  qed
  have "¬A(c,c)"
  proof -
    have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› ..
    then show "¬A(c,c)" ..
  qed
  then show "¬(∃x. A(c,x))" using ‹A(c,c)› ..
qed

― ‹La demostración detallada es›
lemma
  assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
proof -
  have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE)
  have "A(c,c)"
  proof (rule ccontr)
    assume "¬A(c,c)"
    with assms(2) have "C(c) ∧ ¬A(c,c)" by (rule conjI)
    with 1 have "A(c,c)" by (rule iffD2)
    with ‹¬A(c,c)› show False by (rule notE)
  qed
  have "¬A(c,c)"
  proof -
    have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› by (rule iffD1)
    then show "¬A(c,c)" by (rule conjunct2)
  qed
  then show "¬(∃x. A(c,x))" using ‹A(c,c)› by (rule notE)
qed

end

theory El_problema_del_barbero

imports Main

begin

― ‹La demostración automática es›

lemma

assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"

"C(c)"

shows "¬(∃x. A(c,x))"

using assms

by auto

― ‹La demostración estructurada es›

lemma

assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"

"C(c)"

shows "¬(∃x. A(c,x))"

proof -

have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) ..

have "A(c,c)"

proof (rule ccontr)

assume "¬A(c,c)"

with assms(2) have "C(c) ∧ ¬A(c,c)" ..

with 1 have "A(c,c)" ..

with ‹¬A(c,c)› show False ..

qed

have "¬A(c,c)"

proof -

have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› ..

then show "¬A(c,c)" ..

qed

then show "¬(∃x. A(c,x))" using ‹A(c,c)› ..

qed

― ‹La demostración detallada es›

lemma

assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"

"C(c)"

shows "¬(∃x. A(c,x))"

proof -

have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE)

have "A(c,c)"

proof (rule ccontr)

assume "¬A(c,c)"

with assms(2) have "C(c) ∧ ¬A(c,c)" by (rule conjI)

with 1 have "A(c,c)" by (rule iffD2)

with ‹¬A(c,c)› show False by (rule notE)

qed

have "¬A(c,c)"

proof -

have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› by (rule iffD1)

then show "¬A(c,c)" by (rule conjunct2)

qed

then show "¬(∃x. A(c,x))" using ‹A(c,c)› by (rule notE)

qed

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

José A. Alonso

4 Comentarios

inmrodmon dice:

a las

Isabelle/Isar

lemma assumes "∀x. A(c,x) ⟷ (C(x) ∧ ¬A(x,x))" "C(c)" shows "¬(∃x. A(c,x))" using assms by auto

1
2
3
4
5

lemma
  assumes "∀x. A(c,x) ⟷ (C(x) ∧ ¬A(x,x))"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
  using assms by auto

Loading...

Responder

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))"
proof - 
  have "¬A(c,c) ∨ A(c,c)" by (rule excluded_middle)
  then show "¬(∃x. A(c,x))"
  proof (rule disjE)
    assume "¬A(c,c)"
    have "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE)
    have "C(c) ∧ ¬A(c,c)" using assms(2) ‹¬A(c,c)› by (rule conjI)
    with ‹A(c,c) ⟷ C(c) ∧ ¬A(c,c)› have "A(c,c)" by (rule iffD2)
    with ‹¬A(c,c)› have False by (rule notE)
    then show "¬(∃x. A(c,x))" by (rule FalseE)
  next 
    assume "A(c,c)"
    have "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE)
    then have "C(c) ∧ ¬A(c,c)" using ‹A(c,c)› by (rule iffD1)
    then have "¬A(c,c)" by (rule conjunct2)
    then have False using ‹A(c,c)› by (rule notE)
    then show "¬(∃x. A(c,x))" by (rule FalseE)
  qed
qed

end

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))"

proof -

have "¬A(c,c) ∨ A(c,c)" by (rule excluded_middle)

then show "¬(∃x. A(c,x))"

proof (rule disjE)

assume "¬A(c,c)"

have "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE)

have "C(c) ∧ ¬A(c,c)" using assms(2) ‹¬A(c,c)› by (rule conjI)

with ‹A(c,c) ⟷ C(c) ∧ ¬A(c,c)› have "A(c,c)" by (rule iffD2)

with ‹¬A(c,c)› have False by (rule notE)

then show "¬(∃x. A(c,x))" by (rule FalseE)

assume "A(c,c)"

have "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE)

then have "C(c) ∧ ¬A(c,c)" using ‹A(c,c)› by (rule iffD1)

then have "¬A(c,c)" by (rule conjunct2)

then have False using ‹A(c,c)› by (rule notE)

then show "¬(∃x. A(c,x))" by (rule FalseE)

qed

end

Responder

theory El_problema_del_barbero
imports Main
begin

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
  by auto

lemma aux:
  assumes "p"
  shows "¬(q ∧ ¬p)"
proof (rule notI)
  assume "q∧ ¬p"
  then have "¬p" 
    by (rule conjunct2)
  then show False 
    using assms by (rule notE)
qed

lemma
  assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
proof (rule notI)
  assume  "∃x. A(c,x)"
  have "¬A(c,c) ∨ A(c,c)" 
    by (rule excluded_middle)
  then show False
  proof (rule disjE)
    assume 1: "¬A(c,c)"
    with assms(2) have 2: "C(c) ∧ ¬A(c,c)" 
      by (rule conjI)
    have "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" 
      using assms(1) by (rule allE)
    then have " C(c) ∧ ¬A(c,c)⟶A(c,c)" 
      by (rule iffE)
    then have "A(c,c)" 
      using 2 by (rule mp)
    with 1 show False 
      by (rule notE)
  next
    assume 3:"A(c,c)"
    then have 4: "¬(C(c) ∧ ¬A(c,c))" 
      by (rule aux)
    have "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" 
      using assms(1) by (rule allE)
    then have "A(c,c) ⟶ C(c) ∧ ¬A(c,c)"  
      by (rule iffE)
    then have "¬ A(c,c)" 
      using 4 by (rule mt)
    then show False 
      using 3 by (rule notE)
  qed
qed

end

theory El_problema_del_barbero

imports Main

begin

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"

by auto

lemma aux:

assumes "p"

shows "¬(q ∧ ¬p)"

proof (rule notI)

assume "q∧ ¬p"

then have "¬p"

by (rule conjunct2)

then show False

using assms by (rule notE)

qed

lemma

assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"

"C(c)"

shows "¬(∃x. A(c,x))"

proof (rule notI)

assume "∃x. A(c,x)"

have "¬A(c,c) ∨ A(c,c)"

by (rule excluded_middle)

then show False

proof (rule disjE)

assume 1: "¬A(c,c)"

with assms(2) have 2: "C(c) ∧ ¬A(c,c)"

by (rule conjI)

have "A(c,c) ⟷ C(c) ∧ ¬A(c,c)"

using assms(1) by (rule allE)

then have " C(c) ∧ ¬A(c,c)⟶A(c,c)"

by (rule iffE)

then have "A(c,c)"

using 2 by (rule mp)

with 1 show False

by (rule notE)

assume 3:"A(c,c)"

then have 4: "¬(C(c) ∧ ¬A(c,c))"

by (rule aux)

have "A(c,c) ⟷ C(c) ∧ ¬A(c,c)"

using assms(1) by (rule allE)

then have "A(c,c) ⟶ C(c) ∧ ¬A(c,c)"

by (rule iffE)

then have "¬ A(c,c)"

using 4 by (rule mt)

then show False

using 3 by (rule notE)

qed

end

Responder

Demostración intuicionista en Lean

constant α : Type
variables (A : α -> α -> Prop) (C : α -> Prop)
constant c : α

theorem el_problema_del_barbero
   (afeitar : ∀ x, (A c x) ↔ ((C x) ∧ (¬A x x)))
   (carlos : C c)
   : (¬(∃ x, (A c x))) :=
   have hpc : (A c c) ↔ (¬A c c),
      from iff.trans (afeitar c) (and_iff_right carlos),
   false.elim (iff.elim_left (iff_not_self (A c c)) hpc)

constant α : Type

variables (A : α -> α -> Prop) (C : α -> Prop)

constant c : α

theorem el_problema_del_barbero

(afeitar : ∀ x, (A c x) ↔ ((C x) ∧ (¬A x x)))

(carlos : C c)

: (¬(∃ x, (A c x))) :=

have hpc : (A c c) ↔ (¬A c c),

from iff.trans (afeitar c) (and_iff_right carlos),

false.elim (iff.elim_left (iff_not_self (A c c)) hpc)

Responder

Soluciones con Isabelle/HOL

Otras soluciones

Share this:

4 Comentarios

Escribe un comentarioCancel reply