Documentation

Foundation.LinearLogic.FirstOrder.ClassicalEmbedding

Girard's embedding of classical logic into linear logic #

$\mathbf{LL}$ to $\mathbf{LK}$ #

source
def LO.FirstOrder.LinearLogic.Semiformula.forget {L : Language} {ξ : Type u_2} {n : ℕ} :
Semiformula L ξ n → FirstOrder.Semiformula L ξ n

Forget the linear structure and return a classical first-order formula.

Equations
Instances For
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_rel {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :
    (rel r v).forget = FirstOrder.Semiformula.rel r v
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_nrel {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :
    (nrel r v).forget = FirstOrder.Semiformula.nrel r v
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_one {L : Language} {ξ : Type u_1} {n : ℕ} :
    forget 1 = ⊤
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_verum {L : Language} {ξ : Type u_1} {n : ℕ} :
    ⊤.forget = ⊤
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_falsum {L : Language} {ξ : Type u_1} {n : ℕ} :
    ⊥.forget = ⊥
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_zero {L : Language} {ξ : Type u_1} {n : ℕ} :
    forget 0 = ⊥
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_tensor {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :
    (φ ⨂ ψ).forget = φ.forget ⋏ ψ.forget
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_with {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :
    (φ ＆ ψ).forget = φ.forget ⋏ ψ.forget
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_par {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :
    (φ ⅋ ψ).forget = φ.forget ⋎ ψ.forget
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_plus {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :
    (φ ⨁ ψ).forget = φ.forget ⋎ ψ.forget
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_all {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :
    (∀⁰ φ).forget = ∀⁰ φ.forget
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_exs {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :
    (∃⁰ φ).forget = ∃⁰ φ.forget
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_bang {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :
    (！φ).forget = φ.forget
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_quest {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :
    (？φ).forget = φ.forget
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_neg {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :
    (∼φ).forget = ∼φ.forget
    source
    @[simp]
    theorem LO.FirstOrder.LinearLogic.Semiformula.forget_rew {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) :
    ((Rewriting.app ω) φ).forget = (Rewriting.app ω) φ.forget
    source
    @[reducible, inline]
    abbrev LO.FirstOrder.LinearLogic.Sequent.forget {L : Language} (Γ : Sequent L) :
    FirstOrder.Sequent L
    Equations
    Instances For
      source
      @[simp]
      theorem LO.FirstOrder.LinearLogic.Sequent.forget_shift {L : Language} (Γ : Sequent L) :
      forget (Rewriting.shifts Γ) = Rewriting.shifts Γ.forget
      source
      def LO.FirstOrder.LinearLogic.Derivation.forget {L : Language} {Γ : Sequent L} :
      Derivation Γ → ⊢ᵀ Γ.forget
      Equations
      Instances For
        source
        theorem LO.FirstOrder.LinearLogic.Proof.forget {L : Language} {φ : Sentence L} :
        𝐋𝐋 ⊢ φ → 𝐋𝐊 ⊢ Semiformula.forget φ

        $\mathbf{LK}$ to $\mathbf{LL}$ #

        source
        def LO.FirstOrder.Semiformula.girard {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ n) :
        LinearLogic.Semiformula L ξ n

        Girard embedding

        Equations
        Instances For
          source
          @[simp]
          theorem LO.FirstOrder.Semiformula.girard_rel {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :
          (rel r v).girard = ！LinearLogic.Semiformula.rel r v
          source
          @[simp]
          theorem LO.FirstOrder.Semiformula.girard_nrel {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :
          (nrel r v).girard = ？LinearLogic.Semiformula.nrel r v
          source
          @[simp]
          theorem LO.FirstOrder.Semiformula.girard_verum {L : Language} {ξ : Type u_1} {n : ℕ} :
          ⊤.girard = 1
          source
          @[simp]
          theorem LO.FirstOrder.Semiformula.girard_falsum {L : Language} {ξ : Type u_1} {n : ℕ} :
          ⊥.girard = ⊥
          source
          @[simp]
          theorem LO.FirstOrder.Semiformula.girard_neg {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :
          (∼φ).girard = ∼φ.girard
          source
          @[simp]
          theorem LO.FirstOrder.Semiformula.girard_rew {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) :
          ((Rewriting.app ω) φ).girard = (Rewriting.app ω) φ.girard
          source
          def LO.FirstOrder.Semiformula.Girard {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ n) :
          LinearLogic.Semiformula L ξ n
          Equations
          Instances For
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.Girard_rel {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :
            (rel r v).Girard = ？！LinearLogic.Semiformula.rel r v
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.Girard_nrel {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :
            (nrel r v).Girard = ？LinearLogic.Semiformula.nrel r v
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.Girard_verum {L : Language} {ξ : Type u_1} {n : ℕ} :
            ⊤.Girard = ？1
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.Girard_falsum {L : Language} {ξ : Type u_1} {n : ℕ} :
            ⊥.Girard = ⊥
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.Girard_rew {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) :
            ((Rewriting.app ω) φ).Girard = (Rewriting.app ω) φ.Girard
            source
            theorem LO.FirstOrder.Semiformula.girard_negative {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} (h : φ.Negative) :
            φ.girard.Negative
            source
            theorem LO.FirstOrder.Semiformula.girard_positive {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} (h : φ.Positive) :
            φ.girard.Positive
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.girard_negative_iff {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} :
            φ.girard.Negative ↔ φ.Negative
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.girard_positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} :
            φ.girard.Positive ↔ φ.Positive
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.Girard_negative {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :
            φ.Girard.Negative
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.forget_girard {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :
            φ.girard.forget = φ
            source
            @[simp]
            theorem LO.FirstOrder.Semiformula.forget_Girard {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :
            φ.Girard.forget = φ
            source
            @[reducible, inline]
            abbrev LO.FirstOrder.Sequent.Girard {L : Language} (Γ : Sequent L) :
            LinearLogic.Sequent L
            Equations
            Instances For
              source
              @[simp]
              theorem LO.FirstOrder.Sequent.girard_negative {L : Language} (Γ : Sequent L) :
              Γ.Girard.Negative
              source
              @[simp]
              theorem LO.FirstOrder.Sequent.shifts_Girard {L : Language} (Γ : Sequent L) :
              Rewriting.shifts Γ.Girard = Girard (Rewriting.shifts Γ)
              source
              def LO.FirstOrder.Derivation.toLL {L : Language} [L.DecidableEq] {Γ : Sequent L} :
              ⊢ᵀ Γ → LinearLogic.Derivation Γ.Girard
              Equations
              Instances For
                source
                theorem LO.FirstOrder.Proof.girard {L : Language} [L.DecidableEq] {φ : Sentence L} :
                𝐋𝐊 ⊢ φ → 𝐋𝐋 ⊢ Semiformula.Girard φ
                source
                theorem LO.FirstOrder.Proof.girard_faithful {L : Language} [L.DecidableEq] {φ : Sentence L} :
                𝐋𝐋 ⊢ Semiformula.Girard φ ↔ 𝐋𝐊 ⊢ φ
                source
                instance LO.FirstOrder.Proof.instFaithfullyEmbeddableSentenceSentenceTheorySymbolPureLKSymbol {L : Language} [L.DecidableEq] :
                Entailment.FaithfullyEmbeddable 𝐋𝐊 𝐋𝐋