¬¬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
Por reducción al absurdo. 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 44 |
import Mathlib.Tactic variable (P : Prop) -- 1ª demostración -- =============== example (h : ¬¬P) : P := by by_contra h1 -- h1 : ¬P -- ⊢ False exact (h h1) -- 2ª demostración -- =============== example (h : ¬¬P) : P := by_contra (fun h1 ↦ h h1) -- 3ª demostración -- =============== example (h : ¬¬P) : P := -- not_not.mp h of_not_not h -- 4ª demostración -- =============== example (h : ¬¬P) : P := by tauto -- Lemas usados -- ============ -- #check (of_not_not : ¬¬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.
