Complete logics for elementary team properties

TL;DR

This paper introduces a new team semantics-based logic, FOT, which aligns with first-order logic in expressive power, and a sublogic, FOT${}^ extarrow$, that captures downward closed elementary team properties, with complete axiomatizations provided.

Contribution

It presents the first complete axiomatization of FOT and extends dependence logic with logical constants from FOT${}^ extarrow$, advancing the understanding of team semantics.

Findings

FOT has elementary expressive power matching first-order logic.

FOT${}^ extarrow$ captures downward closed elementary team properties.

Complete axiomatizations for FOT and its sublogic are achieved.

Abstract

In this paper, we introduce a logic based on team semantics, called FOT, whose expressive power is elementary, i.e., coincides with first-order logic both on the level of sentences and (possibly open) formulas, and we also show that a sublogic of FOT, called FOT${}^\downarrow$, captures exactly downward closed elementary (or first-order) team properties. We axiomatize completely the logic FOT, and also extend the known partial axiomatization of dependence logic to dependence logic enriched with the logical constants in FOT${}^\downarrow$.