Documentation

Foundation.IntFO.Translation

source
instance LO.FirstOrder.Sequent.instTildeListSemiformula {L : Language} {ξ : Type u_2} {n : ℕ} :
Tilde (List (Semiformula L ξ n))
Equations
source
@[simp]
theorem LO.FirstOrder.Sequent.neg_def {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) :
∼Γ = List.map (fun (x : Semiformula L ξ n) => ∼x) Γ
source
@[simp]
theorem LO.FirstOrder.Sequent.neg_nil {L : Language} {ξ : Type u_2} {n : ℕ} :
∼[] = []
source
@[simp]
theorem LO.FirstOrder.Sequent.neg_cons {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) (φ : Semiformula L ξ n) :
∼(φ :: Γ) = ∼φ :: ∼Γ
source
@[simp]
theorem LO.FirstOrder.Sequent.neg_neg_eq {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) :
∼∼Γ = Γ
source
def LO.FirstOrder.Semiformula.doubleNegation {L : Language} {ξ : Type u_2} {n : ℕ} :
Semiformula L ξ n → Semiformulaᵢ L ξ n
Equations
Instances For
    source
    def LO.FirstOrder.«term_ᴺ» :
    Lean.TrailingParserDescr
    Equations
    Instances For
      source
      @[simp]
      theorem LO.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
      source
      @[simp]
      theorem LO.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
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.doubleNegation_verum {L : Language} {ξ : Type u_2} {n : ℕ} :
      ⊤.doubleNegation = ∼⊥
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.doubleNegation_falsum {L : Language} {ξ : Type u_2} {n : ℕ} :
      ⊥.doubleNegation = ⊥
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.doubleNegation_and {L : Language} {ξ : Type u_2} {n : ℕ} (φ ψ : Semiformula L ξ n) :
      (φ ⋏ ψ).doubleNegation = φ.doubleNegation ⋏ ψ.doubleNegation
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.doubleNegation_or {L : Language} {ξ : Type u_2} {n : ℕ} (φ ψ : Semiformula L ξ n) :
      (φ ⋎ ψ).doubleNegation = ∼(∼φ.doubleNegation ⋏ ∼ψ.doubleNegation)
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.doubleNegation_all {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :
      (∀' φ).doubleNegation = ∀' φ.doubleNegation
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.doubleNegation_ex {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :
      (∃' φ).doubleNegation = ∼(∀' ∼φ.doubleNegation)
      source
      @[simp]
      theorem LO.FirstOrder.Semiformula.doubleNegation_isNegative {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ n) :
      φ.doubleNegation.IsNegative
      source
      theorem LO.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
      source
      theorem LO.FirstOrder.Semiformula.substitute_doubleNegation {L : Language} {ξ : Type u_2} {n₁ n₂ : ℕ} (φ : Semiformula L ξ n₁) (v : Fin n₁ → Semiterm L ξ n₂) :
      φ.doubleNegation ⇜ v = (φ ⇜ v).doubleNegation
      source
      @[reducible, inline]
      abbrev LO.FirstOrder.Theory.doubleNegation {L : Language} (T : Theory L) :
      Theoryᵢ L
      Equations
      Instances For
        source
        def LO.FirstOrder.«term_ᴺ_1» :
        Lean.TrailingParserDescr
        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev LO.FirstOrder.Sequent.doubleNegation {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) :
          List (Semiformulaᵢ L ξ n)
          Equations
          Instances For
            source
            def LO.FirstOrder.«term_ᴺ_2» :
            Lean.TrailingParserDescr
            Equations
            Instances For
              source
              @[irreducible]
              noncomputable def LO.FirstOrder.Derivation.negDoubleNegation {L : Language} [L.DecidableEq] (φ : SyntacticFormula L) :
              𝐌𝐢𝐧¹ ⊢ ∼Semiformula.doubleNegation φ ⭤ (∼φ).doubleNegation
              Equations
              Instances For
                source
                noncomputable def LO.FirstOrder.Derivation.goedelGentzen {L : Language} [L.DecidableEq] {Γ : Sequent L} :
                ⊢ᵀ Γ → Sequent.doubleNegation (∼Γ) ⊢[𝐌𝐢𝐧¹] ⊥
                Equations
                Instances For