Guarded Hybrid Team Logics

Abstract

Team logics are extensions of first-order logic where formulae are not evaluated over assignments, but over sets ("teams") of assignments. In its most basic form, this does not increase the expressiveness of the logic because we can only form statements about the common properties of all assignments ("flatness"). Therefore, additional "team atoms" are introduced to allow for assertions about interdependencies between the assignments like dependence or inclusion. We propose to consider binders known from hybrid logic to increase the expressiveness, where the bound teams may then be referenced as regular relations. We call this hybrid team logic (HTL). Additionally, we define the positive and negative fragments of HTL (HTL^+ and HTL^-) by requiring that relations that arise from binding only occur positively or negatively, respectively.
We find that HTL and its positive and negative fragments are equivalent to prominent team logics: HTL^+ is eqivalent to inclusion logic, HTL^- is equivalent to exclusion/dependence logic and HTL itself is equivalent to independence or inclusion/exclusion logic. This classifies HTL as equivalent to existential second order logic and HTL^+ as equivalent to the positive fragment of greatest fixpoint logic.
Binders also enhance the expressiveness of guarded team logics because they enable access to information that normally is obscured by the built-in limitations of these logics. We will take a closer look at guarded hybrid team logics and establish a finite model property for the guarded fragment of HTL using model checking games. More precisely, we encode winning strategies of model checking games as relations, a process that is a natural fit for binders. Further, we notice that the hierarchy of guarded team logics is more complex than the hierarchy of non-guarded team logics, and we establish a hierarchy of prominent union-closed guarded team logics.