Decidability of predicate logics with team semantics

TL;DR

This paper investigates the computational complexity of various predicate logics with team semantics, establishing NEXPTIME-completeness for some and undecidability for others, thus advancing understanding of their decidability boundaries.

Contribution

It proves NEXPTIME-completeness for satisfiability of two-variable independence and inclusion logic, and undecidability for validity in two-variable dependence logic, solving open problems.

Findings

Satisfiability of two-variable independence logic is NEXPTIME-complete.

Satisfiability of two-variable inclusion logic is NEXPTIME-complete.

Validity of two-variable dependence logic is undecidable.

Abstract

We study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Sch\"onfinkel-Ramsey prefix classes of dependence logic.