Documentation

Foundation.ProvabilityLogic.Arithmetic

Provability logic of arithmetic theory #

source
def LO.Modal.Logic.IsProvabilityLogic (L : Logic ℕ) (T U : FirstOrder.ArithmeticTheory) [FirstOrder.Theory.Δ₁ T] :
Prop

L is provability logic of T relative to metatheory U

Equations
Instances For
    source
    def LO.Modal.Logic.inst_Łukasiewiicz_of_isProvabilityLogic {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] {L : Logic ℕ} (hPL : L.IsProvabilityLogic T U) :
    Entailment.Łukasiewicz L

    L is Łukasiewicz if L is provability logic.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def LO.Modal.Logic.inst_Cl_of_isProvabilityLogic {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] {L : Logic ℕ} (hPL : L.IsProvabilityLogic T U) :
      Entailment.Cl L
      Equations
      Instances For
        source
        theorem LO.Modal.Logic.subset_GL_of_isProvabilityLogic {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] {L : Logic ℕ} [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (hPL : L.IsProvabilityLogic T U) :
        Modal.GL ⊆ L
        source
        theorem LO.Modal.Logic.provable_GL_of_isProvabilityLogic {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] {L : Logic ℕ} {A : Formula ℕ} [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (hPL : L.IsProvabilityLogic T U) :
        Modal.GL ⊢ A → L ⊢ A
        source
        def LO.FirstOrder.ArithmeticTheory.provabilityLogicOn (T U : ArithmeticTheory) [Theory.Δ₁ T] :
        Modal.Logic ℕ

        Provability Logic of T relative to metatheory U

        Equations
        Instances For
          source
          @[simp]
          theorem LO.FirstOrder.ArithmeticTheory.isProvabilityLogic_provabilityLogicOn {T U : ArithmeticTheory} [Theory.Δ₁ T] :
          (T.provabilityLogicOn U).IsProvabilityLogic T U
          source
          theorem LO.FirstOrder.ArithmeticTheory.provabilityLogicOn.provable_iff {T U : ArithmeticTheory} [Theory.Δ₁ T] {A : Modal.Formula ℕ} :
          T.provabilityLogicOn U ⊢ A ↔ ∀ (f : T.StandardRealization), U ⊢ ↑f A
          source
          instance LO.FirstOrder.ArithmeticTheory.instClFormulaNatLogicProvabilityLogicOn {T U : ArithmeticTheory} [Theory.Δ₁ T] :
          Entailment.Cl (T.provabilityLogicOn U)
          Equations