P → ¬¬P
Demostrar con Lean4 que \(P → ¬¬P\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable (P : Prop) example (h : P) : ¬¬P := by sorry |
Demostración en lenguaje natural
Supongamos \(¬P\). Entonces, tenemos una contradicción con la hipótesis (\(P\)).
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 |
import Mathlib.Tactic variable (P : Prop) -- 1ª demostración -- =============== example (h : P) : ¬¬P := by intro h1 -- h1 : ¬P -- ⊢ False exact (h1 h) -- 2ª demostración -- =============== example (h : P) : ¬¬P := fun h1 ↦ h1 h -- 3ª demostración -- =============== example (h : P) : ¬¬P := not_not_intro h -- 4ª demostración -- =============== example (h : P) : ¬ ¬ P := by tauto -- Lemas usados -- ============ -- #check (not_not_intro : P → ¬¬P) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 33.
