def LO.Modal.Logic.αPL (L : Logic ℕ) (X : Set ℕ) : Logic ℕ

α-type provability logic extension

Equations

• L.αPL X = L.sumQuasiNormal (LO.Modal.TBB '' X)

@[simp]

theorem LO.Modal.Logic.eq_GLαω_GLαPL : Modal.GLαω = Modal.GL.αPL Set.univ

instance LO.Modal.Logic.instSubstitutionNatImageFormulaTBB {X : Set ℕ} : Logic.Substitution (TBB '' X)

theorem LO.Modal.Logic.αPL_isProvabilityLogic {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] {L : Logic ℕ} {X : Set ℕ} [L.Substitution] (hPL : L.IsProvabilityLogic T U) : (L.αPL X).IsProvabilityLogic T (U + (fun (x : ℕ) => ↑T.LetterlessStandardRealization (TBB x)) '' X)

theorem LO.Modal.Logic.αPL_subset_S {L : Logic ℕ} {X : Set ℕ} (hS : L ⊆ Modal.S) : L.αPL X ⊆ Modal.S

theorem LO.ProvabilityLogic.subset_GLαω_of_omega_trace {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (L : Modal.Logic ℕ) (hPL : L.IsProvabilityLogic T U) (hT : L.trace = Set.univ) : Modal.GLαω ⊆ L

Corollary 50 (half) in [A.B05]

theorem LO.ProvabilityLogic.subset_D_of_subset_GLαβ_of_omega_trace {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (L : Modal.Logic ℕ) (hPL : L.IsProvabilityLogic T U) (hT : L.trace = Set.univ) : Modal.GLαω ⊂ L → Modal.D ⊆ L

• Corollary 52(2) in [A.B05]

theorem LO.ProvabilityLogic.no_logic_between_GLαω_D {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (L : Modal.Logic ℕ) (hPL : L.IsProvabilityLogic T U) (hT : L.trace = Set.univ) : ¬(Modal.GLαω ⊂ L ∧ L ⊂ Modal.D)

• Corollary 55 in [A.B05]

theorem LO.ProvabilityLogic.eq_S_of_not_subset_D_of_omega_trace {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (L : Modal.Logic ℕ) (hPL : L.IsProvabilityLogic T U) (hT : L.trace = Set.univ) : Modal.D ⊂ L → Modal.S ⊆ L

• Assertion 1 in [Bek90]

theorem LO.ProvabilityLogic.no_logic_between_D_S {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (L : Modal.Logic ℕ) (hPL : L.IsProvabilityLogic T U) (hT : L.trace = Set.univ) : ¬(Modal.D ⊂ L ∧ L ⊂ Modal.S)

• Corollary 58 in [A.B05]

theorem LO.ProvabilityLogic.classification_S_sublogics_of_omega_trace {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (L : Modal.Logic ℕ) (hPL : L.IsProvabilityLogic T U) (hT : L.trace = Set.univ) (L_subset_S : L ⊆ Modal.S) : L = Modal.GLαω ∨ L = Modal.D ∨ L = Modal.S

If L.trace is omega then L is one of GLαω, D, and S.

• Assertion 3 in [Bek90]

theorem LO.ProvabilityLogic.eq_inter_αPL_GLβMinus_of_isProvabilityLogic_of_cofinite_trace {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (L : Modal.Logic ℕ) [L.Substitution] (hPL : L.IsProvabilityLogic T U) (hCf : L.trace.Cofinite) : L = L.αPL L.traceᶜ ∩ Modal.GLβMinus L.trace ⋯

Let L be provability logic L.trace is cofinite. Then L = (L.αPL L.traceᶜ) ∩ (GLβMinus L.trace).

theorem LO.ProvabilityLogic.eq_GLαω_inter_GLβMinus_GLα {L : Modal.Logic ℕ} (hβ : L.trace.Cofinite) : Modal.GLα L.trace = Modal.GLαω ∩ Modal.GLβMinus L.trace ⋯

theorem LO.ProvabilityLogic.aPL_compl_trace_isProvabilityLogic {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] {L : Modal.Logic ℕ} [L.Substitution] (hPL : L.IsProvabilityLogic T U) : (L.αPL L.traceᶜ).IsProvabilityLogic T (U + (fun (x : ℕ) => ↑T.LetterlessStandardRealization (Modal.TBB x)) '' L.traceᶜ)

theorem LO.ProvabilityLogic.aPL_compl_trace_subset_S {L : Modal.Logic ℕ} (hS : L ⊆ Modal.S) : L.αPL L.traceᶜ ⊆ Modal.S

theorem LO.ProvabilityLogic.aPL_compl_trace_omega_trace {L : Modal.Logic ℕ} (hS : L ⊆ Modal.S) : (L.αPL L.traceᶜ).trace = Set.univ

theorem LO.ProvabilityLogic.classification_S_sublogics_of_cofinite_trace {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] {L : Modal.Logic ℕ} [L.Substitution] (hPL : L.IsProvabilityLogic T U) (hCf : L.trace.Cofinite) (hS : L ⊆ Modal.S) : L = Modal.GLα L.trace ∨ L = Modal.D ∩ Modal.GLβMinus L.trace ⋯ ∨ L = Modal.S ∩ Modal.GLβMinus L.trace ⋯

theorem LO.ProvabilityLogic.classification_provability_logics {T U : FirstOrder.ArithmeticTheory} [FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] [T ⪯ U] (L : Modal.Logic ℕ) [L.Substitution] (hPL : L.IsProvabilityLogic T U) : if h_coinfinite : L.trace.Coinfinite then L = Modal.GLα L.trace else if ¬L ⊆ Modal.S then L = Modal.GLβMinus L.trace ⋯ else L = Modal.GLα L.trace ∨ L = Modal.D ∩ Modal.GLβMinus L.trace ⋯ ∨ L = Modal.S ∩ Modal.GLβMinus L.trace ⋯

The classification theorem of provability logics.

• Assertion 6 in [Bek90]
• Theorem 40 in [A.B05]