Strongly First Order, Domain Independent Dependencies: the Union-Closed Case

TL;DR

This paper characterizes when certain domain-independent, union-closed dependency atoms can be added to First Order Logic without increasing its expressive power, ensuring the extended logic remains strongly first order.

Contribution

It provides necessary and sufficient conditions for dependency atoms to be strongly first order, expanding understanding of dependencies in team semantics.

Findings

Identifies conditions for dependency atoms to be strongly first order.

Shows that certain union-closed, domain-independent dependencies do not increase expressiveness.

Clarifies the boundaries of expressiveness in team semantics extensions.

Abstract

Team Semantics generalizes Tarski's Semantics by defining satisfaction with respect to sets of assignments rather than with respect to single assignments. Because of this, it is possible to use Team Semantics to extend First Order Logic via new kinds of connectives or atoms - most importantly, via dependency atoms that express dependencies between different assignments. Some of these extensions are more expressive than First Order Logic proper, while others are reducible to it. In this work, I provide necessary and sufficient conditions for a dependency atom that is domain independent (in the sense that its truth or falsity in a relation does not depend on the existence in the model of elements that do not occur in the relation) and union closed (in the sense that whenever it is satisfied by all members of a family of relations it is also satisfied by their union) to be strongly first order, in the sense that the logic obtained by adding them to First Order Logic is no more expressive than First Order Logic itself.