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

Por reducción al absurdo, supongamos que \(¬(∃x)¬P(x)\). Para obtener contradicción, demostraremos la negación de la hipótesis; es que \((∀x)P(x)\). Para ello, sea \(y\) un elemento cualquiera y tenemos que demostrar \(P(y)\). De nuevo, lo haremos por reducción al absurdo: Para ello, supongamos que \(¬P(y)\). Entonces, se tiene que \((∃x)¬P(x)\) en contradicción con nuestro primer supuesto de \(¬(∃x)¬P(x)\).

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Escribe un comentario