Monadic Semantics, Team Logics and Substitution

Abstract

In this thesis we investigate the issue of non-substitutionality of propositional team logics, in particular propositional dependence logic, by semantic means.

We establish a general language to discuss semantic systems for logics fundamentally based on consensus of truth in a class of objects. Importantly we admit a notion of logic that does not assume closure under substitution. We show how to express traditional semantic systems using this general language and describe a condition of being truth-compositional defined using a notion of defining sets for formulas. We then give an account of propositional dependence logic as described by Yang and Väänänen [YV16], and investigated by Lück [Lüc20] and Quadrellaro [Qua21].This is done using valuational team semantics based on sets of valuations as semantic objects. For valuational team semantics in general we describe the property of flatness and prove that a flat valuational team semantics always is equivalent to a standard valuational semantics. We then formulate the problem of non-substitutionality for logics based on the semantics and describe some of the consequences it has for the development and investigation of team logics.

The main part and contribution of this thesis develops a new semantic framework we call monadic semantics, constructed by considering a universe for which propositional variables are interpreted as unary predicates by monadic models and the interpretation of complex formulas are governed by a monadic frame. We show how monadic semantics are sufficient to express every logic with truth- compositional semantics, in the sense defined, by constructing monadic dual semantics. We also define the maximal and the full semantics of a monadic frame. We show how a notion of monadic team semantics corresponding to Yang and Väänänens construction can be identified as a particular type of monadic semantics and translate the results regarding flatness to this setting. With this se- mantic notion defined we utilise a definiton of interpretation sets for formulas to express notions of independence and generality of atoms in a semantics. With this in place we can prove connections between these properties of a semantics, and substitutionality of the logic it defines. In this way we can give a full semantic categorisation of whether a logic is closed under singular substitution, and both a necessary and a sufficient condition for unrestricted substitution in any logic with monadic semantics. As a direct consequence these categorisations imply that every maximal monadic seman- tics that correspond to a semantics of Yang and Väänänen’s construction is either flat, or its logic is not closed under substitution. We reveal that the main reason for this is the treatment of atomic formulas in valuational team semantics. In the last part of the thesis we use monadic semantics and introduce natural teamifications to construct a semantics defining a new logic we call boolean teamified boolean logic, BTB. We com- plement this by exhibiting a set of axioms that, when assumed in BTB, gives an up to typographical renaming conservative extension of propositional dependence logic. We also hint on strong connec- tions between BTB and Girard’s linear logic [GLR95].