Eliminación de la doble negación
Demostrar con Lean4 que \[ ¬¬P → P \]
Para ello, completar la siguiente teoría de Lean4:
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
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
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