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. 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

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

Escribe un comentario