Classification of provability logics

A provability logic of trace ω contained in 𝐒 is one of 𝐀, 𝐃, and 𝐒. In general, the provability logic of T relative to U is one of GLα X, GLβ X, D ∩ GLβ X, and S ∩ GLβ X, where X is its trace.

References

• [AB05, Theorem 40]
• [Bek90, Assertion 3, Assertion 6]

theorem FFL.ProvabilityLogic.alpha_mem_provabilityLogic_of_provable_localReflectionOn_Sigma1 {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] (h : U ⊢* 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1] T) (n : ℕ) : Formula.alpha n ∈ T.provabilityLogicRelativeTo U

theorem FFL.ProvabilityLogic.provabilityLogic_eq_A_or_eq_D_or_eq_S {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] : (T.provabilityLogicRelativeTo U).trace = Set.univ → T.provabilityLogicRelativeTo U ⪯ 𝐒 → T.provabilityLogicRelativeTo U = 𝐀 ∨ T.provabilityLogicRelativeTo U = 𝐃 ∨ T.provabilityLogicRelativeTo U = 𝐒

A provability logic of trace ω contained in 𝐒 is one of 𝐀, 𝐃, and 𝐒.

• [Bek90, Assertion 3]

theorem FFL.ProvabilityLogic.provabilityLogic_equiv_A_or_equiv_D_or_equiv_S {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] : (T.provabilityLogicRelativeTo U).trace = Set.univ → T.provabilityLogicRelativeTo U ⪯ 𝐒 → T.provabilityLogicRelativeTo U ≊ 𝐀 ∨ T.provabilityLogicRelativeTo U ≊ 𝐃 ∨ T.provabilityLogicRelativeTo U ≊ 𝐒

theorem FFL.ProvabilityLogic.imp_mem_provabilityLogic_of_mem_add_localReflectionOn {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] {N : Set ℕ} {A : Formula α} [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] (hN : N.Finite) (h : A ∈ T.provabilityLogicRelativeTo (U ∪ 𝗥𝗳𝗻[(fun (x : ℕ) => (↑(FirstOrder.Theory.standardProvability T))^[x] ⊥) '' N] T)) : ↑(⩕ (n : ℕ) ∈ hN.toFinset, Formula.alpha n) 🡒 A ∈ T.provabilityLogicRelativeTo U

theorem FFL.ProvabilityLogic.trace_provabilityLogic_add_localReflectionOn_eq_univ {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] : (T.provabilityLogicRelativeTo (U ∪ 𝗥𝗳𝗻[(fun (x : ℕ) => (↑(FirstOrder.Theory.standardProvability T))^[x] ⊥) '' (T.provabilityLogicRelativeTo U).traceᶜ] T)).trace = Set.univ

theorem FFL.ProvabilityLogic.provabilityLogic_classification {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] : T.provabilityLogicRelativeTo U = 𝐆𝐋α (T.provabilityLogicRelativeTo U).trace ∨ ∃ (hL : (T.provabilityLogicRelativeTo U).traceᶜ.Finite), T.provabilityLogicRelativeTo U = 𝐆𝐋β (T.provabilityLogicRelativeTo U).trace hL ∨ T.provabilityLogicRelativeTo U = 𝐃 ∩ 𝐆𝐋β (T.provabilityLogicRelativeTo U).trace hL ∨ T.provabilityLogicRelativeTo U = 𝐒 ∩ 𝐆𝐋β (T.provabilityLogicRelativeTo U).trace hL

The provability logic of T relative to U is one of GLα X, GLβ X, D ∩ GLβ X, and S ∩ GLβ X, where X is its trace.

• [AB05, Theorem 40]
• [Bek90, Assertion 6]

theorem FFL.ProvabilityLogic.provabilityLogic_classification_equiv {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] : T.provabilityLogicRelativeTo U ≊ 𝐆𝐋α (T.provabilityLogicRelativeTo U).trace ∨ ∃ (hL : (T.provabilityLogicRelativeTo U).traceᶜ.Finite), T.provabilityLogicRelativeTo U ≊ 𝐆𝐋β (T.provabilityLogicRelativeTo U).trace hL ∨ T.provabilityLogicRelativeTo U ≊ 𝐃 ∩ 𝐆𝐋β (T.provabilityLogicRelativeTo U).trace hL ∨ T.provabilityLogicRelativeTo U ≊ 𝐒 ∩ 𝐆𝐋β (T.provabilityLogicRelativeTo U).trace hL

theorem FFL.ProvabilityLogic.trace_provabilityLogic_eq_univ_of_provable_localReflectionOn_Sigma1 {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] (h : U ⊢* 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1] T) : (T.provabilityLogicRelativeTo U).trace = Set.univ

theorem FFL.ProvabilityLogic.D_weakerThan_provabilityLogic_of_provable_localReflectionOn_Sigma1 {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] (h : U ⊢* 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1] T) : 𝐃 ⪯ T.provabilityLogicRelativeTo U

theorem FFL.ProvabilityLogic.S_weakerThan_provabilityLogic_of_provable_localReflection {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] (h : U ⊢* 𝗥𝗳𝗻[Set.univ] T) : 𝐒 ⪯ T.provabilityLogicRelativeTo U

theorem FFL.ProvabilityLogic.trace_provabilityLogic_add_con_eq_univ {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [FirstOrder.Theory.Δ₁ U] [𝗜𝚺₁ ⪯ T] (hTU : ∀ (σ : FirstOrder.Sentence ℒₒᵣ), 𝗜𝚺₁ ⊢ ↑(FirstOrder.Theory.standardProvability T) σ 🡒 ↑(FirstOrder.Theory.standardProvability U) σ) (hU : U ⊢* 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1] T) : (T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Con U)).trace = Set.univ

theorem FFL.ProvabilityLogic.A_weakerThan_provabilityLogic_add_con {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [FirstOrder.Theory.Δ₁ U] [𝗜𝚺₁ ⪯ T] (hTU : ∀ (σ : FirstOrder.Sentence ℒₒᵣ), 𝗜𝚺₁ ⊢ ↑(FirstOrder.Theory.standardProvability T) σ 🡒 ↑(FirstOrder.Theory.standardProvability U) σ) (hU : U ⊢* 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1] T) : 𝐀 ⪯ T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Con U)

theorem FFL.ProvabilityLogic.provabilityLogic_add_con_eq_A {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [FirstOrder.Theory.Δ₁ U] [𝗜𝚺₁ ⪯ T] (hTU : ∀ (σ : FirstOrder.Sentence ℒₒᵣ), 𝗜𝚺₁ ⊢ ↑(FirstOrder.Theory.standardProvability T) σ 🡒 ↑(FirstOrder.Theory.standardProvability U) σ) (hU : U ⊢* 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1] T) (hC : Entailment.Consistent (T ∪ FirstOrder.Theory.Con U)) : T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Con U) = 𝐀

• [AB05, Example 63]

theorem FFL.ProvabilityLogic.provabilityLogic_add_con_equiv_A {α : Type u_1} {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [FirstOrder.Theory.Δ₁ U] [𝗜𝚺₁ ⪯ T] (hTU : ∀ (σ : FirstOrder.Sentence ℒₒᵣ), 𝗜𝚺₁ ⊢ ↑(FirstOrder.Theory.standardProvability T) σ 🡒 ↑(FirstOrder.Theory.standardProvability U) σ) (hU : U ⊢* 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1] T) (hC : Entailment.Consistent (T ∪ FirstOrder.Theory.Con U)) : T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Con U) ≊ 𝐀

theorem FFL.ProvabilityLogic.trace_provabilityLogic_turingOmega_eq_univ {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] : (T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Conω T)).trace = Set.univ

theorem FFL.ProvabilityLogic.provabilityLogic_turingOmega_eq_A {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] (hC : Entailment.Consistent (T ∪ FirstOrder.Theory.Conω T)) : T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Conω T) = 𝐀

• [AB05, Example 59]

theorem FFL.ProvabilityLogic.provabilityLogic_turingOmega_equiv_A {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] (hC : Entailment.Consistent (T ∪ FirstOrder.Theory.Conω T)) : T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Conω T) ≊ 𝐀

theorem FFL.ProvabilityLogic.provabilityLogic_turingOmega_eq_A_of_sigma1Sound {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Conω T) = 𝐀

theorem FFL.ProvabilityLogic.trace_provabilityLogic_add_con_self_eq {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : (T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Con T)).trace = {0}

theorem FFL.ProvabilityLogic.provabilityLogic_add_con_self_eq_GLAlpha {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T.provabilityLogicRelativeTo (T ∪ FirstOrder.Theory.Con T) = 𝐆𝐋α {0}

PL(T, T + Con(T)) = 𝐆𝐋 + ¬□⊥ for a 𝚺₁-sound T.

theorem FFL.ProvabilityLogic.provabilityLogic_add_localReflectionOn_Sigma_eq_D {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] {n : ℕ} [NeZero n] [𝗜𝚺₁ ⪯ T] [𝗕𝚺n ⪯ T] : Entailment.Consistent (T ∪ 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 n] T) → T.provabilityLogicRelativeTo (T ∪ 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 n] T) = 𝐃

theorem FFL.ProvabilityLogic.provabilityLogic_add_localReflectionOn_Sigma_equiv_D {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] {n : ℕ} [NeZero n] [𝗜𝚺₁ ⪯ T] [𝗕𝚺n ⪯ T] : Entailment.Consistent (T ∪ 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 n] T) → T.provabilityLogicRelativeTo (T ∪ 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 n] T) ≊ 𝐃

theorem FFL.ProvabilityLogic.provabilityLogic_add_localReflectionOn_Sigma_eq_D_of_sigma1Sound {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] {n : ℕ} [NeZero n] [𝗜𝚺₁ ⪯ T] [𝗕𝚺n ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T.provabilityLogicRelativeTo (T ∪ 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 n] T) = 𝐃

theorem FFL.ProvabilityLogic.provabilityLogic_add_localReflectionOn_Sigma1_eq_D {α : Type u_1} {T : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] : Entailment.Consistent (T ∪ 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1] T) → T.provabilityLogicRelativeTo (T ∪ 𝗥𝗳𝗻[ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1] T) = 𝐃

• [AB05, Example 60]