Not Nothing: Nonemptiness in Team Semantics
Aleksi Anttila

Abstract:
This dissertation collects together five papers which focus primarily on the expressive power, axiomatizations, and proof theory of propositional and modal logics with team semantics. Most of these papers focus on settings in which the empty team property fails—that is, there are formulas which are not true in the empty team—and hence in which we are able to express facts and reason about the emptiness and nonemptiness of teams in the object language.

The first paper studies the mathematical properties of bilateral state-based modal logic (BSML), a modal team logic which has been used to account for free choice inferences and related linguistic phenomena. This logic extends classical modal logic with a nonemptiness atom NE which is true in a team if and only if the team is nonempty. In this paper, we introduce two extensions of BSML, show that the extensions are expressively complete, and develop natural deduction axiomatizations for the three logics.

In the second paper, we prove expressive completeness results for convex propositional and modal team logics, where a logic is convex if, for each of its formulas, if the formula is true in two teams, then it is also true in all the teams between these two teams with respect to set inclusion. Convexity is a natural generalization of the well-known property of downward closure to a setting in which the empty team property fails. We introduce multiple propositional/modal logics which are expressively complete for the class of all convex propositional/modal team properties. We also solve a problem that was left open in the first paper concerning the expressive power of BSML as well as its propositional fragment: we show that BSML is expressively complete for the class of all convex and union-closed modal team properties invariant under bounded bisimulation. We also introduce a generalization of uniform definability and define distinct notions of extension making use of this generalization in order to clarify the sense in which our novel propositional convex logics extend propositional dependence logic and propositional inquisitive logic.

In the third paper, we study the properties of the negation employed in BSML, the bilateral negation ¬. This is essentially the same notion as the dual or game-theoretical negation of independence-friendly logic (IF) and dependence logic (D). In IF and D, the dual negation exhibits an extreme degree of semantic indeterminacy in that for any pair of sentences A and B of IF/D, if A and B are incompatible in the sense that they share no models, there is a sentence C of IF/D such that A≡C and B≡¬C (as shown originally by Burgess in the equivalent context of the prenex fragment of Henkin quantifier logic). We show that by adjusting the notion of incompatibility employed (thus generating, in some cases, notions of incompatibility more suitable for settings in which the empty team property and downward closure fail than the notions imported from downward-closed settings), analogues of this result can be established for a number of modal and propositional team logics, including BSML and propositional dependence logic with the dual negation. Together with its converse, a result of this type can be seen as an expressive completeness theorem with respect to the relevant incompatibility notion; we formulate a notion of expressive completeness for pairs of properties to make this precise.

In the fourth paper, we move to a setting which does have the empty team property, but in which downward closure fails. We provide a complete axiomatization of modal inclusion logic—team-based modal logic extended with inclusion atoms. We review and refine an expressive completeness and normal form theorem for the logic, define a natural deduction proof system, and use the normal form to prove completeness of the axiomatization. Complete axiomatizations are also provided for two other extensions of modal logic with the same expressive power as modal inclusion logic: one augmented with a might-operator and the other with a single-world variant of the might-operator.

In the fifth paper, we introduce a sequent calculus for the propositional team logic with both the split disjunction and the inquisitive disjunction. The sequent calculus consists of a G3-style system for classical propositional logic together with deep-inference rules for the inquisitive disjunction. We show that the system satisfies various desirable properties: it admits height-preserving weakening, contraction and inversion; it supports a procedure for constructing cutfree proofs and countermodels similar to that for G3cp; and cut elimination holds as a corollary of cut elimination for the G3-style subsystem together with a normal form theorem for cutfree derivations in the system.