fullproofs

# A Functional (Monadic) Second-Order Theory of Infinite Trees

Anupam Das  DIKU – University of Copenhagen<EMAIL_ADDRESS>and  Colin
Riba  LIP – ENS de Lyon<EMAIL_ADDRESS>
(Date: August 27, 2024)

###### Abstract.

This paper presents a complete axiomatization of Monadic Second-Order Logic
($\mathsf{MSO}$) over infinite trees. $\mathsf{MSO}$ on infinite trees is a
rich system, and its decidability (“Rabin’s Tree Theorem”) is one of the most
powerful known results concerning the decidability of logics.

By a complete axiomatization we mean a complete deduction system with a
polynomial-time recognizable set of axioms. By naive enumeration of formal
derivations, this formally gives a proof of Rabin’s Tree Theorem. The
deduction system consists of the usual rules for second-order logic seen as
two-sorted first-order logic, together with the natural adaptation In
addition, it contains an axiom scheme expressing the (positional) determinacy
of certain parity games.

The main difficulty resides in the limited expressive power of the language of
$\mathsf{MSO}$. We actually devise an extension of $\mathsf{MSO}$, called
_Functional (Monadic) Second-Order Logic_ ($\mathsf{FSO}$), which allows us to
uniformly manipulate (hereditarily) finite sets and corresponding labeled
trees, and whose language allows for higher abstraction than that of
$\mathsf{MSO}$.

##  1\. Introduction

This paper presents a complete axiomatization of Monadic Second-Order Logic
($\mathsf{MSO}$) over infinite trees. $\mathsf{MSO}$ on infinite trees is a
rich system which contains non trivial mathematical theories (see e.g. [Rab69,
BGG97]) and subsumes many logics, including modal logics (see e.g. [BdRV02])
and logics for verification (see e.g. [VW08]). Rabin’s Tree Theorem [Rab69],
the decidability of $\mathsf{MSO}$ on infinite trees, is one of the most
powerful known results concerning the decidability of logics (see e.g.
[BGG97]).

The original decidability proof of [Rab69] relied on an effective translation
of formulae to finite state automata running on infinite trees. Since then,
there has been considerable work on Rabin’s Tree Theorem, culminating in
streamlined decidability proofs, as presented e.g. in [Tho97, GTW02, PP04].
Most current approaches to $\mathsf{MSO}$ on infinite trees (with the notable
exception of [Blu13]) are based on translations of formulae to automata.

By a complete axiomatization we mean a complete deduction system with a
polynomial-time recognizable set of axioms. By naive enumeration of formal
derivations, this formally gives a proof of Rabin’s Tree Theorem. The
deduction system consists in the usual rules for second-order logic seen as
two-sorted first-order logic (see e.g. [Rib12]), together with the natural
adaptation to infinite trees of the axioms of $\mathsf{MSO}$ on $\omega$-words
[Sie70]. In addition, it contains an axiom scheme expressing the (positional)
determinacy of certain parity games.

We continue a line of work begun by Büchi and Siefkes, who gave
axiomatizations of $\mathsf{MSO}$ on various classes of linear orders (see
e.g. [Sie70, BS73]). These works essentially rely on formalizations of
automata in the logic. A major result in the axiomatic treatment of logics
over infinite structures is Walukiewicz’s proof of completeness of Kozen’s
axiomatization of the modal $\mu$-calculus [Wal00] (see also [AL17] for an
alternative recent proof of this result). Another trend relies on model-
theoretic techniques. For instance [tCF10, GtC12] give complete
axiomatizations of $\mathsf{MSO}$ and the modal $\mu$-calculus over finite
trees; a reworking of the completeness of $\mathsf{MSO}$ on $\omega$-words
[Sie70] is proposed in [Rib12]; and [SV10] gives a model-theoretic
completeness proof for a fragment of the modal $\mu$-calculus. An attractive
feature of model-theoretic completeness proofs for the aforementioned logics
is that they allow elegant reformulations of algebraic approaches to these
logics. Unfortunately, in the case of $\mathsf{MSO}$ over infinite trees, the
only known algebraic approach [Blu13] seems too complex to be easily
formalized. We therefore directly formalize a translation of formulae to
automata in the axiomatic theory.

Mirroring usual automata based decidability proofs (see e.g. [Tho97, GTW02,
PP04]), our method for proving completeness proceeds in two steps. We first
formalize a translation of $\mathsf{MSO}$-formulae to tree automata (using the
positional determinacy of parity games to prove the complementation lemma), so
that each closed formula is provably equivalent to an automaton over the
singleton alphabet. The second (and much shorter) step is a variant of the
Büchi-Landweber Theorem [BL69] which states that $\mathsf{MSO}$ decides
winning for (definable) games of finite graphs, and which is obtained thanks
to the completeness of $\mathsf{MSO}$ over $\omega$-words.

The main expositional difficulty resides in the limited expressive power of
the language of $\mathsf{MSO}$. To ameliorate this we actually devise an
extension of $\mathsf{MSO}$, called _Functional (Monadic) Second-Order Logic_
($\mathsf{FSO}$), allowing uniform manipulation of (hereditarily) finite sets
and corresponding labeled infinite trees. We intuitively see $\mathsf{FSO}$ as
providing a language for higher abstraction than that of $\mathsf{MSO}$,
allowing a uniform formalization of automata and games which would have been
difficult to write down in $\mathsf{MSO}$. However, since $\mathsf{FSO}$ is
interpretable in $\mathsf{MSO}$ (as we show), its language has the same
intrinsic limitations as the language of $\mathsf{MSO}$. In particular it
suffers from the inexpressibility of choice over tree positions [GS83, CL07],
and so predicates such as length comparison of tree positions are not
expressible in $\mathsf{FSO}$. This implies that only positional strategies
(w.r.t. our specific notion of acceptance games), are expressible in
$\mathsf{FSO}$ and moreover that usually unproblematic reasoning on infinite
plays can become cumbersome in this setting.

There are several ways to translate $\mathsf{MSO}$ to tree automata. We choose
to translate formulae to alternating parity automata, following [Wal02]. The
two non-trivial steps in the translation are negation and (existential)
quantification. Negation requires the complementation of automata, relying on
the determinacy of acceptance games, while existential quantifiers require us
to simulate an alternating automaton by an equivalent non-deterministic one
(this is the _Simulation Theorem_ [EJ91, MS95]), thence obtaining an automaton
computing the appropriate projection.

As usual with translations of $\mathsf{MSO}$ to tree automata, we rely on
McNaughton’s Theorem [McN66] (see also e.g. [Tho90, PP04]), stating that non-
deterministic Büchi automata on $\omega$-words are effectively equivalent to
deterministic _parity_ (or Muller, Rabin, Streett) automata on $\omega$-words.
In translations of $\mathsf{MSO}$ to alternating tree automata, McNaughton’s
Theorem is usually invoked for the Simulation Theorem.111The approach of
[MS95] to the Simulation Theorem actually contains a proof of McNaughton
Theorem, but we do not see how to easily formalize it in our context. In our
context, the relevant instances of McNaughton’s Theorem are imported into
$\mathsf{FSO}$ via the completeness of $\mathsf{MSO}$ on $\omega$-words
[Sie70].

It is well-known that the $\mathsf{MSO}$ theory of $k$-ary trees can be
embedded in that of the binary tree [Rab69]. However, it does not seem that
such an embedding yields an axiomatization of $k$-ary trees from an
axiomatization of the binary tree. Therefore, in this work, we axiomatize the
$\mathsf{MSO}$ theory of the full infinite $\mathscr{D}$-ary tree for an
arbitrary non-empty finite set $\mathscr{D}$.

This paper is a corrected version of [DR15], which contains a flaw in the
positional determinacy argument (Thm. VI.15). In the present paper, we augment
the systems $\mathsf{FSO}$ and $\mathsf{MSO}$ with an axiom expressing the
positional determinacy of parity games, thereby obtaining complete
axiomatizations. We do not know yet whether the theory $\mathsf{MSO}$ of
[DR15] is complete.

### Outline.

The paper is organized as follows. We present the basic formal theory for
$\mathsf{MSO}$ in §2 Our theory $\mathsf{FSO}$ is then presented in §3 and we
sketch its mutual interpretability with $\mathsf{MSO}$. §4 and §5 discuss a
formalization of two-players infinite games in $\mathsf{FSO}$, and, in
particular, we give a formulation of the axiom $(\mathit{PosDet})$ of
positional determinacy of parity games. This provides us with the required
tools to formalize in §6 (alternating) tree automata, acceptance games and
basic operations on them (including complementation in
$\mathsf{FSO}+(\mathit{PosDet})$). §7 is an interlude discussing a complete
theory of $\mathsf{MSO}$ over $\omega$-words within the infinite paths of
$\mathsf{FSO}$. Building on §6 and §7, we then give our completeness argument
for $\mathsf{FSO}+(\mathit{PosDet})$ and $\mathsf{MSO}+(\mathit{PosDet})$ in
§8. Finally, §9 contains a proof of the Simulation Theorem in $\mathsf{FSO}$.
The full version [DR19] gives details of proofs omitted here.

##  2\. Preliminaries: $\mathsf{MSO}$ on Infinite Trees as a Second-Order
Logic

We present here a basic formal theory of _Monadic Second-Order Logic_
($\mathsf{MSO}$) over infinite trees. In order to obtain a complete theory,
$\mathsf{MSO}$ will be augmented with an axiom of positional determinacy of
parity games (see §3.6, §5.6 and §8).

We are going to define the theory ${\mathsf{MSO}_{\mathscr{D}}}$ of the
infinite full $\mathscr{D}$-ary tree $\mathscr{D}^{*}$, for $\mathscr{D}$ a
finite non-empty set. Both the language and the axioms of
${\mathsf{MSO}_{\mathscr{D}}}$ will depend on $\mathscr{D}$. The language of
${\mathsf{MSO}_{\mathscr{D}}}$ is the usual language of two-sorted first-order
logic, with one sort for _Individuals_ and one sort for _(Monadic)_
_Predicates_. The axioms of ${\mathsf{MSO}_{\mathscr{D}}}$ are the expected
axioms on the relational structure of the full $\mathscr{D}$-ary tree,
together with induction and comprehension.

We fix for the rest of this Section a finite non-empty set $\mathscr{D}$ of
_tree directions_.

###  2.1. The Language of ${\mathsf{MSO}_{\mathscr{D}}}$

The language of ${\mathsf{MSO}_{\mathscr{D}}}$ has two sorts:

  * •

The sort of _Individuals_ , intended to range over tree positions
$p\in\mathscr{D}^{*}$. We have infinitely many Individual variables $x,y,z$
etc. We also have one constant symbol $\dot{\varepsilon}$ (for the root of
$\mathscr{D}^{*}$), and one unary function symbol $\mathsf{S}_{d}$ for each
$d\in\mathscr{D}$ (for the successor function $p\mapsto p.d$). Individual
terms, written $t,u,\text{etc}.$ are given by:

$t\quad\mathrel{::=}\quad
x\quad|\quad\dot{\varepsilon}\quad|\quad\mathsf{S}_{d}(t)$ (for
$d\in\mathscr{D}$)

  * •

The sort of _(Monadic) Predicates_ , with variables $X,Y,Z,\text{etc}$,
intended to range over sets of tree positions
$A\in\mathcal{P}(\mathscr{D}^{*})$. There are no other term formers for this
sort.

Formulae of ${\mathsf{MSO}_{\mathscr{D}}}$ are given by the following grammar:

$\varphi,\psi\in\bm{\Lambda}_{\mathscr{D}}\quad\mathrel{::=}\quad
X(t)\quad|\quad t\mathrel{\doteq}u\quad|\quad
t\mathrel{\dot{<}}u\quad|\quad(\varphi\lor\psi)\quad|\quad\lnot\varphi\quad|\quad(\exists
x)\varphi\quad|\quad(\exists X)\varphi$

where $t$ is an Individual term. We use the usual derived formulae:

$\begin{array}[]{r !{~~\deq~~} l !{\qquad} r !{~~\deq~~} l}(\forall
x)\varphi\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &\lnot(\exists
x)(\lnot\varphi)&\varphi\land\psi\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lnot(\lnot\varphi\lor\lnot\psi)\\\ (\forall
X)\varphi\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &\lnot(\exists
X)(\lnot\varphi)&\varphi\Rightarrow\psi\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lnot\varphi\lor\psi\\\ \top\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&(\forall x)(x\mathrel{\doteq}x)&\bot\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lnot\top\\\ (t\mathrel{\dot{\leq}}u)\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&(t\mathrel{\dot{<}}u)\lor(t\mathrel{\doteq}u)\end{array}$

We employ usual writing conventions for formulae, for instance omitting
internal and external brackets when appropriate.

###  2.2. The Deduction System of ${\mathsf{MSO}_{\mathscr{D}}}$

Deduction for ${\mathsf{MSO}_{\mathscr{D}}}$ is defined by the system
presented on Figure 1 and Figure 2 (where $\Phi$ stands for a multiset of
formulae), together with the following axioms.

  * •

_Equality on Individuals:_

$(\forall x)(x\mathrel{\doteq}x)\qquad\text{and}\qquad(\forall x)(\forall
y)\big{(}x\mathrel{\doteq}y\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi[x/z]\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \varphi[y/z]\big{)}$
(for each $\varphi$)

  * •

The _Tree Axioms_ of Figure 3.

  * •

_Comprehension Scheme:_

$(\exists X)(\forall y)\big{[}X(y)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longleftrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \varphi\big{]}$
(for each $\varphi$, with $X$ not free in $\varphi$)

  * •

_Induction Axiom:_

$(\forall X)\left(X(\dot{\varepsilon})\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\mathord{\mathop{\bigwedge}}_{d\in\mathscr{D}}(\forall
y)\big{[}X(y)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
X(\mathsf{S}_{d}(y))\big{]}\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\forall
y)X(y)\right)$

$\begin{array}[]{c !{\qquad} c !{\qquad}
c}\dfrac{}{\Phi\vdash\varphi\lor\lnot\varphi}&\dfrac{}{\Phi,\varphi\vdash\varphi}&\dfrac{\Phi\vdash\varphi\qquad\Phi\vdash\lnot\varphi}{\Phi\vdash\psi}\\\
\\\
\dfrac{\Phi\vdash\varphi}{\Phi\vdash\varphi\lor\psi}&\dfrac{\Phi\vdash\psi}{\Phi\vdash\varphi\lor\psi}&\dfrac{\Phi\vdash\varphi\lor\psi\qquad\Phi,\varphi\vdash\vartheta\qquad\Phi,\psi\vdash\vartheta}{\Phi\vdash\vartheta}\\\\[10.00002pt]
\end{array}$

Figure 1. Deduction Rules for Propositional Logic

$\begin{array}[]{c}\dfrac{\Phi\vdash\varphi[t/x]}{\Phi\vdash(\exists
x)\varphi}\qquad\qquad\dfrac{\Phi\vdash(\exists
x)\varphi\qquad\Phi,\varphi\vdash\psi}{\Phi\vdash\psi}\leavevmode\nobreak\
\text{($x$ not free in $\Phi,\psi$)}\\\ \\\
\dfrac{\Phi\vdash\varphi[Y/X]}{\Phi\vdash(\exists
X)\varphi}\qquad\qquad\dfrac{\Phi\vdash(\exists
X)\varphi\qquad\Phi,\varphi\vdash\psi}{\Phi\vdash\psi}\leavevmode\nobreak\
\text{($X$ not free in $\Phi,\psi$)}\\\\[10.00002pt] \end{array}$

Figure 2. Deduction Rules for Predicate Logic

######  Remark 1.

As usual, one can derive
$\vdash(\varphi\Rightarrow\psi\Rightarrow\vartheta)\leavevmode\nobreak\
\Leftrightarrow\leavevmode\nobreak\ ((\varphi\land\psi)\Rightarrow\vartheta)$
and we have the _Deduction Theorem_ :

$\Phi,\varphi\vdash\psi\qquad\text{iff}\qquad\Phi\vdash\varphi\Rightarrow\psi$

Indeed, if $\Phi,\varphi\vdash\psi$, then one gets
$\Phi\vdash\lnot\varphi\lor\psi$ by $\lor$-Elimination on the Excluded Middle
$\Phi\vdash\varphi\lor\lnot\varphi$. Conversely, if
$\Phi\vdash\lnot\varphi\lor\psi$, then one gets $\Phi,\varphi\vdash\psi$ by
$\lor$-Elimination. One similarly obtains the _Modus Ponens_ as a derived rule

$\dfrac{\Phi\vdash\psi\Rightarrow\varphi\qquad\Phi\vdash\psi}{\Phi\vdash\varphi}$

$\begin{array}[]{c !{\qquad\quad} c}\lnot(\exists x)\mathop{\bigvee}_{d\neq
d^{\prime}}\big{(}\mathsf{S}_{d}(x)\mathrel{\doteq}\mathsf{S}_{d^{\prime}}(x)\big{)}&(\forall
x)(\forall
y)\mathop{\bigwedge}_{d\in\mathscr{D}}\big{(}\mathsf{S}_{d}(x)\mathrel{\doteq}\mathsf{S}_{d}(y)\leavevmode\nobreak\
\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
x\mathrel{\doteq}y\big{)}\\\ \\\ \lnot(\exists
x)\big{(}x\mathrel{\dot{<}}x\big{)}&(\forall x)(\forall y)(\forall
z)\big{(}x\mathrel{\dot{<}}y\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
y\mathrel{\dot{<}}z\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
x\mathrel{\dot{<}}z\big{)}\\\ \\\ (\forall
x)\big{(}\dot{\varepsilon}\mathrel{\dot{\leq}}x\big{)}&(\forall x)(\forall
y)\mathop{\bigwedge}_{d\in\mathscr{D}}\big{(}x\mathrel{\dot{<}}\mathsf{S}_{d}(y)\leavevmode\nobreak\
\leavevmode\nobreak\ \Leftrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
x\mathrel{\dot{\leq}}y\big{)}\end{array}$

Figure 3. Tree Axioms of ${\mathsf{MSO}_{\mathscr{D}}}$ and
${\mathsf{FSO}_{\mathscr{D}}}$ (where $(x\mathrel{\dot{\leq}}y)$ stands for
$(x\mathrel{\dot{<}}y\lor x\mathrel{\doteq}y)$)

Henceforth, we write $\mathsf{MSO}$ instead of ${\mathsf{MSO}_{\mathscr{D}}}$
when the set of directions $\mathscr{D}$ is clear from the context.

##  3\. A Functional Extension of $\mathsf{MSO}$ on Infinite Trees

In this Section, we present (bounded) _Functional (Monadic) Second-Order
Logic_ over the full $\mathscr{D}$-ary tree (${\mathsf{FSO}_{\mathscr{D}}}$),
an extension of ${\mathsf{MSO}_{\mathscr{D}}}$ with (hereditarily) _finite
sets_ and bounded quantification over them. As with
${\mathsf{MSO}_{\mathscr{D}}}$ in §2, we will simply write $\mathsf{FSO}$ for
${\mathsf{FSO}_{\mathscr{D}}}$ when $\mathscr{D}$ is irrelevant or clear from
the context.

${\mathsf{FSO}_{\mathscr{D}}}$ is equipped with a basic axiomatization which
will allow us, in §4-§6, to formalize a basic theory of games and automata,
and in particular to state an axiom scheme $(\mathit{PosDet})$ expressing the
positional determinacy of (suitably represented) parity games (§5.6). We will
then show in §8 that ${\mathsf{FSO}_{\mathscr{D}}}+(\mathit{PosDet})$ is
complete.

###  3.1. Motivations and Overview.

Let us first discuss the motivations and guiding principles in the design of
${\mathsf{FSO}_{\mathscr{D}}}$. As usual, within the language of
${\mathsf{MSO}_{\mathscr{D}}}$ presented in §2, we can simulate a labeling of
$\mathscr{D}^{*}$ over a finite non-empty set $\Sigma$

$T:\mathscr{D}^{*}\longrightarrow\Sigma$

There are different ways to achieve this. A possibility is, for say
$\Sigma=\\{\mathtt{a}_{1},\dots,\mathtt{a}_{n}\\}$, to code
$T:\mathscr{D}^{*}\to\Sigma$ using a tuple of Monadic variables
$X_{1},\dots,X_{n}$ such that

$x\in X_{i}\quad\text{iff}\quad T(x)=\mathtt{a}_{i}$ (for $i=1,\dots,n$)

A more succinct coding could be obtained using $\lceil\log n\rceil$ monadic
variables to encode the letter index $i$ of $\mathtt{a}_{i}$ in binary.
However, directly working with such codings would make it cumbersome to
formalize games and automata as presented in this paper. We will therefore
rather work in the system ${\mathsf{FSO}_{\mathscr{D}}}$, which is built
around the following principles:

  1. (1)

${\mathsf{FSO}_{\mathscr{D}}}$ has no primitive notion of _Monadic variables_.
Instead, ${\mathsf{FSO}_{\mathscr{D}}}$ has a primitive notion of _Function
variables_ , of the form

$F:\mathscr{D}^{*}\longrightarrow\Sigma$ ($\Sigma$ a finite set)

  2. (2)

In addition, ${\mathsf{FSO}_{\mathscr{D}}}$ allows us to work _uniformly_ with
arbitrary finite sets. In particular, we have an explicit sort for them,
including terms, variables and quantifications.

  3. (3)

${\mathsf{FSO}_{\mathscr{D}}}$ is faithfully interpretable in
${\mathsf{MSO}_{\mathscr{D}}}$. To this end, all quantifications over finite
sets in ${\mathsf{FSO}_{\mathscr{D}}}$-formulae are required to be bounded.

In particular, there is a syntactic translation $\langle-\rangle$ of
${\mathsf{FSO}_{\mathscr{D}}}$-formulae to
${\mathsf{MSO}_{\mathscr{D}}}$-formulae. The basic idea of this translation is
to interpret finite sets using propositional logic, and to interpret Functions
$F:\mathscr{D}^{*}\to\\{\mathtt{a}_{1},\dots,\mathtt{a}_{n}\\}$ as partitions
$X_{1},\dots,X_{n}$ of $\mathscr{D}^{*}$. But while
${\mathsf{FSO}_{\mathscr{D}}}$ handles free variables over finite sets in a
uniform way, the translation $\langle-\rangle$ only applies to
${\mathsf{FSO}_{\mathscr{D}}}$-formulae without free variables over finite
sets. This means that for an ${\mathsf{FSO}_{\mathscr{D}}}$-formula
$\varphi(k)$ with $k$ a variable over finite sets, for each finite set
$\kappa$ we will have a specific ${\mathsf{MSO}_{\mathscr{D}}}$-formula
$\langle\varphi(\kappa)\rangle$.

Technically, the finite sets of ${\mathsf{FSO}_{\mathscr{D}}}$ will be the
usual _hereditarily_ finite sets.

Let $V_{0}\mathrel{:=}\varnothing$, and
$V_{n+1}\mathrel{:=}\mathcal{P}(V_{n})$ for each $n\in\mathbb{N}$. The set
$V_{\omega}$ of _hereditarily finite_ sets (HF-sets) is defined as

$V_{\omega}\quad\mathrel{:=}\quad\bigcup_{n\in\mathbb{N}}V_{n}$

######  Remark 2.

In the context of this paper, it is useful to note that, as is well-known (see
e.g. [Jec06, Exercise 12.9]), $V_{\omega}$ is a model of $\mathsf{ZFC}^{-}$
(i.e. of $\mathsf{ZFC}$ without the infinity axiom).

We will always assume the finite non-empty set $\mathscr{D}$ of _tree
directions_ to be an $\mathrm{HF}$-set.

The language of ${\mathsf{FSO}_{\mathscr{D}}}$ will have the same sort of
Individuals as ${\mathsf{MSO}_{\mathscr{D}}}$ and a sort for
$\mathrm{HF}$-sets, and its Function variables will be of the form
$F:\mathscr{D}^{*}\to K$ for $K$ a term over $\mathrm{HF}$-sets
($\mathrm{HF}$-term). The design of ${\mathsf{FSO}_{\mathscr{D}}}$ is obtained
as a compromise between the following two conflicting desiderata:

  1. (1)

To be as flexible as possible to allow an easy formalization of games and
automata.

  2. (2)

To be as simple as possible to allow an easy translation to
${\mathsf{MSO}_{\mathscr{D}}}$.

This leads us to two peculiar design choices.

  1. (1)

We have, in addition to the above mentioned sorts, a distinct sort of
_Functions over $\mathrm{HF}$-sets_. This sort contains only constants (so
these functions can not be quantified over), whose purpose is to provide
Skolem functions for those $\forall\exists$ (bounded) statements over
$\mathrm{HF}$-sets which are provable in $\mathsf{ZFC}^{-}$.

  2. (2)

In order to facilitate the translation of ${\mathsf{FSO}_{\mathscr{D}}}$ to
${\mathsf{MSO}_{\mathscr{D}}}$, Function variables, written $(F:K)$ (“$F$ has
codomain $K$”), are not directly allowed in the $\mathrm{HF}$-terms. The
interaction of Functions $(F:K)$ with $\mathrm{HF}$-sets is formally reduced
to atomic formulae of the form,

$F(t)\mathrel{\doteq}L$

The axioms of ${\mathsf{FSO}_{\mathscr{D}}}$ will contain the obvious
adaptation of the Tree Axioms and the Induction Axiom of
${\mathsf{MSO}_{\mathscr{D}}}$. We also have axioms defining the
aforementioned Skolem functions. In addition, the Comprehension Scheme of
${\mathsf{MSO}_{\mathscr{D}}}$ will be replaced by _Functional Choice Axioms_
allowing us to define Functions $F:\mathscr{D}^{*}\to K$ from
$\forall\exists$-statements:

$(\forall x)(\exists k\in K)\varphi(x,k)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\exists F:\mathscr{D}^{*}\to K)(\forall x)\varphi(x,F(x))$

######  Remark 3.

_Functional Choice Axioms_ as above actually amount to _Comprehension_ in
$\mathsf{MSO}$ (§2.2). Such axioms do not create choice predicates for
Individuals, which are known to be undefinable in $\mathsf{MSO}$ [GS83, CL07],
and moreover to break decidability when added to the language of
$\mathsf{MSO}$ [BG00, CL07].

The rest of this Section is organized as follows. The system
${\mathsf{FSO}_{\mathscr{D}}}$ is defined in §3.2-3.4, and its (expected)
interpretation in the standard model of $\mathscr{D}$-ary trees is given in
§3.5. Then in §3.6 we discuss the interpretation of
${\mathsf{FSO}_{\mathscr{D}}}$ in ${\mathsf{MSO}_{\mathscr{D}}}$ and a
straightforward embedding of ${\mathsf{MSO}_{\mathscr{D}}}$ in
${\mathsf{FSO}_{\mathscr{D}}}$. Finally, §3.7 presents notations whose purpose
is to allow some flexibility in the manipulation of functions.

###  3.2. The Language of ${\mathsf{FSO}_{\mathscr{D}}}$

We now formally define the language of ${\mathsf{FSO}_{\mathscr{D}}}$, for
$\mathscr{D}$ an $\mathrm{HF}$-set. It consists of the the following sorts:

  * •

The sort of _Hereditarily finite ( $\mathrm{HF}$) sets_, with infinitely many
$\mathrm{HF}$-variables $k,\ell$ etc., and with one constant symbol
$\dot{\mathsf{\kappa}}$ for each $\kappa\in V_{\omega}$ (we often simply write
$\kappa$ for $\dot{\mathsf{\kappa}}$ in formulae, omitting the overset dot).

  * •

The same sort of _Individuals_ as ${\mathsf{MSO}_{\mathscr{D}}}$ (see §2.1).

  * •

The sort of _Functions_ , with infinitely many variables $F,G,H,\text{etc}$.

  * •

The sort of _$\mathrm{HF}$ -Functions_, with no variable. For each pair
$(n,m)\in\mathbb{N}\times\mathbb{N}$, we assume given a constant symbol
$\dot{\mathsf{g}}_{n,m}$ of arity $n$. The interpretation of these constant
symbols is discussed in §3.4.4.

The language of ${\mathsf{FSO}_{\mathscr{D}}}$ has two kinds of terms. The
_Individual terms_ are the same as those of ${\mathsf{MSO}_{\mathscr{D}}}$. In
addition, ${\mathsf{FSO}_{\mathscr{D}}}$ also has _$\mathrm{HF}$ -terms_,
which are given by

$K,L\quad\mathrel{::=}\quad
k\quad|\quad\dot{\mathsf{\kappa}}\quad|\quad\dot{\mathsf{g}}_{n,m}(L_{1},\dots,L_{n})$

The _formulae_ of ${\mathsf{FSO}_{\mathscr{D}}}$ are built as follows:

$\begin{array}[]{r r
l}\varphi,\psi&\mathrel{::=}&t\mathrel{\doteq}u\quad|\quad
t\mathrel{\dot{<}}u\\\ &\quad|&K\mathrel{\doteq}L\quad|\quad
K\mathrel{\dot{\in}}L\quad|\quad K\mathrel{\dot{\subseteq}}L\quad|\quad
F(t)\mathrel{\doteq}K\\\ &\quad|&\varphi\lor\psi\quad|\quad\lnot\varphi\\\
&\quad|&(\exists x)\varphi\quad|\quad(\exists F:K)\varphi\quad|\quad(\exists
k\mathrel{\dot{\in}}L)\varphi\quad|\quad(\exists
k\mathrel{\dot{\subseteq}}L)\varphi\end{array}$

An ${\mathsf{FSO}_{\mathscr{D}}}$-formula $\varphi$ is _$\mathrm{HF}$ -closed_
if it contains no free $\mathrm{HF}$-variable.

  1. (1)

Usual derived formulae are defined similarly as with $\mathsf{MSO}$ (where
$\mathrel{\star}$ is either $\mathrel{\dot{\in}}$ or
$\mathrel{\dot{\subseteq}}$):

$\begin{array}[]{r !{~~\deq~~} l !{\qquad} r !{~~\deq~~} l}(\forall
x)\varphi\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &\lnot(\exists
x)(\lnot\varphi)&\varphi\land\psi\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lnot(\lnot\varphi\lor\lnot\psi)\\\ (\forall
F:L)\varphi\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &\lnot(\exists
F:L)(\lnot\varphi)&\varphi\Rightarrow\psi\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lnot\varphi\lor\psi\\\ (\forall
k\mathrel{\star}L)\varphi\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &\lnot(\exists
k\mathrel{\star}L)(\lnot\varphi)&(t\mathrel{\dot{\leq}}u)\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&(t\mathrel{\dot{<}}u)\lor(t\mathrel{\doteq}u)\\\
\top\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &(\forall
x)(x\mathrel{\doteq}x)&\bot\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lnot\top\end{array}$

  2. (2)

As well as when we quantify over Functions, we use the notation $(F:K)$ within
formulae as the defined formula:

$(F:K)\quad\mathrel{:=}\quad(\forall x)(\exists
k\mathrel{\dot{\in}}K)(F(x)\mathrel{\doteq}k)$

  3. (3)

For variables $\bm{K}=K_{1},\dots,K_{n}$ and $\bm{L}=L_{1},\dots,L_{n}$, and
$\mathrel{\star}$ either $\mathrel{\doteq}$, $\mathrel{\dot{\in}}$ or
$\mathrel{\dot{\subseteq}}$, we let

$\bm{K}\mathrel{\star}\bm{L}\quad=\quad(K_{1},\dots,K_{n})\mathrel{\star}(L_{1},\dots,L_{n})\quad\mathrel{:=}\quad\mathop{\bigwedge}_{1\leq
i\leq n}K_{i}\mathrel{\star}L_{i}$

######  Remark 4.

The (hereditarily) finite set $\mathscr{D}$ of tree directions is considered
both as a parameter in the definition of ${\mathsf{FSO}_{\mathscr{D}}}$, via
the successor term constructors $\mathsf{S}_{d}$ (for $d\in\mathscr{D}$) and
the corresponding axioms (see §3.4), and as a (constant) $\mathrm{HF}$ set,
which can occur as such in ${\mathsf{FSO}_{\mathscr{D}}}$ formulae. Strictly
speaking, we should write $\dot{\mathsf{\mathscr{D}}}$ rather than
$\mathscr{D}$ in the latter case, but we usually simply omit the overset dot,
as with other HF-sets.

###  3.3. The Deduction System of ${\mathsf{FSO}_{\mathscr{D}}}$

Deduction for ${\mathsf{FSO}_{\mathscr{D}}}$ is defined by the system
presented on Figure 1 (with ${\mathsf{FSO}_{\mathscr{D}}}$ formulae instead of
${\mathsf{MSO}_{\mathscr{D}}}$ formulae) and Figure 4, together with all the
axioms of §3.4.

$\begin{array}[]{c}\dfrac{\bm{\varphi}\vdash\varphi[t/x]}{\bm{\varphi}\vdash(\exists
x)\varphi}\qquad\qquad\dfrac{\bm{\varphi}\vdash(\exists
x)\varphi\qquad\bm{\varphi},\varphi\vdash\psi}{\bm{\varphi}\vdash\psi}\leavevmode\nobreak\
\leavevmode\nobreak\ \text{($x$ not free in $\bm{\varphi},\psi$)}\\\ \\\
\dfrac{\bm{\varphi}\vdash\varphi[G/F]\qquad\bm{\varphi}\vdash(G:K)}{\bm{\varphi}\vdash(\exists
F:K)\varphi}\quad\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \,\dfrac{\bm{\varphi}\vdash(\exists
F:K)\varphi\qquad\bm{\varphi},\,(F:K),\,\varphi\vdash\psi}{\bm{\varphi}\vdash\psi}\leavevmode\nobreak\
\text{($F$ not free in $\bm{\varphi},\psi$)}\\\ \\\
\dfrac{\bm{\varphi}\vdash\varphi[K/k]\qquad\bm{\varphi}\vdash
K\mathrel{\star}L}{\bm{\varphi}\vdash(\exists
k\mathrel{\star}L)\varphi}\leavevmode\nobreak\ \leavevmode\nobreak\ \text{(for
$\mathrel{\star}$ either $\mathrel{\dot{\in}}$ or
$\mathrel{\dot{\subseteq}}$)}\\\ \\\ \dfrac{\bm{\varphi}\vdash(\exists
k\mathrel{\star}K)\varphi\qquad\bm{\varphi},\,k\mathrel{\star}K,\,\varphi\vdash\psi}{\bm{\varphi}\vdash\psi}\leavevmode\nobreak\
\leavevmode\nobreak\ \text{(for $\mathrel{\star}$ either $\mathrel{\dot{\in}}$
or $\mathrel{\dot{\subseteq}}$, and $k$ not free in $\bm{\varphi},\psi$)}\\\
\\\
\dfrac{\bm{\varphi}\vdash\varphi}{\bm{\varphi}[F(t)/k]\vdash\varphi[F(t)/k]}\leavevmode\nobreak\
\leavevmode\nobreak\ \text{($\bm{\varphi}[F(t)/k],\varphi[F(t)/k]$
$\mathsf{FSO}$-formulae)}\\\\[10.00002pt] \end{array}$

Figure 4. Deduction Rules for ${\mathsf{FSO}_{\mathscr{D}}}$

draftnotes

###  3.4. Basic Axiomatization

We now present the axioms of ${\mathsf{FSO}_{\mathscr{D}}}$. The first group
(Equality, Tree Axioms and Induction, §3.4.1-§3.4.2) corresponds to its
counterpart in ${\mathsf{MSO}_{\mathscr{D}}}$. We then present our specific
axioms for $\mathrm{HF}$-Sets in §3.4.4 and our Functional Choice Axioms in
§3.4.5.

####  3.4.1. Equality

The theory ${\mathsf{FSO}_{\mathscr{D}}}$ has usual equality axioms for
individuals and $\mathrm{HF}$-Sets.

  * •

_Equality on Individuals._

$(\forall x)(x\mathrel{\doteq}x)\qquad\text{and}\qquad(\forall x)(\forall
y)\big{(}x\mathrel{\doteq}y\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi[x/z]\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \varphi[y/z]\big{)}$
(for all formula $\varphi$)

  * •

_Equality on $\mathrm{HF}$-Sets_ (for all formula $\varphi$, all
$\mathrm{HF}$-terms $K,L$ and all $\mathrm{HF}$-variable $m$):

$K\mathrel{\doteq}K\qquad\text{and}\qquad\left(K\mathrel{\doteq}L\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi[K/m]\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \varphi[L/m]\right)$

######  Remark 5.

Note that ${\mathsf{FSO}_{\mathscr{D}}}$ is equipped with an explicit
_Substitution Rule_

$\dfrac{\Phi\vdash\varphi}{\Phi[F(t)/k]\vdash\varphi[F(t)/k]}$
($\Phi[F(t)/k],\varphi[F(t)/k]$ $\mathsf{FSO}$-formulae)

Substitution entails the following (where $\varphi(F(t))$ is an
$\mathsf{FSO}$-formula):

$(F(t)\mathrel{\doteq}K)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi(K)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \varphi(F(t))$

as well as the derived rule

$\dfrac{\Phi\vdash\varphi(F(t))\qquad\bm{\varphi}\vdash(F:K)}{\Phi\vdash(\exists
k\mathrel{\dot{\in}}K)\varphi(k)}$

The former is a direct consequence of the Substitution rule together with
elimination of equality on $\mathrm{HF}$-Sets. For the latter, first note that
Remark 1 also holds for ${\mathsf{FSO}_{\mathscr{D}}}$. In particular, one can
derive

$(k\mathrel{\dot{\in}}K)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi(k)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\exists
k\mathrel{\dot{\in}}K)\varphi(k)$

On the other hand, we have

$(\exists\ell\mathrel{\dot{\in}}K)(k\mathrel{\doteq}\ell)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(k\mathrel{\dot{\in}}K)$

We therefore get

$(\exists\ell\in K)(k\mathrel{\doteq}\ell)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi(k)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\exists
k\mathrel{\dot{\in}}K)\varphi(k)$

and the Substitution rule gives

$(\exists\ell\in K)(F(t)\mathrel{\doteq}\ell)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi(F(t))\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\exists
k\mathrel{\dot{\in}}K)\varphi(k)$

∎

####  3.4.2. Induction

We have the following _Induction Scheme_ :

$\varphi(\dot{\varepsilon})\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\mathord{\mathop{\bigwedge}}_{d\in\mathscr{D}}(\forall
x)\big{[}\varphi(x)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi(\mathsf{S}_{d}(x))\big{]}\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\forall
x)\varphi(x)$ (for each formula $\varphi$)

####  3.4.3. Tree Axioms

For the tree structure of $\mathscr{D}^{*}$, we have the same Tree Axioms as
${\mathsf{MSO}_{\mathscr{D}}}$, displayed in Figure 3 (recall that
${\mathsf{FSO}_{\mathscr{D}}}$ has the same Individuals as
${\mathsf{MSO}_{\mathscr{D}}}$).

We now state expected results on the axioms so far introduced. To this end,
let ${\mathsf{FSO}_{\mathscr{D}}^{0}}$ be the system consisting of the
deduction rules of Figures 1 and 4, together with the Equality Axioms (§3.4.1)
the Induction Scheme (§3.4.2) and the Tree Axioms (Figure 3).

######  Proposition 6.

${\mathsf{FSO}_{\mathscr{D}}^{0}}$ proves the following.

  1. (1)

$(\forall x)(\forall
y)(x\mathrel{\dot{\leq}}y\mathrel{\dot{\leq}}x\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
x\mathrel{\doteq}y)$

  2. (2)

$(\forall x)(x\mathrel{\dot{\leq}}\dot{\varepsilon}\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
x\mathrel{\doteq}\dot{\varepsilon})$

  3. (3)

$\lnot(\exists x)(x\mathrel{\dot{<}}\dot{\varepsilon})$

  4. (4)

$\lnot(\exists x)(\mathsf{S}_{d}(x)\mathrel{\doteq}\dot{\varepsilon})$

  5. (5)

$(\forall x)(x\mathrel{\doteq}\dot{\varepsilon}\leavevmode\nobreak\
\leavevmode\nobreak\ \lor\leavevmode\nobreak\ \leavevmode\nobreak\ (\exists
y)\lor_{d\in\mathscr{D}}x\mathrel{\doteq}\mathsf{S}_{d}(y))$

  6. (6)

$(\forall x)(\forall y)(x\mathrel{\dot{<}}y\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\lor_{d\in\mathscr{D}}\mathsf{S}_{d}(x)\mathrel{\dot{\leq}}y)$

A consequence of Proposition 6 is that the Induction Scheme of
${\mathsf{FSO}_{\mathscr{D}}}$ (§3.4.2) implies the usual scheme of _Well-
Founded Induction_ w.r.t. the strict prefix order $\mathrel{\dot{<}}$.

######  Theorem 7 (Well-Founded Induction).

${\mathsf{FSO}_{\mathscr{D}}^{0}}$ proves the following form of well-founded
induction:

$(\forall x)\big{[}(\forall
y\mathrel{\dot{<}}x)(\varphi(y))\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi(x)\big{]}\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\forall
x)\varphi(x)$

######  Remark 8.

Both Proposition 6 and Theorem 7 also hold for ${\mathsf{MSO}_{\mathscr{D}}}$.

####  3.4.4. $\mathrm{HF}$-Sets

We now present our axioms on $\mathrm{HF}$-Sets. Their purpose is to ease
formalization in ${\mathsf{FSO}_{\mathscr{D}}}$. Recall that
$\mathrm{HF}$-sets range over $V_{\omega}$ (Definition 3.1). The idea of these
axioms is to incorporate in ${\mathsf{FSO}_{\mathscr{D}}}$ as much of the
theory of $V_{\omega}$ as possible, while keeping
${\mathsf{FSO}_{\mathscr{D}}}$ interpretable in ${\mathsf{MSO}_{\mathscr{D}}}$
and with a semi-recursive notion of provability. The interpretation of
${\mathsf{FSO}_{\mathscr{D}}}$ in ${\mathsf{MSO}_{\mathscr{D}}}$ relies on the
fact that in ${\mathsf{FSO}_{\mathscr{D}}}$-formulae, all quantifications over
$\mathrm{HF}$-Sets are bounded (either by $\mathrel{\dot{\in}}$ or
$\mathrel{\dot{\subseteq}}$), so that in a closed
${\mathsf{FSO}_{\mathscr{D}}}$-formula, quantifications over
$\mathrm{HF}$-Sets can be interpreted using usual propositional logic.

We will have, as particular cases of our axioms on $\mathrm{HF}$-Sets, all
bounded formulae over $\mathrm{HF}$-Sets which are true in $V_{\omega}$.
Moreover, w.r.t. the interpretation of ${\mathsf{FSO}_{\mathscr{D}}}$ in
${\mathsf{MSO}_{\mathscr{D}}}$ (§3.6) and in particular w.r.t. its application
to ${\mathsf{MSO}_{\mathscr{D}}}$ over $\omega$-words (§7, §8 and §9), it is
important to have sufficiently many functions over $V_{\omega}$ available
within _closed_ $\mathrm{HF}$-terms. This is the main purpose of our axioms on
$\mathrm{HF}$-Sets. They state that the $\mathrm{HF}$-Functions
$\dot{\mathsf{g}}_{n,m}$ are Skolem functions for $\forall\exists!$-statements
over $\mathrm{HF}$-Sets. These axioms are further commented in §8.5.

[$\mathrm{HF}$-Formula] An _$\mathrm{HF}$ -formula_ is an
${\mathsf{FSO}_{\mathscr{D}}}$-formula with atoms of the form
$K\mathrel{\doteq}L$, $K\mathrel{\dot{\in}}L$ or $K\mathrel{\dot{\subseteq}}L$
where $K$ and $L$ are $\mathrm{HF}$-terms.

Fix a distinguished $\mathrm{HF}$-variable $\ell$, and an enumeration
$k_{1},k_{2},\dots$ of distinct $\mathrm{HF}$-variables all different from
$\ell$. Furthermore, fix an enumeration $(\varphi_{n,m})_{n,m\in\mathbb{N}}$
of $\mathrm{HF}$-formulae satisfying the following conditions:

  1. (1)

Each formula $\varphi_{n,m}$ has free variables among
$k_{1},\dots,k_{n},\ell$.

  2. (2)

All $\mathrm{HF}$-Functions occurring in $\varphi_{n,m}$ have the form
$\dot{\mathsf{g}}_{n^{\prime},m^{\prime}}$ with $m^{\prime}<m$.

  3. (3)

Each $\mathrm{HF}$-formula $\varphi$ satisfying (1) and (2) occurs infinitely
often in $(\varphi_{n,m})_{n,m\in\mathbb{N}}$, in the following sense. If
$\varphi$ has free variables among $k_{1},\dots,k_{n},\ell$, then there are
infinitely many $m\in\mathbb{N}$ such that $\varphi$ is $\varphi_{n,m}$.

Recall from Remark 2 that $V_{\omega}$ is a model of $\mathsf{ZFC}^{-}$. The
idea of our Axioms on $\mathrm{HF}$-Sets is that

${\mathsf{FSO}_{\mathscr{D}}}\vdash\varphi_{n,m}[\dot{\mathsf{g}}_{n,m}(k_{1},\dots,k_{n})/\ell]\qquad\text{whenever}\qquad\mathsf{ZFC}^{-}\vdash(\forall
k_{1},\dots,k_{n})(\exists!\ell)\varphi_{n,m}$ (1)

(where $(k\mathrel{\dot{\subseteq}}k^{\prime})$ is interpreted as $(\forall
m\mathrel{\dot{\in}}k)(m\mathrel{\dot{\in}}k^{\prime})$). However, recall that
$\varphi_{n,m}$ in (1) may contain $\mathrm{HF}$-Functions
$\dot{\mathsf{g}}_{n^{\prime},m^{\prime}}$ with $m^{\prime}<m$. The premise of
(1) can thus not be formulated in $\mathsf{ZFC}^{-}$, but requires a suitable
extension of it. We let $\mathbf{Sk}(\mathsf{ZFC}^{-})$ consist of
$\mathsf{ZFC}^{-}$ augmented with the axioms

$(\forall k_{1},\dots,k_{n})(\exists!\ell)(\varphi_{n,m})\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\forall
k_{1},\dots,k_{n})\varphi_{n,m}[\dot{\mathsf{g}}_{n,m}(k_{1},\dots,k_{n})/\ell]$
(for each $n,m\in\mathbb{N}$)

draftnotes

It is well-known that $\mathbf{Sk}(\mathsf{ZFC}^{-})$ is thus a conservative
extension of $\mathsf{ZFC}^{-}$ (see e.g. [vD04, §3.4]).
${\mathsf{FSO}_{\mathscr{D}}}$ has the following axiom scheme for
$\mathrm{HF}$-Sets, which simply consists in (1) formulated for
$\mathbf{Sk}(\mathsf{ZFC}^{-})$ rather than $\mathsf{ZFC}^{-}$:

  * •

_Axioms on $\mathrm{HF}$-Sets._ For each $n,m\in\mathbb{N}$ such that

$\mathbf{Sk}(\mathsf{ZFC}^{-})\vdash\quad(\forall
k_{1},\dots,k_{n})(\exists!\ell)\varphi_{n,m}$ (2)

and for all $\mathrm{HF}$-terms $\bm{K}=K_{1},\dots,K_{n}$, we have the axiom

$\varphi_{n,m}[\bm{K}/\bm{k}][\dot{\mathsf{g}}_{n,m}(\bm{K})/\ell]$

######  Remark 9.

Note that this axiom scheme makes the axiom set of
${\mathsf{FSO}_{\mathscr{D}}}$ not recursive. But as expected for a proof
system, _provability_ in ${\mathsf{FSO}_{\mathscr{D}}}$ remains semi-
recursive.

We fix here once and for all an interpretation of the $\mathrm{HF}$-Function
symbols $\dot{\mathsf{g}}_{n,m}$ as functions over $V_{\omega}$. The idea is
that if (2) holds, then $\dot{\mathsf{g}}_{n,m}$ is interpreted as a
computable function $\mathtt{g}_{n,m}:V_{\omega}^{n}\to V_{\omega}$ such that

$V_{\omega}\models\quad(\forall
k_{1},\dots,k_{n})\varphi_{n,m}[\mathtt{g}_{n,m}(k_{1},\dots,k_{n})/\ell]$ (3)

But again recall that $\varphi_{n,m}$ may contain $\mathrm{HF}$-Functions
$\dot{\mathsf{g}}_{n^{\prime},m^{\prime}}$ with $m^{\prime}<m$. We therefore
proceed inductively, as follows.

By induction on $m\in\mathbb{N}$, we interpret the $\mathrm{HF}$-Function
symbols $\dot{\mathsf{g}}_{n,m}$ as computable functions

$\mathtt{g}_{n,m}\leavevmode\nobreak\ \leavevmode\nobreak\
:\leavevmode\nobreak\ \leavevmode\nobreak\ V_{\omega}^{n}\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
V_{\omega}$

Consider the formula $\varphi_{n,m}$, and assume that all
$\mathrm{HF}$-Functions $\dot{\mathsf{g}}_{n^{\prime},m^{\prime}}$ with
$m^{\prime}<m$ are already interpreted. If (2) holds then by the Countable
Axiom of Choice we interpret $\dot{\mathsf{g}}_{n,m}$ as the unique function
$\mathtt{g}_{n,m}:V^{n}_{\omega}\to V_{\omega}$ such that (3) holds. Note that
such functions are computable. Otherwise, we interpret
$\dot{\mathsf{g}}_{n,m}$ as the function with constant value $\varnothing$.

######  Remark 10.

Note each $\mathrm{HF}$-Function symbol is interpreted by a recursive function
in Convention 3.4.4. However, since (2) is undecidable, there is no algorithm
taking $(n,m)\in\mathbb{N}^{2}$ to the interpretation of
$\dot{\mathsf{g}}_{n,m}$. This point is further discussed in §8.5, where a
natural workaround is proposed, as well as some explanations for our present
choice of Axioms on $\mathrm{HF}$-Sets.

We now discuss some consequences of these axioms. First note that if $\varphi$
is a _closed_ $\mathrm{HF}$-formula, then it is provable in
$\mathbf{Sk}(\mathsf{ZFC}^{-})$ if and only if it holds in $V_{\omega}$. We
state this fact as a Remark for the record, and also to reiterate how much
deductive power underlies the axioms on $\mathrm{HF}$-sets.

######  Remark 11.

Given a closed $\mathrm{HF}$-formula $\varphi$,

${\mathsf{FSO}_{\mathscr{D}}}\vdash\varphi\qquad\text{whenever}\qquad
V_{\omega}\models\varphi$

draftnotes

Moreover, we have all instances of the following:

  1. (1)

_Extensionality_.

$(\forall m\mathrel{\dot{\in}}k)(m\mathrel{\dot{\in}}\ell)\leavevmode\nobreak\
\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\forall m\mathrel{\dot{\in}}\ell)(m\mathrel{\dot{\in}}k)\leavevmode\nobreak\
\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
k\mathrel{\doteq}\ell$

  2. (2)

_Finite sets_. For each $n\in\mathbb{N}$ we have an $n$-ary
$\mathrm{HF}$-Function symbol $\\{-,\dots,-\\}$ such that

$\mathop{\bigwedge}_{1\leq i\leq
n}(k_{i}\mathrel{\dot{\in}}\\{k_{1},\dots,k_{n}\\})\quad\land\quad(\forall
m\mathrel{\dot{\in}}\\{k_{1},\dots,k_{n}\\})\mathop{\bigvee}_{1\leq i\leq
n}(m\mathrel{\doteq}k_{i})$

We have in particular singletons $\\{-\\}$ and unordered pairs $\\{-,-\\}$.
Using Extensionality, ${\mathsf{FSO}_{\mathscr{D}}}$ proves that

$\\{\\{k\\},\\{k,\ell\\}\\}\mathrel{\doteq}\\{\\{k^{\prime}\\},\\{k^{\prime},\ell^{\prime}\\}\\}\quad\Longleftrightarrow\quad
k\mathrel{\doteq}k^{\prime}\land\ell\mathrel{\doteq}\ell^{\prime}$

We use the following shorthand:

$(k,\ell)\quad\mathrel{:=}\quad\\{\\{k\\},\\{k,\ell\\}\\}$

  3. (3)

_Union_. We have an $\mathrm{HF}$-Function symbol $\cup(-)$ such that

$(\forall\ell\mathrel{\dot{\in}}\cup(k))(\exists
m\mathrel{\dot{\in}}k)(\ell\mathrel{\dot{\in}}m)\quad\land\quad(\forall\ell\mathrel{\dot{\in}}k)(\forall
m\mathrel{\dot{\in}}\ell)(m\mathrel{\dot{\in}}\cup(k))$

  4. (4)

_Powerset._ We have an $\mathrm{HF}$-Function symbol $\mathcal{P}(-)$ such
that

$(\forall\ell\mathrel{\dot{\in}}\mathcal{P}(k))(\forall
m\mathrel{\dot{\in}}\ell)(m\mathrel{\dot{\in}}k)\quad\land\quad(\forall\ell\mathrel{\dot{\subseteq}}k)(\ell\mathrel{\dot{\in}}\mathcal{P}(k))$

The powerset is the reason for our introduction of inclusion
($\mathrel{\dot{\subseteq}}$) as an atomic formula: It is well-known that the
powerset cannot be defined by a $\Delta_{0}(\mathrel{\dot{\in}})$-formula. A
possible formula defining it is:

$(\forall\ell\mathrel{\dot{\in}}\mathcal{P}(k))(\forall
m\mathrel{\dot{\in}}\ell)(m\mathrel{\dot{\in}}k)\quad\land\quad(\forall\ell)\big{[}(\forall
m\mathrel{\dot{\in}}\ell)(m\mathrel{\dot{\in}}k)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\ell\mathrel{\dot{\in}}\mathcal{P}(k)\big{]}$

The quantification $\forall\ell$ in the right conjunct is not
$\mathrel{\dot{\in}}$-bounded, and cannot be so. In addition, we also have an
$\mathrm{HF}$-Function symbol $\mathcal{P}_{*}(-)$ for the _non-empty
powerset_ , that is such that

$k\mathrel{\dot{\in}}\mathcal{P}_{*}(\ell)\quad\Longleftrightarrow\quad\big{(}k\mathrel{\dot{\in}}\mathcal{P}(\ell)\leavevmode\nobreak\
\land\leavevmode\nobreak\ (\exists m\mathrel{\dot{\in}}k)\big{)}$

  5. (5)

_Comprehension._ Given an $\mathrm{HF}$-formula $\varphi$ with free variables
among $k_{1},\dots,k_{n},k$, we have an $\mathrm{HF}$-Function
$\\{k\mathrel{\dot{\in}}(-)\leavevmode\nobreak\ |\leavevmode\nobreak\
\varphi[-,\dots,-,k]\\}$ such that

$m\mathrel{\dot{\in}}\\{k\mathrel{\dot{\in}}k_{0}\leavevmode\nobreak\
|\leavevmode\nobreak\
\varphi[k_{1},\dots,k_{n},k]\\}\quad\Longleftrightarrow\quad
m\mathrel{\dot{\in}}k_{0}\land\varphi[k_{1},\dots,k_{n},m]$

  6. (6)

_Products._ We have a binary $\mathrm{HF}$-Function $(-)\times(-)$ such that

$k\times\ell\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{m\mathrel{\dot{\in}}\mathcal{P}(\mathcal{P}(k\cup\ell))\leavevmode\nobreak\
|\leavevmode\nobreak\ (\exists
k_{0}\mathrel{\dot{\in}}k)(\exists\ell_{0}\mathrel{\dot{\in}}\ell)\big{[}m\mathrel{\doteq}(k_{0},\ell_{0})\big{]}\right\\}$

Moreover, we have binary projections given by $\mathrm{HF}$-Functions
$\pi_{1}^{-,-}(-)$ and $\pi_{2}^{-,-}(-)$ such that

$\pi_{1}^{k,\ell}(m)\leavevmode\nobreak\ \leavevmode\nobreak\
=\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{n\in\ell\leavevmode\nobreak\ |\leavevmode\nobreak\
m\mathrel{\dot{\subseteq}}k\times\ell\leavevmode\nobreak\
\land\leavevmode\nobreak\ (\exists n^{\prime}\in
k)\big{[}(n,n^{\prime})\mathrel{\dot{\in}}m\big{]}\right\\}$

and similarly for $\pi_{2}^{-,-}(-)$. Whenever possible, we write $\pi_{i}(-)$
instead of $\pi_{i}^{k,\ell}(-)$. Note that by composing binary projections
$\pi_{1}$ and $\pi_{2}$ we obtain projections

$\pi^{n}_{i}\leavevmode\nobreak\ \leavevmode\nobreak\ :\leavevmode\nobreak\
\leavevmode\nobreak\ k_{1}\times\dots\times k_{n}\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
k_{i}$

for any $k_{1},\dots,k_{n}$ and $i\in\\{1,\dots,n\\}$

  7. (7)

_Function Spaces and Application._ We have an exponent $\mathrm{HF}$-Function
$(-)^{(-)}$ such that

$\ell^{k}\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{m\mathrel{\dot{\in}}\mathcal{P}(k\times\ell)\leavevmode\nobreak\
|\leavevmode\nobreak\ (\forall
k_{0}\mathrel{\dot{\in}}k)(\exists!\ell_{0}\mathrel{\dot{\in}}\ell)\big{[}(k_{0},\ell_{0})\mathrel{\dot{\in}}m\big{]}\right\\}$

Moreover, function application is given by the $\mathrm{HF}$-Function
$@_{-,-}(-,-)$ with

$@_{k,\ell}(f,a)\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{m\mathrel{\dot{\in}}\cup(\ell)\leavevmode\nobreak\
|\leavevmode\nobreak\
(\exists\ell_{0}\mathrel{\dot{\in}}\ell)\big{[}m\mathrel{\dot{\in}}\ell_{0}\land(a,\ell_{0})\mathrel{\dot{\in}}f\big{]}\right\\}$

(here $f$ and $a$ are $\mathrm{HF}$-variables). Whenever possible, we omit the
subscripts $k,\ell$ of $@_{k,\ell}(f,a)$ and write simply $f(a)$ for
$@_{k,\ell}(f,a)$.

  8. (8)

_Disjoint Unions._ We have a binary $\mathrm{HF}$-Function $(-)+(-)$ with

$k+\ell\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{\doteq}\leavevmode\nobreak\ \leavevmode\nobreak\ (\\{0\\}\times
k)\cup(\\{1\\}\times\ell)$

(see Convention 5.5 for a further discussion on finite ordinals in our
context). We moreover have $\mathrm{HF}$-Functions
$\mathsf{in}^{k,\ell}_{k}(-)$, $\mathsf{in}^{k,\ell}_{\ell}(-)$, and
$[-,-]_{k,\ell}^{\imath}$ such that (dropping subscripts and superscripts)

$\mathsf{in}(m)\mathrel{\doteq}(0,m)\qquad\mathsf{in}(n)\mathrel{\doteq}(1,n)\qquad[f,g](0,m)\mathrel{\doteq}f(m)\qquad[f,g](1,n)\mathrel{\doteq}g(n)$

for $m\mathrel{\dot{\in}}k$, $\ell\mathrel{\dot{\in}}n$ and
$f\mathrel{\dot{\in}}\imath^{k}$, $g\mathrel{\dot{\in}}\imath^{\ell}$.

draftnotes

Regarding function spaces as in (7) above, ${\mathsf{FSO}_{\mathscr{D}}}$
proves

$(k^{\ell})^{m}\quad\cong\quad k^{\ell\times m}$

In the following, we reason modulo that bijection, and simply identify
$(k^{\ell})^{m}$ with $k^{\ell\times m}$.

######  Remark 12.

An $\mathrm{HF}$-relation $\mathord{\preceq}\subseteq K\times K$ is a _partial
order_ on an $\mathrm{HF}$-term $K$, if the formula $\mathrm{PO}(\preceq,K)$
holds in $V_{\omega}$, where $\mathrm{PO}(\preceq,K)$ is the
$\mathrm{HF}$-formula:

$(\forall
k,\ell,m\mathrel{\dot{\in}}K)\Big{[}\big{(}k\preceq\ell\leavevmode\nobreak\
\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\ell\preceq k\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
k\mathrel{\doteq}\ell\big{)}\leavevmode\nobreak\ \leavevmode\nobreak\
\land\leavevmode\nobreak\ \leavevmode\nobreak\
\big{(}k\preceq\ell\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \ell\preceq
m\leavevmode\nobreak\ \leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\
\leavevmode\nobreak\ k\preceq m\big{)}\Big{]}$

A partial order $\mathord{\preceq}\subseteq K\times K$ is a _well-order_ if
every subset of $K$ has a $\preceq$-least element, that is, if the following
formula $\mathrm{WO}(\preceq,K)$ holds in $V_{\omega}$:

$(\forall\ell\mathrel{\dot{\subseteq}}K)\big{[}\ell\neq\varnothing\leavevmode\nobreak\
\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\exists m\mathrel{\dot{\in}}\ell)(\forall n\mathrel{\dot{\in}}\ell)(m\preceq
n)\big{]}$

Since every $\mathrm{HF}$-set is finite and can be well-ordered, we have

$V_{\omega}\quad\models\quad(\forall
k)\underbrace{(\exists\mathord{\preceq}\mathrel{\dot{\subseteq}}k\times
k)\big{[}\mathrm{PO}(\preceq,k)\leavevmode\nobreak\ \leavevmode\nobreak\
\land\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrm{WO}(\preceq,k)\leavevmode\nobreak\ \leavevmode\nobreak\
\land\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrm{WO}(\succeq,k)\big{]}}_{\varphi(k)}$

Since $\varphi(k)$ is an $\mathrm{HF}$-formula $\varphi(k)$, it follows that
${\mathsf{FSO}_{\mathscr{D}}}$ proves $\varphi(k)$, hence in particular that
every $\mathrm{HF}$-set is well-ordered. ∎

####  3.4.5. Functional Choice Axioms

We have the following functional choice axiom schemes.

  * •

_$\mathrm{HF}$ -Bounded Choice for $\mathrm{HF}$-Sets_.

$(\forall
k\mathrel{\dot{\in}}K)(\exists\ell\mathrel{\dot{\in}}L)\varphi(k,\ell)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\big{(}\exists f\mathrel{\dot{\in}}L^{K}\big{)}(\forall
k\mathrel{\dot{\in}}K)\varphi(k,f(k))$

  * •

_$\mathrm{HF}$ -Bounded Choice for Functions_.

$(\forall x)(\exists k\mathrel{\dot{\in}}K)\varphi(x,k)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\exists F:K)(\forall x)(\exists
k\mathrel{\dot{\in}}K)\left(F(x)\mathrel{\doteq}k\leavevmode\nobreak\
\land\leavevmode\nobreak\ \varphi(x,k)\right)$

  * •

_Iterated $\mathrm{HF}$-Bounded Choice_.

$(\forall k\mathrel{\dot{\in}}K)(\exists F:L)\varphi(k,F)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\big{(}\exists G:L^{K}\big{)}(\forall
k\mathrel{\dot{\in}}K)\varphi(k,F)[G(k)\sslash F]$

where the substitution $[G(k)\sslash F]$ is defined as usual but with

$(F(t)\mathrel{\doteq}M)[G(k)\sslash F]\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
\big{(}\exists
f\mathrel{\dot{\in}}L^{K}\big{)}\left(G(t)\mathrel{\doteq}f\leavevmode\nobreak\
\land\leavevmode\nobreak\ f(k)\mathrel{\doteq}M\right)$

We insist that none of these axioms create choice functions for the
_individuals_ of ${\mathsf{FSO}_{\mathscr{D}}}$ (cf Remark 3). Despite their
common shape, these three axiom schemes are actually of different nature.
First, the axiom of _$\mathrm{HF}$ -Bounded Choice for Functions_

$(\forall x)(\exists k\mathrel{\dot{\in}}K)\varphi(x,k)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\exists F:K)(\forall x)(\exists
k\mathrel{\dot{\in}}K)\left(F(x)\mathrel{\doteq}k\leavevmode\nobreak\
\land\leavevmode\nobreak\ \varphi(x,k)\right)$ (4)

is a counterpart in ${\mathsf{FSO}_{\mathscr{D}}}$ of the Comprehension Scheme
of ${\mathsf{MSO}_{\mathscr{D}}}$. Recalling the informal discussion in §3.1
and anticipating on §3.5 and §3.6, let us assume a translation
$\langle-\rangle$ from ($\mathrm{HF}$-closed)
${\mathsf{FSO}_{\mathscr{D}}}$-formulae to
${\mathsf{MSO}_{\mathscr{D}}}$-formulae, and let us assume that $K$ is a
closed $\mathrm{HF}$-term representing the $\mathrm{HF}$-set
$\\{\kappa_{1},\dots,\kappa_{n}\\}$. Then the premise of (4) can be read as

$(\forall x)\mathop{\bigvee}_{1\leq i\leq
n}\langle\varphi(x,\kappa_{i})\rangle$

The conclusion easily follows from the fact that using Comprehension, one can
define in ${\mathsf{MSO}_{\mathscr{D}}}$ a partition $X_{1},\dots,X_{n}$ of
$\mathscr{D}^{*}$ such that

$(\forall x)\mathop{\bigvee}_{1\leq i\leq
n}\Big{(}X_{i}(x)\leavevmode\nobreak\ \leavevmode\nobreak\
\land\leavevmode\nobreak\ \leavevmode\nobreak\
\langle\varphi(x,\kappa_{i})\rangle\Big{)}$

Second, _$\mathrm{HF}$ -Bounded Choice for $\mathrm{HF}$-Sets_

$(\forall
k\mathrel{\dot{\in}}K)(\exists\ell\mathrel{\dot{\in}}L)\varphi(k,\ell)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\big{(}\exists f\mathrel{\dot{\in}}L^{K}\big{)}(\forall
k\mathrel{\dot{\in}}K)\varphi(k,f(k))$ (5)

may look similar to the Axioms on $\mathrm{HF}$-Sets of §3.4.4. The
differences are that the formula $\varphi$ here is an _arbitrary_ formula of
${\mathsf{FSO}_{\mathscr{D}}}$, not necessarily an $\mathrm{HF}$-formula in
the sense of Definition 3.4.4, and moreover that this axiom only involves
${\mathsf{FSO}_{\mathscr{D}}}$ (i.e. _bounded_) quantifications, contrary to
(2). Note that for $\mathrm{HF}$-formulae $\varphi$, this axiom is indeed an
instance of the axioms of §3.4.4. In the general case, this axiom can be seen
as following from the fact that quantifications over $\mathrm{HF}$-Sets in
${\mathsf{FSO}_{\mathscr{D}}}$ are ultimately interpreted in propositional
logic. Assume that the $\mathrm{HF}$-terms $K$ and $L$ are closed, and
correspond to the $\mathrm{HF}$-sets $\kappa$ and $\lambda$ respectively. Then
the premise of (5) can be read as

$\mathop{\bigwedge}_{\kappa_{0}\in\kappa}\mathop{\bigvee}_{\lambda_{0}\in\lambda}\langle\varphi(\kappa_{0},\lambda_{0})\rangle$

which is equivalent in propositional logic to the interpretation of the
conclusion

$\mathop{\bigvee}_{f\in\lambda^{\kappa}}\mathop{\bigwedge}_{\kappa_{0}\in\kappa}\langle\varphi(\kappa_{0},f(\kappa_{0}))\rangle$

Similarly, _Iterated $\mathrm{HF}$-Bounded Choice_ reduces to an equivalence
of the form

$\mathop{\bigwedge}_{1\leq i\leq
n}(\exists\bm{X})\varphi(\kappa_{i},\bm{X})\quad\Longleftrightarrow\quad(\exists\bm{X}_{1})\dots(\exists\bm{X}_{n})\mathop{\bigwedge}_{1\leq
i\leq n}\varphi(\kappa_{i},\bm{X}_{i})$

and follows from Comprehension.

The definition of ${\mathsf{FSO}_{\mathscr{D}}}$ is now complete.

Similarly as with ${\mathsf{MSO}_{\mathscr{D}}}$, we shall write
$\mathsf{FSO}$ for ${\mathsf{FSO}_{\mathscr{D}}}$ when the set of tree
directions $\mathscr{D}$ is clear from the context.

###  3.5. The Standard Model of $\mathsf{FSO}$

The _standard model_ $\mathfrak{T}$ of ${\mathsf{FSO}_{\mathscr{D}}}$ is the
full $\mathscr{D}$-ary tree $\mathscr{D}^{*}$ equipped with suitable domains
for each sort:

  * •

_$\mathrm{HF}$ -Sets_ range over $V_{\omega}$, and each constant
$\dot{\mathsf{\kappa}}$ is interpreted by the corresponding $\mathrm{HF}$-set
$\kappa\in V_{\omega}$.

  * •

_Individuals_ range over $\mathscr{D}^{*}$, the constant $\dot{\varepsilon}$
is interpreted by the empty sequence $\varepsilon\in\mathscr{D}^{*}$ and
$\mathsf{S}_{d}$ as the map taking $p\in\mathscr{D}^{*}$ to
$p.d\in\mathscr{D}^{*}$. Moreover, we write $<$ for the strict prefix order on
$\mathscr{D}^{*}$.

  * •

_Functions_ range over

$\bigcup_{\kappa\in V_{\omega}}\left(\mathscr{D}^{*}\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\kappa\right)$

  * •

For each $n,m\in\mathbb{N}$, the $\mathrm{HF}$-Function
$\dot{\mathsf{g}}_{n,m}$ (of arity $n$) is interpreted as the function

$\mathtt{g}_{n,m}\leavevmode\nobreak\ \leavevmode\nobreak\
:\leavevmode\nobreak\ \leavevmode\nobreak\ V_{\omega}^{n}\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
V_{\omega}$

fixed in Convention 3.4.4.

######  Remark 13.

Note that $\mathfrak{T}$ has the same individuals as the standard model of
${\mathsf{MSO}_{\mathscr{D}}}$. Moreover we write $\mathfrak{T}$ for both the
standard model of ${\mathsf{FSO}_{\mathscr{D}}}$ and that of
${\mathsf{MSO}_{\mathscr{D}}}$, as an abuse of notation.

We have the usual an interpretation $\llbracket t\rrbracket\in\mathscr{D}^{*}$
for each closed individual term $t$ with parameters in $\mathfrak{T}$, and an
interpretation $\llbracket K\rrbracket\in V_{\omega}$ for each closed
$\mathrm{HF}$-term $K$ with parameters in $\mathfrak{T}$. The relation
$\mathfrak{T}\models\varphi$, for a closed $\mathsf{FSO}$-formula $\varphi$
with parameters in $\mathfrak{T}$, is defined by induction on $\varphi$ as
follows:

$\begin{array}[]{!{\Std\models} l !{\quad\text{iff}\quad} l !{\quad}
l}\mathfrak{T}\models\lx@intercol
K\mathrel{\dot{\mathsf{\mathrel{\star}}}}L&\llbracket
K\rrbracket\mathrel{\star}\llbracket L\rrbracket&\text{(for $\mathrel{\star}$
either $=$, $\in$, or $\subseteq$)}\\\ \mathfrak{T}\models\lx@intercol
t\mathrel{\dot{\mathsf{\mathrel{\star}}}}u&\llbracket
t\rrbracket\mathrel{\star}\llbracket u\rrbracket&\text{(for $\mathrel{\star}$
either $=$ or $<$)}\\\
\mathfrak{T}\models\lx@intercol\varphi\lor\psi&(\mathfrak{T}\models\varphi)\text{
or }(\mathfrak{T}\models\psi)\\\
\mathfrak{T}\models\lx@intercol\lnot\varphi&\mathfrak{T}\not\models\varphi\\\
\mathfrak{T}\models\lx@intercol(\exists
x)\varphi&\mathfrak{T}\models\varphi[p/x]\leavevmode\nobreak\
\leavevmode\nobreak\ \text{for some $p\in\mathscr{D}^{*}$}\\\
\mathfrak{T}\models\lx@intercol(\exists
k\mathrel{\dot{\mathsf{\mathrel{\star}}}}L)\varphi&\mathfrak{T}\models\varphi[\kappa/k]\leavevmode\nobreak\
\leavevmode\nobreak\ \text{for some $\kappa\mathrel{\star}\llbracket
L\rrbracket$}&\text{(for $\mathrel{\star}$ either $\in$ or $\subseteq$)}\\\
\mathfrak{T}\models\lx@intercol(\exists
F:L)\varphi&\mathfrak{T}\models\varphi[\mathtt{F}/F]\leavevmode\nobreak\
\leavevmode\nobreak\ \text{for some $\mathtt{F}\in\llbracket
L\rrbracket^{\mathscr{D}^{*}}$}\end{array}$

By a routine induction argument, we may show the soundness of
${\mathsf{FSO}_{\mathscr{D}}}$ w.r.t. $\mathfrak{T}$:

######  Proposition 14.

Given $\mathsf{FSO}$-formulae $\psi_{1},\dots,\psi_{n},\varphi$ with free
$\mathrm{HF}$-variables among $\bm{k}$, free Individual variables among
$\bm{x}$, and free Function variables among $\bm{F}$, if

$\psi_{1},\dots,\psi_{n}\vdash_{\mathsf{FSO}}\varphi$

then for all $\mathrm{HF}$-Sets $\bm{\kappa}$, all $\bm{p}\in\mathscr{D}^{*}$
and all $\bm{\mathtt{F}}\in\bigcup_{\kappa\in
V_{\omega}}\left(\mathscr{D}^{*}\to\kappa\right)$, we have

$\mathfrak{T}\models\varphi[\bm{\kappa}/\bm{k},\bm{p}/\bm{x},\bm{\mathtt{F}}/\bm{F}]\qquad\text{whenever}\qquad\mathfrak{T}\models\mathop{\bigwedge}_{1\leq
i\leq n}\psi_{i}[\bm{\kappa}/\bm{k},\bm{p}/\bm{x},\bm{\mathtt{F}}/\bm{F}]$

######  Remark 15.

It follows from Remark 10 that the map $\llbracket-\rrbracket$ is not
computable on $\mathrm{HF}$-terms. We refer to §8.5 for a discussion and a
workaround.

###  3.6. Mutual Interpretability of $\mathsf{FSO}$ and $\mathsf{MSO}$

While $\mathsf{FSO}$ seems more expressive than $\mathsf{MSO}$ (and, indeed,
is easier to work with), the two theories can mutually interpret each other
via two formula-level translations:

$\langle-\rangle\leavevmode\nobreak\ \leavevmode\nobreak\
:\leavevmode\nobreak\ \leavevmode\nobreak\ \mathsf{FSO}\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\mathsf{MSO}\qquad\text{and}\qquad(-)^{\circ}\leavevmode\nobreak\
\leavevmode\nobreak\ :\leavevmode\nobreak\ \leavevmode\nobreak\
\mathsf{MSO}\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \mathsf{FSO}$

As we shall see, both translations preserve and reflect provability:

$\displaystyle\mathsf{FSO}\vdash\varphi\quad\text{if and only
if}\quad\mathsf{MSO}\vdash\langle\varphi\rangle$ ($\varphi$ closed
$\mathsf{FSO}$-formula) $\displaystyle\mathsf{MSO}\vdash\varphi\quad\text{if
and only if}\quad\mathsf{FSO}\vdash\varphi^{\circ}$ ($\varphi$ closed
$\mathsf{MSO}$-formula)

The interpretation $(-)^{\circ}$ of $\mathsf{MSO}$ in $\mathsf{FSO}$ simply
amounts to simulate the (Monadic) Predicate variables of $\mathsf{MSO}$ by
$\mathsf{FSO}$-Function variables $\mathscr{D}^{*}\to 2$. We therefore see
$(-)^{\circ}$ as an embedding, and see $\mathsf{FSO}$ as a conservative
extension of $\mathsf{MSO}$ which is faithfully interpretable in
$\mathsf{MSO}$. This property is not only a sanity check: we actually rely on
it in our completeness argument (see Rem. 21). We discuss the translations
$\langle-\rangle$ and $(-)^{\circ}$ separately in §3.6.1 and §3.6.2 below.
Full proofs are detailed in [DR19, App. A].

####  3.6.1. From $\mathsf{FSO}$ to $\mathsf{MSO}$

The translation $\langle-\rangle:\mathsf{FSO}\to\mathsf{MSO}$ interprets the
$\mathrm{HF}$-part of $\mathsf{FSO}$ using propositional logic. It is
essentially straightforward, except for the case of Functions, which require
some care. We will work with the following convention:

We assume that each $\mathrm{HF}$-set $\kappa$ comes with a fixed enumeration
$\bm{\kappa}=\kappa_{1},\dots,\kappa_{n}$ of its elements.

The translation $\langle-\rangle$ will map an $\mathrm{HF}$-closed
$\mathsf{FSO}$-formula $\varphi$ without free Function variables to an
$\mathsf{MSO}$-formula $\langle\varphi\rangle$. As stated earlier,
quantifications over $\mathrm{HF}$-Sets will be interpreted using
propositional logic. For instance we have,

$\left\langle(\exists
k\mathrel{\dot{\in}}K)\varphi\right\rangle\leavevmode\nobreak\
\leavevmode\nobreak\ =\leavevmode\nobreak\ \leavevmode\nobreak\
\mathop{\bigvee}_{\kappa\in\llbracket
K\rrbracket}\langle\varphi[\kappa/k]\rangle$

where $\llbracket K\rrbracket\in V_{\omega}$ is the standard interpretation of
the closed $\mathrm{HF}$-term $K$ defined in §3.5. As a consequence, the
translation $\langle-\rangle$ is _non-uniform_ w.r.t. $\mathrm{HF}$-Sets. In
particular, for an $\mathsf{FSO}$-formula $\varphi$ with free
$\mathrm{HF}$-variables among $\bm{k}=k_{1},\dots,k_{p}$, each
$\mathrm{HF}$-sets $\bm{\kappa}=\kappa_{1},\dots,\kappa_{p}$ will induce a
specific $\mathsf{MSO}$-formula $\langle\varphi[\bm{\kappa}/\bm{k}]\rangle$.

The interpretation of Function variables is more complex. Consider a closed
$\mathrm{HF}$-term $K$ and assume $\llbracket
K\rrbracket=\\{\kappa_{1},\dots,\kappa_{c}\\}$. Then a Function $(F:K)$ can be
seen as a function

$F\leavevmode\nobreak\ \leavevmode\nobreak\ :\leavevmode\nobreak\
\leavevmode\nobreak\ \mathscr{D}^{*}\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\\{\kappa_{1},\dots,\kappa_{c}\\}$

As indicated in §3.1, we interpret $F$ as a tuple $X_{1},\dots,X_{c}$ of
Monadic variables such that

$x\in X_{i}\quad\text{iff}\quad F(x)=\kappa_{i}$ (for $i=1,\dots,c$)

In other words, $F:\mathscr{D}^{*}\to\\{\kappa_{1},\dots,\kappa_{c}\\}$ is
seen as a partition $X_{1},\dots,X_{c}$ of $\mathscr{D}^{*}$. To handle the
interpretation of Functions in the inductive definition of $\langle-\rangle$,
it is actually convenient to temporarily work in an extension of
$\mathsf{FSO}$ with the following atomic formulae:

  * •

$\arrowvert X_{1}\dots X_{n}(t)\mathrel{\doteq}_{\bm{\kappa}}L\arrowvert$
where $\bm{\kappa}=\kappa_{1},\dots,\kappa_{n}$ enumerates an
$\mathrm{HF}$-set and $X_{1},\dots,X_{n}$ are monadic variables of
$\mathsf{MSO}$.

We call _extended_ $\mathsf{FSO}$-formulae those formulae build as the
$\mathsf{FSO}$-formulae, but possibly using the atomic formulae above.
Extended atomic formulae are useful for dealing with $\mathrm{HF}$-bounded
quantifications over Functions, say $(\exists F:K)\varphi$. The point is that
$F$ occurs in subformulae of $\varphi$ of the form $F(t)\mathrel{\doteq}L$,
where the $\mathrm{HF}$-term $L$ may contain free $\mathrm{HF}$-variables.
Hence the value of $L$ is not known when the translation of $(\exists F:K)$
has to be computed. Extended atomic formulae allow us to delay the
interpretation of $F(t)\mathrel{\doteq}L$ until $\llbracket L\rrbracket$ is
known.

The interpretation of an extended $\mathrm{HF}$-closed $\mathsf{FSO}$-formula
$\varphi$ _without free Function variables_ is the $\mathsf{MSO}$-formula
$\langle\varphi\rangle$ defined by induction on $\varphi$ as follows:

$\begin{array}[]{r !{~~}@{}c@{}!{~~} l !{\qquad} l}\langle\arrowvert
X_{1}\dots
X_{n}(t)\mathrel{\doteq}_{\bm{\kappa}}L\arrowvert\rangle\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ &\mathrel{:=}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\ &\mathop{\bigvee}_{1\leq i\leq n\ \&\
\kappa_{i}=\llbracket L\rrbracket}X_{i}(t)\\\ \langle
K\mathrel{\dot{\mathsf{\mathrel{\star}}}}L\rangle\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ &\mathrel{:=}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\ &\left\\{\begin{array}[]{l l}\top&\text{if $\llbracket
K\rrbracket\mathrel{\star}\llbracket L\rrbracket$}\\\
\bot&\text{otherwise}\end{array}\right.&\text{(where
$\mathord{\mathrel{\star}}\in\\{=,\in,\subseteq\\}$)}\\\ \langle
t\mathrel{\star}u\rangle\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
&\mathrel{:=}\hfil\leavevmode\nobreak\ \leavevmode\nobreak\
&t\mathrel{\star}u&\text{(where
$\mathord{\mathrel{\star}}\in\\{\mathrel{\doteq},\mathrel{\dot{<}}\\}$)}\\\
\langle\lnot\varphi\rangle\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ &\mathrel{:=}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\ &\lnot\langle\varphi\rangle\\\
\langle\varphi\lor\psi\rangle\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ &\mathrel{:=}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\ &\langle\varphi\rangle\lor\langle\psi\rangle\\\
\langle(\exists
k\mathrel{\dot{\mathsf{\mathrel{\star}}}}K)\varphi\rangle\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ &\mathrel{:=}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\ &\mathop{\bigvee}_{\kappa\mathrel{\star}\llbracket
K\rrbracket}\langle\varphi[\kappa/k]\rangle&\text{(where
$\mathord{\mathrel{\star}}\in\\{\in,\subseteq\\}$)}\\\ \langle(\exists
x)\varphi\rangle\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
&\mathrel{:=}\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ &(\exists
x)\langle\varphi\rangle\\\ \langle(\exists
F:K)\varphi\rangle\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
&\mathrel{:=}\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ &(\exists
X_{1})\dots(\exists X_{c})\\\ \lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\ \leavevmode\nobreak\
&\lx@intercol\hfil\left\\{\begin{array}[]{c
l}&\Upsilon_{c}(X_{1},\dots,X_{c})\\\ \land&\langle\varphi[\arrowvert
X_{1}\dots
X_{c}(t)\mathrel{\doteq}_{\bm{\kappa}}L\arrowvert\leavevmode\nobreak\
/\leavevmode\nobreak\
(F(t)\mathrel{\doteq}L)]\rangle\end{array}\right.\lx@intercol\end{array}$

where in the last clause, ${\llbracket K\rrbracket}$ is enumerated by
$\bm{\kappa}=\kappa_{1},\dots,\kappa_{c}$, and
$\Upsilon_{c}(X_{1},\dots,X_{c})$ is the following $\mathsf{MSO}$-formula,
expressing that $X_{1},\dots,X_{c}$ form a partition of $\mathscr{D}^{*}$:

$\Upsilon_{c}(X_{1},\dots,X_{c})\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ (\forall
x)\left[\mathop{\bigvee}_{1\leq i\leq
c}\left(X_{i}(x)\quad\land\quad\mathop{\bigwedge}_{j\neq i}\lnot
X_{j}(x)\right)\right]$

Note that in the definition of $\langle\varphi\rangle$ above, since $\varphi$
is assumed to be $\mathrm{HF}$-closed, the displayed $\mathrm{HF}$-terms $K$
and $L$ are closed, so that their $\mathfrak{T}$-interpretation $\llbracket
K\rrbracket,\llbracket L\rrbracket\in V_{\omega}$ is defined (see §3.5).

######  Remark 16.

Since it involves the standard interpretation map $\llbracket-\rrbracket$ on
$\mathrm{HF}$-terms, it follows from Remark 15 (§3.5) that the interpretation
$\langle-\rangle$ is not recursive. We refer to §5.6.1 and §8.5 for
discussions and workarounds.

######  Theorem 17.

For every closed $\mathsf{FSO}$-formula $\varphi$, we have

$\mathsf{MSO}\vdash\langle\varphi\rangle\qquad\text{whenever}\qquad\mathsf{FSO}\vdash\varphi$

The proof of Theorem 17 is deferred to [DR19, App. A]. The logical rules of
$\mathsf{FSO}$ are handled routinely. The interpretations of most of the
axioms of $\mathsf{FSO}$ are almost trivially provable from the corresponding
axioms of $\mathsf{MSO}$. The Functional Choice Axioms are dealt-with
essentially as explained in §3.4.5.

####  3.6.2. From $\mathsf{MSO}$ to $\mathsf{FSO}$

The translation $(-)^{\circ}:\mathsf{MSO}\to\mathsf{FSO}$ is much simpler than
$\langle-\rangle$. Assume given a $\mathsf{FSO}$-Function variable $F_{X}$ for
each monadic $\mathsf{MSO}$-variable $X$. The map $(-)^{\circ}$ is inductively
defined as follows:

$\begin{array}[]{r !{~~}@{}c@{}!{~~} l !{\qquad\qquad} r !{~~\deq~~}
l}(X(t))^{\circ}\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
&\mathrel{:=}\hfil\leavevmode\nobreak\ \leavevmode\nobreak\
&F_{X}(t)\mathrel{\doteq}1&(\varphi\lor\psi)^{\circ}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\varphi^{\circ}\lor\psi^{\circ}\\\
(t\mathrel{\doteq}u)^{\circ}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ &\mathrel{:=}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\
&t\mathrel{\doteq}u&(\lnot\varphi)^{\circ}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lnot(\varphi^{\circ})\\\
(t\mathrel{\dot{\leq}}u)^{\circ}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ &\mathrel{:=}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\ &t\mathrel{\dot{\leq}}u&((\exists
x)\varphi)^{\circ}\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &(\exists
x)\varphi^{\circ}\\\ \lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
&\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ &&((\exists
X)\varphi)^{\circ}\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &(\exists
F_{X}:2)\varphi^{\circ}\end{array}$

It is easy to see that $(-)^{\circ}$ is truth preserving (and reflecting)
w.r.t. the standard model $\mathfrak{T}$, by a direct induction on formulae
relying on the bijection $\mathcal{P}(\mathscr{D}^{*})\cong
2^{\mathscr{D}^{*}}$.

######  Lemma 18.

Given a closed $\mathsf{MSO}$-formula $\varphi$, we have

$\mathfrak{T}\models\varphi\qquad\text{if and only
if}\qquad\mathfrak{T}\models\varphi^{\circ}$

The main result on $(-)^{\circ}$ is the following. Its proof is deferred to
[DR19, App. A].

######  Theorem 19.

Given a closed $\mathsf{MSO}$-formula $\varphi$,

$\mathsf{FSO}\vdash\varphi^{\circ}\qquad\text{if and only
if}\qquad\mathsf{MSO}\vdash\varphi$

Theorem 19 can actually be extended to $\mathsf{FSO}$ formulae. This is
essentially the content of the following result.

######  Proposition 20.

For a closed $\mathsf{FSO}$-formula $\varphi$, we have the following.

$\displaystyle\mathsf{FSO}\vdash\quad\varphi\leavevmode\nobreak\
\leavevmode\nobreak\ \Longleftrightarrow\leavevmode\nobreak\
\leavevmode\nobreak\ \langle\varphi\rangle^{\circ}$ (6)
$\displaystyle\mathsf{FSO}\vdash\varphi\quad\text{iff}\quad\mathsf{MSO}\vdash\langle\varphi\rangle$
(7)
$\displaystyle\mathfrak{T}\models\varphi\quad\text{iff}\quad\mathfrak{T}\models\langle\varphi\rangle$
(8)

######  Remark 21.

Theorem 19 and Proposition 20 will be used in our completeness argument (§8)
in two different ways:

  1. (1)

We first obtain completeness of $\mathsf{FSO}$ (augmented with the Axiom
$(\mathit{PosDet})$ of §5.6) for $\mathsf{MSO}$ formulae via a usual
translation of formulae to automata. From this result, completeness of
$\mathsf{FSO}+(\mathit{PosDet})$ follows by Proposition 20, while completeness
of $\mathsf{MSO}$ (augmented with $\langle-\rangle$-translations of suitable
instances of $(\mathit{PosDet})$) follows by Theorem 19.

  2. (2)

In addition, we will use Proposition 20 in §7 in order to import the
$\mathsf{MSO}$-theory of $\mathbb{N}$ for the infinite paths of
$\mathfrak{T}$. We rely on this for the version of the Büchi-Landweber Theorem
(namely that $\mathsf{FSO}$ decides parity games on finite graphs) used in the
completeness argument of §8, as well as for the Simulation Theorem in §9.

###  3.7. Notations

We now introduce some notations that we will use throughout our formalization
of games and automata in $\mathsf{FSO}$.

####  3.7.1. $\mathsf{FSO}$ with Extended $\mathrm{HF}$-Terms

First, recall that the syntax of $\mathsf{FSO}$ formally disallows Functions
in $\mathrm{HF}$-terms. We propose here a notation system that allows them in
some circumstances. For instance, assuming $(F:K)$, we can use the notation

$(F(t)\mathrel{\dot{\in}}L)\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ (\exists
k\mathrel{\dot{\in}}K)\big{(}F(t)\mathrel{\doteq}k\leavevmode\nobreak\
\leavevmode\nobreak\ \land\leavevmode\nobreak\ \leavevmode\nobreak\
k\mathrel{\dot{\in}}L\big{)}$

More generally, consider an atomic formula

$M\mathrel{\star}N$ (for
$\mathord{\mathrel{\star}}\in\\{\mathrel{\doteq},\mathrel{\dot{\in}},\mathrel{\dot{\subseteq}}\\}$)

with $M$ and $N$ terms on the following grammar:

$M,M\quad\mathrel{::=}\quad k\quad|\quad\dot{\mathsf{\kappa}}\quad|\quad
F(t)\quad|\quad\dot{\mathsf{g}}_{n,m}(L_{1},\dots,L_{n})$ (9)

Such formulae can be interpreted in $\mathsf{FSO}$, provided one assumes
bounds for the Function variables occurring in them. Let $M$ and $N$ be as
above, and assume their free Function variables to be among
$\bm{F}=F_{1},\dots,F_{n}$. Note that there are (proper) $\mathrm{HF}$-terms
$M^{\prime}$ and $N^{\prime}$ such that

$M=M^{\prime}[\bm{F(t)}/\bm{\ell}]\qquad\text{and}\qquad
N=N^{\prime}[\bm{F(t)}/\bm{\ell}]$

for some $\mathrm{HF}$-variables $\bm{\ell}=\ell_{1},\dots,\ell_{c}$ and where
$\bm{F(t)}=F_{i_{1}}(t_{1}),\dots,F_{i_{c}}(t_{c})$. Given proper
$\mathrm{HF}$-terms $K_{1},\dots,K_{n}$, assuming $\bm{F}:\bm{K}$, one can let

$M\mathrel{\star}N\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
\big{(}\exists\bm{\ell}\in\bm{L}\big{)}\left(\bm{F(t)}\mathrel{\doteq}\bm{\ell}\leavevmode\nobreak\
\leavevmode\nobreak\ \land\leavevmode\nobreak\ \leavevmode\nobreak\
M^{\prime}\mathrel{\star}N^{\prime}\right)$

where $\bm{L}=L_{1},\dots,L_{c}$ is such that $L_{j}=K_{i}$ iff the $j$th
element of $\bm{F(t)}$ is $F_{i}(t_{j})$. Note however that the above defined
formula $M\mathrel{\star}N$ actually depends on the choice of $\bm{K}$, so we
rather write it as:

$(M\mathrel{\star}N)_{\bm{F},\bm{K}}$

Generalizing further we can, with the above method, interpret in
$\mathsf{FSO}$ formulae build with $\mathrm{HF}$-terms in the sense of (9).
The interpretation in $\mathsf{FSO}$ of such a formula $\varphi$ with free
Function variables among $\bm{F}=F_{1},\dots,F_{n}$ is defined by induction,
and depends on a choice of proper $\mathrm{HF}$-terms
$\bm{K}=K_{1},\dots,K_{n}$. Using notations as above, we arrive at the
following definition:

$\begin{array}[]{r !{~~\deq~~} l @{~~}
l}(t\mathrel{\star}u)_{\bm{F},\bm{K}}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&(t\mathrel{\star}u)\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ &\text{(for
$\mathord{\mathrel{\star}}\in\\{\mathrel{\doteq},\mathrel{\dot{\in}}\\}$)}\\\
(M\mathrel{\star}N)_{\bm{F},\bm{K}}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\left\\{\begin{array}[]{l l}G(u)\mathrel{\doteq}N&\text{if
$(M\mathrel{\star}N)=(G(u)\mathrel{\doteq}N)$}\\\ &\text{with $N$ a proper
$\mathrm{HF}$-term}\\\
\lx@intercol(\exists\bm{\ell}\mathrel{\dot{\in}}\bm{L})\left(\bm{F(t)}\mathrel{\doteq}\bm{\ell}\leavevmode\nobreak\
\leavevmode\nobreak\ \land\leavevmode\nobreak\ \leavevmode\nobreak\
M^{\prime}\mathrel{\star}N^{\prime}\right)\hfil\lx@intercol\\\
&\text{otherwise}\end{array}\right.\hfil\leavevmode\nobreak\
\leavevmode\nobreak\ &\text{(for
$\mathord{\mathrel{\star}}\in\\{\mathrel{\doteq},\mathrel{\dot{\in}},\mathrel{\dot{\subseteq}}\\}$)}\\\
(\lnot\varphi)_{\bm{F},\bm{K}}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lnot(\varphi_{\bm{F},\bm{K}})\hfil\leavevmode\nobreak\ \leavevmode\nobreak\
\\\ (\varphi\lor\psi)_{\bm{F},\bm{K}}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\varphi_{\bm{F},\bm{K}}\leavevmode\nobreak\ \leavevmode\nobreak\
\lor\leavevmode\nobreak\ \leavevmode\nobreak\
\psi_{\bm{F},\bm{K}}\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ \\\
((\exists x)\varphi)_{\bm{F},\bm{K}}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&(\exists x)\varphi_{\bm{F},\bm{K}}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\ \\\ ((\exists
m\mathrel{\star}M)\varphi)_{\bm{F},\bm{K}}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lx@intercol(\exists\bm{\ell}\mathrel{\dot{\in}}\bm{L})(\exists
m\mathrel{\star}M^{\prime})\left(\bm{F(t)}\mathrel{\doteq}\bm{\ell}\leavevmode\nobreak\
\leavevmode\nobreak\ \land\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi_{\bm{F},\bm{K}}\right)\hfil\lx@intercol\\\ ((\exists
G:M)\varphi)_{\bm{F},\bm{K}}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\lx@intercol(\exists\bm{\ell}\mathrel{\dot{\in}}\bm{L})(\exists
G:M^{\prime})\left(\bm{F(t)}\mathrel{\doteq}\bm{\ell}\leavevmode\nobreak\
\leavevmode\nobreak\ \land\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi_{G\bm{F},M^{\prime}\bm{K}}\right)\hfil\lx@intercol\end{array}$

Beware that $(\varphi)_{\bm{F},\bm{K}}$ only makes sense under the assumptions
$\bm{F}:\bm{K}$. Keeping this in mind we may obtain, for instance, the
following formulations of the Functional Choice Axioms of §3.4.5.

  * •

_$\mathrm{HF}$ -Bounded Choice for Functions_.

$(\forall x)(\exists k\mathrel{\dot{\in}}K)\varphi(x,k)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\exists F:K)(\forall x)\varphi(x,F(x))$

  * •

_Iterated $\mathrm{HF}$-Bounded Choice_.

$(\forall k\mathrel{\dot{\in}}K)(\exists F:L)\varphi(k,F)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\left(\exists F:L^{K}\right)(\forall k\mathrel{\dot{\in}}K)\varphi(k,F(-,k))$

####  3.7.2. Notations for Products and Functions

We now introduce notations for a form of _product type_ , based on the
function spaces and application functions of §3.4.4.(7). The main idea is to
be able to manipulate a Function variable

$F\leavevmode\nobreak\ \leavevmode\nobreak\ :\leavevmode\nobreak\
\leavevmode\nobreak\ K^{L}$

as a function

$F\leavevmode\nobreak\ \leavevmode\nobreak\ :\leavevmode\nobreak\
\leavevmode\nobreak\ \mathscr{D}^{*}\times L\leavevmode\nobreak\
\leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
K$

Furthermore, it is convenient to allow such $F$ to have a domain defined by an
$\mathsf{FSO}$ formula $\psi(-)$, and to write

$F\leavevmode\nobreak\ \leavevmode\nobreak\ :\leavevmode\nobreak\
\leavevmode\nobreak\ \psi(-)\times L\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
K\qquad\text{for}\qquad(\forall x)\big{(}\psi(x)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
F(x)\mathrel{\dot{\in}}K^{L}\big{)}$

We develop here a notation system for such “function” and “product types”. In
§3.7.3, we discuss formulations of the Functional Choice Axioms of §3.4.5
induced by these notations. In order not to overload the arrow symbol
$\longrightarrow$ (which will be used with games later on), we will write
typing declarations as

$F:\mathscr{D}^{*}\times L\mathrel{\mathfrak{to}}K\qquad\text{instead
of}\qquad F:\mathscr{D}^{*}\times L\longrightarrow K$

_Product types_ are given by the following grammar, where $\psi(-)$ is an
$\mathsf{FSO}$ formula of an individual variable (with possibly other free
variables of any sort), and where $K$ is an $\mathrm{HF}$-term.

$\Pi\quad\mathrel{::=}\quad\psi(-)\quad|\quad K\quad|\quad\Pi\times K$

The _arity_ of a product type $\Pi$ is:

  * •

$(1,n)$ if $\Pi$ is of the form $\psi(-)\times K_{1}\times\dots\times K_{n}$,

  * •

$(0,n)$ if $\Pi$ is of the form $K_{1}\times\dots\times K_{n}$.

Product types are to be used with the following defined formulae.

$\begin{array}[]{r !{~~\deq~~}
l}(t,\bm{K})\mathrel{\ddot{=}}(u,\bm{L})\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&t\mathrel{\doteq}u\leavevmode\nobreak\ \leavevmode\nobreak\
\land\leavevmode\nobreak\ \leavevmode\nobreak\ \bm{K}\mathrel{\doteq}\bm{L}\\\
(t,\bm{K})\mathrel{\ddot{\in}}\psi(-)\times\bm{L}\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\psi(t)\leavevmode\nobreak\ \leavevmode\nobreak\ \land\leavevmode\nobreak\
\leavevmode\nobreak\ \bm{K}\mathrel{\dot{\in}}\bm{L}\\\\[10.00002pt]
f:K\mathrel{\mathfrak{to}}L\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&f\mathrel{\dot{\in}}L^{K}\\\
F:\psi(-)\mathrel{\mathfrak{to}}L\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&(\forall x)(\psi(x)\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
F(x)\mathrel{\dot{\in}}L)\\\ \textsc{{f}}:\Pi\times
K\mathrel{\mathfrak{to}}L\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&\textsc{{f}}:\Pi\mathrel{\mathfrak{to}}L^{K}\end{array}$

Here f stands for a Function variable $F$ if the arity of $\Pi$ is of the form
$(1,n)$, and for an $\mathrm{HF}$-variable $f$ if the arity of $\Pi$ is of the
form $(0,n)$. Moreover, for $\Pi=\psi(-)\times K_{1}\times\dots\times K_{n}$,
we let

$(\exists F:\Pi\mathrel{\mathfrak{to}}L)\varphi\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
\left(\exists F:L^{K_{n}\times\dots\times
K_{1}}\right)\big{[}F:\Pi\mathrel{\mathfrak{to}}L\leavevmode\nobreak\
\leavevmode\nobreak\ \land\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi\big{]}$

  1. (1)

Thanks to Rem. 12, using the Axiom of $\mathrm{HF}$-Bounded Choice for
Functions (§3.4.5), we have

$\big{(}F:\Pi\mathrel{\mathfrak{to}}L\leavevmode\nobreak\ \leavevmode\nobreak\
\land\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi\big{)}\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\exists
F:\Pi\mathrel{\mathfrak{to}}L)\varphi$

  2. (2)

Using Convention 3.4.4, for each product type $\Pi$ we have

$(\textsc{{f}}:\Pi\times K_{1}\times\dots\times
K_{n}\mathrel{\mathfrak{to}}K)\quad\Longleftrightarrow\quad\left(\textsc{{f}}:\Pi\mathrel{\mathfrak{to}}K^{K_{n}\times\dots\times
K_{1}}\right)$

It follows that for each product type $\Pi$ and each formula $\varphi$ we have

$(\exists\textsc{{f}}:\Pi\times K_{1}\times\dots\times
K_{n}\mathrel{\mathfrak{to}}K)\varphi\quad\Longleftrightarrow\quad\left(\exists\textsc{{f}}:\Pi\mathrel{\mathfrak{to}}K^{K_{n}\times\dots\times
K_{1}}\right)\varphi$

  1. (1)

Given a product type $\Pi$, we use the notation $\tilde{t}:\Pi$, where
$\tilde{t}$ stands for a tuple of the form $(t,K_{1},\dots,K_{n})$ if $\Pi$
has arity $(1,n)$, or of the form $(K_{1},\dots,K_{n})$ if $\Pi$ has arity
$(0,n)$. When $\Pi$ is clear from the context, we write $\tilde{t}$ instead of
$\tilde{t}:\Pi$, and furthermore we may omit the overset tilde, writing $t$
instead of $\tilde{t}$.

Write $\tilde{x}$ for tuples of variables of the form $(x,k_{1},\dots,k_{n})$
or of the form $(k_{1},\dots,k_{n})$.

  2. (2)

If $\Pi=\psi(-)\times K_{1}\times\dots\times K_{n}$ and
$\tilde{t}=(t,L_{1},\dots,L_{n})$, we write $F^{\Pi\to K}(\tilde{t})$ for the
$\mathrm{HF}$-term

$@_{K_{1}\times\dots\times K_{n},K}(F(t),(L_{1},\dots,L_{n}))$

If $\Pi=K_{1}\times\dots\times K_{n}$ and $\tilde{t}=(L_{1},\dots,L_{n})$, we
write $f^{\Pi\to K}(\tilde{t})$ for the $\mathrm{HF}$-term

$@_{K_{1}\times\dots\times K_{n},K}(f,(L_{1},\dots,L_{n}))$

When $\Pi$ and $K$ are clear from the context, in either case above we write
$\textsc{{f}}(\tilde{t})$ for $\textsc{{f}}^{\Pi\to K}(\tilde{t})$.

  3. (3)

We furthermore write $\tilde{t}\mathrel{\dot{\in}}\textsc{{f}}$ or even
$\textsc{{f}}(\tilde{t})$ for the formula

$\textsc{{f}}(\tilde{t})\mathrel{\doteq}1$

  4. (4)

We extend product types as follows

$\Pi\quad\mathrel{::=}\quad\ldots\quad|\quad\mathscr{D}^{*}\quad|\quad X$

where $X$ is a Function variable. We let

$\begin{array}[]{r !{~~\deq~~}
l}F:X\mathrel{\mathfrak{to}}L\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&(\forall x)(X(x)\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
F(x)\mathrel{\dot{\in}}L)\\\
F:\mathscr{D}^{*}\mathrel{\mathfrak{to}}L\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&(\forall x)(F(x)\mathrel{\dot{\in}}L)\end{array}$

Note that

$\begin{array}[]{r !{\quad\longliff\quad} l}F:(\mathscr{D}^{*}\times
K_{1}\times\dots\times
K_{n})\mathrel{\mathfrak{to}}L\lx@intercol\quad\Longleftrightarrow&F:(\top\times
K_{1}\times\dots\times K_{n})\mathrel{\mathfrak{to}}L\\\ (\exists
F:\mathscr{D}^{*}\mathrel{\mathfrak{to}}L)\varphi\lx@intercol\quad\Longleftrightarrow&(\exists
F:L)\varphi\end{array}$

We shall not use the notation $(\exists F:L)\varphi$ again, except when
discussing meta-theoretical properties of ${\mathsf{FSO}_{\mathscr{D}}}$.

####  3.7.3. Choice and Comprehension

We list here some important straightforward consequences of the Functional
Choice Axioms of §3.4.5 pertaining to Product Types.

######  Theorem 22.

${\mathsf{FSO}_{\mathscr{D}}}$ proves the following generalizations of the
Functional Choice Axioms of §3.4.5:

  * •

_$\mathrm{HF}$ -Bounded Choice_.

$(\forall\tilde{x}\mathrel{\dot{\in}}\Pi)(\exists
k\mathrel{\dot{\in}}L)\varphi(\tilde{x},k)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\exists\textsc{{f}}:\Pi\mathrel{\mathfrak{to}}L)(\forall\tilde{x}\mathrel{\dot{\in}}\Pi)\varphi(\tilde{x},\textsc{{f}}(\tilde{x}))$

  * •

_Iterated $\mathrm{HF}$-Bounded Choice_.

$(\forall
k\mathrel{\dot{\in}}K)(\exists\textsc{{f}}:\Pi\mathrel{\mathfrak{to}}L)\varphi(k,\textsc{{f}})\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\left(\exists\textsc{{f}}:\Pi\mathrel{\mathfrak{to}}L^{K}\right)(\forall
k\mathrel{\dot{\in}}K)\varphi(k,\textsc{{f}}(-,k))$

######  Theorem 23 (Comprehension for Product Types).

${\mathsf{FSO}_{\mathscr{D}}}$ proves the following form of Comprehension,
where $V$ does not occur free in $\varphi$:

$(\exists
V:\Pi\mathrel{\mathfrak{to}}2)(\forall\tilde{x}\mathrel{\dot{\in}}\Pi)\big{(}V(\tilde{x})\leavevmode\nobreak\
\leavevmode\nobreak\ \Longleftrightarrow\leavevmode\nobreak\
\leavevmode\nobreak\ \varphi(\tilde{x})\big{)}$

######  Proof 3.5.

We require

$(\exists
V:\Pi\mathrel{\mathfrak{to}}2)(\forall\tilde{x}\mathrel{\dot{\in}}\Pi)\big{(}V(\tilde{x})\mathrel{\doteq}1\leavevmode\nobreak\
\leavevmode\nobreak\ \Longleftrightarrow\leavevmode\nobreak\
\leavevmode\nobreak\ \varphi(x)\big{)}$

By excluded middle, bounded existentials and generalization we have,

$(\forall\tilde{x}\mathrel{\dot{\in}}\Pi)(\exists
k\mathrel{\dot{\in}}2)\big{(}k\mathrel{\doteq}1\leavevmode\nobreak\
\leavevmode\nobreak\ \Longleftrightarrow\leavevmode\nobreak\
\leavevmode\nobreak\ \varphi(x)\big{)}$

and we conclude by $\mathrm{HF}$-Bounded Choice.

  1. (1)

In the case of $\Pi=\mathscr{D}^{*}$, Theorem 23 gives Comprehension for
characteristic functions:

$(\exists X:\mathscr{D}^{*}\mathrel{\mathfrak{to}}2)(\forall x)\big{(}x\in
X\leavevmode\nobreak\ \leavevmode\nobreak\
\Longleftrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi(x)\big{)}$ ($X$ not free in $\varphi$)

  2. (2)

We have the following form of Comprehension for $\mathrm{HF}$-Sets:

$(\exists\ell\mathrel{\dot{\subseteq}}K)(\forall
k\mathrel{\dot{\in}}K)\big{(}k\mathrel{\dot{\in}}\ell\leavevmode\nobreak\
\leavevmode\nobreak\ \Longleftrightarrow\leavevmode\nobreak\
\leavevmode\nobreak\ \varphi(k)\big{)}$ ($\ell$ not free in $\varphi$)

  3. (3)

Using Comprehension for $\mathrm{HF}$-Sets, the well-orders on
$\mathrm{HF}$-Sets given by Remark 12 give the following Induction Scheme for
$\mathrm{HF}$-Sets:

$(\forall
k\mathrel{\dot{\in}}K)\Big{[}(\forall\ell\mathrel{\dot{\in}}K)\big{(}\ell\prec_{K}k\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \varphi(\ell)\big{)}\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi(k)\Big{]}\quad\Longrightarrow\quad(\forall
k\mathrel{\dot{\in}}K)\varphi(k)$

where $\preceq_{K}$ is the well-order on $K$ given by Remark 12.

##  4\. Game Positions

This Section and the next one describe our setting for games. The games we
consider ultimately aim at formalizing acceptance games of tree automata (§6),
and thus must encompass acceptance games for _non-deterministic_ tree
automata. We shall therefore give a setting for infinite games, with players
_Proponent_ $\mathsf{P}$ (corresponding to _Automaton_ or $\exists$loïse) and
_Opponent_ $\mathsf{O}$ (corresponding to _Pathfinder_ or $\forall$bérlard).
In the case of acceptance games, $\mathsf{P}$ plays for acceptance and
$\mathsf{O}$ plays for rejection, and in the particular case of non-
deterministic automata, $\mathsf{P}$ chooses transitions from the non-
deterministic transition relation, while $\mathsf{O}$ chooses tree directions
$d\in\mathscr{D}$, with the aim of building an infinite path. This leads to an
inherent asymmetry in the very notion of games, where, from a game position
with a given tree position $x\in\mathscr{D}^{*}$, $\mathsf{P}$ can only go to
game positions with tree position $x$, while $\mathsf{O}$ must go to a game
position with tree position a successor of $x$.

Due to the fact that we cannot access the usual primitive recursive codings in
the monadic language, we will only consider games that are ‘superposed’ onto
the infinite $\mathscr{D}$-tree, with only boundedly many positions associated
with each tree node. Such a setting indeed suffices for the case of acceptance
games arising from tree automata. Assume that we are given disjoint non-empty
$\mathrm{HF}$-Sets $\mathsf{P}_{\mathcal{G}}$ and $\mathsf{O}_{\mathcal{G}}$
of _Proponent_ and _Opponent_ labels respectively. Intuitively, _Proponent_
will play from game positions of the form

$\mathscr{D}^{*}\times\mathsf{P}_{\mathcal{G}}$

while _Opponent_ will play from positions of the form

$\mathscr{D}^{*}\times\mathsf{O}_{\mathcal{G}}$

A game will be given by specifying edge relations of the form

$(x,k)\mathchoice{\mathrel{\overset{}{\underset{\mathsf{P}}{\longrightarrow}}}}{\mathrel{\longrightarrow_{\mathsf{P}}}}{\longrightarrow_{\mathsf{P}}}{\longrightarrow_{\mathsf{P}}}(x,\ell)\quad\text{or}\quad(x,\ell)\mathchoice{\mathrel{\overset{}{\underset{\mathsf{O}}{\longrightarrow}}}}{\mathrel{\longrightarrow_{\mathsf{O}}}}{\longrightarrow_{\mathsf{O}}}{\longrightarrow_{\mathsf{O}}}(x.d,k)\qquad\text{where
$k\in\mathsf{P}_{\mathcal{G}}$, $\ell\in\mathsf{O}_{\mathcal{G}}$ and
$d\in\mathscr{D}$.}$

So $\mathsf{P}$ can only move to a game position with the same underlying tree
position, while $\mathsf{O}$ is forced to move to a game position with a
successor underlying tree position. This induces a dag structure on game
positions, whose underlying partial order $\trianglelefteq_{\mathcal{G}}$ is
the lexicographic product of the usual tree order with the one setting
$\mathsf{P}$-labels smaller than all $\mathsf{O}$-labels. The games we shall
consider will all be subrelations of $\trianglelefteq_{\mathcal{G}}$.

This Section is devoted to the definition of this dag structure. We shall also
prove some basic results related to induction in §4.2 and to infinite paths in
§4.3. These will help proving some similar results for games in §5, for which
arguments are more naturally given at the level of
$\trianglelefteq_{\mathcal{G}}$.

###  4.1. A Partial Order of Game Positions

We first introduce the formal notion of labels of game positions.

[Labels of Game Positions] _Labels of game positions_ are pairs
$(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})$ of $\mathrm{HF}$-terms
satisfying the following formula:

$\mathrm{Labels}(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})\quad\mathrel{:=}\quad\lnot(\exists
k\mathrel{\dot{\in}}\mathsf{P}_{\mathcal{G}}\cap\mathsf{O}_{\mathcal{G}})\leavevmode\nobreak\
\leavevmode\nobreak\ \land\leavevmode\nobreak\ \leavevmode\nobreak\ (\exists
k\mathrel{\dot{\in}}\mathsf{P}_{\mathcal{G}})\leavevmode\nobreak\
\leavevmode\nobreak\ \land\leavevmode\nobreak\ \leavevmode\nobreak\
(\exists\ell\mathrel{\dot{\in}}\mathsf{O}_{\mathcal{G}})$

We write $\mathsf{P}\mathsf{O}_{\mathcal{G}}$ for
$\mathsf{P}_{\mathcal{G}}\cup\mathsf{O}_{\mathcal{G}}$. When no ambiguity
arises, we write $\mathsf{P}$, $\mathsf{O}$ and $\mathsf{P}\mathsf{O}$ for
$\mathsf{P}_{\mathcal{G}}$, $\mathsf{O}_{\mathcal{G}}$ and
$\mathsf{P}\mathsf{O}_{\mathcal{G}}$ respectively.

Assume $(\mathsf{P},\mathsf{O})$ are labels of game positions. Intuitively,
game positions are pairs $(x,k)$ with $x\in\mathscr{D}^{*}$ and
$k\in\mathsf{P}\mathsf{O}$, Proponent’s positions are game positions with
$k\in\mathsf{P}$ and Opponent’s positions are game positions with
$k\in\mathsf{O}$. To summarize, we have the informal correspondence:

$\begin{array}[]{l !{\qquad}
l}\mathscr{D}^{*}\times\mathsf{P}\mathsf{O}&\text{Game positions}\\\
\mathscr{D}^{*}\times\mathsf{P}&\text{Proponent's positions}\\\
\mathscr{D}^{*}\times\mathsf{O}&\text{Opponent's positions}\end{array}$

We will throughout the paper use the following notations to manipulate game
positions and sets of game positions.

[Game Positions] We introduce the following notations, assuming
$\mathrm{Labels}(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})$.

  1. (1)

Variables, written $u,v,w,\text{etc}$, range over game positions, that is over
pairs $(x,k)$ with $x$ an Individual variable and $k$ an
$\mathrm{HF}$-variable ranging over $\mathsf{P}\mathsf{O}_{\mathcal{G}}$.

  2. (2)

Sets of game positions, written $U,V,W,\text{etc}$, range over Functions
$\mathscr{D}^{*}\times\mathsf{P}\mathsf{O}_{\mathcal{G}}\mathrel{\mathfrak{to}}2$.
We will systematically use the following notations:

$\begin{array}[]{l !{~~\deq~~} l !{\qquad}
l}V:\mathcal{G}_{\phantom{\mathsf{O}}}\mathrel{\mathfrak{to}}2\hfil\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&V:\mathscr{D}^{*}\times\mathsf{P}\mathsf{O}_{\mathcal{G}}\mathrel{\mathfrak{to}}2&\text{(sets
of Game positions)}\\\
V:\mathcal{G}_{\mathsf{P}}\mathrel{\mathfrak{to}}2\hfil\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&V:\mathscr{D}^{*}\times\mathsf{P}_{\mathcal{G}}\phantom{\mathsf{O}}\mathrel{\mathfrak{to}}2&\text{(sets
of Proponent's positions)}\\\
V:\mathcal{G}_{\mathsf{O}}\mathrel{\mathfrak{to}}2\hfil\lx@intercol\leavevmode\nobreak\
\leavevmode\nobreak\ \mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\
&V:\mathscr{D}^{*}\times\mathsf{O}_{\mathcal{G}}\phantom{\mathsf{P}}\mathrel{\mathfrak{to}}2&\text{(sets
of Opponent's positions)}\end{array}$

We often write $v\in V$ or $V(v)$ for $V(v)\mathrel{\doteq}1$.

  3. (3)

For a set of game positions $V$, we write $V_{\mathsf{P}}$ and
$V_{\mathsf{O}}$ for the $\mathsf{P}$ and $\mathsf{O}$ subsets of $V$
respectively. This amounts to the following abbreviations:

$\begin{array}[]{r !{~~\deq~~} l}v\in
V_{\mathsf{P}}\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &v\in
V\leavevmode\nobreak\ \leavevmode\nobreak\ \land\leavevmode\nobreak\
\leavevmode\nobreak\ v\in(\mathscr{D}^{*}\times\mathsf{P}_{\mathcal{G}})\\\
v\in V_{\mathsf{O}}\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &v\in
V\leavevmode\nobreak\ \leavevmode\nobreak\ \land\leavevmode\nobreak\
\leavevmode\nobreak\
v\in(\mathscr{D}^{*}\times\mathsf{O}_{\mathcal{G}})\end{array}$

Intuitively, $V_{\mathsf{P}}$ represents
$V\cap(\mathscr{D}^{*}\times\mathsf{P}_{\mathcal{G}})$ while $V_{\mathsf{O}}$
represents $V\cap(\mathscr{D}^{*}\times\mathsf{O}_{\mathcal{G}})$.

  4. (4)

In formulae we interpret quantifiers over (sets of) game positions as follows:

$\begin{array}[]{r !{~~\deq~~} l}(\exists
v)\varphi\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &(\exists
x)(\exists\ell\mathrel{\dot{\in}}\mathsf{P}\mathsf{O}_{\mathcal{G}})\varphi[(x,\ell)/v]\\\
(\exists V)\varphi\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ &(\exists
V:\mathcal{G}\mathrel{\mathfrak{to}}2)\varphi\end{array}$

where, in the $\exists v$ case, we choose $x,\ell$ not free in $\varphi$.

We now introduce the partial order $\trianglelefteq$ on game positions.

[Partial Order on Game Positions] The relations
$\vartriangleleft_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}$,
$\trianglelefteq_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}$ and
$\mathsf{s}^{\vartriangleleft}_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}$,
where $\mathsf{P}_{\mathcal{G}}$ and $\mathsf{O}_{\mathcal{G}}$ are
$\mathrm{HF}$-variables, are defined as follows:

$\begin{array}[]{r @{~~}c@{~~} l c l}(x,k)\leavevmode\nobreak\
\leavevmode\nobreak\
&\vartriangleleft_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\
&(y,\ell)&\mathrel{:=}&x\mathrel{\dot{<}}y\leavevmode\nobreak\
\lor\leavevmode\nobreak\ (x\mathrel{\doteq}y\leavevmode\nobreak\
\land\leavevmode\nobreak\
k\mathrel{\dot{\in}}\mathsf{P}_{\mathcal{G}}\leavevmode\nobreak\
\land\leavevmode\nobreak\ \ell\mathrel{\dot{\in}}\mathsf{O}_{\mathcal{G}})\\\
u\leavevmode\nobreak\ \leavevmode\nobreak\
&\trianglelefteq_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}\hfil\leavevmode\nobreak\
\leavevmode\nobreak\
&v&\mathrel{:=}&u\vartriangleleft_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}v\leavevmode\nobreak\
\lor\leavevmode\nobreak\ u=v\\\
\lx@intercol\hfil\mathsf{s}^{\vartriangleleft}_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}(u,v)\lx@intercol&\mathrel{:=}&u\vartriangleleft_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}v\leavevmode\nobreak\
\land\leavevmode\nobreak\ \lnot(\exists
w)\left(u\vartriangleleft_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}w\vartriangleleft_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}v\right)\end{array}$

When no ambiguity arises, we write $\vartriangleleft_{\mathcal{G}}$,
$\trianglelefteq_{\mathcal{G}}$ and
$\mathsf{s}^{\vartriangleleft}_{\mathcal{G}}$, or even $\vartriangleleft$,
$\trianglelefteq$ and $\mathsf{s}^{\vartriangleleft}$ for
$\vartriangleleft_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}$,
$\trianglelefteq_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}$ and
$\mathsf{s}^{\vartriangleleft}_{(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})}$
respectively.

Note that the formula $\mathsf{s}^{\vartriangleleft}(-,-)$ is actually
bounded, since by Notation 4.1.(1), the variable $w$ ranges over game
positions, so that $(\exists w)$ stands for $(\exists
w\in\mathscr{D}^{*}\times\mathsf{P}\mathsf{O})$.

We note a number of useful properties of $\vartriangleleft$, in particular
that it is a discrete partial order.

######  Proposition 24.

${\mathsf{FSO}_{\mathscr{D}}}$ proves following, under the assumption
$\mathrm{Labels}(\mathsf{P},\mathsf{O})$.

  1. (1)

$u\vartriangleleft v\vartriangleleft w\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
u\vartriangleleft w$

  2. (2)

$\lnot(u\vartriangleleft u)$

  3. (3)

$u\trianglelefteq v\trianglelefteq u\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ u=v$

  4. (4)

$u\vartriangleleft v\quad\Longleftrightarrow\quad(\exists w\trianglelefteq
v)(\mathsf{s}^{\vartriangleleft}(u,w))\quad\Longleftrightarrow\quad(\exists
w^{\prime}\trianglerighteq u)(\mathsf{s}^{\vartriangleleft}(w^{\prime},v))$

  5. (5)

$(\forall
k\in\mathsf{P})\big{(}u\trianglelefteq(\dot{\varepsilon},k)\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
u=(\dot{\varepsilon},k)\big{)}$

###  4.2. Induction and Recursion

We now present some basic results on induction and recursion w.r.t. the
partial order on game positions.

draftnotes

We can show that $\vartriangleleft$ satisfies well-founded induction from the
induction principle on the underlying tree.

######  Theorem 25 ($\vartriangleleft$-Induction).

${\mathsf{FSO}_{\mathscr{D}}}$ proves the following, under the assumption
$\mathrm{Labels}(\mathsf{P},\mathsf{O})$.

$(\forall V)\Big{(}(\forall v)\big{[}(\forall u\vartriangleleft v)(u\in
V)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ v\in
V\big{]}\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\forall v)(v\in
V)\Big{)}$

######  Proof 4.2.

Let $V$ be such that, for any game position $v$:

$(\forall u\vartriangleleft v)\leavevmode\nobreak\
\big{(}V(u)\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ V(v)\big{)}$ (10)

We show that

$(\forall x)(\forall
y\mathrel{\dot{\leq}}x)(\forall\ell\mathrel{\dot{\in}}\mathsf{P}\mathsf{O})\big{(}(y,\ell)\in
V\big{)}$

by induction on $x$, whence the theorem will follow.

Suppose that $x=\dot{\varepsilon}$, and so $y=\dot{\varepsilon}$. We prove
first the statement for arbitrary $\ell\mathrel{\dot{\in}}\mathsf{P}$; in this
case notice that there is no $u$ such that
$u\vartriangleleft(\dot{\varepsilon},\ell)$, and so we vacuously satisfy the
LHS of (10) above. Therefore we have that $(\dot{\varepsilon},\ell)\in V$.
Otherwise $\ell\mathrel{\dot{\in}}\mathsf{O}$ and every
$u\vartriangleleft(\dot{\varepsilon},\ell)$ is of the form
$(\dot{\varepsilon},k)$ for some $k\mathrel{\dot{\in}}\mathsf{P}$, and we have
just shown that such $u$ must be contained in $V$. Therefore we can conclude
that $(\dot{\varepsilon},\ell)\in V$, again by (10), as required.

Now we consider the inductive step, assuming the statement above is already
true for $x$ and considering the case of $\mathsf{S}_{d}x$. If
$y\mathrel{\dot{\leq}}\mathsf{S}_{d}x$ then either $y\mathrel{\dot{\leq}}x$ or
$y\mathrel{\doteq}\mathsf{S}_{d}x$. In the former case we have by the
inductive hypothesis that, for any
$\ell\mathrel{\dot{\in}}\mathsf{P}\mathsf{O}$, $(y,\ell)\in V$. So assume that
$y\mathrel{\doteq}\mathsf{S}_{d}x$. Again we distinguish when
$\ell\mathrel{\dot{\in}}\mathsf{P}$ and when
$\ell\mathrel{\dot{\in}}\mathsf{O}$ in order to exhibit the LHS of (10) above.
In the former case, notice that any $(z,k)\vartriangleleft(y,\ell)$ is such
that $z\mathrel{\dot{\leq}}x$, and so we have that $(z,k)\in V$ by the
inductive hypothesis; thus $(y,\ell)\in V$ by (10). In the latter case (when
$\ell\mathrel{\dot{\in}}\mathsf{O}$) we have for any
$(z,k)\vartriangleleft(y,\ell)$ either $z\mathrel{\dot{\leq}}x$ or
($z\mathrel{\doteq}\mathsf{S}_{d}x$ and $k\mathrel{\dot{\in}}\mathsf{P}$). In
both cases we have seen that $(z,k)\in V$, and so again we have that
$(y,\ell)\in V$ by (10).

Since $\vartriangleleft$ is a partial order with induction, comprehension
(Theorem 23) gives a _Recursion Theorem_ , which allows us to define a set of
game positions $V$ by induction on game positions. This requires the value of
$V$ at a position $v$ to be determined by its values at positions
$u\vartriangleleft v$. Thus, if the value of $V$ at $v$ is given by a formula
$\varphi(V,v)$, we assume that the following formula holds

$\mathrm{Rec}(\varphi)\leavevmode\nobreak\ \leavevmode\nobreak\
\mathrel{:=}\leavevmode\nobreak\ \leavevmode\nobreak\ (\forall v)(\forall
V,V^{\prime})\Big{[}(\forall w\vartriangleleft v)\big{(}Vw\leavevmode\nobreak\
\Leftrightarrow\leavevmode\nobreak\ V^{\prime}w\big{)}\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\big{(}\varphi(V,v)\leavevmode\nobreak\ \Leftrightarrow\leavevmode\nobreak\
\varphi(V^{\prime},v)\big{)}\Big{]}$

The Recursion Theorem says that, assuming $\mathrm{Rec}(\varphi)$, the set of
game positions $V$ given by

$Vv\quad\Longleftrightarrow\quad(\forall U)\Big{[}(\forall u\trianglelefteq
v)\big{(}Uu\leavevmode\nobreak\ \Leftrightarrow\leavevmode\nobreak\
\varphi(U,u)\big{)}\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ Uv\Big{]}$

is the unique set of game positions such that

$Vv\quad\Longleftrightarrow\quad\varphi(V,v)$

######  Proposition 26 (Recursion Theorem).

${\mathsf{FSO}_{\mathscr{D}}}$ proves that
$\mathrm{Labels}(\mathsf{P},\mathsf{O})\land\mathrm{Rec}(\varphi)$ imply

$\begin{array}[]{l r !{~~\longlimp~~} l}\lx@intercol\hfil(\forall
v)\bigg{(}Vv\leavevmode\nobreak\ \Longleftrightarrow\leavevmode\nobreak\
(\forall U)\Big{[}(\forall u\trianglelefteq v)\big{(}Uu\leavevmode\nobreak\
\Leftrightarrow\leavevmode\nobreak\ \varphi(U,u)\big{)}\leavevmode\nobreak\
\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
Uv\Big{]}\bigg{)}\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\lx@intercol&(\forall v)\left(Vv\leavevmode\nobreak\
\Leftrightarrow\leavevmode\nobreak\ \varphi(V,v)\right)\\\ \land&(\forall
v)(Vv\leavevmode\nobreak\ \Leftrightarrow\leavevmode\nobreak\
\varphi(V,v))\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\forall
v)(Uv\leavevmode\nobreak\ \Leftrightarrow\leavevmode\nobreak\
\varphi(U,v))\lx@intercol\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ &(\forall
v)\left(Vv\leavevmode\nobreak\ \Leftrightarrow\leavevmode\nobreak\
Uv\right)\end{array}$

######  Proof 4.3.

Consider a formula $\varphi(V,v)$ and assume $\mathrm{Rec}(\varphi)$ and
$\mathrm{Labels}(\mathsf{P},\mathsf{O})$. We begin with the second part of the
statement, namely the uniqueness part. Fix $V,U$. By
$\vartriangleleft$-induction on $v$, we show that $\mathsf{FSO}$ proves the
following formula $\psi(v)=\psi(V,U,v)$:

$(\forall u\trianglelefteq
v)(Vu\Leftrightarrow\varphi(V,u))\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ (\forall
u\trianglelefteq v)(Uu\Leftrightarrow\varphi(U,u))\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\forall u\trianglelefteq v)(Vu\Leftrightarrow Uu)$

Let $v$ and assume both premises of $\psi(v)$, as well as $\psi(w)$ for all
$w\vartriangleleft v$. The premises of $\psi(v)$ imply that of $\psi(w)$ for
$w\vartriangleleft v$, so that we have $(Vw\Leftrightarrow Uw)$ for all
$w\vartriangleleft v$. Hence, given $u\trianglelefteq v$, if
$u\vartriangleleft v$ then we are done. It thus remains to show
$(Vv\Leftrightarrow Uv)$. Thanks to the premises of $\psi(v)$, this amounts to
showing $\varphi(V,v)\Leftrightarrow\varphi(U,v)$, which itself follows from
$\mathrm{Rec}(\varphi)$, since $(Vw\Leftrightarrow Uw)$ for all
$w\vartriangleleft v$.

We now turn to the first part of the statement. Let $V$ such that

$Vv\quad\Longleftrightarrow\quad(\forall U)\Big{[}(\forall u\trianglelefteq
v)\big{(}Uu\leavevmode\nobreak\ \Leftrightarrow\leavevmode\nobreak\
\varphi(U,u)\big{)}\leavevmode\nobreak\ \leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ Uv\Big{]}$

By $\vartriangleleft$-induction on $v$, we show that $\mathsf{FSO}$ proves the
following formula

$\theta(v)\quad\mathrel{:=}\quad(\forall u\trianglelefteq
v)\underbrace{\big{(}Vu\leavevmode\nobreak\ \leavevmode\nobreak\
\Longleftrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\varphi(V,u)\big{)}}_{\vartheta(u)}$

So let $v$ and assume $\theta(w)$ for all $w\vartriangleleft v$. Given
$u\trianglelefteq v$, if $u\vartriangleleft v$ then $\vartheta(u)$ follows
from $\theta(u)$. It thus remains to show $\vartheta(v)$. We consider the two
implications separately.

  * •

_Case of $\varphi(V,v)\Longrightarrow Vv$._ Assume $\varphi(V,v)$. By
definition of $V$, we are done if we show

$(\forall U)\Big{[}(\forall u\trianglelefteq v)\big{(}Uu\leavevmode\nobreak\
\Leftrightarrow\leavevmode\nobreak\ \varphi(U,u)\big{)}\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
Uv\Big{]}$

Given $U$ such that $\big{(}Uu\leavevmode\nobreak\
\Leftrightarrow\leavevmode\nobreak\ \varphi(U,u)\big{)}$ for all
$u\trianglelefteq v$, we obtain $Uv$ from $\varphi(U,v)$, which itself follows
$\varphi(V,v)$ and $\mathrm{Rec}(\varphi)$. The premise of
$\mathrm{Rec}(\varphi)$ follows from $(\forall w\vartriangleleft
v)\psi(V,U,w)$, whose premises are in turn given by resp. $(\forall
w\vartriangleleft v)\vartheta(w)$ and the assumption on $U$.

  * •

_Case of $Vv\Longrightarrow\varphi(V,v)$._ Assume $Vv$. By comprehension
(Theorem 23) let $U$ such that

$Uu\quad\Longleftrightarrow\quad\Big{[}(u\vartriangleleft
v\leavevmode\nobreak\ \land\leavevmode\nobreak\ Vu)\leavevmode\nobreak\
\lor\leavevmode\nobreak\ \big{(}u=v\leavevmode\nobreak\
\land\leavevmode\nobreak\ \varphi(V,v)\big{)}\Big{]}$

We obtain $\varphi(V,v)$ from $Uv$, which in turn by def. of $V$ follows from
$(\forall u\trianglelefteq v)\big{(}Uu\leavevmode\nobreak\
\Leftrightarrow\leavevmode\nobreak\ \varphi(U,u)\big{)}$. In order to show the
latter, note that by definition of $U$ we have $(Uu\Leftrightarrow Vu)$ for
all $u\vartriangleleft v$. Hence $\mathrm{Rec}(\varphi)$ gives
$\varphi(U,v)\Leftrightarrow\varphi(V,v)$ and we get
$(Uv\Leftrightarrow\varphi(U,v))$ from the definition of $U$. In the case of
$u\vartriangleleft v$, namely $(Uu\Leftrightarrow\varphi(U,u))$, we have
$(\forall w\trianglelefteq u)(Uw\Leftrightarrow Vw)$ so that
$\mathrm{Rec}(\varphi)$ implies $\varphi(U,u)\Leftrightarrow\varphi(V,u)$ and
the result follows form $\vartheta(u)$.

###  4.3. Infinite Paths

We develop here a notion of infinite paths (i.e. unbounded linearly order
sets) for the partial order $\trianglelefteq$ on game positions. This material
will be useful in Section 5.2 to handle properties of infinite plays in games
which intrinsically rely on the particular structure of the relation
$\trianglelefteq$ on game positions. A typical example is the Predecessor
Lemma 34.

[Game Paths] Let $\mathsf{P},\mathsf{O}$ be $\mathrm{HF}$-variables. Given a
game position $u$ and a set of game positions $U$, we say that $U$ is a _path
from $u$_ if the following formula $\mathrm{Path}(\mathsf{P},\mathsf{O},u,U)$
holds:

$\mathrm{Path}(\mathsf{P},\mathsf{O},u,U)\quad\mathrel{:=}\quad\left\\{\begin{array}[]{c
l}&u\in U\\\ \land&(\forall v\in U)(u\trianglelefteq v)\\\ \land&(\forall v\in
U)(\exists w\in U)(\mathsf{s}^{\vartriangleleft}(v,w))\\\ \land&(\forall
v,w\in U)(w\vartriangleleft v\leavevmode\nobreak\ \lor\leavevmode\nobreak\
v=w\leavevmode\nobreak\ \lor\leavevmode\nobreak\ v\vartriangleleft
w)\end{array}\right.$

We write $\mathrm{Path}(u,U)$ when $\mathsf{P}$ and $\mathsf{O}$ are clear
from the context.

As a preparation to the Predecessor Lemma 34 for Infinite Plays, we prove here
the analogous property for infinite paths.

######  Lemma 27 (Predecessor Lemma for Game Paths).

${\mathsf{FSO}_{\mathscr{D}}}$ proves the following. Assuming that
$\mathrm{Labels}(\mathsf{P},\mathsf{O})$ and that
$\mathrm{Path}(\mathsf{P},\mathsf{O},u_{0},U)$ hold for a game position
$u_{0}$ and a set of game positions $U$, we have

$(\forall v\in U)\left[u_{0}\vartriangleleft v\leavevmode\nobreak\
\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
(\exists u\in U)(\mathsf{s}^{\vartriangleleft}(u,v))\right]$

The proof of Lemma 27 relies on the following usual maximality principle for
non-empty linearly-ordered bounded sets.

######  Lemma 28.

${\mathsf{FSO}_{\mathscr{D}}}$ proves the following, assuming
$\mathrm{Labels}(\mathsf{P},\mathsf{O})$. Given a set of game positions $V$,
if $V$ is bounded (i.e. $(\exists u)(\forall v\in V)(v\vartriangleleft u)$),
non-empty and linearly ordered, then $V$ has a maximum element: $(\exists u\in
V)(\forall v\in V)(v\trianglelefteq u)$.

######  Proof 4.4.

By $\vartriangleleft$-induction, we prove the following property:

  1. (1)

For all $u$, for all $V$, if $V$ is non-empty, linearly ordered by
$\vartriangleleft$ and such that $\forall v\in V(v\trianglelefteq u)$, then
$V$ has a $\vartriangleleft$-maximal element.

Let $u$ and $V$ satisfy the assumptions from 1 above, and assume 1 for all
$c\vartriangleleft u$. First, if $u=v$ for some $v\in V$, then $u$ is indeed
the maximal element of $V$. So we can assume $v\vartriangleleft u$ for all
$v\in V$.

By Comprehension for Product Types (Thm. 23), let $U$ be the set of all $w$
such that $\mathsf{s}^{\vartriangleleft}(w,u)$ and such that $v\trianglelefteq
w$ for some $v\in V$. For each $v\in V$, it follows from Proposition 24.(4)
that there is some $w\in U$ such that $v\trianglelefteq w$. In particular, $U$
is non-empty since $V$ is non-empty.

We claim the following:

######  Claim 28.1.

$(\forall w\in U)(\exists!\tilde{w}\in V)\underbrace{(\forall v\in
V)\Big{(}v\trianglelefteq w\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
v\trianglelefteq\tilde{w}\Big{)}}_{\vartheta(w,\tilde{w})}$

######  Proof 4.5 (Proof of Claim 28.1).

Let $w\in U$. By Comprehension for Product Types (Thm. 23), let $W$ be the set
of all $v\in V$ such that $v\trianglelefteq w$. Note that $W$ is non-empty by
definition of $U$. It is inherits the property of being linearly ordered from
$V$, and by construction it is bounded by $w$ with $w\vartriangleleft u$. By
induction hypothesis, $W$ has a maximal element, say $\tilde{w}$. We indeed
have $\tilde{w}\in V$ and $v\trianglelefteq\tilde{w}$ for all $v\in V$ with
$v\trianglelefteq w$. Since $\tilde{w}\trianglelefteq w$, uniqueness follows
from the antisymmetry of $\trianglelefteq$.

The remainder of the argument relies on the particular structure of
$\vartriangleleft$. Using Comprehension on $\mathrm{HF}$-Sets, it follows from
the definition of $\vartriangleleft$ that there is some $x\in\mathscr{D}^{*}$
and some $\mathrm{HF}$-Set $k$ such that $U$ is exactly the set of all
$(x,\ell)$ with $\ell\in k$. This observation allows us to show

######  Claim 28.2.

$(\exists\tilde{w}_{m}\in V)\underbrace{(\forall w\in U)(\forall\tilde{w}\in
V)\big{(}\vartheta(w,\tilde{w})\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\tilde{w}\trianglelefteq\tilde{w}_{m}\big{)}}_{\varphi(\tilde{w}_{m})}$

######  Proof 4.6 (Proof of Claim 28.2).

Write $\preceq$ for the well-order on $k$ given by Remark 12. By
$\preceq$-Induction (Remark 3.7.3.(3)) we show the following:

$(\forall\ell\in k)(\exists m\in k)\underbrace{(\forall
n\preceq\ell)(\forall\tilde{w}_{n},\tilde{w}_{m}\in
V)\big{(}\vartheta((x,n),\tilde{w}_{n})\leavevmode\nobreak\
\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\vartheta((x,m),\tilde{w}_{m})\leavevmode\nobreak\ \leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\tilde{w}_{n}\trianglelefteq\tilde{w}_{m}\big{)}}_{\psi(\ell,m)}$

Let $\ell\in k$ be such that the property holds for all
$\ell^{\prime}\prec\ell$. If $\ell$ is $\preceq$-minimal, the result follows
from the existence of a unique $\tilde{w}$ such that
$\vartheta((x,\ell),\tilde{w})$. Otherwise, let $\ell^{\prime}$ be the
$\preceq$-predecessor of $\ell$, and let $m\in k$ such that
$\psi(\ell^{\prime},m)$ be given by induction hypothesis. By Claim 28.1, let
$\tilde{w}_{\ell},\tilde{w}_{m}$ be the unique elements of $V$ such that
$\vartheta((x,\ell),\tilde{w}_{\ell})$ and $\vartheta((x,m),\tilde{w}_{m})$.
Since $V$ is linearly ordered, we have either that
$\tilde{w}_{m}\trianglelefteq\tilde{w}_{\ell}$ or that
$\tilde{w}_{m}\trianglelefteq\tilde{w}_{\ell}$. In the former case, we take
$\ell$ for the new $m$, and in the latter we keep the same $m$.

Since $U$ is non-empty, there is a $\preceq$-maximal $\ell\in k$. Let $m\in k$
such that $\psi(\ell,m)$, and by Claim 28.1, let $\tilde{w}_{m}\in V$ such
that $\vartheta((x,m),\tilde{w}_{m})$. By definition of $k$, we do have
$\tilde{w}\trianglelefteq\tilde{w}_{m}$ for all $\tilde{w}\in V$ with
$\vartheta(w,\tilde{w})$ for some $w\in U$. Hence we have that
$\varphi(\tilde{w}_{m})$.

Consider now $\tilde{w}_{m}\in V$ such that $\varphi(\tilde{w}_{m})$. As noted
above, for all $v\in V$ there is some $w\in U$ such that $v\vartriangleleft
w$. But we also have $v\trianglelefteq\tilde{w}$ where $\tilde{w}$ is unique
such that $\vartheta(w,\tilde{w})$. It thus follows that
$v\trianglelefteq\tilde{w}_{m}$ for all $v\in V$.

This concludes the proof of Lemma 28.

We can now prove Lemma 27.

######  Proof 4.7 (Proof of Lemma 27).

Fix $v\in U$ with $u_{0}\vartriangleleft v$. By Comprehension for Product
Types (Thm. 23), let $W$ be the set of all $w\in U$ such that
$w\vartriangleleft v$. Since $u_{0}\vartriangleleft v$ and
$\mathrm{Path}(u_{0},U)$, the set $W$ is non-empty, linearly ordered and
bounded by $v$. By Lemma 28, it has a maximal element, say $w$. We have
$u_{0}\trianglelefteq w$ and $w\vartriangleleft v$. Moreover, by
$\mathrm{Path}(u_{0},U)$ there is some $\tilde{w}\in U$ such that
$\mathsf{s}^{\vartriangleleft}(w,\tilde{w})$. Again by
$\mathrm{Path}(u_{0},U)$, we have

$\left(\tilde{w}\vartriangleleft v\quad\lor\quad\tilde{w}=v\quad\lor\quad
v\vartriangleleft\tilde{w}\right)$

But $\tilde{w}\vartriangleleft v$ implies $\tilde{w}\trianglelefteq w$, a
contradiction, while $v\vartriangleleft\tilde{w}$ implies $w\vartriangleleft
v\vartriangleleft\tilde{w}$, contradicting
$\mathsf{s}^{\vartriangleleft}(w,\tilde{w})$. It thus follows that
$\tilde{w}=v$ and we are done.

##  5\. Infinite Two-Player Games

This Section is devoted to definitions and basic properties relating to games,
building on §4. We will use these games in §6 and §9 to formalize a basic
theory of tree automata in $\mathsf{FSO}$.

Our games are played on bipartite dags (with partial order
$\trianglelefteq_{\mathcal{G}}$) induced by labels of game positions
$(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})$ in the sense of §4.
Continuing §4, _Proponent_ will play from positions of the form

$\mathcal{G}_{\mathsf{P}}\quad=\quad\mathscr{D}^{*}\times\mathsf{P}_{\mathcal{G}}$

while _Opponent_ will play from positions of the form

$\mathcal{G}_{\mathsf{O}}\quad=\quad\mathscr{D}^{*}\times\mathsf{O}_{\mathcal{G}}$

A game will be given by specifying edge relations of the form

$(x,k)\mathchoice{\mathrel{\overset{}{\underset{\mathsf{P}}{\longrightarrow}}}}{\mathrel{\longrightarrow_{\mathsf{P}}}}{\longrightarrow_{\mathsf{P}}}{\longrightarrow_{\mathsf{P}}}(x,\ell)\quad\text{and}\quad(x,\ell)\mathchoice{\mathrel{\overset{}{\underset{\mathsf{O}}{\longrightarrow}}}}{\mathrel{\longrightarrow_{\mathsf{O}}}}{\longrightarrow_{\mathsf{O}}}{\longrightarrow_{\mathsf{O}}}(x.d,k)\qquad\text{where
$k\in\mathsf{P}_{\mathcal{G}}$, $\ell\in\mathsf{O}_{\mathcal{G}}$ and
$d\in\mathscr{D}$,}$

so that, for $\mathsf{J}$ either $\mathsf{P}$ or $\mathsf{O}$,

$u\vartriangleleft v\qquad\text{whenever}\qquad
u\mathchoice{\mathrel{\overset{}{\underset{\mathsf{J}}{\longrightarrow}}}}{\mathrel{\longrightarrow_{\mathsf{J}}}}{\longrightarrow_{\mathsf{J}}}{\longrightarrow_{\mathsf{J}}}v$

(actually even $\mathsf{s}^{\vartriangleleft}(u,v)$). We insist on the fact
that $\mathsf{P}$ can only move to a game position with the same underlying
tree position, while $\mathsf{O}$ is forced to move to a game position with a
successor tree position.

We first give basic definitions and results on games (§5.1) and infinite plays
(§5.2). Besides the above mentioned constraints on the shape of games, these
notions are standard. Our notion of strategy is presented in §5.3. A crucial
point here is that, w.r.t. our games, the monadic language imposes all
strategies to be by construction _positional_ in the usual sense (see e.g.
[Tho97]). Finally, §5.4 briefly discusses our setting for _winning_ in games,
and §5.5 presents in more detail the important particular case of _parity_
conditions. Parity conditions are one of the prominent formulations of winning
conditions for $\omega$-regular games. This is in particular due to the fact
that they are _positionally_ determined, i.e. the winner of a parity game can
always win with a _positional_ winning strategy [EJ91] (see also [Tho97,
Wal02, PP04]). This is of crucial importance in our setting as all our
strategies are inherently positional, due to the underlying limits on
expressivity in the language of $\mathsf{MSO}$. Finally, the Axiom
$(\mathit{PosDet})$ of Positional Determinacy of Parity Games is formulated in
§5.6.

###  5.1. Games

A game $\mathcal{G}$ will be given by labels of game positions
$\mathsf{P}_{\mathcal{G}}$ and $\mathsf{O}_{\mathcal{G}}$ together with
Functions

$E_{\mathsf{P}}:\mathcal{G}_{\mathsf{P}}\mathrel{\mathfrak{to}}\mathcal{P}_{*}(\mathsf{O}_{\mathcal{G}})\qquad\text{and}\qquad
E_{\mathsf{O}}:\mathcal{G}_{\mathsf{O}}\mathrel{\mathfrak{to}}\mathcal{P}_{*}(\mathscr{D}\times\mathsf{P}_{\mathcal{G}})$

where $\mathcal{P}_{*}(-)$ is the $\mathrm{HF}$-Function of §3.4.4.(4). Such
Functions $E_{\mathsf{P}},E_{\mathsf{O}}$ induce edge relations
$\mathchoice{\mathrel{\overset{}{\underset{\mathsf{P}_{\mathcal{G}}}{\longrightarrow}}}}{\mathrel{\longrightarrow_{\mathsf{P}_{\mathcal{G}}}}}{\longrightarrow_{\mathsf{P}_{\mathcal{G}}}}{\longrightarrow_{\mathsf{P}_{\mathcal{G}}}}$
and
$\mathchoice{\mathrel{\overset{}{\underset{\mathsf{O}_{\mathcal{G}}}{\longrightarrow}}}}{\mathrel{\longrightarrow_{\mathsf{O}_{\mathcal{G}}}}}{\longrightarrow_{\mathsf{O}_{\mathcal{G}}}}{\longrightarrow_{\mathsf{O}_{\mathcal{G}}}}$
given by

$\begin{array}[]{l !{\quad\text{iff}\quad}
l}(x,k)\mathchoice{\mathrel{\overset{}{\underset{\mathsf{P}_{\mathcal{G}}}{\longrightarrow}}}}{\mathrel{\longrightarrow_{\mathsf{P}_{\mathcal{G}}}}}{\longrightarrow_{\mathsf{P}_{\mathcal{G}}}}{\longrightarrow_{\mathsf{P}_{\mathcal{G}}}}(x,\ell)&\ell\in
E_{\mathsf{P}}(x,k)\\\
(x,\ell)\mathchoice{\mathrel{\overset{}{\underset{\mathsf{O}_{\mathcal{G}}}{\longrightarrow}}}}{\mathrel{\longrightarrow_{\mathsf{O}_{\mathcal{G}}}}}{\longrightarrow_{\mathsf{O}_{\mathcal{G}}}}{\longrightarrow_{\mathsf{O}_{\mathcal{G}}}}(x.d,k)&(d,k)\in
E_{\mathsf{O}}(x,\ell)\end{array}$

We make this formal in the following definition.

[Games and Edge Relations]

  1. (1)

A _game_ $\mathcal{G}$ is given by $\mathrm{HF}$-terms
$\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}}$ and Functions
$E(\mathcal{G})_{\mathsf{P}},E(\mathcal{G})_{\mathsf{O}}$ which satisfy the
following formula

$\mathrm{Game}(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}},E(\mathcal{G})_{\mathsf{P}},E(\mathcal{G})_{\mathsf{O}})\quad\mathrel{:=}\quad\left\\{\begin{array}[]{c
l}&\mathrm{Labels}(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}})\\\
\land&E(\mathcal{G})_{\mathsf{P}}:\mathcal{G}_{\mathsf{P}}\mathrel{\mathfrak{to}}\mathcal{P}_{*}(\mathsf{O}_{\mathcal{G}})\\\
\land&E(\mathcal{G})_{\mathsf{O}}:\mathcal{G}_{\mathsf{O}}\mathrel{\mathfrak{to}}\mathcal{P}_{*}(\mathscr{D}\times\mathsf{P}_{\mathcal{G}})\end{array}\right.$

We often write $\mathrm{Game}(\mathcal{G})$ for
$\mathrm{Game}(\mathsf{P}_{\mathcal{G}},\mathsf{O}_{\mathcal{G}},E(\mathcal{G})_{\mathsf{P}},E(\mathcal{G})_{\mathsf{O}})$.