Starting from a logic given by traditional semantics formulated in terms of semantic objects (assignments, valuations or worlds) team semantics lifts the denotations of formulas to sets, or teams, of semantic objects instead enabling the formulation of properties, such as variable dependency, not available in the traditional setting. Since the introduction by Hodges, and refinement by Väänänen, team semantic constructions have been used to generate expressively enriched logics still conserving nice properties, such as compactness or decidability. In contrast these logics fail to be substitutional, limiting any algebraic treatment, and rendering fully schematic proof systems impossible. This shortcoming can be attributed to the flatness principle, commonly adhered to when generating team semantics.

Investigating the formation of team logics from an algebraic perspective, and disregarding the flatness-principle, I will present the logic of teams (LT), a substitutional logic for which important propositional team logics are axiomatisable as fragments. Starting from classical propositional logic and Boolean algebras, we give semantics for LT by considering algebras of the form P(B) being the powerset of a Boolean algebra B, treated with treated with an internal (derived from B) and an external (set-theoretic) set of connectives. Furthermore, we present a well-motivated labelled natural deduction system for LT, for which a further analysis motivates a generalisation to constructions of logics by combinations of an internal and an external logic, where for LT both are classical propositional logic.

This is joint work with Fredrik Engström.