Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The flattening operator in team-based logics

Arnaud Durand, Juha Kontinen, Werner Mérian, Jouko Väänänen

TL;DR

This paper studies the flattening operator $\mathsf{F}$ in team semantics, focusing on how it interacts with core logics such as dependence, anonymity, inclusion, and exclusion. It provides an axiomatic and semantic account of $\mathsf{F}$, analyzes its impact on flatness and closure properties, and derives precise expressivity results across full FO and fixed-arity fragments. Notably, $\mathsf{F}$ is conservative for many logics (e.g., dependence, exclusion, independence, and full FO with negation), but it increases expressive power for certain unary fragments (e.g., unary inclusion and unary anonymity) and enables explicit separations (e.g., non-connectedness of graphs). The work uses translations to GFP$^{+}$ and ESO to justify safeness, and it identifies concrete separating formulas, clarifying the nuanced role of $\mathsf{F}$ in the landscape of team-based logics.

Abstract

We propose a systematic study of the so-called flattening operator in team semantics. This operator was first introduced by Hodges in 1997, and has not been studied in more detail since. We begin a systematic study of the expressive power this operator adds to the most well-known team-based logics, such as dependence logic, anonymity logic, inclusion logic and exclusion logic.

The flattening operator in team-based logics

TL;DR

This paper studies the flattening operator in team semantics, focusing on how it interacts with core logics such as dependence, anonymity, inclusion, and exclusion. It provides an axiomatic and semantic account of , analyzes its impact on flatness and closure properties, and derives precise expressivity results across full FO and fixed-arity fragments. Notably, is conservative for many logics (e.g., dependence, exclusion, independence, and full FO with negation), but it increases expressive power for certain unary fragments (e.g., unary inclusion and unary anonymity) and enables explicit separations (e.g., non-connectedness of graphs). The work uses translations to GFP and ESO to justify safeness, and it identifies concrete separating formulas, clarifying the nuanced role of in the landscape of team-based logics.

Abstract

We propose a systematic study of the so-called flattening operator in team semantics. This operator was first introduced by Hodges in 1997, and has not been studied in more detail since. We begin a systematic study of the expressive power this operator adds to the most well-known team-based logics, such as dependence logic, anonymity logic, inclusion logic and exclusion logic.

Paper Structure

This paper contains 20 sections, 22 theorems, 41 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Our contributions
  3. Preliminaries
  4. Team semantics
  5. Closure properties
  6. Flattening of a formula
  7. Flattening operator
  8. Definition
  9. Basic properties of the flattening operator
  10. Preservation of closure properties
  11. The expressive power of the flattening operator
  12. Adding F to inclusion and anonymity logic
  13. Adding F to unary inclusion logic
  14. Adding F to unary anonymity logic
  15. Expressivity of unary anonymity atoms and the flattening operator
  16. ...and 5 more sections

Key Result

Proposition 3.1

The following equivalences are implied by the above axioms:

Figures (3)

  • Figure 4.1: Relation between all flatness notions
  • Figure 5.1: Illustration of the anonymity atom mechanism to fill a cycle
  • Figure 6.1: Expressive power of logics on the level of formulas

Theorems & Definitions (48)

  • Example
  • Definition 2.1: Team semantics for first-order logic
  • Definition 2.2
  • Proposition 3.1
  • proof
  • Remark 3.2
  • Definition 4.1: Syntax of the flattening operator
  • Definition 4.2: Semantics of the flattening operator
  • proof
  • proof
  • ...and 38 more