We study the mathematical properties of bilateral state-based modal logic (BSML), a modal logic employing state-based semantics (also known as team semantics), which has been used to account for free choice inferences and related linguistic phenomena. This logic extends classical modal logic with a nonemptiness atom which is true in a state if and only if the state is nonempty. We introduce two extensions of BSML and show that the extensions are expressively complete, and develop natural deduction axiomatizations for the three logics.

翻译：我们研究双边基于状态的模态逻辑（BSML）的数学性质。该逻辑采用基于状态的语义（也称为团队语义），已用于解释自由选择推理及相关语言现象。该逻辑在经典模态逻辑基础上扩展了一个非空原子，该原子在某个状态中为真当且仅当该状态非空。我们引入了BSML的两种扩展，证明这些扩展具有表达完备性，并为这三种逻辑建立了自然演绎公理化系统。