¬¬P → P
Demostrar con Lean4 que
\[ ¬¬P → P \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Tactic variable (P : Prop) example : ¬¬P → P := by sorry |
1. Demostración en lenguaje natural
Supongamos que
\[ ¬¬P \tag{1} \]
Por el principio del tercio excluso, se tiene
\[ P ∨ ¬P \]
lo que da lugar a dos casos.
En el primer caso, se supone \(P\) que es lo que hay que demostrar.
En el primer caso, se supone \(¬P\) que es una contradicción con (1).
2. 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 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 |
import Mathlib.Tactic variable (P : Prop) -- 1ª demostración -- =============== example : ¬¬P → P := by intro h1 -- h1 : ¬¬P -- ⊢ P have h2 : P ∨ ¬ P := em P rcases h2 with h3 | h4 . -- h3 : P exact h3 . -- h4 : ¬P exfalso -- ⊢ False exact h1 h4 -- 2ª demostración -- =============== example : ¬¬P → P := by intro h1 -- h1 : ¬¬P -- ⊢ P rcases em P with h2 | h3 . -- h2 : P exact h2 . -- h3 : ¬P exact absurd h3 h1 -- 3ª demostración -- =============== example : ¬¬P → P := by intro h1 -- h1 : ¬¬P -- ⊢ P cases em P . -- h2 : P assumption . -- h3 : ¬P contradiction -- 4ª demostración -- =============== example : ¬¬P → P := by intro h by_cases P . assumption . contradiction -- 4ª demostración -- =============== example : ¬¬P → P := by intro h1 -- h1 : ¬¬P -- ⊢ P by_contra h -- h : ¬P -- ⊢ False exact h1 h -- 5ª demostración -- =============== example : ¬¬P → P := by tauto |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 40.
3. Demostraciones con Isabelle/HOL
|
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 |
theory Eliminacion_de_la_doble_negacion imports Main begin (* 1ª demostración *) lemma "¬¬P ⟶ P" proof assume h1 : "¬¬P" have "¬P ∨ P" by (rule excluded_middle) then show "P" proof assume "¬P" then show "P" using h1 by (simp only: notE) next assume "P" then show "P" . qed qed (* 2ª demostración *) lemma "¬¬P ⟶ P" proof assume h1 : "¬¬P" show "P" proof (rule ccontr) assume "¬P" then show False using h1 by simp qed qed (* 3ª demostración *) lemma "¬¬P ⟶ P" by simp end |
