La semana en Calculemus (2 de diciembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Si ¬(∃x)P(x), entonces (∀x)¬P(x)
- 2. Si (∀x)¬P(x), entonces ¬(∃x)P(x)
- 3. Si ¬(∀x)P(x), entonces (∃x)¬P(x)
- 4. Si (∃x)¬P(x), entonces ¬(∀x)P(x)
- 5. ¬¬P → P
A continuación se muestran las soluciones.
1. Si ¬(∃x)P(x), entonces (∀x)¬P(x)
Demostrar con Lean4 que si \(¬(∃x)P(x)\), entonces \((∀x)¬P(x)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by sorry |
Demostración en lenguaje natural
Sea \(y\) un elemento cualquiera. Tenemos que demostrar \(¬P(y)\). Para ello, supongamos que \(P(y)\). Entonces, \((∃x)P(x)\) que es una contradicción con la hipótesis,
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 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) -- 1ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by intros y h1 -- y : α -- h1 : P x -- ⊢ False apply h -- ⊢ ∃ x, P x existsi y -- ⊢ P y exact h1 -- 2ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by intros y h1 -- y : α -- h1 : P x -- ⊢ False apply h -- ⊢ ∃ x, P x use y -- ⊢ P y exact h1 -- 3ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by intros y h1 -- y : α -- h1 : P x -- ⊢ False apply h -- ⊢ ∃ x, P x exact ⟨y, h1⟩ -- 4ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by intros y h1 -- y : α -- h1 : P x -- ⊢ False exact h ⟨y, h1⟩ -- 5ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := fun y h1 ↦ h ⟨y, h1⟩ -- 6ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by push_neg at h exact h -- 7ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := not_exists.mp h -- 8ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by aesop -- Lemas usados -- ============ -- #check (not_exists : (¬∃ x, P x) ↔ ∀ (x : α), ¬P x) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 33.
2. Si (∀x)¬P(x), entonces ¬(∃x)P(x)
Demostrar con Lean4 que si \((∀x)¬P(x)\), entonces \(¬(∃x)P(x)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by sorry |
Demostración en lenguaje natural
Supongamos que \((∃x)P(x)\). Sea \(y\) tal que \(P(y)\). Puesto que \((∀x)¬P(x)\), se tiene que \(¬P(y)\) que es una contradicción con \(P(y)\).
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 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) -- 1ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by intro h1 -- h1 : ∃ x, P x -- ⊢ False rcases h1 with ⟨y, hy : P y⟩ have h2 : ¬P y := h y exact h2 hy -- 2ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by intro h1 -- h1 : ∃ x, P x -- ⊢ False rcases h1 with ⟨y, hy : P y⟩ exact (h y) hy -- 3ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by rintro ⟨y, hy : P y⟩ exact (h y) hy -- 4ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := fun ⟨y, hy⟩ ↦ (h y) hy -- 5ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := not_exists_of_forall_not h -- 6ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by aesop -- Lemas usados -- ============ -- variable (q : Prop) -- #check (not_exists_of_forall_not : (∀ x, P x → q) → (∃ x, P x) → q) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 33.
3. Si ¬(∀x)P(x), entonces (∃x)¬P(x)
Demostrar con Lean4 que si \(¬(∀x)P(x)\), entonces \((∃x)¬P(x)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := by sorry |
Demostración en lenguaje natural
Por reducción al absurdo, supongamos que \(¬(∃x)¬P(x)\). Para obtener contradicción, demostraremos la negación de la hipótesis; es que \((∀x)P(x)\). Para ello, sea \(y\) un elemento cualquiera y tenemos que demostrar \(P(y)\). De nuevo, lo haremos por reducción al absurdo: Para ello, supongamos que \(¬P(y)\). Entonces, se tiene que \((∃x)¬P(x)\) en contradicción con nuestro primer supuesto de \(¬(∃x)¬P(x)\).
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 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) -- 1ª demostración -- =============== example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := by by_contra h1 -- h1 : ¬∃ x, ¬P x -- ⊢ False apply h -- ⊢ ∀ (x : α), P x intro y -- y : α -- ⊢ P y show P y by_contra h2 -- h2 : ¬P y -- ⊢ False exact h1 ⟨y, h2⟩ -- 2ª demostración -- =============== example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := not_forall.mp h -- 3ª demostración -- =============== example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := by aesop -- Lemas usados -- ============ -- #check (not_forall : (¬∀ x, P x) ↔ ∃ x, ¬P x) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 33.
4. Si (∃x)¬P(x), entonces ¬(∀x)P(x)
Demostrar con Lean4 que si \((∃x)¬P(x)\), entonces \(¬(∀x)P(x)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := by sorry |
Demostración en lenguaje natural
Supongamos que \((∀x)P(x)\) y tenemos que demostrar contradicción. Por hipótesis, \((∃x)¬P(x)\). Sea \(y\) tal que \(¬P(y)\). Entonces, como \((∀x)P(x)\), se tiene \(P(y)\) que es una contradicción con \(¬P(y)\).
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 77 78 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) -- 1ª demostración -- =============== example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := by intro h1 -- h1 : ∀ (x : α), P x -- ⊢ False cases' h with y hy -- y : α -- hy : ¬P y apply hy -- ⊢ P y exact (h1 y) -- 2ª demostración -- =============== example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := by intro h1 -- h1 : ∀ (x : α), P x -- ⊢ False rcases h with ⟨y, hy : ¬P y⟩ apply hy -- ⊢ P y exact (h1 y) -- 3ª demostración -- =============== example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := by intro h1 -- h1 : ∀ (x : α), P x -- ⊢ False rcases h with ⟨y, hy : ¬P y⟩ exact hy (h1 y) -- 4ª demostración -- =============== example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := not_forall.mpr h -- 5ª demostración -- =============== example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := not_forall_of_exists_not h -- 6ª demostración -- =============== example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := by aesop -- Lemas usados -- ============ -- #check (not_forall : (¬∀ x, P x) ↔ ∃ x, ¬P x) -- #check (not_forall_of_exists_not : (∃ x, ¬P x) → ¬∀ x, P x) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 33.
5. ¬¬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.