# Polyteam Semantics

## TL;DR

This paper introduces Polyteam Semantics, a new framework evaluating formulas over families of teams, advancing the understanding of dependence and independence logics and their relation to database theory.

## Contribution

It defines a novel polyteam variant of dependence atoms, provides a finite axiomatisation, and characterizes the expressive power of poly-dependence and poly-independence logics.

## Key findings

- Finite axiomatisation for the implication problem of polyteam dependence atoms
- Poly-dependence and poly-independence logics characterize properties downwards closed and ESO-definable
- Poly-inclusion logic relates to greatest fixed point logic

## Abstract

Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define "Polyteam Semantics" in which formulae are evaluated over a family of teams. We begin by defining a novel polyteam variant of dependence atoms and give a finite axiomatisation for the associated implication problem. We relate polyteam semantics to team semantics and investigate in which cases logics over the former can be simulated by logics over the latter. We also characterise the expressive power of poly-dependence logic by properties of polyteams that are downwards closed and definable in existential second-order logic (ESO). The analogous result is shown to hold for poly-independence logic and all ESO-definable properties. We also relate poly-inclusion logic to greatest fixed point logic.