Si (∃x)¬P(x), entonces ¬(∀x)P(x)

Demostrar con Lean4 que si \((∃x)¬P(x)\), entonces \(¬(∀x)P(x)\).

Para ello, completar la siguiente teoría de Lean4:

Demostración en lenguaje natural

Supongamos que \((∀x)P(x)\) y tenemos que demostrar contradicción. Por hipótesis, \((∃x)¬P(x)\). Sea \(y\) tal que \(¬P(y)\). Entonces, como \((∀x)P(x)\), se tiene \(P(y)\) que es una contradicción con \(¬P(y)\).

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Escribe un comentario