José A. Alonso

P → ¬¬P

Demostrar con Lean4 que \(P → ¬¬P\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable (P : Prop)
 
example
  (h : P)
  : ¬¬P :=
by sorry

Demostrar con Lean4 que \(¬¬P → P\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable (P : Prop)
 
example
  (h : ¬¬P)
  : P :=
by sorry

Demostrar con Lean4 que si \((∃x)¬P(x)\), entonces \(¬(∀x)P(x)\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable {α : Type _}
variable (P : α → Prop)
 
example
  (h : ∃ x, ¬ P x)
  : ¬ ∀ x, P x :=
by sorry

Demostrar con Lean4 que si \(¬(∀x)P(x)\), entonces \((∃x)¬P(x)\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable {α : Type _}
variable (P : α → Prop)
 
example
  (h : ¬ ∀ x, P x)
  : ∃ x, ¬ P x :=
by sorry

Demostrar con Lean4 que si \((∀x)¬P(x)\), entonces \(¬(∃x)P(x)\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable {α : Type _}
variable (P : α → Prop)
 
example
  (h : ∀ x, ¬ P x)
  : ¬ ∃ x, P x :=
by sorry