Logics for First-Order Team Properties

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