Formalized Formal Logic

2.5. Löb's Theorem🔗

Löb's theorem states that if "if σ is provable, then σ" is provable, then σ is provable.

🔗theorem
LO.FirstOrder.Arithmetic.löb_theorem {T : ArithmeticTheory}
  [Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] {σ : ArithmeticSentence} :
  T ⊢ ↑(Theory.standardProvability T) σ ➝ σ → T ⊢ σ
LO.FirstOrder.Arithmetic.löb_theorem
  {T : ArithmeticTheory} [Theory.Δ₁ T]
  [𝗜𝚺₁ ⪯ T] {σ : ArithmeticSentence} :
  T ⊢
      ↑(Theory.standardProvability T) σ ➝
        σ →
    T ⊢ σ

The argument can be formalized within arithmetic.

🔗theorem
LO.FirstOrder.Arithmetic.formalized_löb_theorem {T : ArithmeticTheory}
  [Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] {σ : ArithmeticSentence} :
  𝗜𝚺₁ ⊢
    ↑(Theory.standardProvability T)
        (↑(Theory.standardProvability T) σ ➝ σ) ➝
      ↑(Theory.standardProvability T) σ
LO.FirstOrder.Arithmetic.formalized_löb_theorem
  {T : ArithmeticTheory} [Theory.Δ₁ T]
  [𝗜𝚺₁ ⪯ T] {σ : ArithmeticSentence} :
  𝗜𝚺₁ ⊢
    ↑(Theory.standardProvability T)
        (↑(Theory.standardProvability T)
            σ ➝
          σ) ➝
      ↑(Theory.standardProvability T) σ

In the perspective of modal logic, this is modal axiom L.