Capturing dual team properties with inclusion atoms

TL;DR

This paper develops dual propositional team-based logics using inclusion atoms to capture properties that are closed under certain team operations, providing a syntactic duality and complete deduction systems.

Contribution

It introduces dual propositional team logics with variants of inclusion atoms, establishing their expressiveness, duality, and complete natural deduction systems.

Findings

Logics are expressively complete for (quasi) downward and upward closed properties.

Variants of inclusion atoms are equivalent to might modality formulas.

Sound and complete natural deduction systems are constructed.

Abstract

We introduce propositional team-based logics expressively complete for (quasi) downward and (quasi) upward closed properties in a syntactically dual way, by using variants of the inclusion atom. In particular, the variants of the primitive inclusion atoms used in the (quasi) upward closed setting have equivalent formulas using variants of the might modality. The duality is visible in the logics' normal forms, mirroring the duality between the (quasi) upward and downward closed settings, where the quasi variants take special care of the empty and full team. Furthermore, we defined sound and complete natural deduction systems for each logic.