Formalizing Strong Completeness of Normal Modal Logic

Stream: new members

[SnO2WMaN]

Hello. I recently completed to formalize the strong completeness(↓) for Normal Modal Logic (K and its axiom T,B,D,4,5 extensions: e.g. KD, S4, S5) in Palalansoukî's Logic Formalization Project.

$$\Gamma \vDash_{\mathbb{F}(\Lambda)} \varphi \iff \Gamma \vdash_\Lambda \varphi$$

refer: https://github.com/iehality/lean4-logic/blob/master/Logic/Modal/Normal/Completeness.lean

Next, I am planning to formalize:

• the finite modeling properties
• intuitional modal logic
• provability logic (Gödel-Lob Logic GL)
• modal companion (intuitional propositional logic can be translated to S4)
• frame definabilities
• extended sequent calculus for modal logic

But if there is something else that might be interesting to formalize or a good material/document about modal logic, please let me know.

Currently I referenced:

• Open Logic Project
• P. Blackburn, et al, "Modal Logic"

Related works for Modal Logic in Lean 4 (and old version of lean)

• https://github.com/alexoltean61/hybrid_logic_lean
• https://github.com/m4lvin/lean4-pdl
• https://github.com/paulaneeley/modal (Lean 3)
• https://github.com/ljt12138/Formalization-PAL (Lean 3)