Documentation

Foundation.FirstOrder.LJ.GoedelGentzen

source
def FFL.FirstOrder.Semiformula.doubleNegation {L : Language} {ξ : Type u_2} {n : ℕ} :
Semiformula L ξ n → Semiformulaᵢ L ξ n
Equations
Instances For
    source
    def FFL.FirstOrder.«term_ᴺ» :
    Lean.TrailingParserDescr
    Equations
    Instances For
      source
      @[simp]
      theorem 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
      source
      @[simp]
      theorem 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
      source
      @[simp]
      theorem FFL.FirstOrder.Semiformula.doubleNegation_verum {L : Language} {ξ : Type u_2} {n : ℕ} :
      ⊤.doubleNegation = ∼⊥
      source
      @[simp]
      theorem FFL.FirstOrder.Semiformula.doubleNegation_falsum {L : Language} {ξ : Type u_2} {n : ℕ} :
      ⊥.doubleNegation = ⊥
      source
      @[simp]
      theorem FFL.FirstOrder.Semiformula.doubleNegation_and {L : Language} {ξ : Type u_2} {n : ℕ} (φ ψ : Semiformula L ξ n) :
      (φ ⋏ ψ).doubleNegation = φ.doubleNegation ⋏ ψ.doubleNegation
      source
      @[simp]
      theorem FFL.FirstOrder.Semiformula.doubleNegation_or {L : Language} {ξ : Type u_2} {n : ℕ} (φ ψ : Semiformula L ξ n) :
      (φ ⋎ ψ).doubleNegation = ∼(∼φ.doubleNegation ⋏ ∼ψ.doubleNegation)
      source
      @[simp]
      theorem FFL.FirstOrder.Semiformula.doubleNegation_all {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :
      (∀¹ φ).doubleNegation = ∀¹ φ.doubleNegation
      source
      @[simp]
      theorem FFL.FirstOrder.Semiformula.doubleNegation_ex {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :
      (∃¹ φ).doubleNegation = ∼(∀¹ ∼φ.doubleNegation)
      source
      theorem FFL.FirstOrder.Semiformula.doubleNegation_imply {L : Language} {ξ : Type u_2} {n : ℕ} (φ ψ : Semiformula L ξ n) :
      (φ 🡒 ψ).doubleNegation = ∼(∼(∼φ).doubleNegation ⋏ ∼ψ.doubleNegation)
      source
      @[simp]
      theorem FFL.FirstOrder.Semiformula.doubleNegation_isNegative {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ n) :
      φ.doubleNegation.IsNegative
      source
      @[simp]
      theorem FFL.FirstOrder.Semiformula.doubleNegation_conj₂ {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) :
      (⋀Γ).doubleNegation = ⋀List.map doubleNegation Γ
      source
      theorem FFL.FirstOrder.Semiformula.doubleNegation_fconj {L : Language} {ξ : Type u_2} {n : ℕ} (s : Finset (Semiformula L ξ n)) :
      s.conj.doubleNegation = ⋀List.map doubleNegation s.toList
      source
      theorem 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
      source
      theorem 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
      source
      theorem FFL.FirstOrder.Semiformula.emb_doubleNegation {L : Language} {n₁ : ℕ} {ξ : Type u_2} (φ : Semisentence L n₁) :
      Rewriting.emb (doubleNegation φ) = (Rewriting.emb φ).doubleNegation
      source
      def FFL.FirstOrder.LK.Sequent.doubleNegation {L : Language} (Γ : Sequent L) :
      LJ.Sequent L
      Equations
      Instances For
        source
        def FFL.FirstOrder.«term_ᴺ_1» :
        Lean.TrailingParserDescr
        Equations
        Instances For
          source
          @[simp]
          theorem FFL.FirstOrder.LK.Sequent.doubleNegation_zero {L : Language} :
          doubleNegation 0 = 0
          source
          @[simp]
          theorem FFL.FirstOrder.LK.Sequent.doubleNegation_atom {L : Language} (φ : Proposition L) :
          doubleNegation ⦃φ⦄ = ⦃Semiformula.doubleNegation φ⦄
          source
          @[simp]
          theorem FFL.FirstOrder.LK.Sequent.doubleNegation_add {L : Language} (Γ Δ : Sequent L) :
          (Γ + Δ).doubleNegation = Γ.doubleNegation + Δ.doubleNegation
          source
          theorem FFL.FirstOrder.LK.Sequent.shift_doubleNegation {L : Language} (Γ : Sequent L) :
          Rewriting.shifts Γ.doubleNegation = doubleNegation (Rewriting.shifts Γ)
          source
          def FFL.FirstOrder.Theory.doubleNegation {L : Language} (T : Theory L) :
          Theoryᵢ L
          Equations
          Instances For
            source
            @[irreducible]
            def FFL.FirstOrder.LJ.Derivation.negDoubleNegation {L : Language} [L.DecidableEq] (φ : Proposition L) :
            InterDerivation L (∼Semiformula.doubleNegation φ) (Semiformula.doubleNegation (∼φ))
            Equations
            Instances For
              source
              def FFL.FirstOrder.LJ.Derivation.negDoubleNegation' {L : Language} [L.DecidableEq] (φ : Proposition L) :
              InterDerivation L (∼Semiformula.doubleNegation (∼φ)) (Semiformula.doubleNegation φ)
              Equations
              Instances For
                source
                def 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
                Instances For
                  source
                  def FFL.FirstOrder.LK.Derivation.gödelGentzen {L : Language} [L.DecidableEq] {Γ : Sequent L} :
                  ⊢ᴸᴷ¹ Γ → (∼Γ).doubleNegation ⊢ᴸᴶ¹ some ⊥
                  Equations
                  Instances For
                    source
                    theorem FFL.FirstOrder.Provable.gödel_gentzen {L : Language} [L.DecidableEq] {φ : Proposition L} :
                    𝐋𝐊¹ ⊢ φ → 𝐋𝐉¹ ⊢ Semiformula.doubleNegation φ