Supporting results for pointwise provable equality.

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

The double Negation construction in FFL.FirstOrder.Semiformula.

Equations

• (PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v).doubleNegation = ∼∼PointwiseComposition.FFL.FirstOrder.Semiformulaᵢ.rel r v
• (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v).doubleNegation = ∼PointwiseComposition.FFL.FirstOrder.Semiformulaᵢ.rel r v
• PointwiseComposition.FFL.FirstOrder.Semiformula.verum.doubleNegation = ⊤
• PointwiseComposition.FFL.FirstOrder.Semiformula.falsum.doubleNegation = ⊥
• (φ.and ψ).doubleNegation = φ.doubleNegation ⋏ ψ.doubleNegation
• (φ.or ψ).doubleNegation = ∼(∼φ.doubleNegation ⋏ ∼ψ.doubleNegation)
• φ.all.doubleNegation = ∀¹ φ.doubleNegation
• φ.exs.doubleNegation = ∼(∀¹ ∼φ.doubleNegation)

def PointwiseComposition.FFL.FirstOrder.«term_ᴺ» : Lean.TrailingParserDescr

The «term ᴺ» construction in FFL.FirstOrder.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.doubleNegation_imply {L : Language} {ξ : Type u_2} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⇒ₗ ψ).doubleNegation = ∼(∼(∼φ).doubleNegation ⋏ ∼ψ.doubleNegation)

@[simp]

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.doubleNegation_conj₂ {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) : (⋀Γ).doubleNegation = ⋀List.map doubleNegation Γ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.doubleNegation_fconj {L : Language} {ξ : Type u_2} {n : ℕ} (s : Finset (Semiformula L ξ n)) : (Finset.conj s).doubleNegation = ⋀List.map doubleNegation s.toList

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

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.subst_doubleNegation {L : Language} {ξ : Type u_2} {n₁ n₂ : ℕ} (φ : Semiformula L ξ n₁) (v : Fin n₁ → Semiterm L ξ n₂) : φ.doubleNegation ↜ v = (φ ↜ v).doubleNegation

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.emb_doubleNegation {L : Language} {n₁ : ℕ} {ξ : Type u_2} (φ : Semisentence L n₁) : Rewriting.emb (doubleNegation φ) = (Rewriting.emb φ).doubleNegation

def PointwiseComposition.FFL.FirstOrder.LK.Sequent.doubleNegation {L : Language} (Γ : Sequent L) : LJ.Sequent L

The double Negation construction in FFL.FirstOrder.LK.Sequent.

Equations

• Γ.doubleNegation = Multiset.map PointwiseComposition.FFL.FirstOrder.Semiformula.doubleNegation Γ

def PointwiseComposition.FFL.FirstOrder.«term_ᴺ_1» : Lean.TrailingParserDescr

The «term ᴺ 1» construction in FFL.FirstOrder.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Sequent.doubleNegation_zero {L : Language} : doubleNegation 0 = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Sequent.doubleNegation_atom {L : Language} (φ : Proposition L) : doubleNegation ⦃φ⦄ = ⦃Semiformula.doubleNegation φ⦄

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Sequent.doubleNegation_add {L : Language} (Γ Δ : Sequent L) : (Γ + Δ).doubleNegation = Γ.doubleNegation + Δ.doubleNegation

theorem PointwiseComposition.FFL.FirstOrder.LK.Sequent.shift_doubleNegation {L : Language} (Γ : Sequent L) : Rewriting.shifts Γ.doubleNegation = doubleNegation (Rewriting.shifts Γ)

def PointwiseComposition.FFL.FirstOrder.Theory.doubleNegation {L : Language} (T : Theory L) : Theoryᵢ L

The double Negation construction in FFL.FirstOrder.Theory.

Equations

• T.doubleNegation = PointwiseComposition.FFL.FirstOrder.Semiformula.doubleNegation '' T

@[irreducible]

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.negDoubleNegation {L : Language} [L.DecidableEq] (φ : Proposition L) : InterDerivation L (∼Semiformula.doubleNegation φ) (Semiformula.doubleNegation (∼φ))

The neg Double Negation construction in FFL.FirstOrder.LJ.Derivation.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.negDoubleNegation' {L : Language} [L.DecidableEq] (φ : Proposition L) : InterDerivation L (∼Semiformula.doubleNegation (∼φ)) (Semiformula.doubleNegation φ)

The neg Double Negation' construction in FFL.FirstOrder.LJ.Derivation.

Equations

• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.negDoubleNegation' φ = ⋯.mp (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.negDoubleNegation (∼φ))

def PointwiseComposition.FFL.FirstOrder.LK.Derivation.deductNeg {L : Language} {Γ : Sequent L} {φ : Proposition L} (d : (∼(Γ + ⦃φ⦄)).doubleNegation ⊢ᴸᴶ¹ some ⊥) : (∼Γ).doubleNegation ⊢ᴸᴶ¹ some (∼Semiformula.doubleNegation (∼φ))

Discharges a translated negated formula from an LJ contradiction derivation.

Equations

• PointwiseComposition.FFL.FirstOrder.LK.Derivation.deductNeg d = (d.cast ⋯ ⋯).positiveNeg

def PointwiseComposition.FFL.FirstOrder.LK.Derivation.gödelGentzen {L : Language} [L.DecidableEq] {Γ : Sequent L} : ⊢ᴸᴷ¹ Γ → (∼Γ).doubleNegation ⊢ᴸᴶ¹ some ⊥

The gödel Gentzen construction in FFL.FirstOrder.LK.Derivation.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.verum.gödelGentzen = ⋯.mpr (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta ⊥)
• d.or.gödelGentzen = (d.gödelGentzen.cast ⋯ ⋯).negativeAnd.cast ⋯ ⋯
• d.all.gödelGentzen = ((((PointwiseComposition.FFL.FirstOrder.LK.Derivation.deductNeg d.gödelGentzen).cast ⋯ ⋯).cast ⋯ ⋯).positiveForall.negativeNeg.cast ⋯ ⋯).weakeningRight
• d.exs.gödelGentzen = (d.gödelGentzen.cast ⋯ ⋯).negativeForall.cast ⋯ ⋯
• d.contraction.gödelGentzen = (d.gödelGentzen.cast ⋯ ⋯).contraction.cast ⋯ ⋯
• d.weakening.gödelGentzen = d.gödelGentzen.weakening.cast ⋯ ⋯

theorem PointwiseComposition.FFL.FirstOrder.Provable.gödel_gentzen {L : Language} [L.DecidableEq] {φ : Proposition L} : 𝐋𝐊¹ ⊢ φ → 𝐋𝐉¹ ⊢ Semiformula.doubleNegation φ