On the Succinctness of Atoms of Dependency

TL;DR

This paper compares the succinctness of various non-classical atoms in propositional team logic, establishing exponential lower bounds in the existential fragment and polynomial upper bounds in the full logic.

Contribution

It introduces a formula size game to analyze the succinctness of dependence, independence, inclusion, exclusion, and anonymity atoms in propositional team logic.

Findings

Exponential lower bounds for all atoms in the existential fragment.

Polynomial upper bounds for all atoms in the full propositional team logic.

Systematic comparison of atom succinctness in different logical fragments.

Abstract

Propositional team logic is the propositional analog to first-order team logic. Non-classical atoms of dependence, independence, inclusion, exclusion and anonymity can be expressed in it, but for all atoms except dependence only exponential translations are known. In this paper, we systematically compare their succinctness in the existential fragment, where the splitting disjunction only occurs positively, and in full propositional team logic with unrestricted negation. By introducing a variant of the Ehrenfeucht-Fra\"{i}ss\'{e} game called formula size game into team logic, we obtain exponential lower bounds in the existential fragment for all atoms. In the full fragment, we present polynomial upper bounds also for all atoms.