On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics

TL;DR

This paper characterizes the union closed fragment of existential second-order logic and team semantics, introduces inclusion-exclusion games for model checking, and provides new logical tools to understand and capture this fragment.

Contribution

It offers syntactic characterizations, introduces inclusion-exclusion games, and defines a team atom that captures the union closed fragment, answering an open question.

Findings

Syntactic characterization of union closed fragments.

Introduction of inclusion-exclusion games for model checking.

A team atom that captures the union closed fragment of ESO.

Abstract

We present syntactic characterisations for the union closed fragments of existential second-order logic and of logics with team semantics. Since union closure is a semantical and undecidable property, the normal form we introduce enables the handling and provides a better understanding of this fragment. We also introduce inclusion-exclusion games that turn out to be precisely the corresponding model-checking games. These games are not only interesting in their own right, but they also are a key factor towards building a bridge between the semantic and syntactic fragments. On the level of logics with team semantics we additionally present restrictions of inclusion-exclusion logic to capture the union closed fragment. Moreover, we define a team based atom that when adding it to first-order logic also precisely captures the union closed fragment of existential second-order logic which answers an open question by Galliani and Hella.