Expressibility and inexpressibility in propositional team logics

TL;DR

This paper introduces dimension theoretic methods to analyze propositional team logics, establishing expressibility limits, estimating complexity costs of atom reductions, and exploring new variants of atoms and operations.

Contribution

It develops quantitative dimension theoretic techniques for propositional team logics, extending previous first-order logic methods to analyze expressibility and complexity.

Findings

Certain team atoms can be expressed with lower arity atoms.

The complexity cost of arity reduction is quantified.

New variants of atoms and operations are introduced.

Abstract

We develop dimension theoretic methods for propositional team based logics. Such quantitative methods were defined for team based first-order logic in a recent paper by Hella, Luosto and the third author and were used to obtain strong hierarchy results in the first-order logic context. We show that in propositional logic and in several important cases, a team theoretical atom can be expressed in terms of atoms of lower arity. We estimate the `price' of such a reduction of arity, i.e. how much more complicated the new expression is. Our estimates involve as parameters the arity of the atoms involved, as well as the number of times the atom occurs in a formula. We also consider new variants of atoms and propositional operations, inspired by our work. We believe that our quantitative analysis leads to a deeper understanding of the scope and limits of propositional team based logic.