  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.
