P → ¬¬P

Demostrar con Lean4 que \(P → ¬¬P\).

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

Demostración en lenguaje natural

Supongamos \(¬P\). Entonces, tenemos una contradicción con la hipótesis (\(P\)).

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Escribe un comentario