Standard Modal Logic - Logic Formalization in Lean 4

As a general term for various modal logics commonly known as $K$ , $S4$ , etc., we refer to the logic defined on a language that includes the modal operators $□$ (Box) and $◊$ (Diamond), where $◊$ is defined as the dual of $□$ (i.e., $◊ φ \equiv \neg □ \neg φ$ ), as Standard Modal Logic¹.

Be cautious similar notations for different concepts. We use $T E X$ notation for concept that unrelated to our formalization, and code block `` for related our formalization.

$K$ (\sf K) is axiom schema unrelated to formalization.

$K$ (\bf K) is logic unrelated to formalization.

𝗞 (Mathematical Sans-Serif Bold) is AxiomSet in formalization.

𝐊 (Mathematical Bold Capital) is DeductionParameter in formalization.

This term is probably not usual. We introducing for convenience in naming and organizing within our formalization.