Axiomatizations of Team Logics

TL;DR

This paper develops sound and complete axiomatizations for various team-based logics, extending classical proof systems to handle dependence, independence, and other team semantics, with a focus on elimination of modalities and quantifiers.

Contribution

It introduces a modular framework for axiomatizing team logics, including dependence-free fragments and their extensions, with a novel semantics-preserving elimination technique.

Findings

Established sound and complete axiomatizations for multiple team logics.

Proved that modalities and quantifiers can be eliminated without loss of semantics.

Provided a unified approach to axiomatizing dependence, independence, and inclusion logics.

Abstract

In a modular approach, we lift Hilbert-style proof systems for propositional, modal and first-order logic to generalized systems for their respective team-based extensions. We obtain sound and complete axiomatizations for the dependence-free fragment FO(~) of V\"a\"an\"anen's first-order team logic TL, for propositional team logic PTL, quantified propositional team logic QPTL, modal team logic MTL, and for the corresponding logics of dependence, independence, inclusion and exclusion. As a crucial step in the completeness proof, we show that the above logics admit, in a particular sense, a semantics-preserving elimination of modalities and quantifiers from formulas.