17314 LABEL:LastPageMay 25, 2020Jul. 30, 2021

# On the Union Closed Fragment of Existential Second-Order Logic and Logics
with Team Semantics

Matthias Hoelzel  and  Richard Wilke  Mathematical Foundations of Computer
Science, RWTH Aachen University, Aachen, Germany<EMAIL_ADDRESS>aachen.de<EMAIL_ADDRESS>
###### Abstract.

We present syntactic characterisations for the union closed fragments of
existential second-order logic and of logics with team semantics. Since union
closure is a semantical and undecidable property, the normal form we introduce
enables the handling and provides a better understanding of this fragment. We
also introduce inclusion-exclusion games that turn out to be precisely the
corresponding model-checking games. These games are not only interesting in
their own right, but they also are a key factor towards building a bridge
between the semantic and syntactic fragments. On the level of logics with team
semantics we additionally present restrictions of inclusion-exclusion logic to
capture the union closed fragment. Moreover, we define a team based atom that
when adding it to first-order logic also precisely captures the union closed
fragment of existential second-order logic which answers an open question by
Galliani and Hella.

###### Key words and phrases:

Higher order logic, Existential second-order logic, Team semantics, Closure
properties, Union closure, Model-checking games, Syntactic charactisations of
semantical fragments

The research of Matthias Hoelzel has been supported by the German Research
Foundation (DFG). Richard Wilke is a doctoral student in the Research Training
Group 2236 UnRAVeL, also funded by DFG. Both authors carried out this research
as part of their PhD studies, under the supervision of Erich Grädel.

##  1\. Introduction

One branch of model theory engages with the characterisation of semantical
fragments, which typically are undecidable, as syntactical fragments of the
logics under consideration. Prominent examples are van Benthem’s Theorem
characterising the bisimulation invariant fragment of first-order logic as the
modal-logic [vB76] or preservation theorems like the Łoś-Tarski Theorem, which
states that formulae preserved in substructures are equivalent to universal
formulae [Hod97b]. In this paper we consider formulae $\varphi(X)$ of
existential second-order logic, $\operatorname{\Sigma^{1}_{1}}$, in a free
relational variable $X$ and investigate the property of being closed under
unions, meaning that whenever a family of relations $X_{i}$ all satisfy
$\varphi$, then their union $\bigcup_{i}X_{i}$ should also do so. Certainly
closure under unions is an undecidable property. We provide a syntactical
characterisation of all formulae of existential second-order logic obeying
this property via a normal form called _myopic_
-$\operatorname{\Sigma^{1}_{1}}$, a notion based on ideas of Galliani and
Hella [GH13]. By Fagin’s Theorem, $\operatorname{\Sigma^{1}_{1}}$ is the
logical equivalent of the complexity class NP which highlights the importance
to understand its fragments. Towards this end we employ game theoretic
concepts and introduce a novel game type, called _inclusion-exclusion games_ ,
suited for formulae $\varphi(X)$ with a free relational variable. In these
games a strategy no longer is simply winning for one player — and hence
proving whether a sentence is satisfied — but it is moreover adequate for a
certain relation $Y$ over $\mathfrak{A}$ showing that the formula is satisfied
by $\mathfrak{A}$ and $Y$, in symbols $\mathfrak{A}\vDash\varphi(Y)$. We
construct myopic-$\operatorname{\Sigma^{1}_{1}}$ formulae that can define the
winning regions of specifically those inclusion-exclusion games that are
(semantically) closed under unions. Conceptually such games are eligible for
any $\operatorname{\Sigma^{1}_{1}}$-formula, but since our interest lies in
those formulae that are closed under unions, we introduce a restricted version
of such games, called _union games_ , that precisely correspond to the model-
checking games of union closed $\operatorname{\Sigma^{1}_{1}}$-formulae.
Consequently, the notion of union closure is captured on the level of formulae
by the myopic fragment of $\operatorname{\Sigma^{1}_{1}}$ and on the game
theoretic level by union games.

Existential second-order logic has a tight connection to modern logics of
dependence and independence that are based on the concept of teams, introduced
by Hodges [Hod97a], and later refined by Väänänen in 2007 [Vää07]. In contrast
to classical logics, formulae of such a logic are evaluated against a set of
assignments, called a _team_. One main characteristic of these logics is that
dependencies between variables, such as “$x$ depends solely on $y$”, are
expressed as atomic properties of teams. Widely used dependency atoms include
dependence ($\operatorname{=}(x,y)$), inclusion ($x\subseteq y$), exclusion
($x\mathbin{|}y$) and independence ($x\bot y$). It is known that both
independence logic $\operatorname{FO}(\bot)$ and inclusion-exclusion logic
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$ have the same expressive power
as full existential second-order logic $\operatorname{\Sigma^{1}_{1}}$
[Gal12]. The team in such logics corresponds to the free relational variable
in existential second-order formulae, enabling us to ask the same questions
about fragments with certain closure properties in both frameworks. One
example of a well understood closure property is _downwards closure_ stating
that if a formula is satisfied by a team then it is also satisfied by all
subteams (i.e. subsets of that team). It is well known that exclusion logic
$\operatorname{FO}({}\mathbin{|}{})$ is equivalent to dependence logic
$\operatorname{FO}(\operatorname{dep})$ [Gal12], which corresponds to the
downwards closed fragment of $\operatorname{\Sigma^{1}_{1}}$ [KV09]. The issue
of union closure is different. Galliani and Hella have shown that inclusion
logic $\operatorname{FO}(\subseteq)$ corresponds to greatest fixed-point-logic
$\text{GFP}^{+}$ and, hence, by using the Immerman-Vardi Theorem, it captures
all Ptime computable queries on ordered structures [GH13]. They also proved
that every union closed dependency notion that itself is first-order definable
(where the formula has access to a predicate for the team) is already
definable in inclusion logic. However, there are union closed properties that
are not definable in inclusion logic (think of a union closed NP property).
For a concrete example we refer to the atom $\mathcal{R}$ from [GH13]. Thus
Galliani and Hella asked the question whether there is a union closed atomic
dependency notion $\beta$, such that the logic $\operatorname{FO}(\beta)$
captures precisely the union closed fragment of
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$. In the present work we answer
this question positively with the aid of inclusion-exclusion games.
Furthermore, we present a syntactical restriction of all
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$ formulae that also precisely
describe the union closed fragment. This syntactical fragment corresponds to
myopic-$\operatorname{\Sigma^{1}_{1}}$ and is in harmony with the game
theoretical view, which is described by union games.

This paper is based on [HW19, HW20] and also contains some improvements from
[Hoe19] like the more direct translations into the myopic fragments (Theorem 6
and Theorem 15), while Theorem 9 and Theorem 21 are based on the original
proofs and are enhanced by the observation that they produce only a limited
number of in-/exclusion atoms or literals with second-order symbols.
Furthermore, we also present restricted variants of the inclusion-exclusion
games that are the model-checking games of $\operatorname{FO}(\subseteq)$ or
$\operatorname{FO}({}\mathbin{|}{})$.

Sections 3, 4 and 5 deal with second-order logic and can be read without
knowledge about team semantics. In section three the central notion of this
paper, inclusion-exclusion games, is introduced, which is used in section four
to characterise the union closed fragment within existential second-order
logic. Section five provides a restriction of the games specifically suited
for this fragment. Based on these notions, Section 6 describes the union
closed fragment of inclusion-exclusion logic in terms of syntactical
restrictions. The question of Galliani and Hella, whether there is a union
closed atom that constitutes the union closed fragment, is answered positively
in Section 7. Finally, in Section 8 we discuss restrictions of inclusion-
exclusion games suited for example for the downwards closed fragment.

##  2\. Preliminaries

We assume familiarity with first-order logic and existential second-order
logic, $\operatorname{FO}$ and $\operatorname{\Sigma^{1}_{1}}$ for short. For
a background we refer to the textbook [GKL+07].

### Graphs

Let $G=(V,E)$ be a graph, that is $V$ is a possibly empty set of vertices and
$E\subseteq V\times V$ the edge set. The neighbourhood of a vertex $v$ in $G$
is denoted by $\operatorname{N}_{G}(v)=\\{w\in V:(v,w)\in E\\}$. The
restriction of $G$ to $W\subseteq V$ is defined as
$G{\upharpoonright_{W}}\coloneqq(W,E\cap(W\times W))$. By $G-W$ we denote the
graph $G{\upharpoonright_{V\setminus W}}$. For a set $F\subseteq V\times V$
the extension of $G$ by $F$ is denoted by $G+F\coloneqq(V,E\cup F)$.

### Logic

For a given $\tau$-structure $\mathfrak{A}$ with universe $A$111We write
structures in Fraktur letters and use the corresponding Latin letters to
denote their respective universe. and formula $\varphi({\bar{x}})$ we define
$\varphi^{\mathfrak{A}}\coloneqq\\{{\bar{a}}\in
A^{|{\bar{x}}|}:\mathfrak{A}\vDash\varphi({\bar{a}})\\}$,
$\operatorname{free}(\varphi)$ is the set of free first-order variables and
$\operatorname{subf}(\psi)$ is the set of subformulae of $\psi$; sometimes for
technical reasons it is necessary to consider $\operatorname{subf}(\psi)$ as a
_multiset_ , and we will do so tacitly. Notations like ${\bar{v}},{\bar{w}}$
always indicate that ${\bar{v}}=(v_{1},\dotsc,v_{k})$ and
${\bar{w}}=(w_{1},\dotsc,w_{\ell})$ are some (finite) tuples. Here
$k=|{\bar{v}}|$ and $\ell=|{\bar{w}}|$, so ${\bar{v}}$ is a $k$-tuple while
${\bar{w}}$ is an $\ell$-tuple. We write $\\{{\bar{v}}\\}$ or
$\\{{\bar{v}},{\bar{w}}\\}$ as abbreviations for $\\{v_{1},\dotsc,v_{k}\\}$
resp. $\\{v_{1},\dotsc,v_{k},w_{1},\dotsc,w_{\ell}\\}$ while
$\\{({\bar{v}}),({\bar{w}})\\}$ is the set consisting of the two tuples
${\bar{v}}$ and ${\bar{w}}$ (as elements). The _concatenation_ of ${\bar{v}}$
and ${\bar{w}}$ is
$({\bar{v}},{\bar{w}})\coloneqq(v_{1},\dotsc,v_{k},w_{1},\dotsc,w_{\ell})$.
The power set of a set $A$ is denoted by $\mathcal{P}(A)$ and
$\mathcal{P}^{+}(A)\coloneqq\mathcal{P}(A)\setminus\\{\varnothing\\}$.

### Team Semantics

A _team_ $X$ over $\mathfrak{A}$ is a _set_ of assignments mapping a common
domain $\operatorname{dom}(X)=\\{{\bar{x}}\\}$ of variables into $A$. The
restriction of $X$ to some first-order formula $\varphi({\bar{x}})$ is
$X{\upharpoonright_{\varphi}}\coloneqq\\{s\in
X:\mathfrak{A}\vDash_{s}\varphi\\}$. For a given subtuple
${\bar{y}}=(y_{1},\dots,y_{\ell})\subseteq{\bar{x}}$ and every $s\in X$ we
define $s({\bar{y}})\coloneqq(s(y_{1}),\dotsc,s(y_{\ell}))$. Furthermore, we
frequently use $X({\bar{y}})\coloneqq\\{s({\bar{y}}):s\in X\\}$, which is an
$\ell$-ary relation over $\mathfrak{A}$. For an assignment $s$, a variable $x$
and $a\in A$ we use $s[x\mapsto a]$ to denote the assignment resulting from
$s$ by adding $x$ to its domain (if it is not already contained) and declaring
$a$ as the image of $x$.

Let $\mathfrak{A}$ be a $\tau$-structure, $X$ a team of $\mathfrak{A}$. In the
following $\lambda$ denotes a first-order $\tau$-literal and $\varphi,\psi$
arbitrary formulae in negation normal form.

  * $\bullet$

$\mathfrak{A}\vDash_{X}\lambda\mathbin{:\\!\\!\iff}\mathfrak{A}\vDash_{s}\lambda$
for all $s\in X$

  * $\bullet$

$\mathfrak{A}\vDash_{X}\varphi\land\psi\mathbin{:\\!\\!\iff}\mathfrak{A}\vDash_{X}\varphi$
and $\mathfrak{A}\vDash_{X}\psi$

  * $\bullet$

$\mathfrak{A}\vDash_{X}\varphi\lor\psi\mathbin{:\\!\\!\iff}\mathfrak{A}\vDash_{Y}\varphi$
and $\mathfrak{A}\vDash_{Z}\psi$ for some $Y,Z\subseteq X$ such that $Y\cup
Z=X$

  * $\bullet$

$\mathfrak{A}\vDash_{X}\forall
x\varphi\mathbin{:\\!\\!\iff}\mathfrak{A}\vDash_{X[x\mapsto A]}\varphi$

  * $\bullet$

$\mathfrak{A}\vDash_{X}\exists
x\varphi\mathbin{:\\!\\!\iff}\mathfrak{A}\vDash_{X[x\mapsto F]}\varphi$ for
some $F\colon X\to\mathcal{P}^{+}(A)$

Here $X[x\mapsto A]\coloneqq\\{s[x\mapsto a]:s\in X,\,a\in A\\}$ and
$X[x\mapsto F]\coloneqq\\{s[x\mapsto a]:s\in X,\,a\in F(s)\\}$.

Team semantics for a first-order formula $\varphi$ (without any dependency
concepts) boils down to evaluating $\varphi$ against every single assignment,
i.e. more formally we have
$\mathfrak{A}\vDash_{X}\varphi\iff\mathfrak{A}\vDash_{s}\varphi$ for _every_
$s\in X$ (in usual Tarski semantics). This is also known as the _flatness
property_ of $\operatorname{FO}$. The reason for considering teams instead of
single assignments is that they allow the formalisation of dependency
statements in the form of dependency atoms. Among the most frequently
considered atoms are the following.

Dependence:

$\mathfrak{A}\vDash_{X}\operatorname{=}({\bar{x}},y)\mathbin{:\\!\\!\iff}s({\bar{x}})=s^{\prime}({\bar{x}})\text{
implies }s(y)=s^{\prime}(y)\text{ for all }s,s^{\prime}\in X$

Inclusion:

$\mathfrak{A}\vDash_{X}{\bar{x}}\subseteq{\bar{y}}\mathbin{:\\!\\!\iff}X({\bar{x}})\subseteq
X({\bar{y}})$

Exclusion:

$\mathfrak{A}\vDash_{X}{\bar{x}}\mathbin{|}{\bar{y}}\mathbin{:\\!\\!\iff}X({\bar{x}})\cap
X({\bar{y}})=\varnothing$

Independence:

$\mathfrak{A}\vDash_{X}{\bar{x}}\bot{\bar{y}}\mathbin{:\\!\\!\iff}\text{for
all }s,s^{\prime}\in X\text{ exists }s^{\prime\prime}\in X\text{
s.t.~{}}s({\bar{x}})=s^{\prime\prime}({\bar{x}})$ and
$s^{\prime}({\bar{y}})=s^{\prime\prime}({\bar{y}})$

Dependence was introduced by Väänänen [Vää07], inclusion and exclusion by
Galliani [Gal12] and independence by Grädel and Väänänen [GV13]. When we speak
about first-order team logic augmented with a certain atomic dependency
notion, for example inclusion, we denote it by writing
$\operatorname{FO}(\subseteq)$ and so forth. All of these logics have the
empty team property, which means that
$\mathfrak{A}\vDash_{\varnothing}\varphi$ is always true. This is also the
reason why _sentences_ are not evaluated against $\varnothing$ but rather
against $\\{\varnothing\\}$, which is the team consisting of the empty
assignment. Let $\varphi$ be a first-order formula and $\psi$ be any formula
of a logic with team semantics. We define $\varphi\rightarrow\psi$ as
$\operatorname{nnf}(\neg\varphi)\lor(\varphi\land\psi)$ where
$\operatorname{nnf}(\neg\varphi)$ is the negation normal form of
$\neg\varphi$. It is easy to see that
$\mathfrak{A}\vDash_{X}\varphi\rightarrow\psi\iff\mathfrak{A}\vDash_{X{\upharpoonright_{\varphi}}}\psi$.

#### Union Closure

A formula $\varphi$ of a logic with team semantics is said to be _union
closed_ if whenever $\mathfrak{A}\vDash_{X_{i}}\varphi$ holds for all $i\in I$
then also $\mathfrak{A}\vDash_{X}\varphi$, where $X=\bigcup_{i\in I}X_{i}$.
Analogously, a formula $\varphi(X)$ of $\operatorname{\Sigma^{1}_{1}}$ with a
free relational variable $X$ is union closed if
$\mathfrak{A}\vDash\varphi(X_{i})$ for all $i\in I$ implies
$\mathfrak{A}\vDash\varphi(X)$.

### FO Interpretations

A first-order interpretation from $\sigma$ to $\tau$ of arity $k$ is a
sequence $\mathcal{I}=(\delta,\varepsilon,(\psi_{S})_{S\in\tau})$ of
$\operatorname{FO}(\sigma)$-formulae, called the domain, equality and relation
formulae respectively. We say that $\mathcal{I}$ interprets a $\tau$-structure
$\mathfrak{B}$ in some $\sigma$-structure $\mathfrak{A}$ and write
$\mathfrak{B}\cong\mathcal{I}(\mathfrak{A})$ if and only if there exists a
surjective function $h$, called the coordinate map, that maps
$\delta^{\mathfrak{A}}=\\{{\bar{a}}\in
A^{k}:\mathfrak{A}\vDash\delta({\bar{a}})\\}$ to $B$ preserving and reflecting
the equalities and relations provided by $\varepsilon$ and $\psi_{S}$, such
that $h$ induces an isomorphism between the quotient structure
$(\delta^{\mathfrak{A}},(\psi^{\mathfrak{A}}_{S})_{S\in\tau})/\varepsilon^{\mathfrak{A}}$
and $\mathfrak{B}$. A more detailed explanation can be found in [GKL+07]. For
a $\tau$-formula $\varphi$ we associate the $\sigma$-formula
$\varphi^{\mathcal{I}}$ by relativising quantifiers to $\delta$, using
$\varepsilon$ as equality and $\psi_{S}$ instead of $S$. We extend this
translation to $\operatorname{\Sigma^{1}_{1}}$ by the following rules for
additional free/quantified relation symbols $S$.

  * $\bullet$

$(\exists S\vartheta)^{\mathcal{I}}\coloneqq\exists
S^{\star}\big{(}\forall{\bar{x}}_{1}\dotsb{\bar{x}}_{\operatorname{ar}(S)}\big{(}S^{\star}{\bar{x}}_{1}\dotsb{\bar{x}}_{\operatorname{ar}(S)}\rightarrow\bigwedge^{\operatorname{ar}({S})}_{j=1}\delta({\bar{x}}_{j})\big{)}\land\vartheta^{\mathcal{I}}\big{)}$,

  * $\bullet$

$(Sv_{1}\dotsb
v_{\operatorname{ar}(S)})^{\mathcal{I}}\coloneqq\exists{\bar{w}}_{1}\dotsb{\bar{w}}_{\operatorname{ar}(S)}\big{(}\bigwedge^{\operatorname{ar}(S)}_{j=1}(\delta({\bar{w}}_{j})\land\varepsilon({\bar{v}}_{j},{\bar{w}}_{j}))\land
S^{\star}{\bar{w}}_{1}\dotsb{\bar{w}}_{\operatorname{ar}(S)}\big{)}$.

An assignment $s\colon\\{{\bar{x}}_{1},\dots,{\bar{x}}_{m}\\}\to A$ is well-
formed (w.r.t. $\mathcal{I}$), if
$s({\bar{x}}_{i})\in\delta^{\mathfrak{A}}(=\operatorname{dom}(h))$ for every
$i=1,\dots,m$. Such an assignment encodes $h\circ
s\colon\\{x_{1},\dots,x_{m}\\}\to B$ with $(h\circ s)(x_{i})\coloneqq
h(s({\bar{x}}_{i}))$ which is an assignment over $\mathfrak{B}$. Similarly, a
relation $Q$ is well-formed (w.r.t. $\mathcal{I}$), if
$Q\subseteq(\delta^{\mathfrak{A}})^{\ell}$ where
$\ell=\frac{\operatorname{ar}(Q)}{k}\in\mathbb{N}$, and we define
$h(Q)\coloneqq\\{(h({\bar{a}}_{1}),\dots,h({\bar{a}}_{\ell})):({\bar{a}}_{1},\dots,{\bar{a}}_{\ell})\in
Q\\}$, which is the $\ell$-ary relation over $\mathfrak{B}$ that was described
by $Q$. The connection between $\varphi^{\mathcal{I}}$ and $\varphi$ is made
precise in the well-known interpretation lemma.

######  Lemma 1 (Interpretation Lemma for $\operatorname{\Sigma^{1}_{1}}$).

Let $\varphi(S_{1},\dotsc,S_{n})\in\operatorname{\Sigma^{1}_{1}}$. Let
$R^{\star}_{i}\subseteq A^{k\cdot\operatorname{ar}(S_{i})}$ for all $i$ and
$s\colon\\{{\bar{x}}_{1},\dots,{\bar{x}}_{m}\\}\to A$ be well-formed. Then:
$(\mathfrak{A},R_{1}^{\star},\dots,R^{\star}_{n})\vDash_{s}\varphi^{\mathcal{I}}\iff(\mathfrak{B},h(R^{\star}_{1}),\dots,h(R^{\star}_{n}))\vDash_{h\circ
s}\varphi.$

##  3\. Inclusion-Exclusion Games

Classical model-checking games are designed to express satisfiability of
sentences, i.e. formulae without free variables. The instantiation of a first-
order formula with free variables by some values is dealt with by constructing
expanded structures having constants that are assigned the respective values.
Since our focus lies on second-order formulae in a free relational variable we
are in need for a game that is able to not only express that a formula is
satisfied, but moreover that it is satisfied by a certain relation. In the
games we are about to describe a set of designated positions is present —
called the _target set_ — which corresponds to the full relation $A^{k}$
(where the free relational variable has arity $k$). A winning strategy is said
to be _adequate_ for a subset $X$ of the target positions, if the target
vertices visited by it are $X$. On the level of logics this matches the
relation satisfying the corresponding formula, i.e. there is a winning
strategy adequate for $X$ if and only if the formula is satisfied by $X$.

An _inclusion-exclusion game_
$\mathcal{G}=(V,V_{0},V_{1},E,I,T,{E_{\mathsf{ex}}})$ is played by two players
0 and 1 where

  * $\bullet$

$V_{\sigma}$ is the set of vertices of player $\sigma$,

  * $\bullet$

$V=V_{0}\mathbin{\mathaccent 0{\cdot}\cup}V_{1}$,

  * $\bullet$

$E\subseteq V\times V$ is a set of possible moves,

  * $\bullet$

$I\subseteq V$ is the (possibly empty) set of initial positions,

  * $\bullet$

$T\subseteq V$ is the set of target vertices and

  * $\bullet$

${E_{\mathsf{ex}}}\subseteq V\times V$ is the exclusion condition, which
defines the winning condition for player $0$.222${E_{\mathsf{ex}}}$ can always
be replaced by the symmetric closure of ${E_{\mathsf{ex}}}$ without altering
its semantics.

The edges going into $T$, that is ${E_{\mathsf{in}}}\coloneqq E\cap(V\times
T)$, are called _inclusion edges_ , while ${E_{\mathsf{ex}}}$ is the set of
_exclusion edges_ (sometimes also called conflicting pairs).

Inclusion-exclusion games are _second-order_ games, so instead of single plays
we are more interested in sets of plays that are admitted by some winning
strategy for player $0$. Model-checking games for logics with team semantics
made their first appearance in [Grä13] and, in fact, inclusion-exclusion games
can be considered to be a variant of the second-order games introduced in the
same paper.

For a subset $X\subseteq T$ the aim of player 0 is to provide a winning
strategy (which can be viewed as a set of plays respecting the exclusion
condition and containing all possible strategies of player 1) such that the
vertices of $T$ that are visited by this strategy correspond precisely to $X$.

A _winning strategy_ (for player 0) $\mathcal{S}$ is a possibly empty subgraph
$\mathcal{S}=(W,F)$ of $G=(V,E)$ ensuring the following four consistency
conditions.

  1. (1)

For every $v\in W\cap V_{0}$ holds
$\operatorname{N}_{\mathcal{S}}(v)\neq\varnothing$.

  2. (2)

For every $v\in W\cap V_{1}$ holds
$\operatorname{N}_{\mathcal{S}}(v)=\operatorname{N}_{G}(v)$.

  3. (3)

$I\subseteq W$.

  4. (4)

$(W\times W)\cap{E_{\mathsf{ex}}}=\varnothing$.

Intuitively, the conditions (1) and (2) state that the strategy must provide
at least one move from each node of player $0$ used by the strategy but does
not make assumptions about the moves that player $1$ may make whenever the
strategy plays a node belonging to player $1$. In particular, the strategy
must not play any terminal vertices that are in $V_{0}$. Furthermore, (3)
enforces that at least the initial vertices are contained while (4) disallows
playing with conflicting pairs $(v,w)\in{E_{\mathsf{ex}}}$, i.e. $v$ and $w$
must not coexist in any winning strategy for player $0$. If $I=\varnothing$,
then $(\varnothing,\varnothing)$ is the trivial winning strategy. Another
interesting observation is that $(W,F)$ is a winning strategy for player $0$,
if and only if the subgraph of the game induced by $W$, which is $(W,(W\times
W)\cap E)$, is a winning strategy. In other words, me may freely add edges
that are present in the game graph between nodes of a winning strategy, i.e. a
winning strategy is determined by its nodes.

Since we do _not_ have a notion for a winning strategy for player $1$,
inclusion-exclusion games can be viewed as solitaire games.

Of course, the winning condition of an inclusion-exclusion game $\mathcal{G}$
is first-order definable. The formula $\varphi_{\operatorname{win}}(W)$ has
the property that $\mathcal{G}\vDash\varphi_{\operatorname{win}}(W)$ if and
only if $(W,(W\times W)\cap E)$ is a winning strategy for player 0 in
$\mathcal{G}$, where

$\displaystyle\varphi_{\operatorname{win}}(W)\;\coloneqq\;$
$\displaystyle\forall v(Wv\rightarrow[(V_{0}v\land\exists w(Evw\land
Ww))\,\lor$ $\displaystyle\phantom{\forall
v[Wv\rightarrow(]}(V_{1}v\land\forall w(Evw\rightarrow Ww))])\,\land$
$\displaystyle\forall v(Iv\rightarrow Wv)\land\forall v\forall w((Wv\land
Ww)\rightarrow\neg{E_{\mathsf{ex}}}vw).$

describes the winning conditions imposed on the subgraph induced by $W$.

We are mainly interested in the subset of target vertices that are visited by
a winning strategy $\mathcal{S}=(W,F)$. More formally, $\mathcal{S}$ induces
$\mathcal{T}(\mathcal{S})\coloneqq W\cap T$, which we also call the _target_
of $\mathcal{S}$. This definition is reminiscent to the notion
$\text{Team}(\mathcal{S},\psi)$ from [Grä13], but instead of relying on a
formula $\psi$ we are using the component $T$ of the game to define
$\mathcal{T}(\mathcal{S})$. Now we can associate with every inclusion-
exclusion game $\mathcal{G}$ the set of targets of winning strategies:
$\mathcal{T}(\mathcal{G})\coloneqq\\{\mathcal{T}(\mathcal{S}):\mathcal{S}\text{
is a winning strategy for player 0 in }\mathcal{G}\\}$.

Intuitively, as already pointed out, games of this kind will also be the
model-checking games for $\operatorname{\Sigma^{1}_{1}}$-formulae $\varphi(X)$
that have a free relational variable $X$. Given a structure $\mathfrak{A}$ and
such a formula, we are interested in the possible relations $Y$ that satisfy
the formula, in symbols $(\mathfrak{A},Y)\vDash\varphi(X)$. We will construct
the game such that $Y$ satisfies $\varphi$ if and only if there is a strategy
of player 0 winning for the set $Y\subseteq T$, thus
$\mathcal{T}(\mathcal{G})=\\{Y:(\mathfrak{A},Y)\vDash\varphi\\}$. It will be
more convenient for our purposes that the target vertices of an inclusion-
exclusion game are not required to be terminal positions. However it would be
no restriction as it is easy to transform any given game into one that agrees
on the (possible) targets, in which all target vertices are terminal.

Let us start the analysis of inclusion-exclusion games from a complexity
theoretical point of view. The satisfiability problem of propositional logic
can be reduced to deciding whether player 0 has a winning strategy in an
inclusion-exclusion game.

######  Theorem 2.

The problem of deciding whether $X\in\mathcal{T}(\mathcal{G})$ for a finite
inclusion-exclusion game $\mathcal{G}$ is NP-complete in the size of
$\mathcal{G}$.

######  Proof 3.1.

Determining whether $X\in\mathcal{T}(\mathcal{G})$ holds is clearly in NP, as
the winning strategy can be guessed and verified in polynomial time.

For the NP-hardness we present a reduction from the satisfiability problem of
propositional logic. Let $\varphi$ be formula in conjunctive normal form, i.e.
$\varphi=\bigwedge_{j\leq m}C_{j}$ where $C_{j}=\bigvee_{i}L_{i}$ is a
disjunction of literals (variables or negated variables). The game
$\mathcal{G}_{\varphi}$ is constructed as follows. For every variable $x$ we
add two vertices (of player 1) $x$ and $\neg x$ connected by an exclusion
edge. Moreover, for every clause $C_{j}$ we add a vertex, belonging to player
0, which has an outgoing edge into each literal $L_{i}$ occurring in it. There
are no initial vertices, i.e. $I\coloneqq\varnothing$ and the target set $T$
is the set of all clauses $C_{j}$ of $\varphi$. Now,
$S\in\mathcal{T}(\mathcal{G})$ if and only if $\bigwedge_{C_{j}\in S}C_{j}$ is
satisfiable. In particular, $T\in\mathcal{T}(\mathcal{G}_{\varphi})$ if and
only if $\varphi$ is satisfiable.

The complexity is, of course, ascribed to the exclusion edges.

The problem of deciding whether $X\in\mathcal{T}(\mathcal{G})$ for a finite
inclusion-exclusion game $\mathcal{G}$ without exclusion edges, i.e.
${E_{\mathsf{ex}}}=\varnothing$ is in Ptime and in fact complete for this
class.

######  Proof 3.2.

We describe the reduction from, and to, the well known Ptime complete problem
$\mathsf{Game}$. The input is a game graph $G=(V,V_{0},V_{1},E)$ and a vertex
$v$ and the task is to determine whether player 0 has a winning strategy
starting from $v$. Here again a player loses if he cannot make a move.

It is easy to see that inclusion-exclusion games are an extension of this
problem. For the converse direction add a fresh vertex $v$ of player 1 to the
game that has outgoing edges to all $i\in I$ and $t\in X$. Further, turn all
$t\in T\setminus X$ into player 0 vertices and remove all their outgoing
edges. Now player 0 wins the $\mathsf{Game}$ problem on this graph if, and
only if, $X\in\mathcal{T}(\mathcal{G})$.

###  3.1. Model-Checking Games for Existential Second-Order Logic

In this section we define model-checking games for formulae
$\varphi(X)\in\Sigma^{1}_{1}$ with a free relational variable. These games are
inclusion-exclusion games $\mathcal{G}$ whose target sets
$\mathcal{T}(\mathcal{G})$ are precisely the sets of relations $X$ that
satisfy $\varphi(X)$ under a fixed structure $\mathfrak{A}$.

Let $\mathfrak{A}$ be a $\tau$-structure and
$\varphi(X)=\exists{\bar{R}}\varphi^{\prime}(X,{\bar{R}})\in\operatorname{\Sigma^{1}_{1}}$
(in negation-normal form) where
$\varphi^{\prime}(X,{\bar{R}})\in\operatorname{FO}(\tau\cup\\{X,{\bar{R}}\\})$
using a free relation symbol $X$ of arity $r\coloneqq\operatorname{ar}(X)$.
The game
$\mathcal{G}_{X}(\mathfrak{A},\varphi)\coloneqq(V,V_{0},V_{1},E,I,T,{E_{\mathsf{ex}}})$
consists of the following components:

  * $\bullet$

$V\coloneqq\\{(\vartheta,s):\vartheta\in\operatorname{subf}(\varphi^{\prime}),s\colon\operatorname{free}(\vartheta)\rightarrow
A\\}\cup A^{r}$

  * $\bullet$

$I\coloneqq\\{(\varphi^{\prime},\varnothing)\\}$,

  * $\bullet$

$T\coloneqq A^{r}$,

  * $\bullet$

$\begin{aligned} V_{1}\,\coloneqq\,&\\{(\vartheta,s):\vartheta=\forall
y\gamma\text{ or
}\vartheta=\gamma_{1}\land\gamma_{2}\\}\cup\\{(\gamma,s):\gamma\text{ is a
$\tau$-literal and }\mathfrak{A}\vDash_{s}\gamma\\}\,\cup\\\
&\\{(\gamma,s):\gamma=\neg X{\bar{x}}\text{ or }\gamma\text{ is a
$\\{{\bar{R}}\\}$-literal}\\}\cup T\end{aligned}$,

  * $\bullet$

$V_{0}\coloneqq V\setminus V_{1}$,

  * $\bullet$

$\begin{aligned}
E\,\coloneqq\,&\\{((\gamma\circ\vartheta,s),(\delta,s{\upharpoonright_{\operatorname{free}(\delta)}})):\circ\in\\{\land,\lor\\},\delta\in\\{\gamma,\vartheta\\}\\}\,\cup\\\
&\\{((X{\bar{x}},s),s({\bar{x}})):X{\bar{x}}\in\operatorname{subf}(\varphi^{\prime})\\}\,\cup\\\
&\\{((Qx\gamma,s),(\gamma,s^{\prime})):Q\in\\{\exists,\forall\\},s^{\prime}=s[x\mapsto
a],a\in A\\},\end{aligned}$

  * $\bullet$

${E_{\mathsf{ex}}}\coloneqq\\{((R_{i}{\bar{x}},s),(\neg
R_{i}{\bar{y}},s^{\prime})):s({\bar{x}})=s^{\prime}({\bar{y}})\\}\cup\\{((\neg
X{\bar{x}},s),{\bar{a}}):s({\bar{x}})={\bar{a}}\\}$.

These games capture the behaviour of existential second-order formulae which
provides us with the following theorem.

######  Theorem 3.

$(\mathfrak{A},X)\vDash\varphi(X)\iff$ Player 0 has a winning strategy
$\mathcal{S}$ in $\mathcal{G}_{X}(\mathfrak{A},\varphi)$ with
$\mathcal{T}(\mathcal{S})=X$. Or, in other words:
$\mathcal{T}(\mathcal{G}_{X}(\mathfrak{A},\varphi))=\\{Y\subseteq
A^{r}:(\mathfrak{A},Y)\vDash\varphi(X)\\}$.

######  Proof 3.3.

First let
$(\mathfrak{A},Y)\vDash\varphi=\exists{\bar{R}}\varphi^{\prime}(X,{\bar{R}})$.
Then there exist relations ${\bar{P}}$ such that
$(\mathfrak{A},Y,{\bar{P}})\vDash\varphi^{\prime}(X,{\bar{R}})$. So player $0$
wins the (first-order) model-checking game
$\mathcal{G}^{\prime}\coloneqq\mathcal{G}((\mathfrak{A},Y,{\bar{P}}),\varphi^{\prime}(X,{\bar{R}}))$.
Let $\mathcal{S}^{\prime}=(W^{\prime},F^{\prime})$ be a winning strategy for
player 0 in $\mathcal{G}^{\prime}$ and $\mathcal{S}\coloneqq(W,F)$ where
$W\coloneqq W^{\prime}\cup Y$ and $F\coloneqq
F^{\prime}\cup\\{((X{\bar{x}},s),{\bar{a}})\in V\times V:{\bar{a}}\in Y\text{
and }s({\bar{x}})={\bar{a}}\\}$. Clearly we have that $\mathcal{T}(S)=W\cap
T=Y$. To conclude this direction of the proof, we still need to prove that
$\mathcal{S}$ is indeed a winning strategy in
$\mathcal{G}\coloneqq\mathcal{G}_{X}(\mathfrak{A},\varphi)$. The required
properties for player $0$ and $1$, that is (1) and (2) of Definition 3, are
inherited from $\mathcal{S}^{\prime}$ for every node of the form
$(\vartheta,s)\in V\setminus T$ with $\vartheta\neq X{\bar{x}}$. For nodes of
the form $v=(X{\bar{x}},s)\in W$ we have that $v\in V_{0}$ and, because of
$v\in W^{\prime}$ and the fact that $\mathcal{S}^{\prime}$ is a winning
strategy in $\mathcal{G}^{\prime}$, $s({\bar{x}})\in Y$ must follow. As
result, we have $s({\bar{x}})\in\operatorname{N}_{\mathcal{S}}(v)$. Since
$T\subseteq V_{1}$ and are terminal positions, condition (2) is trivially
satisfied for all $v\in W\cap T$.

Property (3) is clearly satisfied, because $(\varphi^{\prime},\varnothing)$ is
the initial position of $\mathcal{G}^{\prime}$ and, hence,
$(\varphi^{\prime},\varnothing)\in W^{\prime}\subseteq W$. In order to prove
that the last remaining condition, the exclusion condition (4), is satisfied,
consider any $(v,w)\in{E_{\mathsf{ex}}}$. Then there are two possible cases:

Case $(v,w)=((R_{i}{\bar{x}},s),(\neg R_{i}{\bar{y}},s^{\prime}))$ with
$s({\bar{x}})=s^{\prime}({\bar{y}})$: Then either $v$ or $w$ is a losing
position for player $0$ in $\mathcal{G}^{\prime}$. As a result, $W^{\prime}$
does not contain both $v$ and $w$ and, thus, neither does $W$.

Case $(v,w)=((\neg X{\bar{x}},s),{\bar{a}})$ and $s({\bar{x}})={\bar{a}}$: If
$v\in W$, then $v=(\neg X{\bar{x}},s)\in W^{\prime}$ and, since
$\mathcal{S}^{\prime}$ is a winning strategy for player $0$ in
$\mathcal{G}^{\prime}$, it must be the case that $s({\bar{x}})\notin Y$ which
implies that ${\bar{a}}=s({\bar{x}})\notin W$. So, $v\in W$ and $w\in W$
exclude each other.

For the converse direction, let $\mathcal{S}=(W,F)$ now be a winning strategy
for player $0$ in $\mathcal{G}$ with $\mathcal{T}(\mathcal{S})=Y$. We have to
show that
$(\mathfrak{A},Y)\vDash\exists{\bar{R}}\varphi^{\prime}(X,{\bar{R}})$. Let
$P_{i}\coloneqq\\{s({\bar{x}}):(R_{i}{\bar{x}},s)\in W\\}$. Furthermore, we
define $\mathcal{S}^{\prime}\coloneqq\mathcal{S}-A^{\operatorname{ar}(X)}$,
that is the restriction of the strategy $\mathcal{S}$ to
$V(\mathcal{G}^{\prime})=V\setminus A^{\operatorname{ar}(X)}$.

We prove that $\mathcal{S}^{\prime}$ is a winning strategy for player $0$ in
the first-order model-checking game
$\mathcal{G}^{\prime}\coloneqq\mathcal{G}((\mathfrak{A},Y,{\bar{P}}),\varphi^{\prime}(X,{\bar{R}}))$.
First of all, the conditions for player $0$ and $1$ for non-terminal positions
are inherited from $\mathcal{S}$. For the same reason we also have
$(\varphi^{\prime},\varnothing)\in V(\mathcal{S}^{\prime})$. We still need to
prove that $\mathcal{S}^{\prime}$ contains only terminal positions that are
winning for player $0$. This is inherited for all terminal positions that are
not using any $R_{i}$ nor $X$. We will now investigate the other terminal
positions, i.e. positions of the form $((\neg)R_{i}{\bar{x}},s)$ or
$((\neg)X{\bar{x}},s)$. Clearly, if $\mathcal{S}^{\prime}$ plays
$(R_{i}{\bar{x}},s)$, then $(R_{i}{\bar{x}},s)\in W$ and $s({\bar{x}})\in
P_{i}$ (by definition of $P_{i}$) implying that
$(\mathfrak{A},Y,{\bar{P}})\vDash_{s}R_{i}{\bar{x}}$ and, hence,
$(R_{i}{\bar{x}},s)$ is a winning position for player $0$ in
$\mathcal{G}^{\prime}$. In the case that $\mathcal{S}^{\prime}$ visits $(\neg
R_{i}{\bar{x}},s)$, we know that $(\neg R_{i}{\bar{x}},s)\in W$ and, because
$\mathcal{S}$ respects the exclusion condition, a position of the form
$(R_{i}{\bar{y}},s^{\prime})$ with $s^{\prime}({\bar{y}})=s({\bar{x}})$ cannot
be in $W$. So, in this case, we have that $s({\bar{x}})\notin P_{i}$ and,
hence, $(\neg R_{i}{\bar{x}},s)$ is again a winning position for player $0$.
If $\mathcal{S}^{\prime}$ contains $v\coloneqq(X{\bar{x}},s)$, then the edge
$(v,s({\bar{x}}))$ is played by $\mathcal{S}$ and, consequently,
$s({\bar{x}})\in W\cap T=\mathcal{T}(\mathcal{S})=Y$ which shows that $v$ is a
winning position for player $0$ in $\mathcal{G}^{\prime}$. If, however, $(\neg
X{\bar{x}},s)$ is played by $\mathcal{S}^{\prime}$, then $(\neg
X{\bar{x}},s)\in W$ and, due to exclusion condition, $s({\bar{x}})\notin W$
which proves that $s({\bar{x}})\notin W\cap T=Y$ and, again, $(\neg
X{\bar{x}},s)$ is a winning for player $0$ in $\mathcal{G}^{\prime}$. As a
result, we have that $(\mathfrak{A},Y)\vDash\varphi$.

##  4\. Characterising the Union Closed Formulae within Existential Second-
Order Logic

In this section we investigate formulae $\varphi(X)$ of existential second-
order logic that are closed under unions with respect to their free relational
variable $X$. Union closure, being a semantical property of formulae, is
undecidable. However, we present a _syntactical_ characterisation of all such
formulae via the following normal form.

A formula $\varphi(X)\in\operatorname{\Sigma^{1}_{1}}$ is called _myopic_ if
it has the shape
$\varphi(X)=\forall{\bar{x}}(X{\bar{x}}\rightarrow\exists{\bar{R}}\varphi^{\prime}(X,{\bar{R}}))$,
where $\varphi^{\prime}\in\operatorname{FO}$ and $X$ occurs only
positively333That is under an even number of negations. in $\varphi^{\prime}$.

Variants of myopic formulae have already been considered for first-order logic
[GH13, Definition 19] and for greatest fixed-point logics [Grä16, Theorem 24
and Theorem 26], but to our knowledge myopic
$\operatorname{\Sigma^{1}_{1}}$-formulae have not been studied so far.

Let $\mathcal{U}$ denote the set of all union closed
$\operatorname{\Sigma^{1}_{1}}$-formulae. To establish the claim that myopic
formulae are a normal form of $\mathcal{U}$ we need to show that all myopic
formulae are indeed closed under unions and, more importantly, that every
union closed formula can be translated into an equivalent myopic formula. This
translation is in particular constructive.

In order to strengthen the intuition on myopic formulae we start with a basic
property.

######  Proposition 4.

Every myopic formula is union closed.

######  Proof 4.1.

Let
$\varphi=\forall{\bar{x}}(X{\bar{x}}\rightarrow\exists{\bar{R}}\varphi^{\prime}(X,{\bar{R}}))$
and $(\mathfrak{A},X_{i})\vDash\varphi$ for all $i\in I$. We claim that
$(\mathfrak{A},X)\vDash\varphi$ for $X=\bigcup_{i\in I}X_{i}$. Let
${\bar{a}}\in X_{i}\subseteq X$. By assumption
$(\mathfrak{A},X_{i})\vDash_{{\bar{x}}\mapsto{\bar{a}}}\exists{\bar{R}}\varphi^{\prime}(X,{\bar{R}})$.
A fortiori ($X$ occurs only positively in $\varphi^{\prime}$), we obtain
$(\mathfrak{A},X)\vDash_{{\bar{x}}\mapsto{\bar{a}}}\exists{\bar{R}}\varphi^{\prime}(X,{\bar{R}})$.
Since ${\bar{a}}$ was chosen arbitrarily, this property holds for all
${\bar{a}}\in X$, hence the claim follows.

Of course, the reverse direction is the difficult and interesting part. The
main theorem of this section combines both parts.

######  Theorem 5.

$\varphi(X)\in\operatorname{\Sigma^{1}_{1}}$ is union closed if and only if
$\varphi(X)$ is equivalent to some myopic
$\operatorname{\Sigma^{1}_{1}}$-formula.

We provide two proofs of the remaining direction, a direct one which is short
and easy to understand, while it does not utilise the methods developed in
Section 3, which the second proof does. This leads to a more difficult
construction but provides more insight into the resulting formula.

The first variant shows that for every $\operatorname{\Sigma^{1}_{1}}$-formula
we can construct a myopic “companion” formula that basically is the union
closed version of the original one.

######  Theorem 6.

For every $\varphi(X)\in\operatorname{\Sigma^{1}_{1}}$ there is myopic formula
$\mu(X)\in\operatorname{\Sigma^{1}_{1}}$ such that for every suitable
structure $\mathfrak{A}$ and relation $X$ over $\mathfrak{A}$ holds

$(\mathfrak{A},X)\vDash\mu(X)\Longleftrightarrow X\text{ can be written as
}X=\bigcup_{i\in I}X_{i}\text{ where }\mathfrak{A}\vDash\varphi(X_{i})\text{
for every }i\in I.$

######  Proof 4.2.

Let $\mu(X)\coloneqq\forall{\bar{x}}(X{\bar{x}}\rightarrow\exists Y(Y\subseteq
X\land Y{\bar{x}}\land\varphi(Y)))$ where $Y\subseteq X$ is a shorthand for
the formula $\forall{\bar{y}}(Y{\bar{y}}\rightarrow X{\bar{y}})$. Now,
$\mu(X)$ is a myopic formula, since $X$ occurs only positively after the
implication. We still need to prove the two directions of the claim.

“$\Longrightarrow$”: First assume that $(\mathfrak{A},X)\vDash\mu(X)$. Then,
for every ${\bar{a}}\in X$, there exists some $Y_{\bar{a}}\subseteq X$ with
$(\mathfrak{A},Y\mapsto Y_{\bar{a}})\vDash Y{\bar{a}}\land\varphi(Y)$. Thus,
we have $\mathfrak{A}\vDash\varphi(Y_{\bar{a}})$ and ${\bar{a}}\in
Y_{\bar{a}}\subseteq X$ for every ${\bar{a}}\in X$. The last property entails
that $X=\bigcup_{{\bar{a}}\in X}Y_{\bar{a}}$.

“$\Longleftarrow$”: Now let $X=\bigcup_{i\in I}X_{i}$ where
$\mathfrak{A}\vDash\varphi(X_{i})$ for every $i\in I$. For every ${\bar{a}}\in
X$, choose some index $i_{\bar{a}}\in I$ with ${\bar{a}}\in X_{i_{\bar{a}}}$.
Then we have $(\mathfrak{A},X,Y\mapsto X_{i_{\bar{a}}})\vDash Y\subseteq
X\land Y{\bar{a}}\land\varphi(Y)$ and, thus, $(\mathfrak{A},X)\vDash\mu(X)$.

######  Corollary 7.

For every union closed formula $\varphi(X)\in\operatorname{\Sigma^{1}_{1}}$
there is an equivalent myopic formula
$\mu(X)\in\operatorname{\Sigma^{1}_{1}}$.

Theorem 5 now follows from Proposition 4 and Theorem 6. Towards greater
insight into the myopic fragment we will now turn towards an alternative proof
that every union closed formula is equivalent to a myopic one which utilises
game theoretical methods. For a fixed formula $\varphi(X)$ the corresponding
inclusion-exclusion game $\mathcal{G}_{X}$ can be constructed by a first-order
interpretation depending of course on the current structure.

######  Lemma 8.

Let
$\varphi(X)=\exists{\bar{R}}\varphi^{\prime}(X,{\bar{R}})\in\Sigma^{1}_{1}$
where $\varphi^{\prime}\in\operatorname{FO}(\tau\cup\\{X,{\bar{R}}\\})$ and
$r\coloneqq\operatorname{ar}(X)$. Then there exists a quantifier-free
interpretation $\mathcal{I}$ such that
$\mathcal{G}_{X}(\mathfrak{A},\varphi)\cong\mathcal{I}(\mathfrak{A})$ for
every structure $\mathfrak{A}$ (with at least two elements).

######  Proof 4.3.

The construction we use in this proof is similar to the one from [Grä16,
Proposition 18]. An equality type $e({\bar{v}})$ over a tuple
${\bar{v}}=(v_{1},\dotsc,v_{n})$ is a maximal consistent set of (in)equalities
using only variables from ${\bar{v}}$. Since equality types over finitely many
variables are finite, we can, by slight abuse of notation, identify
$e({\bar{v}})$ with the formula $\bigwedge e({\bar{v}})$. Let $n$ be chosen
sufficiently large so that we can fix for every
$\vartheta\in\operatorname{subf}(\varphi^{\prime})\cup\\{T\\}$ a unique
equality type $e_{\vartheta}({\bar{v}})$.

Let ${\bar{x}}=(x_{1},\dotsc,x_{m})$ be a tuple of variables such that for
every subformula $\vartheta\in\operatorname{subf}(\varphi^{\prime})$ holds
$\operatorname{free}(\vartheta)\subseteq\\{{\bar{x}}\\}$. For each variable
$x_{i}\in\\{{\bar{x}}\\}$ let $\iota(x_{i})\coloneqq i$. A position
$(\vartheta,s)$ of the game $\mathcal{G}_{X}(\mathfrak{A},\varphi)$ will be
encoded by an $(n+m)$-tuple of the form $({\bar{u}},{\bar{a}})$ where
${\bar{u}}$ has equality type $e_{\vartheta}$ and $s(x_{i})=a_{i}$ for every
$x_{i}\in\operatorname{free}(\vartheta)$, while a position of the form
${\bar{a}}\in T(=A^{r})$ will be encoded by $({\bar{u}},{\bar{a}}{\bar{b}})$
such that ${\bar{u}}$ has equality type $e_{T}$ whereas ${\bar{b}}\in A^{m-r}$
can be an arbitrary tuple. Now we are in the position to define the
interpretation
$\mathcal{I}=(\delta,\varepsilon,\psi_{V_{0}},\psi_{V_{1}},\psi_{E},\psi_{I},\psi_{T},\psi_{{E_{\mathsf{ex}}}})$:

  * $\bullet$

$\begin{aligned}
\delta({\bar{v}},{\bar{y}})\coloneqq\bigvee_{\vartheta\in\operatorname{subf}(\varphi^{\prime})\cup\\{T\\}}e_{\vartheta}({\bar{v}})\end{aligned}$

  * $\bullet$

$\begin{aligned}
\varepsilon({\bar{v}},{\bar{y}},{\bar{w}},{\bar{z}})\coloneqq\\!\\!\bigvee_{\vartheta\in\operatorname{subf}(\varphi^{\prime})}(e_{\vartheta}({\bar{v}})\land
e_{\vartheta}({\bar{w}})\land\bigwedge_{x_{i}\in\operatorname{free}(\vartheta)}y_{i}=z_{i})\lor(e_{T}({\bar{v}})\land
e_{T}({\bar{w}})\land\bigwedge^{r}_{i=1}y_{i}=z_{i})\end{aligned}$

  * $\bullet$

$\psi_{V_{1}}({\bar{v}},{\bar{y}})\coloneqq\bigvee_{(\vartheta,s)\in
V_{1}(\mathcal{G}_{X}(\mathfrak{A},\varphi))}e_{\vartheta}({\bar{v}})\lor
e_{T}({\bar{v}})$ and
$\psi_{V_{0}}({\bar{v}},{\bar{y}})\coloneqq\delta({\bar{v}},{\bar{y}})\wedge\neg\psi_{V_{1}}({\bar{v}},{\bar{y}})$.

  * $\bullet$

Let
$R\coloneqq\\{(\vartheta,\vartheta^{\prime}):((\vartheta,s),(\vartheta^{\prime},s^{\prime}))\in
E(\mathcal{G}_{X}(\mathfrak{A},\varphi))\\}$. Then we define

$\displaystyle\psi_{E}({\bar{v}},{\bar{y}},{\bar{w}},{\bar{z}})\coloneqq$
$\displaystyle\bigvee_{(\vartheta,\vartheta^{\prime})\in
R}(e_{\vartheta}({\bar{v}})\land
e_{\vartheta^{\prime}}({\bar{w}})\land\bigwedge_{x_{i}\in\operatorname{free}(\vartheta)\cap\operatorname{free}(\vartheta^{\prime})}y_{i}=z_{i})$
$\displaystyle\lor\bigvee_{X{\bar{u}}\in\operatorname{subf}(\varphi^{\prime})}(e_{X{\bar{u}}}({\bar{v}})\land
e_{T}({\bar{w}})\land\bigwedge^{r}_{i=1}y_{\iota(u_{i})}=z_{i}).$

  * $\bullet$

Let $S\coloneqq\\{(R_{i}{\bar{u}},\neg
R_{i}{\bar{u}}^{\prime}):((R_{i}{\bar{u}},s),(\neg
R_{i}{\bar{u}}^{\prime},s^{\prime}))\in{E_{\mathsf{ex}}}(\mathcal{G}_{X}(\mathfrak{A},\varphi))\\}$444Since
the direction of exclusion edges does not matter we assume here that they are
all of this form.. Then we define

$\displaystyle\psi_{{E_{\mathsf{ex}}}}({\bar{v}},{\bar{y}},{\bar{w}},{\bar{z}})\coloneqq$
$\displaystyle\bigvee_{(R_{i}{\bar{u}},\neg R_{i}{\bar{u}}^{\prime})\in
S}(e_{R_{i}{\bar{u}}}({\bar{v}})\land e_{\neg
R_{i}{\bar{u}}^{\prime}}({\bar{w}})\land\bigwedge^{\operatorname{ar}(R_{i})}_{i=1}y_{\iota(u_{i})}=z_{\iota(u^{\prime}_{i})})$
$\displaystyle\lor\bigvee_{\neg
X{\bar{u}}\in\operatorname{subf}(\varphi^{\prime})}(e_{\neg
X{\bar{u}}}({\bar{v}})\land
e_{T}({\bar{w}})\land\bigwedge^{r}_{i=1}y_{\iota(u_{i})}=z_{i}).$

  * $\bullet$

$\psi_{I}({\bar{v}},{\bar{y}})\coloneqq e_{\varphi^{\prime}}({\bar{v}})$

  * $\bullet$

$\psi_{T}({\bar{v}},{\bar{y}})\coloneqq e_{T}({\bar{v}})$.

Now, for every $\mathfrak{A}$ (with at least two elements) we have that
$\mathcal{I}(\mathfrak{A})\cong\mathcal{G}_{X}(\mathfrak{A},\varphi)$.

Remember that the construction used in the proof of Theorem 6 in a way
“imports” the original formula $\varphi$ into $\mu$. Therefore, the number of
atoms using $X$ or some quantified second-order symbol in $\mu(X)$ is not
bounded. Using inclusion-exclusion games, we can construct $\mu(X)$ in a
different way that limits the usage of these symbols.

######  Theorem 9.

For every union closed formula $\varphi(X)\in\operatorname{\Sigma^{1}_{1}}$
there is an equivalent myopic formula $\mu(X)\in\operatorname{\Sigma^{1}_{1}}$
where only $11$ literals use the symbol $X$ or some quantified second-order
symbol.

######  Proof 4.4.

Let
$\varphi(X)=\exists{\bar{R}}\varphi^{\prime}(X,{\bar{R}})\in\operatorname{\Sigma^{1}_{1}}(\tau)$
be closed under unions, $\mathfrak{A}$ be a $\tau$-structure and
$\mathcal{G}\coloneqq\mathcal{G}_{X}(\mathfrak{A},\varphi)$ be the
corresponding game. W.l.o.g. $\mathfrak{A}$ has at least two elements. By
Theorem 3, we have that $\mathcal{T}(\mathcal{G})=\\{Y\subseteq
A^{r}:\mathfrak{A}\vDash\varphi(Y)\\}$ where $r\coloneqq\operatorname{ar}(X)$.
Since $\varphi(X)$ is union closed, it follows that $\mathcal{T}(\mathcal{G})$
is closed under unions as well. Now we observe that $\mathcal{T}(\mathcal{G})$
can be defined in the game $\mathcal{G}$ by the following myopic formula:

$\displaystyle\varphi_{\mathcal{T}}(X)\coloneqq$ $\displaystyle\forall
x(Xx\rightarrow\psi_{\mathcal{T}}(X,x))\text{ where}$
$\displaystyle\psi_{\mathcal{T}}(X,x)\coloneqq$ $\displaystyle\exists
W(\varphi_{\operatorname{win}}(W)\land Wx\land\forall y(Wy\land Ty\rightarrow
Xy))$

Here $\varphi_{\operatorname{win}}$ is the first-order formula verifying
winning strategies. Please note that $\varphi_{\mathcal{T}}$ is indeed a
myopic formula, since $X$ occurs only positively in $\psi_{\mathcal{T}}$.
Furthermore, there are $6$ $W$-atoms in $\varphi_{\operatorname{win}}$ and two
additional $W$-atoms in $\psi_{\mathcal{T}}$, while $X$ occurs twice in
$\varphi_{\mathcal{T}}$. In total, $X$ and $W$ are used exactly $10$ times.
These $10$ atoms will also occur in the final formula $\mu$ that we are going
to construct. This construction will use a $\operatorname{FO}$-interpretation,
which will introduce an additional $W^{\star}$-atom in order to simulate the
quantifier $\exists W$ by a new quantifier $\exists W^{\star}$. This is why,
we will end up with exactly $11$ $\\{X,W^{\star}\\}$-literals in $\mu$.

For every $X\subseteq A^{r}$,
$(\mathcal{G},X)\vDash\varphi_{\mathcal{T}}(X)\iff
X\in\mathcal{T}(\mathcal{G})$.

######  Proof 4.5.

Assume that $(\mathcal{G},X)\vDash\varphi_{\mathcal{T}}(X)$. By construction
of $\varphi_{\mathcal{T}}$, for every ${\bar{a}}\in X$ there exists a winning
strategy $\mathcal{S}_{\bar{a}}=(W_{\bar{a}},F_{\bar{a}})$ with ${\bar{a}}\in
W_{\bar{a}}$ and $\mathcal{T}(\mathcal{S}_{{\bar{a}}})=W_{\bar{a}}\cap
T\subseteq X$. It follows that $X=\bigcup_{{\bar{a}}\in
X}\mathcal{T}(\mathcal{S}_{{\bar{a}}})$. Since $\mathcal{T}(\mathcal{G})$ is
closed under unions, we also obtain that $X\in\mathcal{T}(\mathcal{G})$.

We want to remark that at this point the semantical property is translated
into a syntactical one, as the formula only describes the correct winning
strategy because the initial formula was closed under unions.

To conclude the proof of Claim 4.4, assume that
$X\in\mathcal{T}(\mathcal{G})$. Then there exists a winning strategy
$\mathcal{S}=(W,F)$ for player $0$ with $\mathcal{T}(\mathcal{S})=X$. Thus,
for the quantifier $\exists W$ we can (for all ${\bar{a}}\in X$) choose
$\mathcal{S}$, which, obviously, satisfies the formula.

Recall the first-order interpretation $\mathcal{I}$ (of arity $n+m$) from
Lemma 8 with $\mathcal{I}(\mathfrak{A})\cong\mathcal{G}$ for some coordinate
map $h\colon\delta^{\mathfrak{A}}\rightarrow V(\mathcal{G})$ and for every
${\bar{a}}\in T(\mathcal{G})$,
$h^{-1}({\bar{a}})=\\{({\bar{u}},{\bar{a}},{\bar{b}})\in
A^{n+m}:\mathfrak{A}\vDash e_{T}({\bar{u}}),{\bar{b}}\in A^{m-r}\\}$ where
$e_{T}(x_{1},\dots,x_{n})$ is some quantifier-free first-order formula. By the
interpretation lemma for $\operatorname{\Sigma^{1}_{1}}$ (Lemma 1), for every
$X\subseteq T(\mathcal{G})$,

$(\mathfrak{A},X^{\star})\vDash\varphi_{\mathcal{T}}^{\mathcal{I}}(X^{\star})\Longleftrightarrow(\mathcal{G},X)\vDash\varphi_{\mathcal{T}}(X)$
(1)

where $X^{\star}\coloneqq h^{-1}(X)$ is a relation of arity $(n+m)$. Recall
that every variable $x$ occurring in $\varphi_{\mathcal{T}}$ is replaced by a
tuple ${\bar{x}}$ of length $(n+m)$. Let
${\bar{x}}=({\bar{u}},{\bar{v}},{\bar{w}})$ where $|{\bar{u}}|=n$,
$|{\bar{v}}|=r$ and $|{\bar{w}}|=m-r$ and let

$\mu(X)\coloneqq\forall{\bar{v}}(X{\bar{v}}\rightarrow\forall{\bar{u}}\forall{\bar{w}}(e_{T}({\bar{u}})\rightarrow\psi^{\star}(X,{\bar{u}},{\bar{v}},{\bar{w}})))$

where $\psi^{\star}$ is the formula that results from
$\psi_{\mathcal{T}}^{\mathcal{I}}$ by replacing every occurrence of
$X^{\star}{\bar{u}}^{\prime}{\bar{v}}^{\prime}{\bar{w}}^{\prime}$ (where
$|{\bar{u}}^{\prime}|=n$, $|{\bar{v}}^{\prime}|=r$ and
$|{\bar{w}}^{\prime}|=m-r$) by the formula $e_{T}({\bar{u}}^{\prime})\land
X{\bar{v}}^{\prime}$. By construction, this is a myopic formula, because $X$
occurred only positively in $\psi^{\mathcal{I}}$ and, hence, $X^{\star}$
(resp. $X$) occurs only positively in $\psi^{\mathcal{I}}_{\mathcal{T}}$
(resp. $\psi^{\star}$).

Recall that, in the game $\mathcal{G}\cong\mathcal{I}(\mathfrak{A})$, every
$X\subseteq T(\mathcal{G})$ is a unary relation over $\mathcal{G}$, while the
elements of $T(\mathcal{G})$ themselves are $r$-tuples of $A$. Furthermore, we
have that $h^{-1}(X)\coloneqq\\{({\bar{a}},{\bar{b}},{\bar{c}})\in A^{n}\times
A^{r}\times A^{m-r}:\mathfrak{A}\vDash e_{T}({\bar{a}})\text{ and
}{\bar{b}}\in X\\}$. Because of this and $X^{\star}=h^{-1}(X)$, it follows
that for every
$s\colon\\{{\bar{u}}^{\prime},{\bar{v}}^{\prime},{\bar{w}}^{\prime}\\}\to A$
holds

$(\mathfrak{A},X^{\star})\vDash_{s}X^{\star}{\bar{u}}^{\prime}{\bar{v}}^{\prime}{\bar{w}}^{\prime}\iff\mathfrak{A}\vDash
e_{T}(s({\bar{u}}^{\prime}))\text{ and }s({\bar{v}}^{\prime})\in
X\iff(\mathfrak{A},X)\vDash_{s}e_{T}({\bar{u}}^{\prime})\land
X{\bar{v}}^{\prime}.$ (2)

By construction of $\psi^{\star}$, these are the only subformulae in which
$\psi^{\mathcal{I}}_{\mathcal{T}}$ and $\psi^{\star}$ differ from each other.
As a result, the following claim is true:

For every $X\subseteq A^{r}$ and every assignment
$s\colon\operatorname{free}(\psi^{\mathcal{I}}_{\mathcal{T}})\rightarrow A$,
holds

$(\mathfrak{A},X^{\star})\vDash_{s}\psi^{\mathcal{I}}_{\mathcal{T}}(X^{\star},{\bar{x}})\iff(\mathfrak{A},X)\vDash_{s}\psi^{\star}(X,{\bar{x}}).$

Recall that ${\bar{x}}=({\bar{u}},{\bar{v}},{\bar{w}})$ where
$|{\bar{u}}|=n,|{\bar{v}}|=r$ and $|{\bar{w}}|=(m-r)$. Now we can see that

$\displaystyle(\mathfrak{A},X^{\star})\vDash\varphi_{\mathcal{T}}^{\mathcal{I}}=\forall{\bar{x}}(X^{\star}{\bar{x}}\rightarrow\psi^{\mathcal{I}}_{\mathcal{T}}(X^{\star},{\bar{x}}))$
$\displaystyle\iff$
$\displaystyle(\mathfrak{A},X^{\star})\vDash_{s}\psi^{\mathcal{I}}_{\mathcal{T}}(X^{\star},{\bar{x}})\text{
for every }s\text{ with }s({\bar{x}})\in X^{\star}$ $\displaystyle\iff$
$\displaystyle(\mathfrak{A},X)^{\phantom{\star}}\vDash_{s}\psi^{\star}(X,{\bar{x}})\text{
for every }s\text{ with }s({\bar{x}})\in X^{\star}\;\;(\text{Claim \ref{claim:
construction psistar is correct}})$ $\displaystyle\iff$
$\displaystyle(\mathfrak{A},X)^{\phantom{\star}}\vDash_{s}\psi^{\star}(X,{\bar{x}})\text{
for every }s\text{ with }(\mathfrak{A},X)\vDash_{s}e_{T}({\bar{u}})\land
X{\bar{v}}\;\;(\text{due to (\ref{eq: X vs Xstar})})$ $\displaystyle\iff$
$\displaystyle(\mathfrak{A},X)^{\phantom{\star}}\vDash\forall{\bar{u}}\forall{\bar{v}}\forall{\bar{w}}((e_{T}({\bar{u}})\land
X{\bar{v}})\rightarrow\psi^{\star}(X,{\bar{u}},{\bar{v}},{\bar{w}})))\equiv\mu.$

As a result, we have that
$(\mathfrak{A},X)\vDash\mu(X)\iff(\mathfrak{A},X^{\star})\vDash\varphi^{\mathcal{I}}_{\mathcal{T}}$.
Putting everything together yields:

$(\mathfrak{A},X)\vDash\mu\Longleftrightarrow(\mathfrak{A},X^{\star})\vDash\varphi_{\mathcal{T}}^{\mathcal{I}}\stackrel{{\scriptstyle\eqref{eq:
interpretation lemma
result}}}{{\Longleftrightarrow}}(\mathcal{G},X)\vDash\varphi_{\mathcal{T}}\stackrel{{\scriptstyle(\text{Claim
\ref{claim: phitarget is
correct}})}}{{\Longleftrightarrow}}X\in\mathcal{T}(\mathcal{G})\stackrel{{\scriptstyle(\text{Theorem
\ref{thm: eso <=> inex-
game}})}}{{\Longleftrightarrow}}(\mathfrak{A},X)\vDash\varphi$

Thus, the constructed myopic formula $\mu(X)$ is indeed equivalent to
$\varphi(X)$.

This construction can be applied to non union closed formulae as well, in
which case the statement becomes $(\mathfrak{A},X)\vDash\mu$ if, and only if,
$X=\bigcup_{i\in I}X_{i}$ such that $(\mathfrak{A},X_{i})\vDash\varphi$ for
all $i\in I$. To see this replace Claim 4.4 by “For every $X\subseteq A^{r}$,
$(\mathcal{G},X)\vDash\varphi_{\mathcal{T}}(X)\iff X=\bigcup_{i\in I}X_{i}$,
where $X_{i}\in\mathcal{T}(\mathcal{G})$ for all $i\in I$”. Or, in other
words, $\mu$ is the “smallest” (w.r.t. the set of models) union closed formula
which is implied by $\varphi$: $\varphi\vDash\mu$ and, more importantly, $\mu$
implies all union closed formulae $\nu$ which are implied by $\varphi$, i.e.
if $\varphi\vDash\nu$ and $\nu$ is union closed then $\mu\vDash\nu$ holds.

##  5\. Union Games

In the previous section we have characterised the union closed fragment of
$\operatorname{\Sigma^{1}_{1}}$ by means of a syntactic normal form. Now we
aim at a game theoretic description, which leads to the following restriction
of inclusion-exclusion games that reveals _how_ union closed properties are
assembled.

A _union game_ is an inclusion-exclusion game
$\mathcal{G}=(V,V_{0},V_{1},E,I,T,{E_{\mathsf{ex}}})$ obeying the following
restrictions. For every $t\in T$ the subgraph reachable from $t$ via the edges
$E\setminus{E_{\mathsf{in}}}$, that are the edges of $E$ that do _not_ go back
into $T$, is denoted by ${\mathcal{G}^{\vartriangle}_{t}}$.555Recall that
${E_{\mathsf{in}}}\coloneqq E\cap(V\times T)$. These components must be
disjoint, that is $V({\mathcal{G}^{\vartriangle}_{t}})\cap
V({\mathcal{G}^{\vartriangle}_{t^{\prime}}})=\varnothing$ for all $t\neq
t^{\prime}\in T$. Furthermore, exclusion edges are only allowed between
vertices of the same component, that is
${E_{\mathsf{ex}}}\subseteq\bigcup_{t\in
T}V({\mathcal{G}^{\vartriangle}_{t}})\times
V({\mathcal{G}^{\vartriangle}_{t}})$. The set of initial positions is empty,
i.e. $I=\varnothing$.

$t_{1}$$t_{2}$$t_{k}$$\dotsb$${\mathcal{G}^{\vartriangle}_{t_{1}}}$${\mathcal{G}^{\vartriangle}_{t_{2}}}$${\mathcal{G}^{\vartriangle}_{t_{k}}}$$v$$w$$x$$y$$u$$z$
Figure 1. A drawing of a union game. The target positions
$T=\\{t_{1},\dotsc,t_{k}\\}$ are at the top of the components
${\mathcal{G}^{\vartriangle}_{t}}$, which are depicted by triangles. Recall
that the inclusion edges, that are the edges going into target vertices, do
not account for the reachability of the components
${\mathcal{G}^{\vartriangle}_{t}}$. The exclusion edges ${E_{\mathsf{ex}}}$
are drawn as dashed arrows and, as seen here, are allowed only inside a
component.

See Figure 1 for a graphical representation of a union game. Since the
exclusion edges are only inside a component we can in a way combine different
strategies into one, which is the reason the target set of a union game is
closed under unions.

######  Theorem 10.

Let $\mathcal{G}$ be a union game and $(\mathcal{S}_{i})_{i\in J}$ be a family
of winning strategies for player 0. Then there is a winning strategy
$\mathcal{S}$ for player 0 such that $\mathcal{T}(\mathcal{S})=\bigcup_{i\in
J}\mathcal{T}(\mathcal{S}_{i})$. In other words, the set
$\mathcal{T}(\mathcal{G})$ is closed under unions.

######  Proof 5.1.

Let $\mathcal{S}_{i}=(W_{i},F_{i})$ for $i\in J$. Let $U\coloneqq\bigcup_{i\in
J}\mathcal{T}(\mathcal{S}_{i})$ and $f\colon U\to J$ be a function such that
$t\in\mathcal{T}(\mathcal{S}_{f(t)})$ for all $t\in U$. Define
$\mathcal{S}\coloneqq\bigcup_{t\in
U}(\mathcal{S}_{f(t)}{\upharpoonright_{V({\mathcal{G}^{\vartriangle}_{t}})}}+(E(\mathcal{S}_{f(t)})\cap(V({\mathcal{G}^{\vartriangle}_{t}})\times
T)))$. In words, $\mathcal{S}$ is defined on every component
${\mathcal{G}^{\vartriangle}_{t}}$ with $t\in U$ as an arbitrary strategy
$\mathcal{S}_{t}$ that is defined on ${\mathcal{G}^{\vartriangle}_{t}}$,
including the inclusion edges leaving this component. By definition
$\mathcal{T}(\mathcal{S})=U$ and, furthermore, $\mathcal{S}$ is indeed a
winning strategy since it behaves on every component
${\mathcal{G}^{\vartriangle}_{t}}$ like $\mathcal{S}_{f(t)}$ and there are no
exclusion edges between different components.

Let
$\mu(X)=\forall{\bar{x}}(X{\bar{x}}\rightarrow\exists{\bar{R}}\varphi(X,{\bar{R}},{\bar{x}}))$
be a myopic $\tau$-formula where $\varphi$ is in negation-normal form and
$\mathfrak{A}$ be a $\tau$-structure. The union game
$\mathcal{G}(\mathfrak{A},\mu)\coloneqq(V,V_{0},V_{1},E,I=\varnothing,T=A^{\operatorname{ar}(X)},{E_{\mathsf{ex}}})$
is defined similarly to Definition 3.1 with the difference being that for each
${\bar{a}}\in A^{\operatorname{ar}({\bar{x}})}$ we have to play on a copy of
the game, so positions are now of the form $(\vartheta,s,{\bar{a}})$ instead
of $(\vartheta,s)$, where $\vartheta\in\operatorname{subf}(\varphi)$. The
target vertices are the roots of these components, which is reflected by edges
from ${\bar{a}}$ to $(\varphi,{\bar{x}}\mapsto{\bar{a}},{\bar{a}})$. Because
of this construction exclusion edges can only occur inside a component.

Notice that there are still edges from $(X{\bar{x}},s,{\bar{a}})$ to
$s({\bar{x}})$ — the inclusion edges. It is also worth mentioning that the
empty set is always included in $\mathcal{T}(\mathcal{G}(\mathfrak{A},\mu))$
for all myopic $\mu$ because $(\varnothing,\varnothing)$ is a (trivial)
winning strategy for player $0$. This mimics the behaviour that in case
$X=\varnothing$, the formula $\forall{\bar{x}}(X{\bar{x}}\rightarrow\psi)$ is
satisfied regardless of everything else. The analogue of Theorem 3 holds for
union games and myopic formulae.

######  Proposition 11.

Let $\mathfrak{A}$, $\mu$ and $\mathcal{G}(\mathfrak{A},\mu)$ be as in
Definition 5. Then $(\mathfrak{A},X)\vDash\mu\iff
X\in\mathcal{T}(\mathcal{G}(\mathfrak{A},\mu))$.

######  Proof 5.2.

Assume
$(\mathfrak{A},X)\vDash\mu=\forall{\bar{x}}(X{\bar{x}}\rightarrow\exists{\bar{R}}\varphi(X,{\bar{R}},{\bar{x}}))$.
Thus, for every ${\bar{a}}\in X$ there exist relations ${\bar{R}}_{\bar{a}}$
such that $\mathfrak{A}\vDash\varphi(X,{\bar{R}}_{\bar{a}},{\bar{a}})$. Notice
that every component ${\mathcal{G}^{\vartriangle}_{{\bar{a}}}}$ restricted to
$V,V_{0},V_{1},E$ is essentially isomorphic to the first-order model-checking
game $\mathcal{G}((\mathfrak{A},X,{\bar{R}}_{\bar{a}}),\varphi)$ (besides the
additional node ${\bar{a}}$, the only difference is that in the first-order
model-checking game the vertices of the form $(X{\bar{y}},s,{\bar{a}})$ are
terminal nodes where player 0 loses if and only if $s({\bar{y}})\notin X$).
Let $\mathcal{S}^{\operatorname{FO}}_{\bar{a}}$ be a winning strategy for
player 0 in this game. Since either ${\bar{b}}\in R_{\bar{a}}$ or
${\bar{b}}\notin R_{\bar{a}}$ for all ${\bar{b}}$ and $R$, one vertex
$(R{\bar{x}},s,{\bar{a}})$ or $(\neg R{\bar{y}},s^{\prime},{\bar{a}})$ with
$s({\bar{x}})=s^{\prime}({\bar{y}})$ is not visited by
$\mathcal{S}^{\operatorname{FO}}_{\bar{a}}$. Let
$\mathcal{S}^{\prime}\coloneqq\bigcup_{{\bar{a}}\in
X}\mathcal{S}^{\operatorname{FO}}_{\bar{a}}$ and
$\mathcal{S}\coloneqq\mathcal{S}^{\prime}+{E_{\mathsf{in}}}\cap(V(\mathcal{S}^{\prime})\times
V(\mathcal{S}^{\prime}))$. In words, the strategy $\mathcal{S}$ combines all
first-order strategies together and adds the reached inclusion edges. By
definition $\mathcal{T}(\mathcal{S})=X$. Whenever a node of the form
$(X{\bar{y}},s,{\bar{a}})$ is visited in $\mathcal{S}$ we have that
$s({\bar{y}})\in X$ (because otherwise
$\mathcal{S}^{\operatorname{FO}}_{\bar{a}}$ would not be a winning strategy
for player 0) and hence
$((X{\bar{y}},s,{\bar{a}}),s({\bar{y}}))\in{E_{\mathsf{in}}}\cap(V(\mathcal{S}^{\prime})\times
V(\mathcal{S}^{\prime}))$ is a move that is available to player $0$. That
$\mathcal{S}^{\prime}$ satisfies the conditions for a winning strategy on the
other nodes is inherited from the fact that the individual strategies are
winning strategies on the first-order part. As pointed out before, each
strategy does not visit an exclusion edge.

For the contrary, let $\mathcal{S}$ be a winning strategy with
$\mathcal{T}(\mathcal{S})=X$. For every ${\bar{a}}\in X$ let ${\bar{b}}\in
R_{\bar{a}}$ if and only if there is some $(R{\bar{x}},s,{\bar{a}})\in
V(\mathcal{S})$ with $s({\bar{x}})={\bar{b}}$. We have to show that
$\mathfrak{A}\vDash\varphi(X,{\bar{R}}_{\bar{a}},{\bar{a}})$ for all
${\bar{a}}\in X$. But there is nothing to do here because
$\mathcal{S}{\upharpoonright_{{\mathcal{G}^{\vartriangle}_{{\bar{a}}}}}}$
induces a winning strategy for the first-order model-checking game for
$\left<(\mathfrak{A},X,{\bar{R}}_{\bar{a}}),{\bar{x}}\mapsto{\bar{a}},\varphi\right>$.

##  6\. Myopic Fragment of Inclusion-Exclusion Logic

We turn our attention towards logics with team semantics in this section. Our
findings will be similar in nature to what we observed for existential second-
order logic. In fact, like the normal form of union closed
$\operatorname{\Sigma^{1}_{1}}$-formulae (see Section 4) we present syntactic
restrictions of inclusion-exclusion logic
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$ that correspond precisely to
the union closed fragment $\mathcal{U}$666We have defined $\mathcal{U}$ to be
the set of all union closed $\operatorname{\Sigma^{1}_{1}}$-formulae, by
slight abuse of notation we use the same symbol here to denote the set of all
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$-formulae that are closed under
unions.. Analogously to myopic $\operatorname{\Sigma^{1}_{1}}$-formulae we
will also present a normal form for all union closed
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$-formulae.

A formula $\varphi({\bar{x}})\in\operatorname{FO}(\subseteq,{}\mathbin{|}{})$
is ${\bar{x}}$-myopic, if the following conditions are satisfied:

  1. (1)

The variables from ${\bar{x}}$ are never quantified in $\varphi$.

  2. (2)

Every exclusion atom occurring in $\varphi$ is of the form
${\bar{x}}{\bar{y}}\mathbin{|}{\bar{x}}{\bar{z}}$.

  3. (3)

Every inclusion atom occurring in $\varphi$ is of the form
${\bar{x}}{\bar{y}}\subseteq{\bar{x}}{\bar{z}}$ or
${\bar{y}}\subseteq{\bar{x}}$, where the latter is _only_ allowed if it is not
in the scope of a disjunction.

Please note that $\varphi({\bar{x}})$ must not have any additional free
variables besides ${\bar{x}}$. We call atoms of the form
${\bar{x}}{\bar{y}}\subseteq{\bar{x}}{\bar{z}}$ or
${\bar{x}}{\bar{y}}\mathbin{|}{\bar{x}}{\bar{z}}$ (${\bar{x}}$-)_guarded_ and
${\bar{y}}\subseteq{\bar{z}}$, respectively ${\bar{y}}\mathbin{|}{\bar{z}}$,
the corresponding _unguarded_ versions. Analogously, we call a formula $\psi$
the unguarded version of $\varphi$, if $\psi$ emerges from $\varphi$ by
replacing every dependency atom by the respective unguarded version.

The intuition behind this definition is that every ${\bar{x}}$-myopic formula
can be evaluated componentwise on every team
$X{\upharpoonright_{{\bar{x}}={\bar{a}}}}=\\{s\in X:s({\bar{x}})={\bar{a}}\\}$
for all ${\bar{a}}\in X({\bar{x}})$. For a formula $\varphi$ let $T_{\varphi}$
denote its syntax tree777Since we consider a tree instead of a DAG, identical
subformulae may occur at different nodes.. A (team-)labelling of $T_{\varphi}$
is a function $\lambda$ mapping every node $v_{\psi}$ to a team
$\lambda(v_{\psi})$ whose domain includes $\operatorname{free}(\psi)$. In the
following we write $\lambda(\psi)$ instead of $\lambda(v_{\psi})$ if it is
clear from the context which _occurrence_ of the subformula $\psi$ of
$\varphi$ is meant. We call $\lambda$ a _witness_ for
$\mathfrak{A}\vDash_{X}\varphi$, if $\lambda(\varphi)=X$ and the semantical
rules of Definition 2 are satisfied (e.g.
$\lambda(\psi\lor\vartheta)=\lambda(\psi)\cup\lambda(\vartheta)$) and for
every literal $\beta$ of $\varphi$ we have
$\mathfrak{A}\vDash_{\lambda(\beta)}\beta$. By induction, if $\lambda$ is a
witness for $\mathfrak{A}\vDash_{X}\varphi$, then for every
$\psi\in\operatorname{subf}(\varphi)$ we have
$\mathfrak{A}\vDash_{\lambda(\psi)}\psi$ and, moreover,
$\mathfrak{A}\vDash_{X}\varphi$ if and only if there is a witness $\lambda$
for $\mathfrak{A}\vDash_{X}\varphi$.

######  Proposition 12.

Let $X$ be team over $\mathfrak{A}$ with
$\operatorname{dom}(X)\supseteq\\{{\bar{x}},{\bar{v}},{\bar{w}}\\}$ and
$\varphi({\bar{x}})$ be ${\bar{x}}$-myopic.

  1. (1)

$\mathfrak{A}\vDash_{X}{\bar{x}}{\bar{v}}\subseteq{\bar{x}}{\bar{w}}\iff\mathfrak{A}\vDash_{X{\upharpoonright_{{\bar{x}}={\bar{a}}}}}{\bar{v}}\subseteq{\bar{w}}$
for all ${\bar{a}}\in X({\bar{x}})$

  2. (2)

$\mathfrak{A}\vDash_{X}{\bar{x}}{\bar{v}}\mathbin{|}{\bar{x}}{\bar{w}}\iff\mathfrak{A}\vDash_{X{\upharpoonright_{{\bar{x}}={\bar{a}}}}}{\bar{v}}\mathbin{|}{\bar{w}}$
for all ${\bar{a}}\in X({\bar{x}})$

  3. (3)

For every subformula ${\bar{v}}\subseteq{\bar{x}}$ of $\varphi$ and witness
$\lambda$ for $\mathfrak{A}\vDash_{X}\varphi$ we have
$(\lambda({\bar{v}}\subseteq{\bar{x}}))({\bar{x}})=X({\bar{x}})$.

######  Proof 6.1.

We prove the first item. Let
$\mathfrak{A}\vDash_{X}{\bar{x}}{\bar{v}}\subseteq{\bar{x}}{\bar{w}}$. That
means for every assignment $s\in X$ there is another one, $s^{\prime}\in X$,
with $s({\bar{x}}{\bar{v}})=s^{\prime}({\bar{x}}{\bar{w}})$. Thus
$s({\bar{x}})=s^{\prime}({\bar{x}})$ and therefore $s\in
X{\upharpoonright_{{\bar{x}}={\bar{a}}}}\iff s^{\prime}\in
X{\upharpoonright_{{\bar{x}}={\bar{a}}}}$ from which
$\mathfrak{A}\vDash_{X{\upharpoonright_{{\bar{x}}={\bar{a}}}}}{\bar{v}}\subseteq{\bar{w}}$
follows for all ${\bar{a}}\in X({\bar{x}})$.

Now assume
$\mathfrak{A}\vDash_{X{\upharpoonright_{{\bar{x}}={\bar{a}}}}}{\bar{v}}\subseteq{\bar{w}}$
for all ${\bar{a}}\in X({\bar{x}})$ and let $s\in X$ be an arbitrary
assignment. Since
$\mathfrak{A}\vDash_{X{\upharpoonright_{{\bar{x}}=s({\bar{x}})}}}{\bar{v}}\subseteq{\bar{w}}$
there is an assignment $s^{\prime}\in
X{\upharpoonright_{{\bar{x}}=s({\bar{x}})}}$ with
$s^{\prime}({\bar{w}})=s({\bar{v}})$. This means
$s({\bar{x}}{\bar{v}})=s^{\prime}({\bar{x}}{\bar{w}})$, and because $s$ was
arbitrary,
$\mathfrak{A}\vDash_{X}{\bar{x}}{\bar{v}}\subseteq{\bar{x}}{\bar{w}}$ follows.

We prove the second item.
$\mathfrak{A}\nvDash_{X{\upharpoonright_{{\bar{x}}={\bar{a}}}}}{\bar{v}}\mathbin{|}{\bar{w}}$
holds for some ${\bar{a}}\in X({\bar{x}})$ if and only if there are some
$s,s^{\prime}\in X$ with ${\bar{a}}=s({\bar{x}})=s^{\prime}({\bar{x}})$ and
$s({\bar{v}})=s^{\prime}({\bar{w}})$, i.e.
$s({\bar{x}}{\bar{v}})=s^{\prime}({\bar{x}}{\bar{w}})$ and hence
$\mathfrak{A}\nvDash_{X}{\bar{x}}{\bar{v}}\mathbin{|}{\bar{x}}{\bar{w}}$.
Conversely, if $s({\bar{x}}{\bar{v}})=s^{\prime}({\bar{x}}{\bar{w}})$ for some
$s,s^{\prime}\in X$, then
$\mathfrak{A}\nvDash_{X{\upharpoonright_{{\bar{x}}=s({\bar{x}})}}}{\bar{v}}\mathbin{|}{\bar{w}}$.

The third item follows from the simple fact that ${\bar{x}}$ is never
quantified and that those atoms are not in the scope of a disjunction, hence
the values of ${\bar{x}}$ are preserved.

The ${\bar{x}}$-guarded version of a formula
$\varphi({\bar{y}})\in\operatorname{FO}(\subseteq,{}\mathbin{|}{})$ in which
the variables ${\bar{x}}$ do not occur is the formula
$\varphi^{\star}({\bar{x}},{\bar{y}})$ which results from $\varphi({\bar{y}})$
by replacing every inclusion/exclusion atom by its ${\bar{x}}$-guarded
variant, i.e. ${\bar{u}}\subseteq{\bar{v}}$ would become
${\bar{x}}{\bar{u}}\subseteq{\bar{x}}{\bar{v}}$ and
${\bar{u}}\mathbin{|}{\bar{v}}$ would be turned into
${\bar{x}}{\bar{u}}\mathbin{|}{\bar{x}}{\bar{v}}$. By property (1) and (2) of
Proposition 12, the connection between a formula and its ${\bar{x}}$-guarded
version is the following.

######  Lemma 13.

Let $\varphi^{\star}({\bar{x}},{\bar{y}})$ be the ${\bar{x}}$-guarded version
of $\varphi({\bar{y}})\in\operatorname{FO}(\subseteq,{}\mathbin{|}{})$. Then
$\mathfrak{A}\vDash_{X}\varphi^{\star}({\bar{x}},{\bar{y}})\Longleftrightarrow\mathfrak{A}\vDash_{X{\upharpoonright_{{\bar{x}}={\bar{a}}}}}\varphi({\bar{y}})$
for every ${\bar{a}}\in X({\bar{x}})$.

Like union games an ${\bar{x}}$-myopic formula is evaluated componentwise,
which leads to the union closure of this fragment.

######  Theorem 14.

Let $\varphi({\bar{x}})\in\operatorname{FO}(\subseteq,{}\mathbin{|}{})$ be
${\bar{x}}$-myopic and $\mathfrak{A}\vDash_{X_{i}}\varphi$ for all $i\in I$.
Then $\mathfrak{A}\vDash_{X}\varphi$ for $X=\bigcup_{i\in I}X_{i}$.

######  Proof 6.2.

Let $\lambda_{i}$ be a witness for $\mathfrak{A}\vDash_{X_{i}}\varphi$ and
every $i\in I$. For every ${\bar{a}}\in X({\bar{x}})$ choose $i_{\bar{a}}\in
I$ such that ${\bar{a}}\in X_{i_{\bar{a}}}({\bar{x}})$. Define
$\lambda(\psi)\coloneqq\bigcup_{{\bar{a}}\in
X({\bar{x}})}\lambda_{i_{\bar{a}}}(\psi){\upharpoonright_{{\bar{x}}={\bar{a}}}}$
for every $\psi\in\operatorname{subf}(\varphi)$. We show that $\lambda$ is a
witness for $\mathfrak{A}\vDash_{X}\varphi$. It is not difficult to see that
the requirements on witnesses for composite formulae are satisfied. We prove
that the requirements for the literals are fulfilled as well. By the flatness
property, first-order literals are satisfied by $\lambda$.

We prove now that $\mathfrak{A}\vDash_{\lambda(\gamma)}\gamma$ for
$\gamma={\bar{x}}{\bar{v}}\subseteq{\bar{x}}{\bar{w}}$ or
$\gamma={\bar{x}}{\bar{v}}\mathbin{|}{\bar{x}}{\bar{w}}$. Let
$\gamma^{\prime}$ be the corresponding _unguarded_ formula, that is the
formula resulting from $\gamma$ by removing ${\bar{x}}$, i.e. we have
$\gamma^{\prime}={\bar{v}}\subseteq{\bar{w}}$ or
$\gamma^{\prime}={\bar{v}}\mathbin{|}{\bar{w}}$. Due to Proposition 12, it
suffices to prove that
$\mathfrak{A}\vDash_{\lambda(\gamma){\upharpoonright_{{\bar{x}}={\bar{a}}}}}\gamma^{\prime}$
is true for every ${\bar{a}}\in(\lambda(\gamma))({\bar{x}})$. Notice that
$\lambda(\gamma){\upharpoonright_{{\bar{x}}={\bar{a}}}}=\lambda_{i_{\bar{a}}}(\gamma){\upharpoonright_{{\bar{x}}={\bar{a}}}}$.
Since $\lambda_{i_{\bar{a}}}$ is a witness for
$\mathfrak{A}\vDash_{X_{i_{\bar{a}}}}\varphi$, it must be the case that
$\mathfrak{A}\vDash_{\lambda_{i_{\bar{a}}}(\gamma)}\gamma$. By Proposition 12,
it follows that
$\mathfrak{A}\vDash_{\lambda_{i_{\bar{a}}}(\gamma){\upharpoonright_{{\bar{x}}={\bar{b}}}}}\gamma^{\prime}$
for every ${\bar{b}}\in(\lambda_{i_{\bar{a}}}(\gamma))({\bar{x}})$. If
${\bar{a}}\in(\lambda_{i_{\bar{a}}}(\gamma))({\bar{x}})$, then this implies
that
$\mathfrak{A}\vDash_{\lambda_{i_{\bar{a}}}(\gamma){\upharpoonright_{{\bar{x}}={\bar{a}}}}}\gamma^{\prime}$.
Otherwise we have that
$\lambda_{i_{\bar{a}}}(\gamma){\upharpoonright_{{\bar{x}}={\bar{a}}}}=\varnothing$
and then
$\mathfrak{A}\vDash_{\lambda_{i_{\bar{a}}}(\gamma){\upharpoonright_{{\bar{x}}={\bar{a}}}}}\gamma^{\prime}$
follows from the empty team property of
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$. In both cases,
$\mathfrak{A}\vDash_{\lambda_{i_{\bar{a}}}(\gamma){\upharpoonright_{{\bar{x}}={\bar{a}}}}}\gamma^{\prime}$
holds as desired, which concludes the proof of
$\mathfrak{A}\vDash_{\lambda(\gamma)}\gamma$.

We still need to prove that $\mathfrak{A}\vDash_{\lambda(\gamma)}\gamma$ for
literals of the form
$\gamma={\bar{v}}\subseteq{\bar{x}}\in\operatorname{subf}(\varphi)$. Towards
this end, let $s\in\lambda({\bar{v}}\subseteq{\bar{x}})$ and
${\bar{b}}\coloneqq s({\bar{v}})$. By definition of $\lambda$, there is some
${\bar{a}}\in X({\bar{x}})$ such that
$s\in\lambda_{i_{\bar{a}}}({\bar{v}}\subseteq{\bar{x}}){\upharpoonright_{{\bar{x}}={\bar{a}}}}$.
Since
$\mathfrak{A}\vDash_{\lambda_{i_{\bar{a}}}({\bar{v}}\subseteq{\bar{x}})}{\bar{v}}\subseteq{\bar{x}}$
and
${\bar{b}}=s({\bar{v}})\in\lambda_{i_{\bar{a}}}({\bar{v}}\subseteq{\bar{x}})({\bar{v}})$,
it follows that
${\bar{b}}\in(\lambda_{i_{\bar{a}}}({\bar{v}}\subseteq{\bar{x}}))({\bar{x}})$.
By Proposition 12 we have
$(\lambda_{i_{\bar{a}}}({\bar{v}}\subseteq{\bar{x}}))({\bar{x}})=X_{i_{\bar{a}}}({\bar{x}})$,
wherefore ${\bar{b}}\in X_{i_{\bar{a}}}({\bar{x}})\subseteq X({\bar{x}})$ and,
consequently, we have chosen some index $i_{\bar{b}}\in I$ with ${\bar{b}}\in
X_{i_{\bar{b}}}({\bar{x}})$. By Proposition 12 again, it follows that
$X_{i_{{\bar{b}}}}({\bar{x}})=(\lambda_{i_{\bar{b}}}({\bar{v}}\subseteq{\bar{x}}))({\bar{x}})$.
So there is some
$s^{\prime}\in\lambda_{i_{\bar{b}}}({\bar{v}}\subseteq{\bar{x}})$ with
$s^{\prime}({\bar{x}})={\bar{b}}=s({\bar{v}})$ and thus
$s^{\prime}\in\lambda_{i_{\bar{b}}}({\bar{v}}\subseteq{\bar{x}}){\upharpoonright_{{\bar{x}}={\bar{b}}}}\subseteq\lambda({\bar{v}}\subseteq{\bar{x}})$.
This concludes the proof of
$\mathfrak{A}\vDash_{\lambda({\bar{v}}\subseteq{\bar{x}})}{\bar{v}}\subseteq{\bar{x}}$.

It remains to prove that indeed every union closed formula $\varphi$ of
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$ is equivalent to some
${\bar{x}}$-myopic formula.

######  Theorem 15.

Let $\varphi({\bar{x}})\in\operatorname{FO}(\subseteq,{}\mathbin{|}{})$. There
is an ${\bar{x}}$-myopic formula $\mu({\bar{x}})$ such that for all suitable
structures $\mathfrak{A}$ and teams $X$ with
$\operatorname{dom}(X)=\\{{\bar{x}}\\}$ holds

$\mathfrak{A}\vDash_{X}\mu({\bar{x}})\Longleftrightarrow X\text{ can be
written as }X=\bigcup_{i\in I}X_{i}\text{ where
}\mathfrak{A}\vDash_{X_{i}}\varphi({\bar{x}})\text{ for every }i\in I.$

######  Proof 6.3.

Let ${\bar{y}}$ be a fresh tuple of variables. Let
$\varphi^{\star}({\bar{x}},{\bar{y}})$ be the ${\bar{x}}$-guarded version of
$\varphi({\bar{y}})$, i.e. $\varphi^{\star}$ results from $\varphi$ by first
replacing the variables ${\bar{x}}$ by the new variables ${\bar{y}}$ and then
by adding ${\bar{x}}$ on both sides of every inclusion or exclusion atoms
occurring in $\varphi({\bar{y}})$. We define

$\mu({\bar{x}})\coloneqq\exists{\bar{y}}({\bar{y}}\subseteq{\bar{x}}\land{\bar{x}}{\bar{x}}\subseteq{\bar{x}}{\bar{y}}\land\varphi^{\star}({\bar{x}},{\bar{y}})),$

which is ${\bar{x}}$-myopic. We still need to prove the two directions of the
claim.

“$\Longrightarrow$”: First assume $\mathfrak{A}\vDash_{X}\mu({\bar{x}})$. Then
there exists a team $Y$ of the form $Y=X[{\bar{y}}\mapsto F]$ for some
function $F\colon X\to\mathcal{P}^{+}(A^{|{\bar{x}}|})$ such that

$\mathfrak{A}\vDash_{Y}{\bar{y}}\subseteq{\bar{x}}\land{\bar{x}}{\bar{x}}\subseteq{\bar{x}}{\bar{y}}\land\varphi^{\star}({\bar{x}},{\bar{y}}).$

Thus we have $Y({\bar{y}})\subseteq Y({\bar{x}})=X({\bar{x}})$ and, due to
Lemma 13,
$\mathfrak{A}\vDash_{Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}}{\bar{x}}\subseteq{\bar{y}}\land\varphi({\bar{y}})$
for every ${\bar{a}}\in Y({\bar{x}})$, because
${\bar{x}}{\bar{x}}\subseteq{\bar{x}}{\bar{y}}\land\varphi^{\star}({\bar{x}},{\bar{y}})$
is the ${\bar{x}}$-guarded version of
${\bar{x}}\subseteq{\bar{y}}\land\varphi({\bar{y}})$. We can deduce, for every
${\bar{a}}\in Y({\bar{x}})$, that
$\\{{\bar{a}}\\}=Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}({\bar{x}})\subseteq
Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}({\bar{y}})\subseteq
Y({\bar{y}})\subseteq Y({\bar{x}})$. This implies that

${\bar{a}}\in Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}({\bar{y}})\subseteq
Y({\bar{x}})\text{ for every }{\bar{a}}\in Y({\bar{x}}).$ (3)

For every ${\bar{a}}\in Y({\bar{x}})$, let $X_{\bar{a}}$ be the team with
$\operatorname{dom}(X_{\bar{a}})=\\{{\bar{x}}\\}$ and
$X_{\bar{a}}({\bar{x}})=Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}({\bar{y}})$.
Because of this construction and due to
$\mathfrak{A}\vDash_{Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}}\varphi({\bar{y}})$,
it follows that $\mathfrak{A}\vDash_{X_{\bar{a}}}\varphi({\bar{x}})$.
Furthermore, (3) and $Y({\bar{x}})=X({\bar{x}})$ lead to

${\bar{a}}\in X_{\bar{a}}({\bar{x}})\subseteq X({\bar{x}})\text{ for every
}{\bar{a}}\in X({\bar{x}})$

and, consequently, to $\bigcup_{{\bar{a}}\in
X({\bar{x}})}X_{\bar{a}}({\bar{x}})=X({\bar{x}})$. Because of
$\operatorname{dom}(X)=\\{{\bar{x}}\\}=\operatorname{dom}(X_{\bar{a}})$, we
indeed have $X=\bigcup_{{\bar{a}}\in X({\bar{x}})}X_{\bar{a}}$ where
$\mathfrak{A}\vDash_{X_{\bar{a}}}\varphi({\bar{x}})$ for every ${\bar{a}}\in
X({\bar{x}})$.

“$\Longleftarrow$”: For the converse direction, we assume that $X$ can be
written as $X=\bigcup_{i\in I}X_{i}$ where
$\mathfrak{A}\vDash_{X_{i}}\varphi({\bar{x}})$ for every $i\in I$. Our goal is
to prove that $\mathfrak{A}\vDash_{X}\mu({\bar{x}})$. Towards this end, for
every ${\bar{a}}\in X({\bar{x}})$, we choose some index $i_{\bar{a}}\in I$
with ${\bar{a}}\in X_{i_{\bar{a}}}({\bar{x}})$. Let $F\colon
X\to\mathcal{P}^{+}(A^{|{\bar{y}}|})$ be defined by $F(s)\coloneqq
X_{i_{s({\bar{x}})}}({\bar{x}})$. Then we have

$s({\bar{x}})\in F(s)\subseteq X({\bar{x}})\text{ for every }s\in X.$ (4)

Let $Y\coloneqq X[{\bar{y}}\mapsto F]$. By construction, it follows that
$F(s)=Y{\upharpoonright_{{\bar{x}}=s({\bar{x}})}}({\bar{y}})$ for every $s\in
X$. Furthermore, we also have

$Y({\bar{y}})=\bigcup_{s\in X}F(s)\underset{\eqref{eq: extention function
F}}{=}X({\bar{x}})=Y({\bar{x}}).$

In particular, this implies $Y({\bar{y}})\subseteq Y({\bar{x}})$ and, hence,
$\mathfrak{A}\vDash_{Y}{\bar{y}}\subseteq{\bar{x}}$. Now, in order to prove
$\mathfrak{A}\vDash_{Y}{\bar{x}}{\bar{x}}\subseteq{\bar{x}}{\bar{y}}\land\varphi^{\star}({\bar{x}},{\bar{y}})$
we will use Lemma 13. This means that we only need to prove that
$\mathfrak{A}\vDash_{Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}}{\bar{x}}\subseteq{\bar{y}}\land\varphi({\bar{y}})$
for every ${\bar{a}}\in Y({\bar{x}})$. Towards this end, pick any
${\bar{a}}\in Y({\bar{x}})$. Because of $Y({\bar{x}})=X({\bar{x}})$, there
must be an assignment $s_{\bar{a}}\in X$ with
$s_{\bar{a}}({\bar{x}})={\bar{a}}$. We clearly have

$Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}({\bar{x}})=\\{{\bar{a}}\\}=\\{s_{\bar{a}}({\bar{x}})\\}\underset{\eqref{eq:
extention function
F}}{\subseteq}F(s_{\bar{a}})=Y{\upharpoonright_{{\bar{x}}=s_{\bar{a}}({\bar{x}})}}({\bar{y}})=Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}({\bar{y}})$

and, thus,
$\mathfrak{A}\vDash_{Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}}{\bar{x}}\subseteq{\bar{y}}$.
By assumption, we also know that
$\mathfrak{A}\vDash_{X_{i_{\bar{a}}}}\varphi({\bar{x}})$. Because of
$Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}({\bar{y}})=F(s_{\bar{a}})=X_{i_{s_{\bar{a}}({\bar{x}})}}({\bar{x}})=X_{i_{\bar{a}}}({\bar{x}})$,
this implies that
$\mathfrak{A}\vDash_{Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}}\varphi({\bar{y}})$.
Therefore, we indeed have
$\mathfrak{A}\vDash_{Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}}{\bar{x}}\subseteq{\bar{y}}\land\varphi({\bar{y}})$
for every ${\bar{a}}\in Y({\bar{x}})$. As a result, we have
$\mathfrak{A}\vDash_{Y}{\bar{y}}\subseteq{\bar{x}}\land{\bar{x}}{\bar{x}}\subseteq{\bar{x}}{\bar{y}}\land\varphi^{\star}({\bar{x}},{\bar{y}})$
which leads to $\mathfrak{A}\vDash_{X}\mu({\bar{x}})$.

As we have already seen in Theorem 5, every union closed formula of
existential second-order logic is equivalent to some myopic
$\operatorname{\Sigma^{1}_{1}}$-formula. Moreover, it is well known that every
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$-formula can be translated into
an equivalent $\operatorname{\Sigma^{1}_{1}}$-formula [Gal12]. Such a formula
can be expressed as an ${\bar{x}}$-myopic one of the form
$\exists{\bar{s}}({\bar{s}}\subseteq{\bar{x}}\land\psi)$ where $\psi$ uses
only ${\bar{x}}$-guarded atoms.

######  Lemma 16.

Let $\varphi({\bar{x}})\in\operatorname{FO}(\subseteq,{}\mathbin{|}{})$ be an
${\bar{x}}$-myopic formula of the form
$\exists{\bar{s}}({\bar{s}}\subseteq{\bar{x}}\land\psi)$, where in $\psi$ no
inclusion atoms of the form ${\bar{y}}\subseteq{\bar{x}}$ occur. Then
$\mathfrak{A}\vDash_{X}\varphi$ if and only if there exists $F\colon
X\to\mathcal{P}^{+}(A^{|{\bar{x}}|})$ such that $F(s)\subseteq X({\bar{x}})$
for every $s\in X$ and $\mathfrak{A}\vDash_{X[{\bar{s}}\mapsto
F]{\upharpoonright_{{\bar{x}}={\bar{a}}}}}\psi^{\prime}$ for all ${\bar{a}}\in
X({\bar{x}})$, where $\psi^{\prime}$ is the unguarded version of $\psi$.

######  Proof 6.4.

By induction on $\psi$ and applying Proposition 12.

We present two different proofs for the next theorem, which bring a myopic
$\operatorname{\Sigma^{1}_{1}}$-formula into this normal form. The following
proof is based on methods of Galliani, Kontinen and Väänänen [Gal12, KV09]
while the other one resembles the proof of Theorem 9 and can be found in
Section 6.1.

######  Theorem 17.

Let $\varphi(X)$ be a myopic $\operatorname{\Sigma^{1}_{1}}$-formula. There is
an equivalent ${\bar{x}}$-myopic formula of
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$ where
$|{\bar{x}}|=\operatorname{ar}(X)$.

######  Proof 6.5.

First of all let us introduce a normal form of myopic
$\operatorname{\Sigma^{1}_{1}}$-formulae. Since in myopic formulae the
variable $X$ may occur only positively in the subformula $\varphi^{\prime}$,
we can transform every
$\forall{\bar{x}}(X{\bar{x}}\rightarrow\exists{\bar{R}}\varphi^{\prime}({\bar{R}},X,{\bar{x}}))$
into the equivalent formula $\forall{\bar{x}}(X{\bar{x}}\rightarrow\exists
S(S\subseteq X\land\exists{\bar{R}}\varphi^{\prime}({\bar{R}},S,{\bar{x}})))$,
where $S\subseteq X$ is a shorthand for
$\forall{\bar{y}}(S{\bar{y}}\rightarrow X{\bar{y}})$. We now apply the Skolem-
normal form of $\operatorname{\Sigma^{1}_{1}}$-formulae to
$\exists{\bar{R}}\varphi^{\prime}({\bar{R}},S,{\bar{x}})$, which yields the
formula
$\sigma(S,{\bar{x}})\coloneqq\exists{\bar{f}}\forall{\bar{y}}((f_{1}({\bar{w}})=f_{2}({\bar{w}})\leftrightarrow
S{\bar{w}})\land\psi({\bar{f}},{\bar{x}},{\bar{y}}))$, where $\psi$ is a
quantifier-free first-order formula and ${\bar{w}}$ is a subtuple of
${\bar{y}}$ and, moreover, every $f_{i}$ occurs in $\sigma$ only with a unique
tuple ${\bar{w}}_{i}$ (consisting of pairwise different variables) as
argument, that is $f_{i}({\bar{w}}_{i})$ (see [KV09] where an analogous
construction is made). The original formula can thus be transformed into
$\forall{\bar{x}}(X{\bar{x}}\rightarrow\exists S(S\subseteq
X\land\sigma(S,{\bar{x}})))$. Similarly to [Gal12] we embed
$\sigma(S,{\bar{x}})$ into inclusion-exclusion logic as
$\vartheta({\bar{s}},{\bar{x}})\coloneqq\forall{\bar{y}}\exists{\bar{z}}\big{(}\bigwedge_{i}\operatorname{=}({\bar{x}}{\bar{w}}_{i},z_{i})\land(({\bar{x}}{\bar{w}}\subseteq{\bar{x}}{\bar{s}}\land
z_{1}=z_{2})\lor({\bar{x}}{\bar{w}}\mathbin{|}{\bar{x}}{\bar{s}}\land
z_{1}\neq z_{2}))\land\psi^{\prime}({\bar{x}},{\bar{y}},{\bar{z}})\big{)}$.
Here $\psi^{\prime}$ is obtained from $\psi$ by simply replacing every
occurrence of $f_{i}({\bar{w}}_{i})=f_{j}({\bar{w}}_{j})$ by $z_{i}=z_{j}$.
The only difference in our case is that every dependency atom is
${\bar{x}}$-guarded due to the fact that the subformula at hand is inside the
scope of the universally quantified variables ${\bar{x}}$ in
$\forall{\bar{x}}(X{\bar{x}}\rightarrow\dots)$. Notice that dependence atoms
of the form $\operatorname{=}({\bar{x}}{\bar{w}}_{i},z_{i})$ can also be
regarded as ${\bar{x}}$-myopic. Formally, we can embed such an atom into
exclusion logic via the formula $\forall
v({\bar{x}}{\bar{w}}_{i}v\mathbin{|}{\bar{x}}{\bar{w}}_{i}z_{i}\lor z_{i}=v)$,
which has the intended shape [Gal12]. The whole formula $\varphi(X)$ thus
translates into
$\mu({\bar{x}})\coloneqq\exists{\bar{s}}({\bar{s}}\subseteq{\bar{x}}\land\vartheta({\bar{s}},{\bar{x}}))$.
Let $\vartheta^{\prime}({\bar{s}},{\bar{x}})$ be the unguarded version of
$\vartheta({\bar{s}},{\bar{x}})$. Analogously to the argumentation of Galliani
[Gal12] by additionally making use of Proposition 12, we see that
$(\mathfrak{A},Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}({\bar{s}}))\vDash_{{\bar{x}}\mapsto{\bar{a}}}\sigma(S,{\bar{x}})$
if and only if
$\mathfrak{A}\vDash_{Y{\upharpoonright_{{\bar{x}}={\bar{a}}}}}\vartheta^{\prime}({\bar{x}})$
for ${\bar{a}}\in Y({\bar{x}})$, where $Y$ is a team with domain
$\\{{\bar{s}},{\bar{x}}\\}$ (here the variable $S$ takes the role of the
team). Using Lemma 16 we have $\mathfrak{A}\vDash_{X}\mu({\bar{x}})$ if and
only if there is a function $F\colon
X\to\mathcal{P}^{+}(A^{\operatorname{ar}({\bar{s}})})$ such that
$F(s)\subseteq X({\bar{x}})$ for every $s\in X$ and
$\mathfrak{A}\vDash_{X[{\bar{s}}\mapsto
F]{\upharpoonright_{{\bar{x}}={\bar{a}}}}}\vartheta^{\prime}({\bar{s}},{\bar{x}})$
for all ${\bar{a}}\in X({\bar{x}})$, which again holds if and only if there
exists such an $F$ and $(\mathfrak{A},F(s))\vDash_{t}\sigma(S,{\bar{x}})$ for
all $t\in X$, but this just means
$(\mathfrak{A},X({\bar{x}}))\vDash\forall{\bar{x}}(X{\bar{x}}\rightarrow\exists
S(S\subseteq X\land\sigma(S,{\bar{x}})))$.

######  Corollary 18 (Normal form of
myopic-$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$).

Let $\varphi({\bar{x}})$ be a union closed formula of
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$. There is a logically
equivalent ${\bar{x}}$-myopic formula
$\psi({\bar{x}})=\exists{\bar{s}}({\bar{s}}\subseteq{\bar{x}}\land\vartheta)$
where in $\vartheta$ only ${\bar{x}}$-guarded dependency atoms occur.

###  6.1. Alternative Proof

The proof of Theorem 17 uses a translation into a special Skolem-normal form
that in the end produces a lot of guarded in-/exclusion atoms. We can prevent
this by using a different proof technique that similar to the proof of Theorem
17 exploits that winning strategies of union games are definable in the myopic
fragment of $\operatorname{FO}(\subseteq,{}\mathbin{|}{})$-formulae and that
the model-checking games of myopic formulae are first-order interpretable. The
rest of this section is organised as follows. First, we define target sets of
a union game by a myopic
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$-formula, then we adapt the
interpretation lemma for logics with team semantics and finally present the
alternative proof of Theorem 17.

Let us demonstrate that (vertex sets of) winning strategies of _general_
inclusion-exclusion games can be defined in
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$:

$\displaystyle\psi_{\operatorname{win}}(y)$
$\displaystyle\coloneqq\psi_{\operatorname{init}}(y)\land\psi_{\operatorname{move}}(y)\land\psi_{{E_{\mathsf{ex}}}}(y)\text{
where}$ $\displaystyle\psi_{\operatorname{init}}(y)$
$\displaystyle\coloneqq\forall z(Iz\rightarrow z\subseteq y)$
$\displaystyle\psi_{\operatorname{move}}(y)$ $\displaystyle\coloneqq\exists
z([(V_{0}y\land\exists z^{\prime}(Eyz^{\prime}\land z^{\prime}\subseteq
z))\lor(V_{1}y\land\forall z^{\prime}(Eyz^{\prime}\rightarrow
z^{\prime}\subseteq z))]\land z\subseteq y)$
$\displaystyle\psi_{{E_{\mathsf{ex}}}}(y)$ $\displaystyle\coloneqq\forall
z(({E_{\mathsf{ex}}}yz\lor{E_{\mathsf{ex}}}zy)\rightarrow y\mathbin{|}z)$

It is not difficult to verify that these formulae are just expressing the
conditions for winning strategies (cf. Definition 3). More formally, we have
the following claim:

Let $\mathcal{G}$ be an inclusion-exclusion game and $Y$ be a non-empty team
over $\mathcal{G}$ with $y\in\operatorname{dom}(Y)$. Then
$\mathcal{G}\vDash_{Y}\psi_{\operatorname{win}}(y)$ if and only if $Y(y)$ is
the vertex set of a winning strategy for player $0$ in $\mathcal{G}$. With
these formulae at hand, it is easy to define the target sets in
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$:

$\psi_{\mathcal{T}}(z)\coloneqq Tz\land\exists
y(\psi_{\operatorname{win}}(y)\land z\subseteq y\land(Ty\rightarrow y\subseteq
z)).$

Let $\mathcal{G}$ be an inclusion-exclusion game and let $X$ be a non-empty
team over $\mathcal{G}$ with $z\in\operatorname{dom}(X)$. Then
$\mathcal{G}\vDash_{X}\psi_{\mathcal{T}}(z)$ if and only if
$X(z)\in\mathcal{T}(\mathcal{G})$.

######  Proof 6.6.

“$\Longrightarrow$”: Let $\mathcal{G}\vDash_{X}\psi_{\mathcal{T}}(z)$. Then
$X(z)\subseteq T(\mathcal{G})$ and
$\mathcal{G}\vDash_{Y}\psi_{\operatorname{win}}(y)\land z\subseteq
y\land(Ty\rightarrow y\subseteq z)$ where $Y\coloneqq X[y\mapsto F]$ for some
$F\colon X\to\mathcal{P}^{+}(V(\mathcal{G}))$. From
$\mathcal{G}\vDash_{Y}z\subseteq y\land(Ty\rightarrow y\subseteq z)$ we obtain
that $Y(z)\subseteq Y(y)$ and $Y(y)\cap
T(\mathcal{G})=(Y{\upharpoonright_{Ty}})(y)\subseteq(Y{\upharpoonright_{Ty}})(z)$.
By Claim 6.1 and $\mathcal{G}\vDash_{Y}\psi_{\operatorname{win}}(y)$, we have
$Y(y)=V(\mathcal{S})$ for some winning strategy $\mathcal{S}$. We prove that
$Y(z)=Y(y)\cap T(\mathcal{G})$. The direction “$\supseteq$” follows from
$Y(y)\cap T(\mathcal{G})\subseteq(Y{\upharpoonright_{Ty}})(z)\subseteq Y(z)$,
while the direction “$\subseteq$” is entailed by $Y(z)\subseteq Y(y)$ and
$Y(z)=X(z)\subseteq T(\mathcal{G})$. Thus, $X(z)=Y(z)=Y(y)\cap
T(\mathcal{G})=\mathcal{T}(\mathcal{S})\in\mathcal{T}(\mathcal{G})$.

“$\Longleftarrow$”: Now let $X(z)\in\mathcal{T}(\mathcal{G})$. Then there is
some winning strategy $\mathcal{S}$ with $\mathcal{T}(\mathcal{S})=X(z)$. So
$\mathcal{G}\vDash_{X}Tz$. By letting $Y\coloneqq X[y\mapsto V(\mathcal{S})]$,
we also obtain $\mathcal{G}\vDash_{Y}\psi_{\operatorname{win}}(y)$, by Claim
6.1 and $Y(y)=V(\mathcal{S})$, and $\mathcal{G}\vDash_{Y}z\subseteq y$, since
$Y(z)=X(z)=\mathcal{T}(\mathcal{S})\subseteq V(\mathcal{S})=Y(y)$. We still
need to prove that $\mathcal{G}\vDash_{Y}Ty\rightarrow y\subseteq z$. Towards
this end, consider any $s\in Y{\upharpoonright_{Ty}}$. Then $s(y)\in Y(y)\cap
T(\mathcal{G})=\mathcal{T}(\mathcal{S})=X(z)$ and, thus, there exists some
$s^{\prime}\in X$ with $s^{\prime}(z)=s(y)$. Let $s^{\prime\prime}\coloneqq
s^{\prime}[y\mapsto s(y)]$. It follows that
$s^{\prime\prime}\in{Y{\upharpoonright_{Ty}}}$, because we have
$s^{\prime\prime}(y)=s(y)\in\mathcal{T}(\mathcal{S})=V(\mathcal{S})\cap
T(\mathcal{G})$. So we have $s^{\prime\prime}(z)=s^{\prime}(z)=s(y)$ and
$s^{\prime\prime}\in Y{\upharpoonright_{Ty}}$, which concludes the proof of
$\mathcal{G}\vDash_{Y}Ty\rightarrow y\subseteq z$. All in all, this proves
that $\mathcal{G}\vDash_{X}\psi_{\mathcal{T}}$.

In the last example, we have learned that target sets of general inclusion-
exclusion games can be expressed in full
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$. In particular, this formula
also defines the target sets of union games. But is it possible to do the same
in the _myopic fragment_ of $\operatorname{FO}(\subseteq,{}\mathbin{|}{})$?

Towards giving a positive answer to this question, let
$\psi_{\mathcal{T}}^{G}(x,z)$ be the corresponding $x$-guarded version of
$\psi_{\mathcal{T}}(z)$. Recall that this just means that we add $x$ on both
sides of every occurring in-/exclusion atom. For example, the inclusion atom
$z\subseteq y$ occurring in the subformula $\psi_{\operatorname{init}}$ will
be transformed into $xz\subseteq xy$ when constructing
$\psi_{\mathcal{T}}^{G}$.

Consider the $x$-myopic formula $\vartheta_{\mathcal{T}}(x)$ given by

$\vartheta_{\mathcal{T}}(x)\coloneqq\exists x^{\prime}(x^{\prime}\subseteq
x\land\zeta(x,x^{\prime}))\text{ where }\zeta(x,x^{\prime})\coloneqq
xx\subseteq xx^{\prime}\land\psi_{\mathcal{T}}^{G}(x,x^{\prime}).$

We claim (and prove) that $\vartheta_{\mathcal{T}}(x)$ defines the target sets
in _union_ games which, more formally, means that for every team $X$ over some
union game $\mathcal{G}$ with $x\in\operatorname{dom}(X)$ holds
$\mathcal{G}\vDash_{X}\vartheta_{\mathcal{T}}\iff
X(x)\in\mathcal{T}(\mathcal{G})$.888Since union games do not have any initial
vertices, the formula $\vartheta_{\mathcal{T}}$ could be simplified by
removing the subformula $\psi_{\operatorname{init}}^{G}$ which is in a union
game just trivially satisfied. To see this, let $\zeta^{\prime}$ be the
corresponding unguarded version of $\zeta$, which turns out to be the
following formula:

$\zeta^{\prime}(x,x^{\prime})=x\subseteq
x^{\prime}\land\psi_{\mathcal{T}}(x^{\prime})$

Let $\mathcal{G}$ be an inclusion-exclusion game and let $X$ be a non-empty
team over $\mathcal{G}$ with $x,x^{\prime}\in\operatorname{dom}(X)$. Then
$\mathcal{G}\vDash_{X}\zeta^{\prime}(x,x^{\prime})$ if and only if
$X(x)\subseteq X(x^{\prime})\in\mathcal{T}(\mathcal{G})$.

######  Proof 6.7.

Follows immediately from Claim 6.1.

With this claim at hand, we can prove that $\vartheta_{\mathcal{T}}$ really
defines what we promised:

Let $\mathcal{G}=(V,V_{0},V_{1},E,I,T,{E_{\mathsf{ex}}})$ be a _union_ game
and let $X$ be a team with $x\in\operatorname{dom}(X)$. Then
$\mathcal{G}\vDash_{X}\vartheta_{\mathcal{T}}\iff
X(x)\in\mathcal{T}(\mathcal{G})$.

######  Proof 6.8.

For $X=\varnothing$ the claim is true, because
$\varnothing\in\mathcal{T}(\mathcal{G})$ is true for every union game and
$\mathcal{G}\vDash_{\varnothing}\vartheta_{\mathcal{T}}$ is due to the empty
team property. Let $X\neq\varnothing$. Applying Lemma 16 immediately yields
the equivalence of the following statements:

  1. (1)

$\mathcal{G}\vDash_{X}\vartheta_{\mathcal{T}}=\exists
x^{\prime}(x^{\prime}\subseteq x\land\zeta(x,x^{\prime}))$

  2. (2)

There is a function $F\colon X\to\mathcal{P}^{+}(V)$ such that

    1. (a)

$F(s)\subseteq X(x)$ for every $s\in X$, and

    2. (b)

$\mathcal{G}\vDash_{X_{t}}\zeta^{\prime}(x,x^{\prime})$ where $X_{t}\coloneqq
X[x^{\prime}\mapsto F]{\upharpoonright_{x=t}}$ for every $t\in X(x)$.

Next we will prove that the following propositions are also equivalent:

  1. (3)

For every $t\in X(x)$ exists a winning strategy $\mathcal{S}_{t}$ with
$t\in\mathcal{T}(\mathcal{S}_{t})\subseteq X(x)$.

  2. (4)

$X(x)\in\mathcal{T}(\mathcal{G})$.

######  Proof 6.9.

If $X(x)\in\mathcal{T}(\mathcal{G})$, then there is a strategy $\mathcal{S}$
with $\mathcal{T}(\mathcal{S})=V(\mathcal{S})\cap T=X(x)$ which in particular
implies that $t\in\mathcal{T}(\mathcal{S})\subseteq X(x)$ for every $t\in
X(x)$.

For the converse direction assume (3). Since $\mathcal{G}$ is a union game, we
are allowed to use Theorem 10 to combine the family $(\mathcal{S}_{t})_{t\in
X(x)}$ into a single winning strategy $\mathcal{S}$ with
$\mathcal{T}(\mathcal{S})=\bigcup_{t\in X(x)}\mathcal{T}(\mathcal{S}_{t})$
which is, due to assumptions about $\mathcal{T}(\mathcal{S}_{t})$, equal to
$X(x)$.

So we have already established that $(\ref{claim: thetatarget is correct -
(a)})\iff(\ref{claim: thetatarget is correct - (b)})$ and $(\ref{claim:
thetatarget is correct - (c)})\iff(\ref{claim: thetatarget is correct -
(d)})$, but our goal was to show that $(\ref{claim: thetatarget is correct -
(a)})\iff(\ref{claim: thetatarget is correct - (d)})$ which is exactly what
Claim 6.1 states. Thus, in order to complete our proof of Claim 6.1, we just
have to verify the missing link $(\ref{claim: thetatarget is correct -
(b)})\iff(\ref{claim: thetatarget is correct - (c)})$.

“$(\ref{claim: thetatarget is correct - (b)})\Longrightarrow(\ref{claim:
thetatarget is correct - (c)})$”: Suppose that there is some function $F\colon
X\to\mathcal{P}^{+}(V)$ such that (2a) and (2b) are true. So
$\mathcal{G}\vDash_{X_{t}}\zeta^{\prime}(x,x^{\prime})$ for every $t\in X(x)$
which, by Claim 6.1, yields that $X_{t}(x)\subseteq
X_{t}(x^{\prime})\in\mathcal{T}(\mathcal{G})$. By definition of $X_{t}$ in
(2b), we have $X_{t}(x)=(X[x^{\prime}\mapsto
F]{\upharpoonright_{x=t}})(x)=\\{t\\}$ and, consequently, $t\in
X_{t}(x^{\prime})\in\mathcal{T}(\mathcal{G})$ which, by definition of
$\mathcal{T}(\mathcal{G})$, leads to the existence of winning strategies
$\mathcal{S}_{t}$ with $X_{t}(x^{\prime})=\mathcal{T}(\mathcal{S}_{t})$ for
every $t\in X(x)$. Because of (2a) we can also conclude that
$X_{t}(x^{\prime})=\bigcup_{s\in X{\upharpoonright_{x=t}}}F(s)\subseteq X(x)$.
As a result, we obtain $t\in\mathcal{T}(\mathcal{S}_{t})\subseteq X(x)$ for
every $t\in X(x)$ as desired.

“$(\ref{claim: thetatarget is correct - (b)})\Longleftarrow(\ref{claim:
thetatarget is correct - (c)})$”: We assume now that for every $t\in X(x)$
there exists some winning strategy $\mathcal{S}_{t}$ with
$t\in\mathcal{T}(\mathcal{S}_{t})\subseteq X(x)$. Define $F\colon
X\to\mathcal{P}^{+}(V)$ as $F(s)\coloneqq\mathcal{T}(\mathcal{S}_{s(x)})$ —
notice that $s(x)\in\mathcal{T}(\mathcal{S}_{s(x)})$ holds by assumption, so
$F$ is indeed well-defined. Then (2a) is true, because for every $s\in X$ we
have also assumed that $\mathcal{T}(\mathcal{S}_{s(x)})\subseteq X(x)$.
Because $F(s)$ depends only on $s(x)$ and we have $X_{t}(x)=\\{t\\}$, it
follows that $X_{t}(x^{\prime})=\mathcal{T}(\mathcal{S}_{t})$. As a result, we
have $X_{t}(x)=\\{t\\}\subseteq\mathcal{T}(\mathcal{S}_{t})=X_{t}(x^{\prime})$
from which immediately follows that $X_{t}(x)\subseteq
X_{t}(x^{\prime})\in\mathcal{T}(\mathcal{G})$ for every $t\in X(x)$. Thus, by
Claim 6.1, we obtain $\mathcal{G}\vDash_{X_{t}}\zeta^{\prime}(x,x^{\prime})$
for every $t\in X(x)$, which is exactly (2b).

Now we have already one component, the $x$-myopic formula
$\vartheta_{\mathcal{T}}(x)$, that is needed for the alternative proof of
Theorem 17. However, we still require an interpretation lemma for
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$. Towards this end, consider a
$\tau$-formula
$\varphi(x_{1},\dotsc,x_{m})\in\operatorname{FO}(\subseteq,{}\mathbin{|}{})$
and some first-order interpretation
$\mathcal{I}=(\delta,\varepsilon,(\psi)_{S\in\tau})$. The formula
$\varphi^{\mathcal{I}}$ is defined as in section 2, whereas the occurring
in-/exclusion atoms are handled as follows:

  * $\bullet$

$(v_{1},\dotsc,v_{\ell}\subseteq
w_{1},\dotsc,w_{\ell})^{\mathcal{I}}\coloneqq\exists{\bar{v}}_{1}^{\prime}\dots\bar{v}^{\prime}_{\ell}\big{(}\bigwedge^{\ell}_{i=1}\delta({\bar{v}}^{\prime}_{i})\land\varepsilon({\bar{v}}_{i},{\bar{v}}^{\prime}_{i})\land{\bar{v}}_{1},\dotsc,{\bar{v}}_{\ell}\subseteq{\bar{w}}_{1},\dotsc,{\bar{w}}_{\ell}\big{)}$

  * $\bullet$

$(v_{1},\dotsc,v_{\ell}\mathbin{|}w_{1},\dotsc,w_{\ell})^{\mathcal{I}}\coloneqq\forall{\bar{v}}^{\prime}_{1}\dotsc{\bar{v}}^{\prime}_{\ell}\big{(}\big{[}\bigwedge^{\ell}_{i=1}\delta({\bar{v}}^{\prime}_{i})\land\varepsilon({\bar{v}}_{i},{\bar{v}}^{\prime}_{i})\big{]}\rightarrow{\bar{v}}^{\prime}_{1},\dotsc,{\bar{v}}^{\prime}_{\ell}\mathbin{|}{\bar{w}}_{1},\dotsc,{\bar{w}}_{\ell}\big{)}$

Let $\mathfrak{B}\cong\mathcal{I}(\mathfrak{A})$ with coordinate map
$h\colon\delta^{\mathfrak{A}}\to B$. A team $X$ over $\mathfrak{A}$ with
$\operatorname{dom}(X)=\\{{\bar{x}}_{1},\dots,{\bar{x}}_{m}\\}$ is said to be
well-formed, if every $s\in X$ is well-formed (w.r.t. $\mathcal{I}$), i.e.
$s({\bar{x}}_{i})\in\delta^{\mathfrak{A}}$ for $i=1,\dotsc,m$. For such a
team, $h(X)\coloneqq\\{h\circ s:s\in X\\}$ is a well-defined team over
$\mathfrak{B}$ with $\operatorname{dom}(h(X))=\\{x_{1},\dots,x_{m}\\}$. The
following lemma can be proven by induction over $\varphi$.

######  Lemma 19 (Interpretation Lemma for
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$).

For every well-formed team $X$ over $\mathfrak{A}$ with
$\operatorname{dom}(X)=\\{{\bar{x}}_{1},\dots,{\bar{x}}_{m}\\}$, holds
$\mathfrak{A}\vDash_{X}\varphi^{\mathcal{I}}\iff\mathfrak{B}\vDash_{h(X)}\varphi$.

Consider any team $Y$ over $\mathfrak{B}$ with
$\operatorname{dom}(Y)=\\{x_{1},\dots,x_{m}\\}$. It is an easy consequence of
this lemma, that
$\mathfrak{B}\vDash_{Y}\varphi\iff\mathfrak{A}\vDash_{h^{-1}(Y)}\varphi^{\mathcal{I}}$
where $h^{-1}(Y)\coloneqq\bigcup_{t\in Y}h^{-1}(t)=\\{s:h\circ s\in Y\\}$ can
be viewed as the “full” team describing $Y$. Of course, different tuples of
the base structure $\mathfrak{A}$ may encode the same element of the target
structure $\mathfrak{B}$, thus $Y$ usually contains redundant assignments. For
the same reason, two (well-formed) teams $X\neq X^{\prime}$ (with the same
domain and co-domain $\mathfrak{A}$) may describe the same team over
$\mathfrak{B}$. We say that $X$ and $X^{\prime}$ are _$h$ -similar_, if
$h(X)=h(X^{\prime})$.

######  Lemma 20 (Similarity Lemma).

Let $X,X^{\prime}$ be well-formed teams that are $h$-similar. Then:
$\mathfrak{A}\vDash_{X}\varphi^{\mathcal{I}}\iff\mathfrak{A}\vDash_{X^{\prime}}\varphi^{\mathcal{I}}$.

######  Proof 6.10.

Since $X,X^{\prime}$ are $h$-similar, we have $h(X)=h(X^{\prime})$. By the
interpretation lemma,
$\mathfrak{A}\vDash_{X}\varphi^{\mathcal{I}}\iff\mathfrak{B}\vDash_{h(X)}\varphi\underset{h(X)=h(X^{\prime})}{\iff}\mathfrak{B}\vDash_{h(X^{\prime})}\varphi\iff\mathfrak{A}\vDash_{X^{\prime}}\varphi^{\mathcal{I}}$.

Now we have all the tools assembled that are needed to prove a stronger
variant of Theorem 15 resp. Theorem 17.

######  Theorem 21.

For every myopic second-order-formula999It is well known that every
$\operatorname{FO}(\subseteq,{}\mathbin{|}{})$-formula can be translated into
an equivalent $\operatorname{\Sigma^{1}_{1}}$-formula [Gal12]. As we have
already seen in Theorem 5, every union closed formula of existential second-
order logic is equivalent to some myopic
$\operatorname{\Sigma^{1}_{1}}$-formula. Therefore, we can w.l.o.g. start with
a myopic second-order-formula. $\varphi(X)$ there exists an equivalent myopic
formula $\mu({\bar{x}})$ with only $8$ inclusion atoms and one exclusion atom.

######  Proof 6.11.

Let $\varphi(X)$ be a myopic $\operatorname{\Sigma^{1}_{1}}$-formula. We are
going to find a ${\bar{y}}$-myopic formula
$\mu({\bar{y}})\in\operatorname{FO}(\subseteq,{}\mathbin{|}{})$ with
$(\mathfrak{A},X({\bar{y}}))\vDash\varphi(X)\iff\mathfrak{A}\vDash_{X}\mu({\bar{y}})$
for every $\tau$-structure $\mathfrak{A}$ and every team $X$ with
${\bar{y}}\subseteq\operatorname{dom}(X)$. In the following let $\mathfrak{A}$
be a $\tau$-structure chosen arbitrarily. In Definition 5 we have defined the
model-checking game $\mathcal{G}\coloneqq\mathcal{G}(\mathfrak{A},\varphi)$
for $\mathfrak{A}$ and $\varphi(X)$. By Proposition 11, we know for every
_relation_ $X\subseteq A^{r}$ that:

$(\mathfrak{A},X)\vDash\varphi(X)\iff X\in\mathcal{T}(\mathcal{G})$ (5)

Due to Claim 6.1 we may conclude for every _team_ $X$ with
$x\in\operatorname{dom}(X)$:

$\mathcal{G}\vDash_{X}\vartheta_{\mathcal{T}}(x)\iff
X(x)\in\mathcal{T}(\mathcal{G})$ (6)

By combining (5) and (6), we obtain that for every _team_ $X$ with
$x\in\operatorname{dom}(X)$ over $\mathcal{G}$:

$\mathcal{G}\vDash_{X}\vartheta_{\mathcal{T}}(x)\iff(\mathfrak{A},X(x))\vDash\varphi(X)$
(7)

Notice that $\mathcal{G}\vDash_{X}\vartheta_{\mathcal{T}}(x)$ implies that
$X(x)\subseteq T(\mathcal{G})=A^{r}$ and, hence, $X(x)$ is then actually a
relation of the correct arity for the formula $\varphi(X)$. By counting, it is
easy to verify that exactly $8$ inclusion atoms and one exclusion atom occurs
in $\vartheta_{\mathcal{T}}$. The formula $\mu({\bar{x}})$ that we are going
to build will result from $\vartheta_{\mathcal{T}}$ and use the same number of
inclusion/exclusion atoms.

Using the technique of Lemma 8, it is possible to devise a (quantifier-free)
interpretation
$\mathcal{I}=(\delta,\varepsilon,\psi_{V_{0}},\psi_{V_{1}},\psi_{E},\psi_{I},\psi_{T},\psi_{{E_{\mathsf{ex}}}})$
such that $\mathcal{G}\cong\mathcal{I}(\mathfrak{A})$ with coordinate map
$h\colon\delta^{\mathfrak{A}}\rightarrow V(\mathcal{G})$. This interpretation
encodes a position of the game $\mathcal{G}$ as a tuple
$({\bar{u}},{\bar{v}})\in A^{n+m}$ where the $n$-tuple ${\bar{u}}$ has a
certain equality type (indicating at which type of position we are encoding,
e.g. at which formula we are) while the $m$-tuple ${\bar{v}}$ stores certain
values (e.g. values of free variables and to which component the node
belongs). More importantly, a position ${\bar{a}}\in T(\mathcal{G})=A^{r}$ is
described by the tuple $({\bar{u}},{\bar{a}},{\bar{b}})\in A^{n+m}$ where
${\bar{u}}$ has equality type $e_{T}$ while ${\bar{b}}\in A^{m-r}$ can be
chosen arbitrarily. Also recall that every variable $v$ is replaced by an
$(n+m)$-tuple ${\bar{v}}$ of pairwise different variables. In particular, let
${\bar{x}}=({\bar{u}},{\bar{y}},{\bar{z}})$ where ${\bar{u}}$ is a $n$-tuple,
${\bar{y}}$ some $r$-tuple and ${\bar{z}}$ an $(m-r)$-tuple.

Every inclusion/exclusion atoms occurring in $\vartheta_{\mathcal{T}}$ has one
of the following three possible forms where $v,w$ are some variables:

  * $\bullet$

$\beta_{1}(x,v,w)\coloneqq xv\mathbin{|}xw$

  * $\bullet$

$\beta_{2}(x,v,w)\coloneqq xv\subseteq xw$

  * $\bullet$

$\beta_{3}(x,v)\coloneqq v\subseteq x$

Notice that the only inclusion atom of the form of $\beta_{3}$ is in
$\vartheta_{\mathcal{T}}$ not within the scope of a disjunction (it is
$x^{\prime}\subseteq x$ right after the existential quantifier). In
$\vartheta_{\mathcal{T}}^{\mathcal{I}}$, these formulae are replaced by:

  * $\bullet$

$\beta^{\mathcal{I}}_{1}({\bar{x}},{\bar{v}},{\bar{w}})\coloneqq\forall{\bar{x}}^{\prime}\forall{\bar{v}}^{\prime}([\delta({\bar{x}}^{\prime})\land\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{x}},{\bar{x}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})]\rightarrow{\bar{x}}^{\prime}{\bar{v}}^{\prime}\mathbin{|}{\bar{x}}{\bar{w}})$

  * $\bullet$

$\beta^{\mathcal{I}}_{2}({\bar{x}},{\bar{v}},{\bar{w}})\coloneqq\exists{\bar{x}}^{\prime}\exists{\bar{v}}^{\prime}(\delta({\bar{x}}^{\prime})\land\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{x}},{\bar{x}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})\land{\bar{x}}^{\prime}{\bar{v}}^{\prime}\subseteq{\bar{x}}{\bar{w}})$

  * $\bullet$

$\beta^{\mathcal{I}}_{3}({\bar{x}},{\bar{v}})\coloneqq\exists{\bar{v}}^{\prime}(\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})\land{\bar{v}}^{\prime}\subseteq{\bar{x}})$

Clearly, these formulas are not allowed in ${\bar{y}}$-myopic formulae,
because the occurring inclusion/exclusion atoms are not ${\bar{y}}$-guarded.
However, we know that the tuple ${\bar{x}}=({\bar{u}},{\bar{y}},{\bar{z}})$ is
used in $\vartheta^{\mathcal{I}}_{\mathcal{T}}$ to store elements from
$h^{-1}(T(\mathcal{G}))=\\{({\bar{v}},{\bar{a}},{\bar{b}})\in
A^{n+m}:\mathfrak{A}\vDash e_{T}({\bar{u}}),{\bar{a}}\in A^{r},{\bar{b}}\in
A^{m-r}\\}$, because whenever a team $Y$ interprets ${\bar{x}}$ by values
encoding different game positions, it follows that $h(Y)(x)$ cannot be a
target set of a winning strategy, so Claim 6.1 leads to
$\mathcal{G}\nvDash_{h(Y)}\vartheta_{\mathcal{T}}(x)$ and then, by the
Interpretation Lemma (Lemma 19),
$\mathfrak{A}\nvDash_{Y}\vartheta_{\mathcal{T}}^{\mathcal{I}}$. So for every
team $X$ which is well-formed (w.r.t. $\mathcal{I}$) and satisfies
$\mathfrak{A}\vDash_{X}\vartheta^{\mathcal{I}}_{\mathcal{T}}$ we must have
that $\mathfrak{A}\vDash_{X}\psi_{T}({\bar{x}})=e_{T}({\bar{u}})$. This
observation enables us to define versions of $\beta^{\mathcal{I}}_{i}$ that
are allowed in ${\bar{y}}$-myopic formulae:

  * $\bullet$

$\beta^{\star}_{1}({\bar{y}},{\bar{v}},{\bar{w}})\coloneqq\forall{\bar{v}}^{\prime}([\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})]\rightarrow{\bar{y}}{\bar{v}}^{\prime}\mathbin{|}{\bar{y}}{\bar{w}})$

  * $\bullet$

$\beta^{\star}_{2}({\bar{y}},{\bar{v}},{\bar{w}})\coloneqq\exists{\bar{v}}^{\prime}(\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})\land{\bar{y}}{\bar{v}}^{\prime}\subseteq{\bar{y}}{\bar{w}})$

  * $\bullet$

$\beta^{\star}_{3}({\bar{y}},{\bar{v}})\coloneqq
e_{T}({\bar{v}}_{(1)})\land{\bar{v}}_{(2)}\subseteq{\bar{y}}$ where
${\bar{v}}={\bar{v}}_{(1)}{\bar{v}}_{(2)}{\bar{v}}_{(3)}$ and
$|{\bar{v}}_{(1)}|=n$, $|{\bar{v}}_{(2)}|=r$ and $|{\bar{v}}_{(3)}|=m-r$.

For every team $X$ with
$\operatorname{dom}(X)=\\{{\bar{x}},{\bar{u}},{\bar{w}}\\}$ with
$X({\bar{x}})\subseteq h^{-1}(T)$ and every $i=1,2,3$ holds
$\mathfrak{A}\vDash_{X}\beta^{\mathcal{I}}_{i}\iff\mathfrak{A}\vDash_{X}\beta^{\star}_{i}$.

######  Proof 6.12.

$i=1$: Let $X^{\prime}\coloneqq
X[{\bar{x}}^{\prime}\mapsto\delta^{\mathfrak{A}},{\bar{v}}^{\prime}\mapsto\delta^{\mathfrak{A}}]{\upharpoonright_{\varepsilon({\bar{x}},{\bar{x}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})}}$.
Then we can observe that

$\mathfrak{A}\vDash_{X}\beta^{\mathcal{I}}_{1}\iff\mathfrak{A}\vDash_{X^{\prime}}{\bar{x}}^{\prime}{\bar{v}}^{\prime}\mathbin{|}{\bar{x}}{\bar{w}}\iff\mathfrak{A}\vDash_{X^{\prime}}{\bar{x}}^{\prime}{\bar{v}}^{\prime}\mathbin{|}{\bar{x}}{\bar{w}}\overset{(!)}{\iff}\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}{\bar{v}}^{\prime}\mathbin{|}{\bar{y}}{\bar{w}}\iff\mathfrak{A}\vDash_{X}\beta_{1}^{\star},$

but the equivalence of
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{x}}^{\prime}{\bar{v}}^{\prime}\mathbin{|}{\bar{x}}{\bar{w}}$
and
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}{\bar{v}}^{\prime}\mathbin{|}{\bar{y}}{\bar{w}}$
requires proof. Let
${\bar{x}}^{\prime}\coloneqq({\bar{u}}^{\prime},{\bar{y}}^{\prime},{\bar{z}}^{\prime})$
where $|{\bar{u}}^{\prime}|=|{\bar{u}}|,|{\bar{y}}^{\prime}|=|{\bar{y}}|$ and
$|{\bar{z}}^{\prime}|=|{\bar{z}}|$. Because of
$\mathfrak{A}\vDash_{X^{\prime}}\varepsilon({\bar{x}},{\bar{x}}^{\prime})$ and
$X^{\prime}({\bar{x}})\subseteq h^{-1}(T)$, we have that
$s({\bar{y}})=s({\bar{y}}^{\prime})$ for every $s\in X^{\prime}$. Now, we
prove the two directions of
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{x}}^{\prime}{\bar{v}}^{\prime}\mathbin{|}{\bar{x}}{\bar{w}}\iff\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}{\bar{v}}^{\prime}\mathbin{|}{\bar{y}}{\bar{w}}$
separately:

“$\Leftarrow$”: First, assume that
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}{\bar{v}}^{\prime}\mathbin{|}{\bar{y}}{\bar{w}}$.
It follows that
$s_{1}({\bar{y}}^{\prime}{\bar{v}}^{\prime})=s_{1}({\bar{y}}{\bar{v}}^{\prime})\neq
s_{2}({\bar{y}}{\bar{w}})$ for every $s_{1},s_{2}\in X^{\prime}$. Because
${\bar{y}}$ and ${\bar{y}}^{\prime}$ are subtuples of
${\bar{x}}=({\bar{u}},{\bar{y}},{\bar{z}})$ resp.
${\bar{x}}^{\prime}=({\bar{u}}^{\prime},{\bar{y}}^{\prime},{\bar{z}}^{\prime})$,
this implies that $s_{1}({\bar{x}}^{\prime}{\bar{v}}^{\prime})\neq
s_{2}({\bar{x}}{\bar{w}})$ for every $s_{1},s_{2}\in X^{\prime}$. Hence,
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{x}}^{\prime}{\bar{v}}^{\prime}\mathbin{|}{\bar{x}}{\bar{w}}$.

“$\Rightarrow$”: Now let
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{x}}^{\prime}{\bar{v}}^{\prime}\mathbin{|}{\bar{x}}{\bar{w}}$.
Towards a contradiction assume that
$\mathfrak{A}\nvDash_{X^{\prime}}{\bar{y}}{\bar{v}}^{\prime}\mathbin{|}{\bar{y}}{\bar{w}}$.
Then there are assignments $s_{1},s_{2}\in X^{\prime}$ with
$s_{1}({\bar{y}}{\bar{v}}^{\prime})=s_{2}({\bar{y}}{\bar{w}})$. Since
$X({\bar{x}})\subseteq h^{-1}(T)$ it follows that $\mathfrak{A}\vDash
e_{T}(s_{1}({\bar{u}}))\land e_{T}(s_{2}({\bar{u}}))$. Because we also have
$\mathfrak{A}\vDash_{X^{\prime}}\varepsilon({\bar{x}},{\bar{x}}^{\prime})$, it
must be the case that $\mathfrak{A}\vDash_{s_{1}}e_{T}({\bar{u}})\land
e_{T}({\bar{u}}^{\prime})\land{\bar{y}}={\bar{y}}^{\prime}$. Consider
$s^{\prime}_{1}\coloneqq s_{1}[{\bar{u}}^{\prime}\mapsto
s_{2}({\bar{u}}),{\bar{z}}^{\prime}\mapsto s_{2}({\bar{z}})]$. $s_{1}$ and
$s^{\prime}_{1}$ only differ on ${\bar{u}}^{\prime}$ and ${\bar{z}}^{\prime}$,
but both still encode the equality type $e_{T}$ in ${\bar{u}}^{\prime}$ while
the values of ${\bar{z}}^{\prime}$ are irrelevant. So we still have
$\mathfrak{A}\vDash_{s^{\prime}_{1}}\delta({\bar{x}}^{\prime})\land\varepsilon({\bar{x}},{\bar{x}}^{\prime})$,
implying that $s^{\prime}_{1}\in X^{\prime}$. But then we have
$s^{\prime}_{1}({\bar{x}}^{\prime})=s^{\prime}_{1}({\bar{u}}^{\prime},{\bar{y}}^{\prime},{\bar{z}}^{\prime})=(s^{\prime}_{1}({\bar{u}}^{\prime}),s^{\prime}_{1}({\bar{y}}^{\prime}),s^{\prime}_{1}({\bar{z}}^{\prime}))=(s_{2}({\bar{u}}),s^{\prime}_{1}({\bar{y}}^{\prime}),s_{2}({\bar{z}}))$
and, because of
$s^{\prime}_{1}({\bar{y}}^{\prime})=s^{\prime}_{1}({\bar{y}})=s_{1}({\bar{y}})=s_{2}({\bar{y}})$,
we even have
$(s_{2}({\bar{u}}),s^{\prime}_{1}({\bar{y}}^{\prime}),s_{2}({\bar{z}}))=s_{2}({\bar{x}})$
proving that $s^{\prime}_{1}({\bar{x}}^{\prime})=s_{2}({\bar{x}})$. Because we
also have $s^{\prime}_{1}({\bar{v}}^{\prime})=s_{2}({\bar{w}})$, this leads to
$s^{\prime}_{1}({\bar{x}}^{\prime}{\bar{v}}^{\prime})=s_{2}({\bar{x}}{\bar{w}})$,
which is impossible due to
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{x}}^{\prime}{\bar{v}}^{\prime}\mathbin{|}{\bar{x}}{\bar{w}}$.
Contradiction! Therefore,
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}{\bar{v}}^{\prime}\mathbin{|}{\bar{y}}{\bar{w}}$
must be true.

$i=2$: “$\Leftarrow$”: First let $\mathfrak{A}\vDash_{X}\beta_{2}^{\star}$.
Then there is a function $F\colon X\to\mathcal{P}^{+}(A^{n+m})$ such that
$\mathfrak{A}\vDash_{X^{\prime}}\delta({\bar{v}})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})\land{\bar{y}}{\bar{v}}^{\prime}\subseteq{\bar{y}}{\bar{w}}$
for $X^{\prime}\coloneqq X[{\bar{v}}^{\prime}\mapsto F]$. Due to
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}{\bar{v}}^{\prime}\subseteq{\bar{y}}{\bar{w}}$,
for every assignment $s\in X^{\prime}$ there exists some $\tilde{s}\in
X^{\prime}$ with
$s({\bar{y}}{\bar{v}}^{\prime})=\tilde{s}({\bar{y}}{\bar{w}})$. Now consider
$Y\coloneqq\\{s[{\bar{x}}^{\prime}\mapsto\tilde{s}({\bar{x}})]:s\in
X^{\prime}\\}$. Then we have that
$\mathfrak{A}\vDash_{Y}\delta({\bar{x}}^{\prime})\land\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{x}},{\bar{x}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})\land{\bar{x}}^{\prime}{\bar{v}}^{\prime}\subseteq{\bar{x}}{\bar{w}}$
which proves that $\mathfrak{A}\vDash_{X}\beta^{\mathcal{I}}_{2}$.

“$\Rightarrow$”: Now let $\mathfrak{A}\vDash_{X}\beta_{2}^{\mathcal{I}}$. Then
there is a function $F\colon X\to\mathcal{P}^{+}(A^{2(n+m)})$ such that
$\mathfrak{A}\vDash_{X^{\prime}}\delta({\bar{x}}^{\prime})\land\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{x}},{\bar{x}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})\land{\bar{x}}^{\prime}{\bar{v}}^{\prime}\subseteq{\bar{x}}{\bar{w}}$
where $X^{\prime}\coloneqq X[{\bar{x}}^{\prime}{\bar{v}}^{\prime}\mapsto F]$.
Since
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{x}}^{\prime}{\bar{v}}^{\prime}\subseteq{\bar{x}}{\bar{w}}$
it follows that
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}^{\prime}{\bar{v}}^{\prime}\subseteq{\bar{y}}{\bar{w}}$
(because ${\bar{y}},{\bar{y}}^{\prime}$ are subtuples of
${\bar{x}},{\bar{x}}^{\prime}$). Due to $X({\bar{x}})\subseteq h^{-1}(T)$,
$\mathfrak{A}\vDash_{X^{\prime}}\delta({\bar{x}}^{\prime})\land\varepsilon({\bar{x}},{\bar{x}}^{\prime})$
implies that $\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}={\bar{y}}^{\prime}$.
So,
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}^{\prime}{\bar{v}}^{\prime}\subseteq{\bar{y}}{\bar{w}}$
is equivalent to
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{y}}{\bar{v}}^{\prime}\subseteq{\bar{y}}{\bar{w}}$.
Hence, we have that
$\mathfrak{A}\vDash_{X^{\prime}}\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})\land{\bar{y}}{\bar{v}}^{\prime}\subseteq{\bar{y}}{\bar{w}}$
which implies that $\mathfrak{A}\vDash_{X}\beta^{\star}_{2}$.

$i=3$: “$\Leftarrow$”: First let $\mathfrak{A}\vDash_{X}\beta_{3}^{\star}$.
Then $X({\bar{v}}_{(1)})\subseteq e^{\mathfrak{A}}_{T}$ and
$X({\bar{v}}_{(2)})\subseteq X({\bar{y}})$. So, for every $s\in X$ there
exists some $\tilde{s}\in X$ with $s({\bar{v}}_{(2)})=\tilde{s}({\bar{y}})$.
Consider
$X^{\prime}\coloneqq\\{s[{\bar{v}}^{\prime}\mapsto\tilde{s}({\bar{x}})]:s\in
X\\}$. Since $\tilde{s}({\bar{x}})\in X({\bar{x}})\subseteq h^{-1}(T)$, we
have that
$\mathfrak{A}\vDash_{X^{\prime}}\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})\land{\bar{v}}^{\prime}\subseteq{\bar{x}}$
which proves that $\mathfrak{A}\vDash_{X}\beta^{\mathcal{I}}_{3}$.

“$\Rightarrow$”: Let $\mathfrak{A}\vDash_{X}\beta_{3}^{\mathcal{I}}$. Then
there is a function $F\colon X\to\mathcal{P}^{+}(A^{n+m})$ such that
$\mathfrak{A}\vDash_{X^{\prime}}\delta({\bar{v}}^{\prime})\land\varepsilon({\bar{v}},{\bar{v}}^{\prime})\land{\bar{v}}^{\prime}\subseteq{\bar{x}}$
where $X^{\prime}\coloneqq X[{\bar{v}}^{\prime}\mapsto F]$. Let
${\bar{v}}^{\prime}={\bar{v}}^{\prime}_{(1)}{\bar{v}}^{\prime}_{(2)}{\bar{v}}^{\prime}_{(3)}$
where $|{\bar{v}}^{\prime}_{(1)}|=n,|{\bar{v}}^{\prime}_{(2)}|=r$ and
$|{\bar{v}}^{\prime}_{(3)}|=m-r$. Since
$X^{\prime}({\bar{x}})=X({\bar{x}})\subseteq h^{-1}(T)$, we have
$X^{\prime}({\bar{u}})\subseteq e^{\mathfrak{A}}_{T}$ and, due to
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{v}}^{\prime}\subseteq{\bar{x}}$, it
follows that $X^{\prime}({\bar{v}}^{\prime}_{(1)})\subseteq
e^{\mathfrak{A}}_{T}$. Furthermore,
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{v}}^{\prime}\subseteq{\bar{x}}$ also
implies that
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{v}}^{\prime}_{(2)}\subseteq{\bar{y}}$.
Because of
$\mathfrak{A}\vDash_{X^{\prime}}\varepsilon({\bar{v}},{\bar{v}}^{\prime})$ and
$X^{\prime}({\bar{v}}^{\prime}_{(1)})\subseteq e^{\mathfrak{A}}_{T}$, we also
have $X^{\prime}({\bar{v}}_{(1)})\subseteq e^{\mathfrak{A}}_{T}$ and
$\mathfrak{A}\vDash_{X^{\prime}}{\bar{v}}_{(2)}={\bar{v}}^{\prime}_{(2)}$.
This is why, we have that
$\mathfrak{A}\vDash_{X^{\prime}}e_{T}({\bar{v}}_{(1)})\land{\bar{v}}_{(2)}\subseteq{\bar{y}}=\beta^{\star}_{3}({\bar{y}},{\bar{v}})$.
This concludes the proof of Claim 6.11.

Let $\vartheta^{\star}_{\mathcal{T}}({\bar{x}})$ be the formula that results
from $\vartheta^{\mathcal{I}}_{\mathcal{T}}$ by replacing every subformulae
$\beta^{\mathcal{I}}_{i}({\bar{x}},\dotsc)$ by
$\beta^{\star}_{i}({\bar{y}},\dotsc)$. Now all the inclusion/exclusion atoms
occurring in $\vartheta^{\star}_{\mathcal{T}}({\bar{x}})$ go conform with the
conditions of Definition 6 but it is still not quite a ${\bar{y}}$-myopic
formula, since
$\vartheta^{\star}_{\mathcal{T}}({\bar{x}})=\vartheta^{\star}_{\mathcal{T}}({\bar{u}},{\bar{y}},{\bar{z}})$
has too many free variables. In order to get rid of the superfluous variables
${\bar{u}},{\bar{z}}$ we simply define
$\mu({\bar{y}})\coloneqq\exists{\bar{u}}\exists{\bar{z}}(e_{T}({\bar{u}})\land\vartheta^{\star}_{\mathcal{T}}({\bar{u}},{\bar{y}},{\bar{z}}))$
which is now a ${\bar{y}}$-myopic formula.101010Notice that the interpretation
does _not_ introduce any disjunction above
$\beta_{3}^{\star}({\bar{x}},{\bar{z}})$, because $x\subseteq z$ is only in
the scope of existential quantifiers and we only a need a conjunction in order
to guard the translated existential quantifier in
$\vartheta^{\mathcal{I}}_{\mathcal{T}}$. For a team $X$ with
$\operatorname{dom}(X)=\\{{\bar{y}}\\}$ we call the team $Y$ a $T$-expansion
of $X$, if $\operatorname{dom}(Y)=\\{{\bar{u}},{\bar{y}},{\bar{z}}\\}$,
$Y({\bar{y}})=X({\bar{y}})$ and $Y({\bar{u}})\subseteq e^{\mathfrak{A}}_{T}$.
Clearly, we have that $\mathfrak{A}\vDash_{X}\mu({\bar{y}})$ if and only if
$\mathfrak{A}\vDash_{Y}\vartheta^{\star}_{\mathcal{T}}({\bar{x}})$ for some
$T$-expansion of $X$ and two $T$-expansions of $Y,Y^{\prime}$ are always
$h$-similar to each other, because
$h(Y({\bar{u}},{\bar{y}},{\bar{z}}))=X({\bar{y}})=h(Y^{\prime}({\bar{u}},{\bar{y}},{\bar{z}}))$
already implies that $h(Y)=h(Y^{\prime})$ which, by the Similarity Lemma
(Lemma 20), leads to
$\mathfrak{A}\vDash_{Y}\vartheta_{\mathcal{T}}^{\mathcal{I}}\iff\mathfrak{A}\vDash_{Y^{\prime}}\vartheta_{\mathcal{T}}^{\mathcal{I}}$.

The full $T$-expansion $X_{T}$ of $X$ is
$X_{T}\coloneqq\\{s[{\bar{u}}\mapsto{\bar{a}},{\bar{z}}\mapsto{\bar{c}}]:s\in
X,{\bar{a}}\in e^{\mathfrak{A}}_{T},{\bar{c}}\in A^{m-r}\\}$ while the “game
version” $X_{\mathcal{G}}$ of $X_{T}$ is a team with
$\operatorname{dom}(X_{\mathcal{G}})=\\{x\\}$ defined by
$X_{\mathcal{G}}\coloneqq\\{s_{\bar{b}}:{\bar{b}}\in X({\bar{y}})\\}$ where
$s_{\bar{b}}\colon\\{x\\}\rightarrow T(\mathcal{G}),\,x\mapsto{\bar{b}}$. It
is not difficult to verify that $X_{\mathcal{G}}(x)=X({\bar{y}})$ and
$h(X_{T})=X_{\mathcal{G}}$.

Putting everything together, we obtain:

$\displaystyle\mathfrak{A}\vDash_{X}\mu({\bar{y}})$
$\displaystyle\iff\mathfrak{A}\vDash_{Y}\vartheta^{\star}_{\mathcal{T}}({\bar{x}})\text{
for some $T$-expansion of $X$}\;\;\text{ (by construction of
$\mu({\bar{y}})$)}$
$\displaystyle\iff\mathfrak{A}\vDash_{Y}\vartheta^{\mathcal{I}}_{\mathcal{T}}({\bar{x}})\text{
for some $T$-expansion of $X$}\;\;\text{ (follows from Claim \ref{claim: beta
replacing})}$
$\displaystyle\iff\mathfrak{A}\vDash_{X_{T}}\vartheta^{\mathcal{I}}_{\mathcal{T}}({\bar{x}})\;\;\text{
($X_{T}$ is $h$-similar to every $T$-expansion of $X$)}$
$\displaystyle\iff\mathcal{G}\vDash_{X_{\mathcal{G}}}\vartheta_{\mathcal{T}}(x)\;\;\text{
(Interpretation Lemma (Lemma \ref{lem: interpretation lemma for inex}))}$
$\displaystyle\iff(\mathfrak{A},X_{\mathcal{G}}(x))\vDash\varphi(X)\;\;\text{
(due to \eqref{eq: team <-> relation})}$
$\displaystyle\iff(\mathfrak{A},X({\bar{y}}))\vDash\varphi(X)\;\;\text{
(because $X_{\mathcal{G}}(x)=X({\bar{y}})$)}$

Thus,
$\mathfrak{A}\vDash_{X}\mu({\bar{y}})\iff(\mathfrak{A},X({\bar{y}}))\vDash\varphi(X)$
follows and our proof is completed.

######  Corollary 22.

Every ${\bar{x}}$-myopic formula $\mu({\bar{x}})$ is equivalent to a
${\bar{x}}$-myopic formula that uses exactly six guarded inclusion atoms, one
inclusion atom of the form ${\bar{x}}^{\prime}\subseteq{\bar{x}}$ and one
guarded exclusion atom.

######  Proof 6.13.

Every ${\bar{x}}$-myopic formula $\mu({\bar{x}})$ can be transformed into a
equivalent myopic $\operatorname{\Sigma^{1}_{1}}$-formula $\mu^{\prime}(X)$
and the construction used in the alternative proof produces exactly as many
atoms as specified, if one replaces the unneeded subformula
$\psi_{\operatorname{init}}$ by any tautology (this does not harm, because
union games do not have initial vertices, so $\psi_{\operatorname{init}}$ was
trivially satisfied).

###  6.2. Optimality of the Myopic Fragment of Inclusion-Exclusion Logic

One might ask whether the restrictions of Definition 6 are actually imperative
to capture the union closed fragment. In this section, we will show that
neither condition can be dropped and that every single atom of Definition 6 is
required to express all union closed properties.

We start by showing that neither condition can be dropped. First of all, it is
pretty clear that exclusion atoms have to be ${\bar{x}}$-guarded, because
$x_{1}\mathbin{|}x_{2}$ is not guarded and obviously not closed under unions.
Furthermore, it is clear that the variables among ${\bar{x}}$ must not be
quantified. This points out the necessity of conditions (1) and (2) of
Definition 6. In the next example we demonstrate that neither restriction of
condition (3) can be dropped.

$a$$b$$c$$a_{+}$$a_{-}$$b_{+}$$b_{-}$$c_{+}$$c_{-}$$P$$P$$P$$Q$$Q$$Q$$a$$b$$c$$a_{+}$$a_{-}$$b_{+}$$b_{-}$$c_{+}$$c_{-}$
Figure 2. The structures $\mathfrak{A}$ and $\mathfrak{B}$. The structure
$\mathfrak{A}=(V,E^{\mathfrak{A}},F^{\mathfrak{A}},P^{\mathfrak{A}},Q^{\mathfrak{A}})$
on the left side uses two different kinds of edges: the dashed edges belong to
$F$, while the other are $E$-edges. Furthermore, $\mathfrak{A}$ exhibits two
predicates $P,Q$. The structure $\mathfrak{B}=(V,E^{\mathfrak{B}})$ depicted
on the right is just a directed graph. Please notice that both structures are
using the same universe $V$.

Consider the structures $\mathfrak{A}$ and $\mathfrak{B}$ drawn in Figure 2
and the following formulae:

$\displaystyle\varphi(x)\coloneqq\,$ $\displaystyle\exists y\exists z(Fxy\land
Fxz\land
xy\mathbin{|}xz\land[(Py\land\vartheta(x))\lor(Qy\land\vartheta(x))])$
$\displaystyle\text{where }\vartheta(x)\coloneqq\exists v(Exv\land v\subseteq
x)$ $\displaystyle\psi(x)\coloneqq\,$ $\displaystyle\exists y\exists
z(Exy\land Exz\land xy\mathbin{|}xz\land\exists w(Eyw\land x\subseteq w))$

Neither $\varphi(x)$ nor $\psi(x)$ is $x$-myopic, because the inclusion atom
$v\subseteq x$ from $\vartheta$ occurs inside the scope of a disjunction (and
it is not $x$-guarded), while the atom $x\subseteq w$ is neither $x$-guarded
nor of the form that is allowed outside the scope of disjunctions, because $x$
appears on the wrong side of the inclusion atom.

Let us take a moment to explain these formulae on an intuitive level. We will
evaluate $\varphi$ on $\mathfrak{A}$ in a team which assigns to $x$ values
from $\\{a,b,c\\}$. There the formula states that one has to pick for every
value of $x$ precisely one $F$-successor as a value for $y$, which is enforced
by the exclusion atom. At $a$ and $c$ this choice is meaningless, because only
the label ($P$ or $Q$) is relevant. Further, due to $\vartheta$, we must have
made the same “choice” ($P$ or $Q$) for the vertex $b$, as we have made for
the other vertices. In other words, the presence of $a$ compels to pick
$b_{+}$ while the presence of $c$ forces $b_{-}$. Similarly, $\psi$, in the
context of $\mathfrak{B}$, states that for every vertex among $\\{a,b,c\\}$
one successor can be chosen such that the neighbourhoods of the chosen
successors cover the initial set of vertices. Notice that the relevant choice
is made for the vertex $b$, which may move towards $a$, if $a$ is present in
the team, or to $c$ otherwise. The other vertices found in the graphs are only
there for technical reasons.

For every $v\in V$ let $s_{v}\colon\\{x\\}\to V$ be the assignment with
$s_{v}(x)\coloneqq v$. We define the teams $X_{1}\coloneqq\\{s_{a},s_{b}\\}$,
$X_{2}\coloneqq\\{s_{b},s_{c}\\}$ and $X\coloneqq X_{1}\cup
X_{2}=\\{s_{a},s_{b},s_{c}\\}$. It is not difficult to verify that
$\mathfrak{A}\vDash_{X_{i}}\varphi(x)$ and $\mathfrak{B}\vDash_{X_{i}}\psi(x)$
for $i=1,2$ but $\mathfrak{A}\nvDash_{X}\varphi(x)$ and
$\mathfrak{B}\nvDash_{X}\psi(x)$. In particular, neither $\varphi(x)$ nor
$\psi(x)$ is closed under unions. This shows that the restrictions of
Definition 6 are indeed necessary.

Thus the atoms allowed in Definition 6 are sufficient to capture the union
closed fragment of $\operatorname{FO}(\subseteq,{}\mathbin{|}{})$. On the
contrary, one may ask whether the set of atoms given in Definition 6 is
necessary. Let us argue for all rules of Definition 6.

Assume that all exclusion atoms are forbidden. Then every formula is already
in inclusion logic in which one cannot define every union closed property as
was shown by Galliani and Hella [GH13, p. 16].

If inclusion atoms were only allowed in the form
${\bar{x}}{\bar{y}}\subseteq{\bar{x}}{\bar{z}}$, that means the atoms