Strength between Logics

It is immediately apparent that, when 𝓓₁​ and 𝓓₂ are same inference rule¹, the logical strength between 𝓓₁ and 𝓓₂ is determined by the subset of their axiom set.

lemma reducible_of_subset (hNec : L₁.nec ≤ L₂.nec) (hAx : Ax(L₁) ⊆ Ax(L₂)) : L₁ ≤ₛ L₂ := by

lemma reducible_K_KT : 𝐊 ≤ₛ 𝐊𝐓

• LO.Modal.Standard.Deduction.reducible_of_subset
• LO.Modal.Standard.reducible_K_KT

However, even without the subset of axiomset, it is possible to analyze the strength of logic via Kripke semantics, specifically by analyzing the properties of frames defined by the axioms. For example, since seriality follows from reflexivity, $\mathbf{KT}$ is stronger than $\mathbf{KD}$ ($\mathsf{K}\cup \mathsf{D}⊈\mathsf{K}\cup \mathsf{T}$).

lemma reducible_of_definability
  [Sound 𝓓₁​ 𝔽(Ax(𝓓₁​))] [Complete 𝓓₂ 𝔽(Ax(𝓓₂))]
  [Definability Ax(𝓓₁​) P₁] [Definability Ax(𝓓₂) P₂]
  (hs : ∀ {F : Frame}, P₂ F → P₁ F)
  : 𝓓₁​ ≤ₛ 𝓓₂

theorem reducible_KD_KT : 𝐊𝐃 ≤ₛ 𝐊𝐓

• LO.Modal.Standard.Kripke.reducible_of_definability
• LO.Modal.Standard.reducible_KD_KT

By same argument, the equivalence of provability between logics can be analyzed. $S5$ is equivalent to $KT4B$ ($\mathsf{K}\cup \mathsf{T}\cup 5\ne \mathsf{K}\cup \mathsf{T}\cup 4\cup \mathsf{B}$).

lemma equiv_of_iff_definability
  [Sound 𝓓₁​ 𝔽(Ax(𝓓₁​))] [Sound 𝓓₂ 𝔽(Ax(𝓓₂))]
  [Complete 𝓓₁​ 𝔽(Ax(𝓓₁​))] [Complete 𝓓₂ 𝔽(Ax(𝓓₂))]
  [Definability Ax(𝓓₁​) P₁] [Definability Ax(𝓓₂) P₂]
  (h : ∀ {F : Frame}, P₁ F ↔ P₂ F) : 𝓓₁​ =ₛ 𝓓₂

theorem equiv_S5_KT4B : 𝐒𝟓 =ₛ 𝐊𝐓𝟒𝐁

• LO.Modal.Standard.Kripke.equiv_of_iff_definability
• LO.Modal.Standard.equiv_S5_KT4B