instance LO.FirstOrder.Sequent.instTildeListSemiformula {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} : LO.Tilde (List (LO.FirstOrder.Semiformula L ξ n))

Equations

• LO.FirstOrder.Sequent.instTildeListSemiformula = { tilde := fun (Γ : List (LO.FirstOrder.Semiformula L ξ n)) => List.map (fun (x : LO.FirstOrder.Semiformula L ξ n) => ∼x) Γ }

@[simp]

theorem LO.FirstOrder.Sequent.neg_def {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (Γ : List (LO.FirstOrder.Semiformula L ξ n)) : ∼Γ = List.map (fun (x : LO.FirstOrder.Semiformula L ξ n) => ∼x) Γ

@[simp]

theorem LO.FirstOrder.Sequent.neg_nil {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} : ∼[] = []

@[simp]

theorem LO.FirstOrder.Sequent.neg_cons {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (Γ : List (LO.FirstOrder.Semiformula L ξ n)) (φ : LO.FirstOrder.Semiformula L ξ n) : ∼(φ :: Γ) = ∼φ :: ∼Γ

def LO.FirstOrder.Semiformula.doubleNegation {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} : LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformulaᵢ L ξ n

Equations

• (LO.FirstOrder.Semiformula.rel r v).doubleNegation = ∼∼LO.FirstOrder.Semiformulaᵢ.rel r v
• (LO.FirstOrder.Semiformula.nrel r v).doubleNegation = ∼LO.FirstOrder.Semiformulaᵢ.rel r v
• LO.FirstOrder.Semiformula.verum.doubleNegation = ∼⊥
• LO.FirstOrder.Semiformula.falsum.doubleNegation = ⊥
• (φ.and ψ).doubleNegation = φ.doubleNegation ⋏ ψ.doubleNegation
• (φ.or ψ).doubleNegation = ∼(∼φ.doubleNegation ⋏ ∼ψ.doubleNegation)
• φ.all.doubleNegation = ∀' φ.doubleNegation
• φ.ex.doubleNegation = ∼(∀' ∼φ.doubleNegation)

def LO.FirstOrder.«term_ᴺ» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_ᴺ» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_ᴺ» 1024 1024 (Lean.ParserDescr.symbol "ᴺ")

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_rel {L : LO.FirstOrder.Language} {ξ : Type u_2} {n k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.rel r v).doubleNegation = ∼∼LO.FirstOrder.Semiformulaᵢ.rel r v

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_nrel {L : LO.FirstOrder.Language} {ξ : Type u_2} {n k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.nrel r v).doubleNegation = ∼LO.FirstOrder.Semiformulaᵢ.rel r v

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_verum {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} : ⊤.doubleNegation = ∼⊥

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_falsum {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} : ⊥.doubleNegation = ⊥

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_and {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (φ ψ : LO.FirstOrder.Semiformula L ξ n) : (φ ⋏ ψ).doubleNegation = φ.doubleNegation ⋏ ψ.doubleNegation

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_or {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (φ ψ : LO.FirstOrder.Semiformula L ξ n) : (φ ⋎ ψ).doubleNegation = ∼(∼φ.doubleNegation ⋏ ∼ψ.doubleNegation)

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_all {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∀' φ).doubleNegation = ∀' φ.doubleNegation

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_ex {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∃' φ).doubleNegation = ∼(∀' ∼φ.doubleNegation)

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_isNegative {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (φ : LO.FirstOrder.Semiformula L ξ n) : φ.doubleNegation.IsNegative

theorem LO.FirstOrder.Semiformula.rew_doubleNegation {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (φ : LO.FirstOrder.Semiformula L ξ₁ n₁) : (LO.FirstOrder.Rewriting.app ω) φ.doubleNegation = ((LO.FirstOrder.Rewriting.app ω) φ).doubleNegation

@[reducible, inline]

abbrev LO.FirstOrder.Theory.doubleNegation {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) : LO.FirstOrder.Theoryᵢ L

Equations

• T.doubleNegation = LO.FirstOrder.Semiformula.doubleNegation '' T

def LO.FirstOrder.«term_ᴺ_1» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_ᴺ_1» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_ᴺ_1» 1024 1024 (Lean.ParserDescr.symbol "ᴺ")

@[reducible, inline]

abbrev LO.FirstOrder.Sequent.doubleNegation {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (Γ : List (LO.FirstOrder.Semiformula L ξ n)) : List (LO.FirstOrder.Semiformulaᵢ L ξ n)

Equations

• LO.FirstOrder.Sequent.doubleNegation Γ = List.map (fun (x : LO.FirstOrder.Semiformula L ξ n) => x.doubleNegation) Γ

def LO.FirstOrder.«term_ᴺ_2» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_ᴺ_2» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_ᴺ_2» 1024 1024 (Lean.ParserDescr.symbol "ᴺ")

@[irreducible]

noncomputable def LO.FirstOrder.Derivation.negDoubleNegation {L : LO.FirstOrder.Language} [L.DecidableEq] (φ : LO.FirstOrder.SyntacticFormula L) : 𝐌𝐢𝐧¹ ⊢ ∼LO.FirstOrder.Semiformula.doubleNegation φ ⭤ (∼φ).doubleNegation

noncomputable def LO.FirstOrder.Derivation.goedelGentzen {L : LO.FirstOrder.Language} [L.DecidableEq] {Γ : LO.FirstOrder.Sequent L} : ⊢ᵀ Γ → LO.FirstOrder.Sequent.doubleNegation (∼Γ) ⊢[𝐌𝐢𝐧¹] ⊥