\lmcsdoi
1646
\lmcsheadingLABEL:LastPageMar.Ā 27,Ā 2019Oct.Ā 23,Ā 2020
\optfullproofs
A Functional (Monadic) Second-Order Theory of Infinite Trees
Anupam Das
University of Birmingham
[email protected]
Ā andĀ
Colin Riba
LIP ā ENS de Lyon
[email protected]
(Date: March 12, 2024)
Abstract.
This paper presents a complete axiomatization of Monadic Second-Order
Logic (MSO) over infinite trees.
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
to infinite trees of the axioms of MSO on Ļ-words.
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 MSO.
We actually devise an extension of MSO,
called Functional (Monadic) Second-Order Logic (FSO),
which allows us to uniformly manipulate (hereditarily) finite sets
and corresponding labeled trees,
and whose language allows for higher
abstraction than that of MSO.
1. Introduction
This paper presents a complete axiomatization of Monadic Second-Order
Logic (MSO) over infinite trees.
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 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 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 and rules.
This condition on axiom/rule recognizability is typical in proof theory, where it is known as the Cook-Reckhow criterion [CR79].
The point is that proofs should be āeasily checkableā,
which rules out axiomatizations based on enumerations of all true formulae.
In this way, a complete axiomatization not only constitutes an alternative demonstration of Rabinās Tree theorem itself, by naive enumeration of formal derivations, but also yields a meaningful notion of āproof certificateā for theorems.
Our deduction system consists of 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 MSO on Ļ-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 MSO on various classes of linear orders
(see e.g.Ā [Sie70, BS73]),
as well as an axiomatization of Weak MSO (WMSO) over infinite
treesĀ [Sie78]
(WMSO is MSO with set quantifications restricted to finite sets).
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 μ-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
MSO and the modal μ-calculus over finite trees;
a reworking of the completeness of MSO on Ļ-wordsĀ [Sie70]
is proposed inĀ [Rib12];
andĀ [SV10] gives a model-theoretic completeness proof
for a fragment of the modal μ-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 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 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 MSO decides winning for (definable) games of finite graphs,
and which is obtained thanks to the completeness of MSO over Ļ-words.
The main expositional difficulty resides in the limited expressive power of the language of MSO.
To ameliorate this we actually devise an extension of MSO,
called Functional (Monadic) Second-Order Logic (FSO),
allowing uniform manipulation of (hereditarily) finite sets
and corresponding labeled infinite trees.
We intuitively see FSO as providing a language for higher
abstraction than that of MSO,
allowing a uniform formalization of automata and games
which would have been difficult to write down in MSO.
However, since FSO is interpretable in MSO (as we show), its language
has the same intrinsic limitations as the language
of 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 FSO.
This implies that only positional strategies
(w.r.t. our specific notion of acceptance games),
are expressible in FSO
and moreover that usually unproblematic reasoning on infinite plays
can become cumbersome in this setting.
There are several ways to translate 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 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 Ļ-words
are effectively equivalent to deterministic parity (or Muller, Rabin, Streett) automata
on Ļ-words.
In translations of 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 FSO via the completeness of MSO on
Ļ-wordsĀ [Sie70].
It is well-known that the 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 MSO theory of the full infinite D-ary
tree for an arbitrary non-empty finite set 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 FSO and MSO
with an axiom expressing the positional determinacy of parity games,
thereby obtaining complete axiomatizations.
We do not know yet whether the theory MSO ofĀ [DR15] is complete,
but let us mention that the axiomatization of WMSO
over infinite trees given inĀ [Sie78] augments the natural analogue
for trees of Peanoās arithmetic with an axiom of induction over finite trees.
Outline.
The paper is organized as follows.
We present the basic formal theory for MSO in §2
Our theory FSO is then presented in §3
and we sketch its mutual interpretability with MSO.
§4 and §5 discuss a formalization
of two-players infinite games in FSO,
and, in particular, we give a formulation of the axiom (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 FSO+(PosDet)).
§7 is an interlude discussing
a complete theory of MSO over Ļ-words
within the infinite paths of FSO.
Building on §6 and §7,
we then give our completeness argument for
FSO+(PosDet)
and MSO+(PosDet)
in §8.
Finally, §9 contains a proof of the Simulation Theorem in FSO.
The full versionĀ [DR20] gives details of proofs omitted here.
2. Preliminaries: MSO on Infinite Trees as a Second-Order Logic
We present here
a basic formal theory
of Monadic Second-Order Logic (MSO) over infinite trees.
This theory can be seen as an analogue for trees of Peanoās axioms
for second order arithmetic.
In order to obtain a complete theory, 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 MSODā of the infinite full D-ary tree Dā,
for D a finite non-empty set.
Both the language and the axioms of MSODā will depend on D.
The language of MSODā is the usual language of two-sorted first-order
logic, with one sort for Individuals
and one sort for (Monadic) Predicates.
The axioms of MSODā are the expected axioms on the relational structure
of the full D-ary tree, together with induction and comprehension.
The theory MSODā is essentially that ofĀ [Sie78],
but with second-order quantifications intended to range over arbitrary
subsets of Dā (instead of just finite ones), and without the axiom
of induction over finite trees.
We fix for the rest of this Section
a finite non-empty set D of tree directions.
2.1. The Language of MSODā
The language of MSODā has two sorts:
The sort of Individuals,
intended to range over tree positions pāDā.
We have infinitely many Individual variables x,y,z etc.
We also have one constant symbol ĪµĖ (for the root of Dā),
and one unary function symbol Sdā
for each dāD (for the successor function pā¦p.d).
Individual terms, written t,u,etc. are given by:
[TABLE]
The sort of (Monadic) Predicates,
with variables X,Y,Z,etc,
intended to range over sets of tree positions AāP(Dā).
There are no other term formers for this sort.
Formulae of MSODā are given by the following grammar:
[TABLE]
where t and u are Individual terms.
We use the usual derived formulae:
[TABLE]
We employ usual writing conventions for formulae,
for instance omitting internal and external brackets when appropriate.
2.2. The Deduction System of MSODā
Deduction for MSODā is defined by the system presented
in FigureĀ 1 and FigureĀ 2
(where Φ stands for
a multiset of formulae),
together with the following axioms.
Equality on Individuals:
[TABLE]
The Tree Axioms of FigureĀ 3.
Comprehension Scheme:
[TABLE]
Induction Axiom:
[TABLE]
Remark 1**.**
As usual, one can derive
ā¢(ĻāĻāĻ)\leavevmodeĀ ā\leavevmodeĀ ((Ļā§Ļ)āĻ)
and we have the Deduction Theorem:
[TABLE]
Indeed,
if Φ,Ļā¢Ļ, then one gets Φā¢Ā¬ĻāØĻ
by āØ-Elimination on the Excluded Middle Φā¢ĻāØĀ¬Ļ.
Conversely, if Φā¢Ā¬ĻāØĻ,
then one gets Φ,Ļā¢Ļ by āØ-Elimination.
One similarly obtains the Modus Ponens as a derived rule
[TABLE]
{nota}
Henceforth, we write MSO instead of MSODā when the set of directions
D is clear from the context.
3. A Functional Extension of MSO on Infinite Trees
In this Section,
we present (bounded) Functional (Monadic) Second-Order Logic
over the full D-ary tree (FSODā),
an extension of MSODā with (hereditarily) finite sets and bounded quantification over them.
As with MSODā in §2, we will simply write FSO
for FSODā when D is irrelevant or clear from the context.
FSODā 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 (PosDet)
expressing the positional determinacy of (suitably represented)
parity games (§5.6).
We will then show in §8
that FSODā+(PosDet) is complete.
3.1. Motivations and Overview.
Let us first discuss the motivations and guiding principles
in the design of FSODā.
As usual, within the language of MSODā presented in §2,
we can simulate a labeling of Dā over a finite non-empty set Ī£
[TABLE]
There are different ways to achieve this.
A possibility is, for say Ī£={a1ā,ā¦,anā},
to code T:DāāĪ£ using a tuple of Monadic variables
X1ā,ā¦,Xnā such that
[TABLE]
A more succinct coding could be obtained using ālognā
monadic variables to encode the letter index i of aiā 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 FSODā,
which is built around the following principles:
- (1)
FSODā has no primitive notion of Monadic variables.
Instead, FSODā has a primitive notion of Function variables,
of the form
[TABLE]
2. (2)
In addition, FSODā 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)
FSODā is faithfully interpretable in MSODā.
To this end, all quantifications over finite sets in FSODā-formulae
are required to be bounded.
In particular, there is a syntactic translation āØāā©
of FSODā-formulae to MSODā-formulae.
The basic idea of this translation is to interpret finite sets
using propositional logic,
and to interpret Functions
F:Dāā{a1ā,ā¦,anā}
as partitions X1ā,ā¦,Xnā of Dā.
But while FSODā handles free variables over finite sets in a uniform way,
the translation āØāā© only applies to FSODā-formulae
without free variables over finite sets.
This means that for an FSODā-formula Ļ(k) with k a variable over
finite sets, for each finite set Īŗ we will have a specific
MSODā-formula āØĻ(Īŗ)ā©.
Technically, the finite sets of FSODā will be the usual
hereditarily finite sets.
{defi}
Let V0ā:=ā
,
and Vn+1ā:=P(Vnā) for each nāN.
The set VĻā
of hereditarily finite sets (HF-sets)
is defined as
[TABLE]
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Ļā
is a model of ZFCā
(i.e. of ZFC without the infinity axiom).
{conv}
We will always assume the finite non-empty set D
of tree directions to be an HF-set.
The language of FSODā will have the same sort of Individuals as MSODā
and a sort for HF-sets, and
its Function variables will be
of the form F:DāāK for K a term over HF-sets (HF-term).
The design of FSODā is obtained as a compromise between the following two
conflicting desiderata:
- (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 MSODā.
This leads us to two peculiar design choices.
- (1)
We have, in addition to the above mentioned sorts, a distinct sort of
Functions over HF-sets.
This sort contains only constants (so these functions cannot be quantified over),
whose purpose is to provide Skolem functions
for those āā (bounded) statements over HF-sets
which are provable in ZFCā.
2. (2)
In order to facilitate the translation of FSODā to MSODā,
Function variables, written (F:K) (āF has codomain Kā),
cannot occur in HF-terms.
Formally, Functions (F:K) are only allowed in atomic formulae of the form
[TABLE]
The axioms of FSODā will contain the obvious adaptation of the Tree Axioms
and the Induction Axiom of MSODā.
We also have axioms defining the aforementioned Skolem functions.
In addition, the Comprehension Scheme of MSODā will be replaced
by Functional Choice Axioms
allowing us to define Functions F:DāāK
from āā-statements:
[TABLE]
Remark 3**.**
Functional Choice Axioms* as above
actually amount to Comprehension in MSO (§2.2).
Such axioms do not create choice predicates for Individuals,
which are known to be undefinable in
MSOĀ [GS83, CL07],
and moreover to break decidability when added to the language of
MSOĀ [BG00, CL07].*
The rest of this Section is organized as follows.
The system FSODā is defined in §3.2-3.4,
and its (expected)
interpretation in the standard model of D-ary trees
is given in §3.5.
Then in §3.6 we discuss the interpretation of FSODā in MSODā
and a straightforward embedding of MSODā in FSODā.
Finally, §3.7 presents notation whose purpose is to
allow some flexibility in the manipulation of functions.
The language and axioms of FSODā are summarized in FigureĀ 5,
with references to the relevant parts of the text.
3.2. The Language of FSODā
We now formally define the language of FSODā, for D an HF-set.
It consists of the the following sorts:
The sort of Hereditarily finite (HF) sets,
with infinitely many HF-variables k,ā etc.,
and with one constant symbol ĪŗĖ for each
ĪŗāVĻā
(we often simply write Īŗ for ĪŗĖ in formulae, omitting the overset dot).
The same sort of Individuals as MSODā (see §2.1).
The sort of Functions, with infinitely many variables F,G,H,etc.
The sort of HF-Functions, with no variable.
For each pair (n,m)āNĆN, we assume given
a constant symbol gĖān,mā of arity n.
The interpretation of these constant symbols is discussed in §3.4.4.
The language of FSODā has two kinds of terms.
The Individual terms are the same as those of MSODā.
In addition, FSODā also has HF-terms, which are given by
[TABLE]
The formulae of FSODā are built as follows:
[TABLE]
An FSODā-formula Ļ is HF-closed
if it contains no free HF-variable.
{nota}
- (1)
Usual derived formulae are defined similarly as with MSO
(where ā is either āĖā or āĖā):
[TABLE]
2. (2)
In addition to bounded quantification (āF:K),
we use the notation (F:K) within formulae
as the defined formula:
[TABLE]
3. (3)
For
variables
K=K1ā,ā¦,Knā
and
L=L1ā,ā¦,Lnā,
and
ā either ā, āĖā or āĖā,
we let
[TABLE]
Remark 4**.**
The (hereditarily) finite set D of tree directions is considered
both as a parameter in the definition of FSODā,
via the successor term constructors Sdā (for dāD)
and the corresponding axioms (see §3.4),
and as a (constant) HF set, which can occur as such in FSODā formulae.
Strictly speaking, we should write DĖ rather than D in the latter case, but we usually simply omit the overset dot, as with other HF-sets.
3.3. The Deduction System of FSODā
Deduction for FSODā is defined by the system presented
on FigureĀ 1
(with FSODā formulae instead of MSODā formulae)
and FigureĀ 4,
together with all the axioms of §3.4.
The language and axioms of FSODā are summarized in FigureĀ 5.
\opt
draftnotes
3.4. Basic Axiomatization
We now present the axioms of FSODā.
The first group
(Equality, Tree Axioms and Induction, §3.4.1-§3.4.2)
corresponds to its counterpart in MSODā.
We then present our specific axioms for HF-Sets in §3.4.4
and our Functional Choice Axioms in §3.4.5.
3.4.1. Equality
The theory FSODā has
usual equality axioms for individuals and HF-Sets.
Equality on Individuals.
[TABLE]
Equality on HF-Sets
(for all formula Ļ, all HF-terms K,L and all HF-variable m):
[TABLE]
Remark 5**.**
Note that FSODā is equipped with an explicit Substitution Rule
[TABLE]
Substitution entails the following
(where Ļ(F(t)) is an FSO-formula):
[TABLE]
as well as
the derived rule
[TABLE]
The former is a direct consequence of the Substitution rule
together with elimination of equality on HF-Sets.
For the latter, first note that
RemarkĀ 1 also holds for FSODā.
In particular, one can derive
[TABLE]
On the other hand, we have
[TABLE]
We therefore get
[TABLE]
and the Substitution rule gives
[TABLE]
3.4.2. Induction
We have the following Induction Scheme:
[TABLE]
3.4.3. Tree Axioms
For the tree structure of Dā,
we have the same Tree Axioms as MSODā, displayed in FigureĀ 3
(recall that FSODā has the same Individuals as MSODā).
We now state expected results on the axioms so far introduced.
To this end, let FSOD0ā 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**.**
FSOD0ā* proves the following.*
- (1)
(āx)(āy)(xā¤Ėāyā¤Ėāx\leavevmodeĀ \leavevmodeĀ ā¹\leavevmodeĀ \leavevmodeĀ xāy)**
2. (2)
(āx)(xā¤ĖāεĖ\leavevmodeĀ \leavevmodeĀ ā¹\leavevmodeĀ \leavevmodeĀ xāεĖ)**
3. (3)
¬(āx)(x<ĖāεĖ)**
4. (4)
¬(āx)(Sdā(x)āεĖ)**
5. (5)
(āx)(xāεĖ\leavevmodeĀ \leavevmodeĀ āØ\leavevmodeĀ \leavevmodeĀ (āy)āØdāDāxāSdā(y))**
6. (6)
(āx)(āy)(x<Ėāy\leavevmodeĀ \leavevmodeĀ ā¹\leavevmodeĀ \leavevmodeĀ āØdāDāSdā(x)ā¤Ėāy)**
A consequence of PropositionĀ 6
is that the Induction Scheme of FSODā (§3.4.2)
implies the usual scheme of Well-Founded Induction w.r.t.
the strict prefix order <Ėā.
Theorem 7** (Well-Founded Induction).**
FSOD0ā*
proves the following form of well-founded induction:*
[TABLE]
Remark 8**.**
Both PropositionĀ 6
and TheoremĀ 7 also hold for MSODā.
3.4.4. HF-Sets
We now present our axioms on HF-Sets.
Their
purpose is to ease formalization in FSODā.
Recall that HF-sets range over VĻā
(DefinitionĀ 3.1).
The idea of these axioms
is to incorporate in FSODā as much of the theory of VĻā as possible,
while keeping FSODā interpretable in MSODā
and with a semi-recursive notion of provability.
The interpretation of FSODā in MSODā
relies on the fact that in FSODā-formulae,
all quantifications over HF-Sets are bounded (either by āĖā or āĖā),
so that in a closed FSODā-formula, quantifications
over HF-Sets can be interpreted using usual propositional logic.
We will have, as particular cases of our axioms on HF-Sets,
all bounded formulae over HF-Sets which are true in VĻā.
Moreover, w.r.t. the interpretation of FSODā in MSODā (§3.6)
and in particular w.r.t. its application to MSODā over Ļ-words
(§7, §8 and §9),
it is important to have sufficiently many functions over VĻā
available within closed HF-terms.
This is the main purpose of our axioms on HF-Sets.
They state that the HF-Functions gĖān,mā
are Skolem functions for
āā!-statements over HF-Sets.
These axioms are further commented in §8.5.
{defi}
[HF-Formula]
An HF-formula is an FSODā-formula with atoms
of the form KāL, KāĖāL or KāĖāL
where K and L are HF-terms.
Fix a distinguished HF-variable ā,
and an enumeration k1ā,k2ā,⦠of distinct HF-variables all different from ā.
Furthermore, fix an enumeration (Ļn,mā)n,māNā
of HF-formulae satisfying the following conditions:
- (1)
Each formula Ļn,mā has free variables among k1ā,ā¦,knā,ā.
2. (2)
All HF-Functions occurring in Ļn,mā
have the form gĖānā²,mā²ā with mā²<m.
3. (3)
Each HF-formula Ļ satisfying (1) and (2) occurs infinitely often in
(Ļn,mā)n,māNā, in the following sense.
If Ļ has free variables among k1ā,ā¦,knā,ā,
then there are infinitely many māN such that Ļ
is Ļn,mā.
Recall from RemarkĀ 2 that VĻā
is a model of ZFCā.
The idea of our Axioms on HF-Sets is that
[TABLE]
(where (kāĖākā²) is interpreted as (āmāĖāk)(māĖākā²)).
However, recall that Ļn,mā inĀ (1)
may contain HF-Functions gĖānā²,mā²ā with mā²<m.
The premise ofĀ (1) can thus not be formulated in ZFCā,
but requires a suitable extension of it.
We let Sk(ZFCā) consist of ZFCā augmented with the axioms
[TABLE]
\opt
draftnotes
It is well-known that Sk(ZFCā) is thus a conservative extension of ZFCā
(see e.g. [vD04, §3.4]).
FSODā has the following axiom scheme for HF-Sets,
which simply consists ofĀ (1) formulated for Sk(ZFCā)
rather than ZFCā:
Axioms on HF-Sets.
For each n,māN
such that
[TABLE]
and for all HF-terms K=K1ā,ā¦,Knā, we have the axiom
[TABLE]
Remark 9**.**
Note that this axiom scheme makes the axiom set of FSODā not recursive.
But as expected for a proof system,
provability in FSODā remains semi-recursive.
We fix here once and for all an interpretation
of the HF-Function symbols gĖān,mā
as functions over VĻā.
The idea is
that ifĀ (2) holds,
then gĖān,mā is interpreted
as a computable function gn,mā:VĻnāāVĻā
such that
[TABLE]
But again recall that Ļn,mā
may contain HF-Functions gĖānā²,mā²ā with mā²<m.
We therefore proceed inductively, as follows.
{conv}
By induction on māN,
we interpret the
HF-Function symbols gĖān,mā
as computable functions
[TABLE]
Consider the formula Ļn,mā, and assume that all HF-Functions
gĖānā²,mā²ā with mā²<m are already interpreted.
IfĀ (2) holds
then by the Countable Axiom of Choice
we interpret gĖān,mā as the unique function
gn,mā:VĻnāāVĻā such thatĀ (3)
holds.
Note that such functions are computable.
Otherwise, we interpret gĖān,mā as the function with constant value
ā
.
Remark 10**.**
Note each 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)āN2 to
the interpretation of 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 HF-Sets.
We now discuss some consequences of these axioms.
First note that if Ļ is a closed HF-formula,
then it is provable in Sk(ZFCā) if and only if it holds in VĻā.
We state this fact as a Remark for the record, and also to reiterate how much deductive power underlies the axioms on HF-sets.
Remark 11**.**
Given a closed HF-formula Ļ,
[TABLE]
\opt
draftnotes
Moreover, we have all instances of the following:
- (1)
Extensionality.
[TABLE]
2. (2)
Finite sets.
For each nāN we have an n-ary HF-Function symbol
{ā,ā¦,ā} such that
[TABLE]
We have in particular singletons {ā} and unordered pairs
{ā,ā}.
Using Extensionality, FSODā proves that
[TABLE]
We use the following shorthand:
[TABLE]
3. (3)
Union.
We have an HF-Function symbol āŖ(ā) such that
[TABLE]
4. (4)
Powerset.
We have an HF-Function symbol P(ā) such that
[TABLE]
The powerset is the reason for our introduction of inclusion (āĖā)
as an atomic formula:
It is well-known that the powerset cannot be defined by a Ī0ā(āĖā)-formula.
A possible formula defining it is:
[TABLE]
The quantification āā in the right conjunct is not āĖā-bounded,
and cannot be so.
In addition, we also have an HF-Function symbol Pāā(ā)
for the non-empty powerset, that is such that
[TABLE]
5. (5)
Comprehension.
Given an HF-formula Ļ with free variables
among k1ā,ā¦,knā,k, we have an HF-Function
{kāĖā(ā)\leavevmodeĀ ā£\leavevmodeĀ Ļ[ā,ā¦,ā,k]}
such that
[TABLE]
6. (6)
Products.
We have a binary HF-Function (ā)Ć(ā)
such that
[TABLE]
Moreover, we have binary projections given by HF-Functions
Ļ1ā,āā(ā) and Ļ2ā,āā(ā)
such that
[TABLE]
and similarly for Ļ2ā,āā(ā).
Whenever possible, we write Ļiā(ā) instead of Ļik,āā(ā).
Note that by composing binary projections Ļ1ā and Ļ2ā
we obtain projections
[TABLE]
for any k1ā,ā¦,knā and iā{1,ā¦,n}
7. (7)
Function Spaces and Application.
We have an exponent HF-Function (ā)(ā)
such that
[TABLE]
Moreover, function application is given by the HF-Function
@ā,āā(ā,ā) with
[TABLE]
(here f and a are HF-variables).
Whenever possible, we omit the subscripts k,ā of @k,āā(f,a)
and write simply f(a) for @k,āā(f,a).
8. (8)
Disjoint Unions.
We have a binary HF-Function (ā)+(ā) with
[TABLE]
(see ConventionĀ 5.5
for a further discussion on finite ordinals in our context).
We moreover have HF-Functions
inkk,āā(ā), ināk,āā(ā), and [ā,ā]k,āī±ā
such that (dropping subscripts and superscripts)
[TABLE]
for māĖāk, āāĖān and fāĖāī±k, gāĖāī±ā.
\opt
draftnotes
{conv}
Regarding function spaces as inĀ 7 above,
FSODā proves
[TABLE]
In the following, we reason modulo that bijection, and simply
identify (kā)m with kāĆm.
Remark 12**.**
An HF-relation āŖÆāKĆK is a partial order
on an HF-term K, if the formula PO(āŖÆ,K) holds in VĻā, where
PO(āŖÆ,K) is the HF-formula:
[TABLE]
A partial order āŖÆāKĆK is a well-order
if every subset of K has a āŖÆ-least element,
that is, if the following formula WO(āŖÆ,K) holds
in VĻā:
[TABLE]
Since every HF-set is finite and can be well-ordered, we have
[TABLE]
Since Ļ(k) is an HF-formula Ļ(k),
it follows that FSODā proves Ļ(k),
hence in particular that every HF-set is well-ordered.
ā
3.4.5. Functional Choice Axioms
We have the following functional choice axiom schemes.
HF-Bounded Choice for HF-Sets.
[TABLE]
HF-Bounded Choice for Functions.
[TABLE]
Iterated HF-Bounded Choice.
[TABLE]
where the substitution [G(k)\sslashF] is defined as
the usual substitution operation
but with
[TABLE]
We insist
that none of these axioms create choice functions
for the individuals of FSODā
(cf RemarkĀ 3).
Despite their common shape, these three axiom schemes are actually
of different nature.
First, the axiom of
HF-Bounded Choice for Functions
[TABLE]
is a counterpart in FSODā of the Comprehension Scheme of MSODā.
Recalling the informal discussion in §3.1
and anticipating §3.5 and §3.6,
let us assume a translation āØāā© from (HF-closed)
FSODā-formulae to MSODā-formulae, and
let us assume that K is a closed HF-term
representing the HF-set {Īŗ1ā,ā¦,Īŗnā}.
Then the premise ofĀ (4)
can be read as
[TABLE]
The conclusion easily follows from the fact that
using Comprehension, one can
define in MSODā a partition X1ā,ā¦,Xnā of Dā
such that
[TABLE]
Second, HF-Bounded Choice for HF-Sets
[TABLE]
may look similar to the Axioms on HF-Sets of §3.4.4.
The differences are that the formula Ļ here
is an arbitrary formula of FSODā,
not necessarily an HF-formula in the sense of DefinitionĀ 3.4.4,
and moreover that this axiom only involves FSODā (i.e. bounded)
quantifications, contrary toĀ (2).
Note that for HF-formulae Ļ,
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 HF-Sets in FSODā are
ultimately interpreted in propositional logic.
Assume that the HF-terms K and L are closed, and correspond
to the HF-sets Īŗ and Ī» respectively.
Then the premise ofĀ (5)
can be read as
[TABLE]
which is equivalent in propositional logic to the interpretation of the conclusion
[TABLE]
Similarly, Iterated HF-Bounded Choice
reduces to an equivalence of the form
[TABLE]
and follows from Comprehension.
The definition of FSODā is now complete.
{nota}
Similarly as with MSODā, we shall write FSO for FSODā
when the set of tree directions D is clear from the context.
3.5. The Standard Model of FSO
The standard model T
of FSODā is the full D-ary tree Dā
equipped with suitable domains for each sort:
HF-Sets range over VĻā, and each constant
ĪŗĖ is interpreted by the corresponding HF-set ĪŗāVĻā.
Individuals range over Dā,
the constant εĖ
is interpreted by the empty sequence εāDā
and Sdā as the map
taking pāDā to p.dāDā.
Moreover, we write < for the strict prefix order on Dā.
Functions
range over
[TABLE]
For each n,māN, the HF-Function gĖān,mā
(of arity n) is interpreted as the function
[TABLE]
fixed in ConventionĀ 3.4.4.
Remark 13**.**
*Note that T has the same individuals as the standard model of MSODā.
Moreover we write T for both the standard model
of FSODā and that of MSODā, as an abuse of notation.
*
We have the usual
interpretation [[t]]āDā for each closed
individual term t with parameters in T,
and
an interpretation [[K]]āVĻā for each closed HF-term K
with parameters inĀ T.
The relation TāØĻ,
for a closed FSO-formula Ļ with parameters in T,
is defined by induction on Ļ as follows:
[TABLE]
By a routine induction argument, we can show the soundness of FSODā w.r.t. T:
Proposition 14**.**
Given FSO-formulae Ļ1ā,ā¦,Ļnā,Ļ
with free HF-variables among k,
free Individual variables among x,
and free Function variables among F,
if
[TABLE]
then
for all HF-Sets Īŗ,
all pāDā
and all
FāāĪŗāVĻāā(DāāĪŗ),
we have
[TABLE]
Remark 15**.**
It follows from RemarkĀ 10 that the map
[[ā]] is not computable on HF-terms.
We refer to §8.5 for a discussion and a workaround.
3.6. Mutual Interpretability of FSO and MSO
While FSO seems more expressive than MSO (and, indeed, is easier to work with),
the two theories can mutually interpret each other
via two formula-level translations:
[TABLE]
As we shall see, both translations preserve and
reflect provability:
[TABLE]
The interpretation (ā)ā
of MSO in FSO
simply amounts to simulate the (Monadic) Predicate variables of MSO
by FSO-Function variables Dāā2.
We therefore see (ā)ā as an embedding, and see FSO
as a conservative extension of MSO which is faithfully interpretable in 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 āØāā© and (ā)ā
separately in §3.6.1
and §3.6.2 below.
Full proofs are detailed inĀ [DR20, App. A].
3.6.1. From FSO to MSO
The translation
āØāā©:FSOāMSO
interprets the HF-part of 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:
{conv}
We assume that each HF-set Īŗ comes with a fixed enumeration
Īŗ=Īŗ1ā,ā¦,Īŗnā of its elements.
The translation āØāā© will map an HF-closed FSO-formula Ļ
without free Function variables
to an MSO-formula āØĻā©.
As stated earlier, quantifications over HF-Sets will be interpreted using
propositional logic.
For instance we have,
[TABLE]
where [[K]]āVĻā is the standard interpretation
of the closed HF-term K defined in §3.5.
As a consequence, the translation āØāā© is non-uniform
w.r.t. HF-Sets.
In particular, for an FSO-formula Ļ
with free HF-variables among k=k1ā,ā¦,kpā,
each tuple of HF-sets Īŗ=Īŗ1ā,ā¦,Īŗpā
will induce a specific MSO-formula
āØĻ[Īŗ/k]ā©.
The interpretation of Function variables is more complex.
Consider a closed HF-term K
and assume [[K]]={Īŗ1ā,ā¦,Īŗcā}.
Then a Function (F:K) can be seen as a function
[TABLE]
As indicated in §3.1,
we interpret F as a tuple X1ā,ā¦,Xcā of Monadic variables
such that
[TABLE]
In other words,
F:Dāā{Īŗ1ā,ā¦,Īŗcā}
is seen as a partition X1ā,ā¦,Xcā of Dā.
To handle the interpretation of Functions in the inductive definition
of āØāā©,
it is actually convenient to temporarily work
in an extension of FSO with the following atomic formulae:
\arrowvertX1āā¦Xnā(t)āĪŗāL\arrowvert
where Īŗ=Īŗ1ā,ā¦,Īŗnā
enumerates an HF-set
and X1ā,ā¦,Xnā are monadic variables of MSO.
Extended FSO-formulae are built just like
FSO-formulae, but possibly using the atomic formulae above.
Extended atomic formulae are useful for dealing with
HF-bounded quantifications over Functions, say
(āF:K)Ļ.
The point is that
F occurs
in subformulae of Ļ of the form F(t)āL,
where the HF-term L may contain free HF-variables.
Hence the value of L is not known when the translation
of (āF:K) has to be computed.
Extended atomic formulae allow us to delay the interpretation of F(t)āL
until [[L]] is known.
The interpretation of an extended
HF-closed FSO-formula Ļ
without free Function variables
is the MSO-formula
āØĻā© defined by induction on Ļ as follows:
[TABLE]
where in the last clause,
[[K]] is enumerated by Īŗ=Īŗ1ā,ā¦,Īŗcā,
and Ī„cā(X1ā,ā¦,Xcā)
is the following MSO-formula,
expressing that X1ā,ā¦,Xcā form a partition of Dā:
[TABLE]
Note that in the definition of āØĻā© above,
since Ļ is assumed to be HF-closed,
the displayed HF-terms K and L are closed,
so that
their T-interpretation [[K]],[[L]]āVĻā is defined
(see §3.5).
Remark 16**.**
Since it involves the standard interpretation map [[ā]]
on HF-terms,
it follows from Remark 15 (§3.5)
that the interpretation āØāā© is not recursive.
We refer to §5.6.1
and §8.5
for discussions and workarounds.
Theorem 17**.**
For every closed FSO-formula Ļ, we have
[TABLE]
The proof of TheoremĀ 17 is deferred
toĀ [DR20, App. A].
The logical rules of FSO are handled routinely.
The interpretations of most of the axioms of FSO
are almost trivially provable from the corresponding axioms of MSO.
The Functional Choice Axioms are dealt-with essentially as explained
in §3.4.5.
3.6.2. From MSO to FSO
The translation
(ā)ā:MSOāFSO
is much simpler than āØāā©.
Assume given
a FSO-Function variable FXā
for each monadic MSO-variable X.
The map (ā)ā is inductively defined as follows:
[TABLE]
It is easy to see that (ā)ā is truth preserving (and reflecting) w.r.t. the standard model T,
by a direct induction on formulae
relying on the bijection P(Dā)ā
2Dā.
Lemma 18**.**
Given a closed MSO-formula Ļ, we have
[TABLE]
The main result on (ā)ā is the following.
Its proof is deferred toĀ [DR20, App. A].
Theorem 19**.**
Given a closed MSO-formula Ļ,
[TABLE]
TheoremĀ 19 can actually be extended to FSO formulae.
This is essentially the content of the following result.
Proposition 20**.**
For a closed FSO-formula Ļ, we have the following.
[TABLE]
Remark 21**.**
TheoremĀ 19
and PropositionĀ 20 will be used
in our completeness argument (§8) in two different ways:
- (1)
We first obtain completeness of FSO
(augmented with the Axiom (PosDet) of §5.6)
for MSO formulae via a usual translation of formulae to automata.
From this result, completeness of FSO+(PosDet)
follows by PropositionĀ 20,
while completeness of MSO
(augmented with āØāā©-translations of suitable instances of (PosDet))
follows by TheoremĀ 19.
2. (2)
In addition,
we will use Proposition 20 in §7
in order to import the MSO-theory of N for the infinite paths of T.
We rely on this for
the version of the Büchi-Landweber Theorem
(namely that 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 notation that we will use throughout our formalization
of games and automata in FSO.
3.7.1. FSO with Extended HF-Terms
First, recall that the syntax of FSO formally disallows Functions in HF-terms.
We propose here a notation system that allows them in some circumstances.
For instance, assuming (F:K),
we can use the notation
[TABLE]
More generally, consider an atomic formula
[TABLE]
with M and N terms on the following grammar:
[TABLE]
Such formulae can be interpreted in 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 F=F1ā,ā¦,Fnā.
Note that there are (proper) HF-terms Mā² and Nā² such that
[TABLE]
for some HF-variables ā=ā1ā,ā¦,ācā
and where F(t)=Fi1āā(t1ā),ā¦,Ficāā(tcā).
Given proper HF-terms K1ā,ā¦,Knā,
assuming F:K, one can let
[TABLE]
where L=L1ā,ā¦,Lcā is such that Ljā=Kiā
iff the jth element of F(t) is Fiā(tjā).
Note however that the above defined formula MāN
actually depends on the choice of K, so we rather write it as:
[TABLE]
Generalizing further we can, with the above method, interpret in FSO
formulae build with HF-terms in the sense ofĀ (9).
The interpretation in FSO of such a formula Ļ with free Function variables among F=F1ā,ā¦,Fnā
is defined by induction, and depends on a choice of proper
HF-terms K=K1ā,ā¦,Knā.
Using notation as above, we arrive at the following definition:
[TABLE]
Beware that (Ļ)F,Kā only makes sense under the assumptions
F:K.
Keeping this in mind we may obtain, for instance, the following formulations
of the Functional Choice Axioms of §3.4.5.
HF-Bounded Choice for Functions.
[TABLE]
Iterated HF-Bounded Choice.
[TABLE]
3.7.2. Notations for Products and Functions
We now introduce notation 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
[TABLE]
as a function
[TABLE]
Furthermore, it is convenient to allow such F to have a domain
defined by an FSO formula Ļ(ā), and to write
[TABLE]
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 this notation.
In order not to overload the arrow symbol ā¶
(which will be used with games later on),
we will write typing declarations as
[TABLE]
{nota}
[Product Types]Product types are given by the following grammar,
where Ļ(ā) is an FSO formula of an individual variable
(with possibly other free variables of any sort),
and where K is an HF-term.
[TABLE]
The arity of a product type Ī is:
(1,n) if Ī is of the form
Ļ(ā)ĆK1āĆāÆĆKnā,
(0,n) if Ī is of the form
K1āĆāÆĆKnā.
Product types are to be used with the following defined formulae.
[TABLE]
Here f stands for a Function variable F if the arity of Ī
is of the form (1,n),
and for an HF-variable f if the arity of Ī is of the form (0,n).
Moreover,
for Ī =Ļ(ā)ĆK1āĆāÆĆKnā,
we let
[TABLE]
{rems}
- (1)
Thanks to Rem.Ā 12,
using the Axioms of HF-Bounded Choice
(§3.4.5),
we have
[TABLE]
2. (2)
Using ConventionĀ 3.4.4,
for each product type Ī we have
[TABLE]
It follows that
for each product type Ī
and each formula Ļ
we have
[TABLE]
{nota}
In the following, given a product type Ī ,
we use the notation t~:Ī ,
where t~ stands for a tuple of the form (t,K1ā,ā¦,Knā)
if Ī has arity (1,n),
or of the form (K1ā,ā¦,Knā) if Ī has arity (0,n).
When Ī is clear from the context, we write t~
instead of t~:Ī , and furthermore
we may omit the overset tilde, writing t instead of t~.
Write x~ for tuples of variables of the form
(x,k1ā,ā¦,knā) or of the form (k1ā,ā¦,knā).
- (1)
If Ī =Ļ(ā)ĆK1āĆāÆĆKnā
and t~=(t,L1ā,ā¦,Lnā),
we write FĪ āK(t~) for the HF-term
[TABLE]
If Ī =K1āĆāÆĆKnā
and t~=(L1ā,ā¦,Lnā),
we write fĪ āK(t~) for the HF-term
[TABLE]
When Ī and K are
clear from the context, in either case above we write
\textscf(t~)
for
\textscfĪ āK(t~).
2. (2)
We furthermore write t~āĖā\textscf or even \textscf(t~)
for the formula
[TABLE]
3. (3)
We extend product types as follows
[TABLE]
where X is a Function variable. We let
[TABLE]
Note that
[TABLE]
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**.**
FSODā* proves the following generalizations of the
Functional Choice Axioms of §3.4.5:*
HF-Bounded Choice*.*
[TABLE]
Iterated HF-Bounded Choice*.*
[TABLE]
Theorem 23** (Comprehension for Product Types).**
FSODā*
proves the following form of Comprehension, where V does not occur free in Ļ:*
[TABLE]
Proof 3.5**.**
We require
[TABLE]
By excluded middle, bounded existentials and generalization we have,
[TABLE]
and we conclude by HF-Bounded Choice.
{rems}
- (1)
In the case of Ī =Dā,
TheoremĀ 23 gives Comprehension for characteristic functions:
[TABLE]
2. (2)
We have the following form of Comprehension
for HF-Sets:
[TABLE]
3. (3)
Using Comprehension for HF-Sets, the well-orders on HF-Sets
given by RemarkĀ 12
give the following Induction Scheme for HF-Sets:
[TABLE]
where āŖÆ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 P (corresponding to Automaton or āloĆÆse)
and Opponent O (corresponding to Pathfinder or ābĆ©rlard).
In the case of acceptance games, P plays for acceptance and O
plays for rejection, and in the particular case of
non-deterministic automata, P chooses transitions
from the non-deterministic transition relation, while O
chooses tree directions dā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āDā,
P can only go to game positions with tree position x,
while 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 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 HF-Sets PGā and OGā of
Proponent and Opponent labels respectively.
Intuitively, Proponent will play from game positions of the form
[TABLE]
while Opponent will play from positions of the form
[TABLE]
A game will be given by specifying edge relations of the form
[TABLE]
So P can only move to a game position with the same
underlying tree position,
while 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 ā“Gā
is the lexicographic product of the usual tree order with
the one setting P-labels smaller than all O-labels.
The games we shall consider will all be subrelations of ā“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 ā“Gā.
4.1. A Partial Order of Game Positions
We first introduce the formal notion of labels of game positions.
{defi}
[Labels of Game Positions]
Labels of game positions are pairs (PGā,OGā)
of HF-terms satisfying the following formula:
[TABLE]
We write POGā for PGāāŖOGā.
When no ambiguity arises, we write P, O and PO
for PGā, OGā and POGā respectively.
Assume (P,O) are labels of game positions.
Intuitively, game positions are pairs (x,k) with xāDā and kāPO,
Proponentās positions are game positions with kāP
and Opponentās positions are game positions with kāO.
To summarize, we have the informal correspondence:
[TABLE]
We will throughout the paper use the following notation
to manipulate game positions and sets of game positions.
{nota}
[Game Positions]
We introduce the following notation,
assuming Labels(PGā,OGā).
- (1)
Variables, written u,v,w,etc, range over game positions,
that is over pairs (x,k) with x an Individual variable and
k an HF-variable ranging over POGā.
2. (2)
Sets of game positions, written U,V,W,etc,
range over Functions DāĆPOGāto2.
We will systematically use the following notation:
[TABLE]
We often write vāV or V(v) for V(v)ā1.
3. (3)
For a set of game positions V,
we write VPā and VOā
for the P and O subsets of V respectively.
This amounts to the following abbreviations:
[TABLE]
Intuitively,
VPā represents Vā©(DāĆPGā)
while
VOā represents Vā©(DāĆOGā).
4. (4)
In formulae we interpret quantifiers over (sets of) game positions as follows:
[TABLE]
where, in the āv case, we choose x,ā not free in Ļ.
We now introduce the partial order ā“ on game positions.
{defi}
[Partial Order on Game Positions]
The relations
ā²(PGā,OGā)ā, ā“(PGā,OGā)ā and s(PGā,OGā)ā²ā,
where PGā and OGā are HF-variables,
are defined as follows:
[TABLE]
When no ambiguity arises, we write
ā²Gā, ā“Gā and sGā²ā,
or even ā², ā“ and sā²
for
ā²(PGā,OGā)ā, ā“(PGā,OGā)ā and s(PGā,OGā)ā²ā
respectively.
Note that the formula sā²(ā,ā) is actually bounded,
since by NotationĀ 4.1.(1),
the variable w ranges over game positions,
so that (āw) stands for
(āwāDāĆPO).
We note a number of useful properties of ā²,
in particular that it is a discrete partial order.
Proposition 24**.**
FSODā* proves following, under the assumption Labels(P,O).*
- (1)
uā²vā²w\leavevmodeĀ \leavevmodeĀ ā¹\leavevmodeĀ \leavevmodeĀ uā²w**
2. (2)
¬(uā²u)**
3. (3)
uā“vā“u\leavevmodeĀ \leavevmodeĀ ā¹\leavevmodeĀ \leavevmodeĀ u=v**
4. (4)
uā²vāŗ(āwā“v)(sā²(u,w))āŗ(āwā²āµu)(sā²(wā²,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.
\opt
draftnotes
We can show that ā²
satisfies well-founded induction from the induction principle on the underlying tree.
Theorem 25** (ā²-Induction).**
FSODā* proves the following, under the assumption Labels(P,O).*
[TABLE]
Proof 4.2**.**
Let V be such that, for any game position v:
[TABLE]
We show that
[TABLE]
by induction on x, whence the theorem will follow.
Suppose that x=εĖ, and so y=εĖ.
We first prove the statement for arbitrary āāĖāP;
in this case notice that there is no u such that uā²(εĖ,ā),
and so we vacuously satisfy the LHS ofĀ (10) above.
Therefore we have that (εĖ,ā)āV.
Otherwise āāĖāO and every uā²(εĖ,ā) is of the form (εĖ,k)
for some kāĖāP, and we have just shown that such u must be contained in V.
Therefore we can conclude that (εĖ,ā)ā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 Sdāx.
If yā¤ĖāSdāx then either yā¤Ėāx or yāSdāx.
In the former case we have by the inductive hypothesis that,
for any āāĖāPO, (y,ā)āV.
So assume that yāSdāx.
Again we distinguish when āāĖāP
and when āāĖāO in order to exhibit the
LHS ofĀ (10) above.
In the former case, notice that any (z,k)ā²(y,ā) is such that zā¤Ėāx,
and so we have that (z,k)āV by the inductive hypothesis;
thus (y,ā)āV byĀ (10).
In the latter case (when āāĖāO) we have for any (z,k)ā²(y,ā)
either zā¤Ėāx or (zāSdāx and kāĖāP).
In both cases we have seen that (z,k)āV,
and so again we have that (y,ā)āV byĀ (10).
*
Since ā² 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ā²v.
Thus, if the value of V at v is given by a formula Ļ(V,v),
we assume that the following
formula holds
[TABLE]
The Recursion Theorem says that, assuming Rec(Ļ),
the set of game positions V given by
[TABLE]
is the unique set of game positions such that
[TABLE]
Proposition 26** (Recursion Theorem).**
FSODā* proves that
Labels(P,O)ā§Rec(Ļ) implies*
[TABLE]
Proof 4.3**.**
Consider a formula Ļ(V,v) and assume Rec(Ļ)
and Labels(P,O).
We begin with the second part of the statement, namely the uniqueness part.
Fix V,U.
By ā²-induction on v, we show that
FSO proves the following formula Ļ(v)=Ļ(V,U,v):
[TABLE]
Let v and assume both premises of Ļ(v),
as well as Ļ(w) for all wā²v.
The premises of Ļ(v) imply those of Ļ(w) for wā²v,
so that we have (VwāUw) for all wā²v.
Hence, given uā“v, if uā²v then we are done.
It thus remains to show (VvāUv).
Thanks to the premises of Ļ(v), this amounts to showing
Ļ(V,v)āĻ(U,v),
which itself follows from Rec(Ļ),
since (VwāUw) for all wā²v.
We now turn to the first part of the statement.
Let V such that
[TABLE]
By ā²-induction on v, we show that FSO proves the following formula
[TABLE]
So let v and assume Īø(w) for all wā²v.
Given uā“v, if uā²v then
Ļ(u) follows from Īø(u).
It thus remains to show Ļ(v).
We consider the two implications separately.
Case of Ļ(V,v)ā¹Vv.*
Assume Ļ(V,v).
By definition of V, we are done if we show*
[TABLE]
Given U such that
\big{(}Uu\leavevmode\nobreak\ \Leftrightarrow\leavevmode\nobreak\ \varphi(U,u)\big{)}
for all uā“v, we obtain Uv from Ļ(U,v),
which itself follows Ļ(V,v) and Rec(Ļ).
The premise of Rec(Ļ) follows from
(āwā²v)Ļ(V,U,w),
whose premises are in turn given by resp.
(āwā²v)Ļ(w) and the assumption on U.
Case of Vvā¹Ļ(V,v).*
Assume Vv.
By comprehension (TheoremĀ 23)
let U such that*
[TABLE]
We obtain Ļ(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āVu) for all uā²v.
Hence Rec(Ļ) gives
Ļ(U,v)āĻ(V,v)
and we get
(UvāĻ(U,v)) from the definition of U.
In the case of uā²v, namely (UuāĻ(U,u)),
we have (āwā“u)(UwāVw)
so that Rec(Ļ) implies
Ļ(U,u)āĻ(V,u)
and the result follows form Ļ(u).
4.3. Infinite Paths
We develop here a notion of infinite paths
(i.e. unbounded linearly order sets) for the partial order ā“
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 ā“ on game positions.
A typical example is the Predecessor LemmaĀ 37.
{defi}
[Game Paths]
Let P,O be 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 Path(P,O,u,U) holds:
[TABLE]
We write Path(u,U) when P and O are clear from the context.
As a preparation to the Predecessor LemmaĀ 37
for Infinite Plays, we prove here the analogous property
for infinite paths.
Lemma 27** (Predecessor Lemma for Game Paths).**
FSODā* proves the following.
Assuming that Labels(P,O) and
that Path(P,O,u0ā,U) hold
for a game position u0ā and a set of game positions U,
we have*
[TABLE]
The proof of LemmaĀ 27
relies on the following usual maximality principle
for non-empty linearly-ordered bounded sets.
Lemma 28**.**
FSODā* proves the following, assuming Labels(P,O).
Given a set of game positions V, if
V
is bounded
(i.e. (āu)(āvāV)(vā²u)),
non-empty
and linearly ordered,
then V has a maximum element:
(āuāV)(āvāV)(vā“u).*
Proof 4.4**.**
By ā²-induction, we prove the following property:
- (1)
For all u,
for all V,
if V is non-empty, linearly ordered by ā²
and such that āvāV(vā“u),
then V has a ā²-maximal element.
Let u and V satisfy the assumptions from 1 above,
and assume 1 for all cā²u.
First, if u=v for some vāV, then u is indeed the maximal element
of V.
So we can assume vā²u for all vāV.
By Comprehension for Product Types (Thm.Ā 23),
let U be the set of all
w such that sā²(w,u)
and such that vā“w for some vāV.
For each vāV,
it follows from PropositionĀ 24.(4)
that there is some wāU such that vā“w.
In particular, U is non-empty since V is non-empty.
We claim the following:
Claim 29**.**
[TABLE]
Proof 4.5** (Proof of Claim 29).**
Let wāU.
By Comprehension for Product Types (Thm.Ā 23),
let W be the set of all vāV such that vā“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ā²u.
By induction hypothesis, W has a maximal element, say w~.
We indeed have w~āV
and vā“w~
for all vāV with vā“w.
Since w~ā“w, uniqueness follows from the antisymmetry of ā“.
The remainder of the argument relies on the particular structure of ā².
Using Comprehension on HF-Sets,
it follows from the definition of ā² that there is some xāDā
and some HF-Set k such that
U is exactly the set of all (x,ā) with āāk.
This observation allows us to show
Claim 30**.**
[TABLE]
Proof 4.6** (Proof of Claim 30).**
Write āŖÆ for the well-order on k given by RemarkĀ 12.
By āŖÆ-Induction
(RemarkĀ 3.7.3.(3))
we show the following:
[TABLE]
Let āāk be such that the property holds for all āā²āŗā.
If ā is āŖÆ-minimal, the result follows from the
existence of a unique w~ such that Ļ((x,ā),w~).
Otherwise, let āā² be the āŖÆ-predecessor of ā,
and let māk such that Ļ(āā²,m) be given by induction hypothesis.
By ClaimĀ 29, let
w~āā,w~mā be the unique elements of V such that
Ļ((x,ā),w~āā) and Ļ((x,m),w~mā).
Since V is linearly ordered, we have either that
w~māā“w~āā or that w~māā“w~āā.
In the former case, we take ā for the new m, and in the latter
we keep the same m.
Since U is non-empty, there is a āŖÆ-maximal āāk.
Let māk such that Ļ(ā,m),
and by ClaimĀ 29,
let w~māāV
such that Ļ((x,m),w~mā).
By definition of k, we do have
w~ā“w~mā
for all w~āV with Ļ(w,w~)
for some wāU.
Hence we have that Ļ(w~mā).
Consider now w~māāV such that Ļ(w~mā).
As noted above, for all vāV there is some wāU such that vā²w.
But we also have vā“w~ where w~ is unique such that
Ļ(w,w~).
It thus follows
that vā“w~mā for all vāV.
This concludes the proof of LemmaĀ 28.
We can now prove LemmaĀ 27.
Proof 4.7** (Proof of LemmaĀ 27).**
Fix vāU with u0āā²v.
By Comprehension for Product Types (Thm.Ā 23),
let W be the set of all wāU such that wā²v.
Since u0āā²v and Path(u0ā,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 u0āā“w and wā²v.
Moreover, by Path(u0ā,U)
there is some w~āU such that sā²(w,w~).
Again by Path(u0ā,U), we have
[TABLE]
But w~ā²v implies w~ā“w, a contradiction,
while vā²w~ implies wā²vā²w~,
contradicting sā²(w,w~).
It thus follows that 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 FSO.
Our games are played on bipartite dags (with partial order ā“Gā)
induced by labels of game positions (PGā,OGā) in the sense of §4.
Continuing §4,
Proponent will play from positions of the form
[TABLE]
while Opponent will play from positions of the form
[TABLE]
A game will be given by specifying edge relations of the form
[TABLE]
so that, for J either P or O,
[TABLE]
(actually even sā²(u,v)).
We insist on the fact that P can only move to a game position with the same
underlying tree position,
while 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 Ļ-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 expressiveness in the language of MSO.
Finally, the Axiom (PosDet) of Positional Determinacy
of Parity Games is formulated in §5.6.
5.1. Games
A game G will be given by labels of game positions
PGā and OGā together with Functions
[TABLE]
where Pāā(ā) is the HF-Function of §3.4.4.4.
Such Functions EPā,EOā induce edge relations
ā¶PGāā and ā¶OGāā
given by
[TABLE]
We make this formal in the following definition.
{defi}
[Games and Edge Relations]
- (1)
A game G
is given by HF-terms PGā,OGā and Functions E(G)Pā,E(G)Oā
which satisfy the following formula
[TABLE]
We often write Game(G) for
Game(PGā,OGā,E(G)Pā,E(G)Oā).
Moreover, when no ambiguity arises, we abbreviate
G=(PGā,OGā,E(G)Pā,E(G)Oā) as
G=(PGā,OGā,EPā,EOā)
or even
G=(PGā,OGā,E)
or
G=(P,O,E).
2. (2)
The edge relations induced by
G=(P,O,EPā,EOā)
are defined as follows:
[TABLE]
When no ambiguity arises, we write
ā¶Pā,
ā¶Oā
and
ā¶,
for
ā¶PGāā,
ā¶OGāā
and
ā¶Gā.
Note that Game(G)
implies that the edge relation ā¶ has no dead ends,
i.e. that from any position, a move can always be made by one of the players.
It follows that
the edge relation ā¶ induces
an unbounded partial order.
(Note that it already follows from the structure of ā¶ that
it induces a partial order.)
Lemma 31**.**
FSODā* proves*
[TABLE]
Games are equipped with a natural notion of subgame.
In this paper we will use subgames to ease some reasoning on automata
(in particular in §9),
and also to more easily define certain strategies that are more naturally seen as concepts at the game level
(see §5.3).
We only need the following weak notion of subgame.
{defi}
[Subgame]
We say that Gā² is a subgame of G whenever the following
formula holds
[TABLE]
Remark 32**.**
Let G=(PGā,OGā,E(G)Pā,E(G)Oā) with Game(G).
Then we have Sub(G,G(ā“)),
where G(ā“)
stands for the game
[TABLE]
in which by HF-Bounded Choice we let
[TABLE]
Note that the edge relation of G(ā“)
is precisely the relation ā“(PGā,OGā)ā
of DefinitionĀ 4.1,
hence the notation.
The edge relation ā¶ of a game G only specifies the moves of G.
In order to manipulate plays (i.e. sequences of moves)
we define the reflexive-transitive closure ā¶ā
and the transitive closure ā¶+ of ā¶.
As expected, these are second-order notions.222It is well known (see e.g.Ā [Lib04, Chap. 4])
that transitive closure in graphs
is not expressible in first-order logic over the edge relation.
{defi}
Let G=(P,O,EPā,EOā)
where P,O are HF-variables and EPā,EOā are Function variables.
We define the following formulae.
[TABLE]
Whenever possible, we write ā¶ā and ā¶+
for ā¶Gāā and ā¶G+ā.
The relations ā¶ā and ā¶+
satisfy properties analogous to those of PropositionĀ 24:
Proposition 33** (Properties of Edge Relations).**
FSODā* proves the following, under the assumption Game(G).*
- (1)
uā¶v\leavevmodeĀ \leavevmodeĀ ā\leavevmodeĀ \leavevmodeĀ sā²(u,v)**
2. (2)
ā¶* is irreflexive and asymmetric.*
3. (3)
ā¶ā*
is reflexive and transitive.*
4. (4)
uā¶āvāu=vāØ(āw)(uā¶āwā¶v)āu=vāØ(āw)(uā¶wā¶āv)**
5. (5)
uā¶āv\leavevmodeĀ \leavevmodeĀ ā\leavevmodeĀ \leavevmodeĀ uā“v**
6. (6)
ā¶ā* is antisymmetric.*
7. (7)
uā¶+v\leavevmodeĀ \leavevmodeĀ ā\leavevmodeĀ \leavevmodeĀ uā²v**
8. (8)
ā¶+* is irreflexive and transitive.*
9. (9)
(ākāP)(uā¶ā(εĖ,k)\leavevmodeĀ \leavevmodeĀ ā\leavevmodeĀ \leavevmodeĀ u=(εĖ,k))**
Induction for games (i.e. w.r.t. edge relations)
is an immediate corollary to TheoremĀ 25
and PropositionĀ 33.
Corollary 34** (Game Induction).**
FSODā* proves the following,
under the assumption Game(G).*
[TABLE]
5.2. Infinite Plays
We now define our notion of infinite play.
They are sets of game positions which are unbounded and
linearly ordered w.r.t. ā¶.
Infinite plays will allow us to define winning in games (§5.4)
and thus acceptance for tree automata (§6).
Furthermore, we prove a number of basic properties on infinite plays
on which we rely for the formalization of usual operations
on tree automata.
In the following, given G=(P,O,E),
we write Path(G,u,U) for Path(P,O,u,U),
where Path is as in DefinitionĀ 4.3.
{defi}
[Infinite Plays]
Let G=(P,O,EPā,EOā)
where P,O are HF-variables and EPā,EOā are Function variables.
Given a position u and a set of game positions U,
we say that U is an infinite play in G from u when the following
formula Play(G,u,U) holds:
[TABLE]
Note that Play(G,u,U) is literally just the formula Path(G,u,U)
in which ā¶Gāā replaces ā“,
ā¶Gā replaces sā²(ā,ā) and
ā¶G+ā replaces ā².
It follows from PropositionĀ 33
that Play(G,u,U) implies Path(G,u,U).
In other words, an infinite play in G=(P,O,E)
is simply an infinite path of the underlying
partial order ā“(P,O)ā
which respects the transitions of G induced by E.
Also, if Gā² is a subgame of G,
then Play(Gā²,u,U) implies Play(G,u,U).
We now gather some basic properties on infinite plays.
The first one will help to show that a set of game positions
is linearly ordered.
Proposition 35**.**
FSODā* proves the following, assuming Game(G).
Let V and u0āāV be such that*
[TABLE]
Then
[TABLE]
Proof 5.1**.**
First,
it follows from PropositionĀ 33.(6)
that u0ā is unique such that
(āvāV)(u0āā¶āv).
By induction on the edge relation ā¶+
(cf.Ā CorollaryĀ 34) we show
[TABLE]
Let uāV, and assume that Īø(v) holds for all vāV
such that vā¶+u.
If u=u0ā then we are done since
u0āā¶āv for all vāV.
Otherwise, by assumption there is vāV
with vā¶u, and moreover such that
u is the unique ā¶-successor of v in U.
Note that vā¶u implies
vā¶+u
(PropositionĀ 33,
(2) & (4)),
so that Īø(v) follows from the induction hypothesis.
Given wāV, if wā¶āv then we get wā¶āu and we are done.
Otherwise, since Īø(v) implies vā¶+w,
we may appeal to the following.
Claim 36**.**
[TABLE]
Proof 5.2** (Proof of Claim 36).**
We reason by induction on ā¶+.
So let wāV with vā¶+w
and such that
[TABLE]
Since u0āā¶āvā¶+w
we have wī =u0ā by
PropositionĀ 33.(6),
so that there is wā²āV with wā²ā¶w.
If vā¶+wā² then the induction hypothesis implies uā¶āwā²,
so that uā¶+w and we are done.
Otherwise Īø(v) implies wā²ā¶āv.
Assume for contradiction that wā²ā¶+v.
We thus have
[TABLE]
PropositionĀ 33.(7)
then gives
wā²ā²vā²w.
But this contradicts
wā²ā¶w
since the latter implies
sā²(wā²,w)
by
PropositionĀ 33.(1).
Hence wā²=v. But then v=wā²ā¶wāV and, since u
is the unique ā¶-successor of v in V,
we have u=w, as required.
This concludes the proof of PropositionĀ 35.
PropositionĀ 35 is a useful tool to prove
that given sets of game positions are infinite plays.
Some constructions on automata
(see §6, §9)
furthermore require us to build plays
in one game from plays in another game.
To this end, we note here the following property,
which we informally see as a partial converse to
PropositionĀ 35.
Lemma 37** (Predecessor Lemma for Infinite Plays).**
FSODā* proves the following.
Assuming Game(G) and Play(G,u0ā,U),
we have*
[TABLE]
Proof 5.3**.**
First, it follows from PropositionĀ 33
that Play(G,u0ā,U) implies Path(G,u0ā,U).
We invoke the Predecessor LemmaĀ 27 for Game Paths.
Assuming u0āā¶+v, PropositionĀ 33
implies u0āā²v,
so there is uāU such that sā²(u,v).
Since U is an infinite play, uāU has an ā¶-successor in U,
i.e. there is some uā²āU such that uā¶uā².
Again since U is an infinite play, we have
[TABLE]
But by PropositionĀ 33 again,
vā¶+uā²
implies uā²vā²uā², contradicting sā²(u,uā²),
while uā²ā¶+v implies uā²uā²ā²v,
contradicting sā²(u,v).
Hence uā²=v and we are done.
Next, we show that games have infinite plays from any position, relying on RemarkĀ 12.
Lemma 38**.**
FSODā* proves that Game(G)
implies*
[TABLE]
Proof 5.4**.**
Let G=(P,O,EPā,EOā).
Fix vāV.
Using RemarkĀ 12,
let āŖÆ be a well-order on PāŖO.
We extend the relation āŖÆ to DāĆ(PāŖO) by setting:
[TABLE]
RemarkĀ 12 implies that
every non-empty W such that
[TABLE]
has a āŖÆ-least element.
By HF-Bounded Choice (TheoremĀ 22), we define
[TABLE]
by setting, for J either P or O,
[TABLE]
Let Gā²:=(P,O,Eā²).
Note that we have Game(Gā²)
and that
[TABLE]
By Comprehension for Product Types (TheoremĀ 23),
we then let
[TABLE]
It remains to show
[TABLE]
First, we have vāU by reflexivity of ā¶Gā²āā
(PropositionĀ 33.(3)),
and (āuāU)(vā¶Gāāu)
follows fromĀ (11).
Moreover, we have
[TABLE]
thanks toĀ (11),
since this property already holds for Gā².
It remains to show that U is linearly ordered w.r.t. ā¶Gāā.
We invoke PropositionĀ 35:
its first premise has already been discussed,
its second follows from the definition of Eā²,
and its last one is
PropositionĀ 33.(4).
Finally, in some situations
(typically for the Simulation Theorem in §9),
it is convenient to build infinite plays from
paths (in the sense of DefinitionĀ 4.3).
Lemma 39** (Infinite Plays From Paths).**
Assume Game(G)
and let u0ā and U
be such that
[TABLE]
Then FSODā proves Play(G,u0ā,U).
Proof 5.5**.**
Thanks to PropositionĀ 33,
the result directly follows from the fact that
[TABLE]
Fix uāU. By ā²-induction we show
(āvāU)(uā“v\leavevmodeĀ \leavevmodeĀ ā\leavevmodeĀ \leavevmodeĀ uā¶āv).
So let vāU such that the property holds for all wā²v,
and assume uā“v.
If u=v then we are done.
Otherwise, by the Predecessor LemmaĀ 27 for Paths,
we have sā²(w,v) for some wāU with uā“w.
By induction hypothesis we get uā¶āwā¶v
and we conclude by PropositionĀ 33.
\opt
draftnotes
5.3. Strategies
We now turn to strategies.
Our strategies are Functions from the positions of one player to the set
of labels of the other player,
which
must respect the edge relations.
This implies that all our strategies are, by definition, positional.
{defi}
[Strategies]
Let G=(P,O,EPā,EOā)
where P,O are HF-variables and where EPā,EOā are Function variables.
- (1)
A P-strategy on G
is a Function Ļ
which satisfies the formula
[TABLE]
2. (2)
An O-strategy on G is a Function
Ļ
which satisfies the formula
[TABLE]
Strategies naturally induce subgames in the sense of DefinitionĀ 31.
This will allow us to lift to strategies notions
which are more naturally defined at the level of games.
{defi}
[Subgame induced by a Strategy]
Given a player J (either P or O)
and a J-strategy Ļ on G,
we let
[TABLE]
where
[TABLE]
and where {Ļ}JāāE(G)Jā
is defined by HF-Bounded Choice to be the Function
taking uāDāĆGJā
to the singleton {Ļ(u)}.
Whenever possible, we write Gā¾{Ļ}
or even just Ļ for Gā¾{Ļ}Jā, when it is unambiguous.
Lemma 40**.**
FSODā* proves the following, where J is a player
(either P or O):*
[TABLE]
This in particular allows us to speak of the infinite plays of a strategy
Ļ on G simply as infinite plays of the game Gā¾{Ļ}.
5.4. Winning
In order to deal with acceptance for automata, we equip games
with a notion of winning.
Given a game G, a winning condition on G
is a formula W(U) where U is intended to range over the infinite
plays of G.
As usual a P-strategy Ļ on (G,W)
is winning from a position v
whenever all the infinite plays U of Ļ from v satisfy W(U).
Dually, an O-strategy is winning from v
when all its infinite plays U from v satisfy ¬W(U).
We formally proceed as follows.
{defi}
Let G=(P,O,EPā,EOā)
where P,O are HF-variables and EPā,EOā are Function variables.
Let W(U) be a given FSO-formula where U is a Function variable.
- (1)
We define the following formulae.
[TABLE]
2. (2)
Given a player J (either P or O),
we say that a J-strategy Ļ is
winning in (G,W) from v
if the game (Gā¾{Ļ}Jā,W) is won by J from v,
i.e. if
the following formula holds
[TABLE]
Strictly speaking, in DefinitionĀ 5.4 above,
WonGameJā
and
WinStratJā
are actually families of FSO formulae, parametrized by the choice of FSO-formula W.
As expected, a game position cannot be winning for both players.
Lemma 41**.**
FSODā* proves the following.*
[TABLE]
Proof 5.7**.**
Assume for contradiction that for some v we have
[TABLE]
that is
[TABLE]
Consider the game
[TABLE]
Note that Gā² is a subgame of both Gā¾{ĻPā}
and Gā¾{ĻOā}.
We thus get
[TABLE]
which implies that there is no U
such that Play(Gā²,v,U),
contradicting LemmaĀ 38.
5.5. Parity Conditions
In this paper, we mostly consider winning conditions expressed as
parity conditions.
Parity conditions are defined from colorings
of game positions by natural numbers from a given finite interval.
We represent natural numbers and the operations and relations on them
using the Functions on HF-Sets of FSO and the axioms
of §3.4.4.
{conv}
In order to conveniently manipulate colorings and parity conditions,
we will use the following functions on finite ordinals
(a.k.a. natural numbers),
obtained from the Axioms on HF-Functions (see §3.4.4).
We rely on the well-known fact that ān is an ordinalā
can be expressed by an HF-formula
Ord(n)
(see e.g.Ā [Jec06, Lemma 12.10]).
- (1)
We consider unary HF-Functions
[TABLE]
such that for all finite ordinals n, we have
[TABLE]
2. (2)
We consider binary HF-Functions
[TABLE]
such that for finite ordinals n,m
[TABLE]
In FSO-formulae, we write
nā¤m for the formula gĖāā¤ā(n,m)ā1, and so on.
3. (3)
We consider a unary HF-Function
[TABLE]
such that for each ordinal n,
evenĖ(n) is the set of ordinals mā[0,n]
such that m represents an even number.
4. (4)
We consider HF-Functions max(ā,ā) and (ā)+1,
computing respectively the maximum
of two finite ordinals and the successor ordinal of an ordinal.
Remark 42**.**
Even if ān is an ordinal*ā can be expressed by an
HF-formula, quantification over all finite ordinals
cannot be expressed in VĻā by an HF-formula,
since for each finite ordinal n>0
we have nāVnāāVnā1ā.
In particular, induction over finite HF-ordinals cannot be expressed
by an HF-formula.*
{defi}
[Parity Conditions]
Let G=(P,O,EPā,EOā)
where P,O are HF-variables and EPā,EOā are Function variables.
- (1)
A coloring is given by a Function C and an HF-term n
satisfying the following formula
[TABLE]
2. (2)
We define the following formula:
[TABLE]
Remark 43**.**
The formula Par(G,C,n,U) will be used to say that an infinite play U
satisfies the (min) parity condition induced by the
coloring C:Gto[0,n].
In the standard model T, if U is an infinite play in G, then
Par(G,C,n,U) holds if and only if there is an even mā¤n
such that
U has infinitely many positions colored by m, and
U has only finitely many positions colored by any k<m.
Also, notice that any U (not necessarily a play) satisfying Par(G,C,n,U) in T is infinite.
Remark 44**.**
Assume that Gā² is a subgame of G
(in the sense of DefinitionĀ 31).
Note that FSO proves
[TABLE]
Furthermore, as noted earlier, every infinite play in Gā²
is an infinite play in G.
It follows that FSO proves
[TABLE]
Remark 45**.**
When considering parity automata in §6,
it will actually be convenient to define acceptance via
the formula Par
for games of the form G(ā“) in the sense of RemarkĀ 32.
It follows from RemarksĀ 32 andĀ 44
that FSO proves
[TABLE]
We use the following more succinct notation for winning in the case parity games.
{nota}
[Winning in Parity Games]
Let G=(P,O,EPā,EOā)
where P,O are HF-variables and EPā,EOā are Function variables.
Let C be a Function variable and n be an HF-variable.
We write the following,
where J is a player (either P or O).
[TABLE]
5.6. The Axiom of Positional Determinacy of Parity Games.
We now formulate the axiom scheme (PosDet),
which states the (positional) determinacy of
parity games.
Intuitively (PosDet) should consist of all formulae
of the form
[TABLE]
But note that these formulae are open, and in particular
[TABLE]
contain free Function variables.
On the other hand, when formulating our completeness results in §8,
it will be interesting to have translations of instances of (PosDet) in MSO,
based on the map āØāā©:FSOāMSO of §3.6.
However, the translation āØāā© only handles HF-closed
formulae without free Function variables.
We therefore officially let (PosDet) consist
of all formulae PosDet(P,O,n),
for P, O and n ranging over HF-terms (see §3.2),
where
PosDet(P,O,n) is the formula
[TABLE]
It follows from the positional determinacy of parity gamesĀ [EJ91]
(see alsoĀ [Tho97, Wal02, PP04])
that all instances of (PosDet) hold in the standard model
T of FSO.
We can thus extend PropositionĀ 14
to the following.
Proposition 46**.**
For each closed FSO-formula Ļ,
[TABLE]
5.6.1. The Axiom of Positional Determinacy in MSO.
In order to obtain a complete axiomatization of MSODā from
the completeness of FSODā+(PosDet) (see §8),
we extend the axioms of MSODā with sufficiently many
translated instantiations āØPosDet(P,O,n)ā©
for P, O and n closed HF-terms.
However, in general these terms may contain arbitrary HF-Functions
symbols, which make the translation
āØPosDet(P,O,n)ā©
in general uncomputable from P, O and n
(see Remark 16 and §3.4.4).
However, for each closed HF-terms P, O
and n, there are constant symbols for HF-sets
PĖ, OĖ and nĖ such that the formulae
āØPosDet(P,O,n)ā©
and
āØPosDet(PĖ,OĖ,nĖ)ā©
are syntactically identical.
We therefore officially take the following version of (PosDet)
in MSODā.
{defi}
[The Axiom of Positional Determinacy in MSO]
We let āØPosDetā© consist of all formulae of the form
āØPosDet(PĖ,OĖ,nĖ)ā©,
for PĖ, OĖ and nĖ
ranging over constant symbols for HF-sets.
6. Alternating Tree Automata
We detail in this Section a representation of alternating tree automata
in FSO.
We closely follow the presentation ofĀ [Wal02].
Our main motivation to consider alternating automata is that when formulating
acceptance with (parity) games (of the kind of §5),
complementation follows from (positional) determinacy
(i.e. in our setting from the Axiom (PosDet)).
Let us recall the main ideas underlying alternating automata.
The original formulation, as in e.g.Ā [MS87, MS95],
is for an automaton A with state set Q
to have transitions with values in the free distributive
lattice over DĆQ
(in other words, transitions have positive Boolean formulae over DĆQ
as values).
Actually, followingĀ [Wal02] we can
simply assume that transitions are of the form
[TABLE]
and we read ā(q,a)
as the disjunctive normal form
[TABLE]
This results in acceptance games
where intuitively P plays from disjunctions while O
plays from conjunctions.
In the following we often call the γāā(q,a)
conjunctions.
We begin by giving basic definitions inĀ 6.1.
Because our setting is restricted to only describe
positional strategies, and because parity
games are positionally determined, we give a special emphasis
to parity automata, whose acceptance conditions
are parity conditions generated from a coloring of their states.
We then present a series of operations on automata,
on which we rely in §8.3 for the interpretation
of MSO formulae as automata.
We recapitulate them in TableĀ 1.
First, §6.2 and §6.3 present
two simple constructions
implementing respectively a substitution and a disjunction
operation.
We discuss in §6.4 and §6.5 the important
special case of non-deterministic automata.
Non-deterministic automata are important because they allow us,
via the usual projection operation (§6.5),
to interpret the existential quantifier of MSO (see §8.3).
To this end, an important result of the theory of automata on infinite trees
is the Simulation TheoremĀ [EJ91, MS95],
which states that each alternating automaton is equivalent to a
non-deterministic one.
The formalization of this result in FSO is deferred to §9.
This is the only part of this paper where we shall (momentarily)
use automata with acceptance conditions which are not parity conditions.
This result moreover relies on the complete axiomatization of
MSO on Ļ-words for paths of FSO
(to be discussed in §7).
Finally, in §6.6 we discuss complementation in the setting of FSO,
and show that alternating automata can be complemented in FSO
when we assume the Axiom (PosDet) of Positional Determinacy of Parity Games.
\opt
draftnotes
6.1. Alternating Tree Automata in FSODā
We present here a representation of alternating tree automata
in FSO.
{defi}
[Alternating Tree Automata]
Given an HF-Set Σ,
an Alternating Tree Automaton
(or simply Automaton) A on Σ
(notation A:Ī£)
is given by HF-terms QAā, qAιā
and āAā
together with
an FSO-formula Ī©Aā(U)
of a Function variable U,
which are required to satisfy the following formula:
[TABLE]
where Pāā(ā) is the HF-Function of §3.4.4.4.
We write
[TABLE]
and adopt the following terminology:
Ī£ is the input alphabet
of A, QAā is its set of states
(with qAιā initial),
āAā is the transition function of A
and Ī©Aā is its acceptance condition.
We often write Aut(A:Ī£) or even Aut(A) for
Aut(Ī£,QAā,qAιā,āAā).
An automaton A:Σ is intended to run over Σ-labeled
D-ary trees, represented as Functions F:Ī£
(equivalently F:DātoĪ£, following §3.7).
As usual, acceptance is modeled using games,
which we formalize in the setting of §5.
{defi}
[Acceptance Games]
Given an automaton A:Ī£ and a Function F:Ī£
we define the acceptance game G(A,F) as follows:
[TABLE]
and E(G(A,F))Pā, E(G(A,F))Oā
are defined by
HF-Bounded Choice for Product Types (TheoremĀ 22)
and Comprehension for HF-Sets (RemarkĀ 3.7.3) as
[TABLE]
Remark 47**.**
Note that Aut(A) implies Game(G(A,F)) for
F:Ī£.
The edge relations of G(A,F)
(in the sense of DefinitionĀ 5.1)
are given by
[TABLE]
Note also that an O-position (x,(q,γ))
is equipped with the information
(x,q)āG(A,F)Pā.
It follows that
an O-position has at most one predecessor.
This is useful when complementing automata (§6.6).
{conv}
It the rest of this paper, unless explicitly stated otherwise,
when speaking of an infinite play in an acceptance game G(A,F)
(including infinite plays in strategies in such games),
we always mean an infinite play from position (εĖ,qAιā).
Given A:Ī£ and F:Ī£,
the acceptance condition Ī©Aā(ā) of A
induces a winning condition in the sense of §5.4
in the game G(A,F).
This gives the following notions of tree
acceptance and language generated by an automaton.
{defi}
[Language of an Automaton]
Given an automaton A:Ī£, a winning condition Ī©Aā
(in the sense of DefinitionĀ 5.4) and F:Ī£,
we say that A accepts F
when the following formula FāL(A)
holds.
[TABLE]
Recall that the formulae Strat and WinStrat are defined
in Def. 5.3 (§5.3)
and Def. 5.4 (§5.4) respectively.
In words, the formula FāL(A)
of DefinitionĀ 47
states that
P has a winning strategy from position
(εĖ,qAιā) in the game G(A,F).
Except for the Simulation Theorem in §9,
we shall only consider automata whose acceptance conditions
are given by parity conditions
in the sense of §5.5.
Recall from DefinitionĀ 42
that a parity condition on a game G is given by the formula
[TABLE]
which depends on G.
However, it is desirable that automata come, as in DefinitionĀ 6.1,
with acceptance conditions which are independent from any particular
acceptance game.
Note that for a given automaton A, all acceptance games G(A,F)
have the same sets of P and O labels and positions;
the input trees F can only induce different edge relations.
Recall now the games G(ā“) from RemarkĀ 32.
The game G(ā“) has the same labels and positions as G,
but its edge relation is exactly the partial order ā“ discussed
in §4.
It follows that for a fixed automaton A:Ī£,
all acceptance games G(A,F) for F:Ī£
induce the same G(A,F)(ā“), that we shall write
[TABLE]
{defi}
[Parity Automata]
Let
[TABLE]
We say that A is a parity automaton if
A comes equipped with HF-terms nAā and CAā
such that the two following conditions are satisfied.
- (1)
The following formula holds
[TABLE]
2. (2)
The formula Ī©Aā(U)
is Par(G(A)(ā“),C^Aā,nAā),
where
[TABLE]
We write
[TABLE]
for a parity automaton A with CAā and nAā as above.
Furthermore, we write
Par(A,C^Aā,nAā,U)
or even
Par(A,U)
for the formula
Par(G(A)(ā“),C^Aā,nAā,U).
In DefinitionĀ 47,
the purpose of the coloring C^Aā
is to equip the game G(A)(ā“) with a coloring in the sense of
Def. 42 (§5.5), namely a coloring of the
positions of the game, while the coloring CAā
only colors the states of A.
Note that it follows
from RemarksĀ 32 andĀ 45
that FSO proves
[TABLE]
where the formula Sub(G,Gā²) (stating that G is a subgame of Gā²)
is defined in Def. 31 (§5.1),
and
[TABLE]
The following simple fact will be useful when proving the Simulation Theorem
in §9.
Remark 48**.**
Given two plays U and V in G(A)(ā“), if UPā=VPā
then
[TABLE]
Other than the Simulation Theorem
in §9,
all constructions we need on automata can be performed on automata
A:Ī£
where Ī£, QAā, qAιā, āAā, CAā
and nAā are given by
arbitrary
HF-terms.
However, our completeness result (§8)
ultimately relies, via PropositionĀ 78,
on the completeness of FSO[<Ėā]Ļ over Ļ-words (§7)
and requires automata to be given by closed HF-terms.
In addition, our proof of the
Simulation Theorem uses McNaughtonās TheoremĀ [McN66],
and imports it into FSO by PropositionĀ 78,
which also requires automata to be closed objects.
This leads to the following.
{defi}
A parity automaton A:Ī£ is HF-closed
if Ī£, QAā, qAιā, āAā,
CAā and nAā are closed HF-terms.
Remark 49**.**
For each of our constructions on automata (see TableĀ 1),
the alphabets, states and colorings of new automata
will be obtained by composing simple Functions on HF-Sets
from §3.4.4
and ConventionĀ 5.5.
In particular this means that the obtained automata
have HF-closed alphabets, states and coloring
provided we started from HF-closed ones.
On the other hand, transition functions may be more complex
(see §6.6 or §9),
and we often present them in a way suggesting
the use of the Axiom of HF-Bounded Choice for HF-Sets
(§3.4.5).
This is unproblematic when HF-closedness is not at issue.
To preserve HF-closedness,
starting from HF-closed automata, the transition functions
of the newly built automata must always be read as being
constructed from concrete HF-sets.
{conv}
In the rest of this paper, whenever we speak
of a (parity) automaton A in formal statements, we always mean
that the formula Aut(A) (resp. PAut(A)) holds.
(By contrast, HF-closedness is an external notion.)
6.2. Substitution
Let A:Ī£ be an automaton and let Ī and
f:ĪtoĪ£ be HF-sets.
The automaton A[f]:Ī is defined to have
the same states and acceptance condition as A:Ī£,
and its transitions are given
by
[TABLE]
Note that Aut(A)ā§(ābāĖāĪ) implies Aut(A[f]).
Also, A[f] is a parity automaton
whenever A is.
Furthermore, it follows from RemarkĀ 49 that
A[f]:Ī is HF-closed when A:Ī
is HF-closed
and in addition Ī and f are closed HF-terms.
A typical use of substitution,
on which we rely when translating formulae to automata in §8.3,
is to enlarge the input alphabet of an automaton.
For instance, given HF-closed Ī£1ā,ā¦,Ī£nā
and an HF-closed A:Ī£iā,
we obtain an HF-closed
[TABLE]
where
[TABLE]
is a projection HF-Function of §3.4.4.6.
Lemma 50**.**
Given Ī, f and A as above,
FSODā proves the following.
[TABLE]
Note that by HF-Bounded Choice, FSODā proves that
[TABLE]
so the above Lemma could have equivalently been stated with an existentially bound F.
6.3. Disjunction
We use here the HF-Functions from §3.4.4.8
and ConventionĀ 5.5.4.
Given parity automata A0ā,A1ā:Ī£,
the parity automaton A0āāA1ā:Ī£
has state set
[TABLE]
with qι initial,
transitions given
by
[TABLE]
and coloring C:QA0āāA1āāto[0,n]
(where n=max(nA0āā,nA1āā))
given by
[TABLE]
We have
[TABLE]
Moreover, if follows from RemarkĀ 49 that
A0āāA1ā:Ī£ is
HF-closed
whenever A0ā:Ī£ and A1ā:Ī£ are.
Remark 51**.**
Even in our positional setting,
strictly speaking the automaton A0āāA1ā does not
require A0ā and A1ā to be parity automata
(see TableĀ 1).
However, the acceptance condition of A0āāA1ā
is actually simpler to define when both A0ā and A1ā
are parity automata.
Since we shall only need A0āāA1ā
for parity automata,
we only formally define disjunction
in this setting.
Lemma 52**.**
FSODā* proves the following.*
[TABLE]
Proof 6.2**.**
Assume first that FāL(A0āāA1ā)
for F:Ī£,
and consider a winning P-strategy
Ļ in the acceptance game G(A0āāA1ā,F).
We first look at the move of Ļ on the initial
position (εĖ,qι).
By definition of A0āāA1ā we have
[TABLE]
Assume γāāAiāā(qAiāιā,F(εĖ)).
Then Ļ induces a P-strategy Ļiā in
G(Aiā,F).
The strategy Ļiā is defined using
HF-Bounded Choice for Product Types (TheoremĀ 22)
by putting
[TABLE]
It remains to show that Ļiā is winning, that is
[TABLE]
for ι=(εĖ,qAiāιā).
Consider an infinite play V of Ļiā from ι.
Then by Comprehension for Product Types (TheoremĀ 23),
define U:G(A0āāA1ā,F)to2
as the set of all (x,ā) such that either
(x,ā)=(εĖ,qι) or (x,ā)āV.
It is clear that
[TABLE]
The converse is proved similarly.
6.4. Non-Deterministic Automata
We turn to the important class of alternating automata known as
non-deterministic automata.
Non-deterministic automata are important because they allow us,
via the usual projection operation (§6.5),
to interpret the existential quantifier of MSO (see §8).
An important result in the theory of automata on infinite
trees is the Simulation TheoremĀ [EJ91, MS95]
(addressed in §9),
stating that each alternating automata can be simulated by a non-deterministic one.
Intuitively, an automaton A is non-deterministic
if in acceptance games O can only explicitly choose tree directions
but not states.
{defi}
[Non-Deterministic Automata]
An automaton (A:Ī£) in the sense of DefinitionĀ 6.1,
with
[TABLE]
is non-deterministic if for every qāQAā,
every aāĪ£, every γāāAā(q,a), and every tree direction dāD, there is at most one
qā²āQAā such that (d,qā²)āγ.
The key property of non-deterministic automata
is that in each play of a P-strategy Ļ in an acceptance game,
the sequence of states is uniquely determined from the tree positions.
We formally state this as follows.
Lemma 53**.**
Consider a non-deterministic automaton A:Ī£,
and let F:Ī£.
Furthermore let Ļ be a P-strategy in G(A,F).
Then FSODā proves that
for all xāDā
and all infinite plays V and Vā² of Ļ, if
[TABLE]
then
for all yā¤Ėāx, all qāQAā,
and all γāPāā(DĆQAā),
we have
[TABLE]
Proof 6.3**.**
Fix Ļ and V,Vā² as in the statement of the Lemma
and let xāDā.
First, note that for every yā¤Ėāx
we have
Claim 54**.**
[TABLE]
Proof 6.4** (Proof of Claim 54).**
We use the Induction Axiom of FSO (§3.4.2).
The property holds for εĖā¤Ėāx since
(εĖ,qAιā) belongs to both V and Vā².
Assume now the property for yā¤Ėāx, and consider some tree direction dāD
such that Sdā(y)ā¤Ėāx.
By assumption, we have some qāQAā such that (y,q)āV,
and by using Game(Ļ) twice,
we get some qā²āQAā and some dā²āD
such that
[TABLE]
But since V is a play of Ļ,
by PropositionĀ 33
we must have Sdā²ā(y)ā“x, so that dā²=d
and we are done.
The same reasoning gives the result for Vā².
Using the Induction Axiom of FSO (§3.4.2), we now show that
[TABLE]
First,
we have
[TABLE]
Assume now the property for yā¤Ėāx and let us prove it for
Sdā(y) with Sdā(y)ā¤Ėāx.
It follows from the induction hypothesis and
ClaimĀ 54
that
we have (y,q)āV and (y,q)āVā²
for some qāQAā.
Again by ClaimĀ 54,
let qā²,qā²ā²āQAā such that
(Sdā(y),qā²)āV and (Sdā(y),qā²ā²)āVā².
Now since V and Vā² are plays of Ļ,
there are γ, γⲠsuch that
(y,(q,γ))āV and (y,(q,γā²))āVā²,
and
we necessarily have
[TABLE]
so that γ=γā².
Moreover, we have (d,qā²),(d,qā²ā²)āγ,
but this implies qā²=qā²ā² since A is non-deterministic.
This concludes the proof of LemmaĀ 53.
\opt
draftnotes
Corollary 55**.**
Given A, F and Ļ as in LemmaĀ 53,
FSODā proves that for each xāDā there is at most
one qāQAā
such that
[TABLE]
We now state the Simulation TheoremĀ [EJ91, MS95].
Its proof in FSODā, requiring HF-closedness of automata,
is deferred to §9.
Theorem 56** (Simulation).**
For each HF-closed parity automaton A:Ī£
there is a non-deterministic HF-closed parity automaton
ND(A):Ī£
such that
[TABLE]
6.5. Projection
We now discuss the usual operation of projection,
which allows us to interpret (existential) quantification in MSO
(see §8.3).
This operation is defined on arbitrary alternating automata,
but it only correctly computes the appropriate projection for non-deterministic ones.
Given an automaton A:Ī£ĆĪ
as in DefinitionĀ 6.1,
we define its projection on Σ
to be the automaton āĪāA:Ī£ with
[TABLE]
where
[TABLE]
is given
by
[TABLE]
Note that Aut(A:Ī£ĆĪ)
implies Aut(āĪāA).
Moreover, āĪāA:Ī£ is an (HF-closed) parity
automaton whenever so is A:Ī£ĆĪ.
We shall now prove that āĪāA:Ī£
indeed implements the projection of A:Ī£ĆĪ.
This involves a notion of pairing for trees.
Given
F:Ī£ and G:Ī,
we let
āØF,Gā©:ĪĆĪ£
be given
(using the axiom of HF-Bounded Choice for HF-Functions (§3.4.5))
by
[TABLE]
Proposition 57**.**
Consider a non-deterministic A:Ī£ĆĪ and
let āĪāA:Ī£
be as defined above.
Then FSODā proves the following.
[TABLE]
Proof 6.6**.**
Given G:Ī
and a winning P-strategy Ļ on G(A,āØF,Gā©),
it is easy to see that Ļ is also a winning strategy on
G(āĪāA,F).
Conversely, assume that Ļ is a winning P-strategy on
G(āĪāA,F).
We define a tree G:Ī
by HF-Bounded Choice for HF-Functions (§3.4.5)
as follows:
For xāDā, if there is some infinite play
U of Ļ such that (x,q)āU for some state qāQAā,
then we let G(x) be some bāĪ
such that Ļ(x,q)āāAā(q,(F(x),b)).
Otherwise, we let G(x) be any element of Ī.
We now define a P-strategy ĻGā on G(A,āØF,Gā©)
as follows,
again using
HF-Bounded Choice for HF-Functions (§3.4.5).
If (x,q)āU for some infinite play U of Ļ, then we let
ĻGā(x,q):=Ļ(x,q).
Otherwise, we let ĻGā(x,q)=(q,γ), where
γāāAā(q,āØF,Gā©(x)).
We first check that ĻGā is indeed a strategy on G(A,āØF,Gā©),
namely that for all (x,q)āDāĆQAā,
if ĻGā(x,q)=(q,γ) then
γāāAā(q,āØF,Gā©(x)).
If (x,q) belongs to no infinite play of Ļ, then the result follows
by definition of ĻGā.
Otherwise, by CorollaryĀ 55,
q is unique in QAā such that (x,q) belongs to an infinite play
of Ļ, and we are done since
[TABLE]
In order to show that ĻGā is winning, we show that any infinite play
of ĻGā is also an infinite play of Ļ.
So let U:G(A,āØF,Gā©)to2
such that
[TABLE]
We are done if we show that
[TABLE]
which follows from the fact that
Claim 58**.**
[TABLE]
Proof 6.7** (Proof of Claim 58).**
We apply the Induction Scheme of FSODā
(§3.4.2).
In the base case x=εĖ,
and we conclude by LemmaĀ 38.
For the induction step consider the case of Sdā(x),
assuming the property for x.
So let qā²āQAā such that (Sdā(x),qā²)āU.
First, by applying
twice the Predecessor LemmaĀ 37 for Infinite Plays,
we get some qāQAā such that (x,q)āU,
and by induction hypothesis, there is some infinite play W of Ļ
such that (x,q)āW.
But then, by definition of ĻGā, we have Ļ(x,q)=ĻGā(x,q).
We thus have (d,qā²)āγ, where (q,γ)=Ļ(x,q).
Using LemmaĀ 38, let now Wā²
be an infinite play of Ļ from position (Sdā(x),qā²).
By Comprehension for Product Types
(TheoremĀ 23),
we define an infinite play Wā²ā² of Ļ from position (εĖ,qAιā)
as follows:
Given u a position of G(A,āØF,Gā©), if
uāWā² then uāWā²ā².
Otherwise, we let uāWā²ā² iff uāW and
uā¶Ļāā(Sdā(x),qā²).
It is then easy to check that Wā²ā² is an infinite play of Ļ.
This concludes the proof of PropositionĀ 57.
6.6. Complementation
It is known that, assuming the determinacy of acceptance games,
alternating tree automata are closed under complementĀ [MS87].
On the other hand, our setting only allows us to manipulate
positional strategies on acceptance games,
which leads us to formulate complementation for parity automata,
since their acceptance games are always positionally determined.
Thus, in this section, we formalize the fact that, assuming the axiom
(PosDet), each alternating parity automaton has a complement in FSO.
More precisely, we prove the following.
Theorem 59** (Complementation of Tree Automata).**
For each (HF-closed) parity automaton A:Ī£,
there is an (HF-closed) parity automaton ā¼A:Ī£
such that
[TABLE]
Alternating automata may be directly complemented in a locally syntactic fashion.
For an automaton A:Ī£ we may define a complement automaton
ā¼A:Ī£
with the same states as A, and such that P-strategies
in acceptance games for ā¼A correspond
(w.r.t. the visited states in infinite plays)
to O-strategies in acceptance games for A, and vice-versa.
Closely followingĀ [Wal02],
the basic idea
is to see the transition function of A
[TABLE]
as taking (q,a)
to the disjunctive normal form
[TABLE]
Then, for the complement ā¼A:Ī£ of A,
we can let
[TABLE]
take (q,a)
to the De Morgan dual of āAā(q,a).
We now proceed to the formal definition.
{defi}
Given a parity automaton A:Ī£, we define
the parity automaton
ā¼A:Ī£ as follows.
The automaton ā¼A has the same states and initial state as A.
Its transitions are defined
as
[TABLE]
Its coloring is given as follows,
using ConventionĀ 5.5.4:
[TABLE]
Note that by RemarkĀ 49,
ā¼A:Ī£ is HF-closed
whenever so is A:Ī£.
We are now going to prove TheoremĀ 59.
To this end, fix a parity automaton A:Ī£
and let ā¼A:Ī£ be as in DefinitionĀ 6.6.
Fix also some F:Ī£.
We split TheoremĀ 59 into the following statements.
Proposition 60**.**
FSO+(PosDet)ā¢\leavevmodeĀ \leavevmodeĀ Fā/L(A)\leavevmodeĀ \leavevmodeĀ ā¹\leavevmodeĀ \leavevmodeĀ FāL(ā¼A).
Proposition 61**.**
FSOā¢\leavevmodeĀ \leavevmodeĀ FāL(ā¼A)\leavevmodeĀ \leavevmodeĀ ā¹\leavevmodeĀ \leavevmodeĀ Fā/L(A).
The key
is that
P-strategies on G(ā¼A,F)
correspond to O-strategies on G(A,F), and vice-versa.
We make this formal in §6.6.1 and §6.6.2 below.
First, notice that Qā¼Aā=QAā,
so that
the games G(A,F) and G(ā¼A,F)
have the same sets of labels
[TABLE]
In the following, we let
[TABLE]
be the set of positions of the games
G(A,F) and G(ā¼A,F),
and we let
ι:=(εĖ,qAιā)
be their (common) initial position.
6.6.1. Proof of PropositionĀ 60.
We are going to show that
FSO+(PosDet) proves
[TABLE]
First,
given an O-strategy ĻOā on G(A,F),
we define a P-strategy ĻPā on G(ā¼A,F).
Assuming that
ĻOā
satisfies
StratOā(G(A,F),ĻOā),
the strategy ĻPā
will satisfy StratPā(G(ā¼A,F),ĻPā).
Recall that this in particular means
[TABLE]
By HF-Bounded Choice for Product Types (TheoremĀ 22)
we are going to define ĻPā such that
ĻPā(x,q)āāā¼Aā(q,F(x))
for each
(x,q)āDāĆQAā.
Assume fixed (x,q)āDāĆQAā.
For all γāPāā(DĆQAā)
such that γāāAā(q,F(x)),
we have ĻOā(x,(q,γ))āγ.
By HF-Comprehension (RemarkĀ 3.7.3),
let
[TABLE]
By construction, we thus have γāāāā¼Aā(q,F(x)),
and
we let
[TABLE]
We trivially have StratPā(G(ā¼A,F),ĻPā).
Lemma 62**.**
Consider ĻOā and ĻPā as above.
For every infinite play V of ĻPā in G(ā¼A,F)
there is some infinite play U of ĻOā in G(A,F)
with VPā=UPā.
Proof 6.8**.**
We define U by Comprehension for Product Types (TheoremĀ 23)
as follows.
First, for
(x,k)āGPā, if (x,k)āVPā then we let (x,k)āUPā.
Consider (x,(q,γ))āGOā.
Using RemarkĀ 12,
let āŗ be a well-order on Pāā(DĆQAā).
Then we let (x,(q,γ))āUOā iff
(x,q)āVPā
and γ is āŖÆ-minimal in āAā(q,F(x))
such that (Sdā(x),qā²)āVPā
for (d,qā²)=ĻOā(x,(q,γ)).
Note that consecutive P-positions in UPā are indeed
connected by the edge relation of G(A,F):
Claim 63**.**
[TABLE]
Proof 6.9** (Proof of Claim 63).**
We first show uniqueness. Let
(y0ā,(q0ā,γ0ā)),(y1ā,(q1ā,γ1ā))āUOā
be between (x,q) and (Sdā(x),qā²).
Then we must have y0ā=y1ā=x and q0ā=q1ā=q.
Hence, γ0ā and γ1ā are both āŖÆ-minimal in āAā(q,F(x))
such that ĻOā(x,(q,γ0ā))=ĻOā(x,(q,γ1ā))=(d,qā²),
yielding γ0ā=γ1ā as required.
We now show the existence of an appropriate (x,(q,γ))āUOā.
Since
Play(ĻPā,ι,V),
we have (d,qā²)āγā
with (ā,γā)āĻPā(y,ā)
for some (y,ā)āVPā.
But
Play(ĻPā,ι,V)
moreover implies that either (y,ā)ā²(x,q) or (x,q)ā“(y,ā),
from which follows that (y,ā)=(x,q)
and (q,γā)āĻPā(x,q).
Since
[TABLE]
it follows that (d,qā²)āĻOā(x,γ) for some
γāāAā(q,F(x)), and we are done.
We now check that U is indeed an infinite play of ĻOā,
i.e. that
Play(ĻOā,ι,U)
holds.
First, we have ιāU.
Moreover,
Claim 64**.**
[TABLE]
Proof 6.10** (Proof of Claim 64).**
We reason by induction on
ā¶ĻOāā
(CorollaryĀ 34).
First, if uāUOā, then u is of the form (x,(q,γ)).
By definition of UOā we have (x,q)āUPā with
(x,q)ā¶ĻOāā(x,(q,γ))
and we conclude by induction hypothesis.
Consider now the case of uāUPā=VPā.
In this case, u of the form (x,q).
We apply PropositionĀ 6.(5),
stating that either xāĪµĖ or x=Sdā(y) for some d and y.
In the former case,
since V is a play, we have
ιā¶ĻPāāā(x,q),
and
PropositionĀ 33.(9)
implies u=ι.
In the latter case, assume x is Sdā(y).
We apply twice
the Predecessor LemmaĀ 37 for Infinite Plays,
which gives some (y,qā²)āVPā such that
[TABLE]
By induction hypothesis we get
ιā¶ĻOāāā(y,qā²)
and we conclude by ClaimĀ 63.
Also,
Claim 65**.**
[TABLE]
Proof 6.11** (Proof of Claim 65).**
The case of uāUPā=VPā follows directly from the definition
of UOā and the fact that ĻOā:GOātoDĆP
and
Play(ĻPā,ι,V).
Consider now the case of uāUOā.
By definition of UOā there is some vāUPā
such that
uā¶ĻOāāv.
Uniqueness follows from the fact that UPā=VPā
and
Play(ĻPā,ι,V).
In order to obtain
Play(ĻOā,ι,U),
we invoke PropositionĀ 35
and it remains to show:
Claim 66**.**
[TABLE]
Proof 6.12** (Proof of Claim 66).**
The case of uāUOā follows from the definition of UOā.
The case of uāUPā directly follow from
ClaimĀ 63
(together with PropositionĀ 33.(9))
and
Play(ĻPā,ι,V).
This concludes the proof of LemmaĀ 62.
We use the following simple fact
in order to obtain from LemmaĀ 62
that ĻPā is winning in G(ā¼A,F)
whenever ĻOā is winning in G(A,F).
Lemma 67**.**
Given plays U,V:Gto2
as in LemmaĀ 62,
we have
Par(A,U)\leavevmodeĀ ā\leavevmode ¬Par(ā¼A,V).
We now have everything we need to obtain PropositionĀ 60,
namely
[TABLE]
Assume Fā/L(A).
By DefinitionĀ 47,
there is no winning P-strategy in G(A,F).
By the axiom of positional determinacy of parity games (PosDet)
there is a winning O-strategy ĻOā in G(A,F),
so that
[TABLE]
Consider now the P-strategy ĻPā on G(ā¼A,F)
as defined above.
We claim that ĻPā is winning, that is
{clm}
[TABLE]
Proof 6.13** (Proof of Claim \theclm).**
Given an infinite play V of ĻPā,
by LemmaĀ 62
we can build an infinite play U of ĻOā,
which byĀ (13)
satisfies ¬Par(A,ā),
so that V satisfies Par(ā¼A,ā)
thanks to LemmaĀ 67.
We thus have FāL(ā¼A,F).
This concludes the proof of PropositionĀ 60.
6.6.2. Proof of PropositionĀ 61.
We are now going to show that
FSO proves
[TABLE]
We associate a (winning) O-strategy
ĻOā on G(A,F)
to each (winning) P-strategy ĻPā on G(ā¼A,F).
Assuming that the P-strategy
satisfies
StratPā(G(ā¼A,F),ĻPā),
the O-strategy
will satisfy
StratOā(G(A,F),ĻOā).
Note that
[TABLE]
We define ĻOā(x,(q,γ))
for each position
[TABLE]
By definition of āā¼Aā(q,F(p)),
we have ĻPā(p,q)=(q,γā)
where γā intersects all γāāAā(q,F(p)).
So if γāāAā(q,F(p)),
by HF-Bounded Choice for Product Types (TheoremĀ 22)
we let ĻOā(p,(q,γ)) be some
(d,qā²) such that (d,qā²)āγā©Ī³ā.
Otherwise, since γī =ā
,
we let ĻOā(p,(q,γ)) be some
(d,qā²) such that (d,qā²)āγ.
We also trivially have that StratOā(G(A,F),ĻOā).
Lemma 68**.**
Consider a P-strategy ĻPā and
an O-strategy ĻOā as in above.
For every infinite play V
of ĻOā on G(A,F)
there is some infinite play U of ĻPā on G(ā¼A,F)
with VPā=UPā.
Proof 6.14**.**
We define U by Comprehension for Product Types (TheoremĀ 23)
as follows.
Definition of U.*
For (x,k)āGPā, if (x,k)āVPā then we let (x,k)āUPā,
and for (x,(q,γā))āGOā, we let (x,(q,γā))āUOā
iff (q,γā)=ĻPā(x,q)
for (x,q)āUPā.*
Similarly as in LemmaĀ 62,
we have
Claim 69**.**
[TABLE]
Proof 6.15** (Proof of Claim 69).**
Uniqueness directly follows from the fact that u=(x,ĻPā(x,q)).
As for existence, we directly have
(x,q)ā¶ĻPāāu,
so it remains to show
uā¶ĻPāā(Sdā(x),qā²),
which amounts to (d,qā²)āγā for (q,γā)=ĻPā(x,q).
But (Sdā(x),qā²)āVPā
with
Play(ĻOā,ι,V)
imply that (d,qā²)=ĻOā(x,(ā,γ))
for some ā such that (x,ā)āVPā
and some γāāAā(ā,F(x)).
Moreover,
Play(ĻOā,ι,V)
implies ā=q.
By definition of ĻOā,
we thus have (d,qā²)āγā©Ī³ā and we are done.
We now check that
Play(ĻPā,ι,U).
Note that ιāU.
Moreover, proceeding as in
LemmaĀ 62,
we have
Claim 70**.**
[TABLE]
Proof 6.16** (Proof of Claim 70).**
By induction on ā¶ĻPāā
(CorollaryĀ 34).
The case of uāUOā follows directly form the induction hypothesis
and the definition of UOā.
As for uāUPā, we proceed as
in LemmaĀ 62,
using ClaimĀ 69 and
LemmaĀ 37.
Continuing as in LemmaĀ 62,
we now invoke PropositionĀ 35
and we are left with showing
Claim 71**.**
[TABLE]
Proof 6.17** (Proof of Claim 71).**
The cases of uāUPā follow from the definition of UOā,
and from ClaimĀ 63
(together with PropositionĀ 33.(9))
and
Play(ĻOā,ι,V).
Consider now uāUOā.
The predecessor property follows from the definition of UOā.
The unique successor property
is obtained from ClaimĀ 69
together with
Play(ĻOā,ι,V).
This concludes the proof of LemmaĀ 68.
Similarly as in §6.6.1,
we use the following simple fact.
Lemma 72**.**
Given plays U,V:Gto2
as in LemmaĀ 68,
we have
Par(ā¼A,U)\leavevmodeĀ ā\leavevmode ¬Par(A,V)
It is now easy to obtain PropositionĀ 61,
namely
[TABLE]
Assume that FāL(ā¼A).
By DefinitionĀ 47, we thus have a winning
P-strategy ĻPā in G(ā¼A,F),
so that
[TABLE]
Consider now the O-strategy ĻOā on G(A,F)
as defined above.
Reasoning as in the case Fā/L(A)
(§6.6.1),
LemmasĀ 68
andĀ 72
imply
[TABLE]
It then follows from LemmaĀ 41
that there is no winning P-strategy on G(A,F),
so that Fā/L(A).
This concludes the proof of PropositionĀ 61.
7. MSO on Infinite Words in Paths of FSODā
We discuss here the theory of MSO over Ļ-words
for the infinite paths of FSODā.
Since MSO on Ļ-words admits a complete axiomatizationĀ [Sie70],
this will allow us to
freely import results on MSO over Ļ-words
for the paths of FSODā.
In particular, our completeness argument (§8)
relies on a version of the Büchi-Landweberās TheoremĀ [BL69]
formulated with MSO over Ļ-words,
that we lift for free to FSODā.
Also, to prove
the Simulation Theorem 56 in §9,
we use McNaughtonās TheoremĀ [McN66],
and similarly obtain it for free in FSODā.
An obvious way to obtain MSO over Ļ-words is to consider
the system MSO1ā (that is MSODā for D=1).
However, recall that we want to see each path
of FSODā (in the sense ofĀ (16) below)
as a model of MSO on Ļ-words.
This is technically simpler if, followingĀ [Rib12],
one uses a version of MSO on Ļ-words
over a purely relational vocabulary with only
the strict order <Ėā on numbers as atomic relation
(besides equality ā).
{defi}
[The Theory FSO[<Ėā]Ļ]
The language of FSO[<Ėā]Ļ is the language of FSODā
with the following restriction:
the only Individual terms of FSO[<Ėā]Ļ
are the constant ĪµĖ and
the individual variables (x,y,z etc.)
The deduction rules of FSO[<Ėā]Ļ are the same as the rules of
FSODā.
The axioms of FSO[<Ėā]Ļ are
the Equality Axioms of §3.4.1,
the Axioms on HF-Sets of §3.4.4,
the Functional Choice Axioms of §3.4.5,
together with
the axioms displayed on FigureĀ 6,
stating that <Ėā is a discrete unbounded strict linear order with ĪµĖ as its minimal element
(see e.g.Ā [Rib12]),
and with
the following induction scheme.
Well-Founded Induction.
For each formula Ļ, the axiom
[TABLE]
Remark 73**.**
Note that all Individuals of FSO[<Ėā]Ļ
are Individuals of FSODā, but not conversely.
As a consequence, all HF-terms of FSO[<Ėā]Ļ
are HF-terms of FSODā, but not conversely.
Also, note that it may have seemed more natural not to include the individual
constant ĪµĖ in the language of FSO[<Ėā]Ļ.
We have included it because this eases our concrete uses of FSO[<Ėā]Ļ
in §8.4 and §9.2.
Similarly to the case of D-ary trees (§2),
the theory FSO[<Ėā]Ļ is intended to be interpreted
in a theory MSO[<Ėā]Ļ.
Intuitively, MSO[<Ėā]Ļ is to FSO[<Ėā]Ļ what MSODā is to FSODā.
{defi}
[The Theory MSO[<Ėā]Ļ]
The language of MSO[<Ėā]Ļ is the language of MSODā
with the following restriction:
the only Individual terms of MSO[<Ėā]Ļ
are individual variables (x,y,z etc.).
The axioms of MSO[<Ėā]Ļ are the equality axioms
and the comprehension scheme of MSODā (§2.2),
together with the induction scheme
and the axioms on <Ėā of FSO[<Ėā]Ļ
displayed in FigureĀ 6.
We write N both for the standard model of FSO[<Ėā]Ļ
and for the standard model of MSO[<Ėā]Ļ.
In the case of MSO[<Ėā]Ļ,
formulae are interpreted in N as expected:
individual variables range over N, monadic predicate variables
range over P(N) and <Ėā is the standard order < on N.
The interpretation of FSO[<Ėā]Ļ-formulae in N is similar,
with the obvious changes w.r.t. §3.5 for the interpretation
of terms, and where Functions range over
[TABLE]
The key property of MSO[<Ėā]Ļ we rely on is that it completely axiomatizes the
theory of the standard model N
of Ļ-wordsĀ [Sie70]
(see alsoĀ [Rib12]).
Theorem 74** ([Sie70]).**
For every closed MSO[<Ėā]Ļ-formula Ļ,
[TABLE]
The formula translation from FSODā to MSODā of §3.6
restricts to a translation of FSO[<Ėā]Ļ-formulae
to MSO[<Ėā]Ļ-formulae.
This easily extends to theories,
and we get the following version of PropositionĀ 20.
Proposition 75**.**
For every closed FSO[<Ėā]Ļ-formula Ļ,
[TABLE]
Thanks toĀ (15),
the completeness of MSO[<Ėā]Ļ directly gives the completeness
of MSO[<Ėā]Ļ w.r.t. the translation closed of FSO[<Ėā]Ļ-formulae Ļ:
[TABLE]
Our goal now is to prove that if a closed FSO[<Ėā]Ļ formula holds in the
standard model N of Ļ-words, then FSODā
proves its relativization to any rooted tree path.
Given a formula Ļ of FSO[<Ėā]Ļ and a Function variable P,
write ĻP for the FSODā formula
obtained from Ļ
by relativizing all individual quantifications to P
and by replacing all Function quantifications
F:K by F:PtoK.
Moreover,
we say that P:Dāto2 is a rooted path
when the following formula TPath(P) holds:
[TABLE]
where S(x,y) stands for
[TABLE]
We can now formally state the property we are targeting:
[TABLE]
The proof ofĀ (17) is deferred to PropositionĀ 78.
It relies on two lemmas.
The first one is an adaptation of
Lemma 27 (§4.3)
to rooted tree paths, which will give the last axiom of FigureĀ 6
for rooted tree paths.
The second one is a weakening ofĀ (17)
where FSO[<Ėā]Ļā¢Ļ is assumed instead of NāØĻ.
Lemma 76**.**
FSODā* proves the following, assuming P:Dāto2
and TPath(P):*
[TABLE]
Lemma 77**.**
For all closed FSO[<Ėā]Ļ-formula Ļ, we have
[TABLE]
Proof 7.1**.**
The proof is by induction on derivations of FSO[<Ėā]Ļ-formulae.
For formulae Ļ,Ļ with free Function variables
F=F1ā,ā¦,Fpā and free Individual variables
x=x1ā,ā¦,xqā
(and possibly further free HF-variables), we show that
for all HF-terms K=K1ā,ā¦,Kpā of FSO[<Ėā]Ļ
we have
[TABLE]
The cases for each inference rule are immediate from their respective
induction hypothesis, and we also easily obtain
the Equality Axioms (§3.4.1),
the Axioms of HF-Sets (§3.4.4)
and the Axiom of HF-Bounded Choice for HF-Sets (§3.4.5).
We resort on TheoremĀ 22
for the axioms of HF-Bounded Choice for Functions
and of Iterated HF-Bounded Choice.
Moreover, the Induction axiom of FSO[<Ėā]Ļ on the formula Ļ(x)
directly follows from Well-Founded Induction in FSODā
(TheoremĀ 7)
on the formula
[TABLE]
It remains to deal with the <Ėā-axioms of FigureĀ 6.
The first five axioms
(stating that <Ėā is an unbounded linear order)
directly follow from the Tree axioms of FSODā (FigureĀ 3)
and from relativization to P with TPath(P).
Finally, we have to show that FSODā proves
that the translation of the predecessor axiom
holds within P whenever TPath(P) is assumed:
[TABLE]
*This is handled by LemmaĀ 76.
*
We have now everything we need to proveĀ (17).
Proposition 78**.**
Consider a closed formula Ļ of FSO[<Ėā]Ļ.
Then
[TABLE]
Proof 7.2**.**
Assume
NāØĻ.
ByĀ (15)
we have
NāØāØĻā©.
TheoremĀ 74 then implies
MSO[<Ėā]Ļā¢āØĻā©,
and byĀ (14)
we have that
FSO[<Ėā]Ļā¢Ļ.
We conclude by LemmaĀ 77.
8. Completeness
This Section is devoted to the proof of our main result,
the completeness of FSO+(PosDet).
Theorem 79** (Main Theorem).**
For each closed formula Ļ of FSO,
[TABLE]
8.1. Overview
The two main ingredients of TheoremĀ 79 are the following.
- (1)
The translations
[TABLE]
providing faithful mutual interpretations of FSO and MSO
(§3.6, recapitulated in Table 2).
2. (2)
The translation of MSO-formulae to automata, that we detail
in §8.2 and §8.3 below.
This translation relies on the correctness of the constructions
on automata of §6, which are recapitulated in Table 1.
In particular, we require the Axiom (PosDet)
of positional determinacy of parity games (§5.6)
for the complementation of tree automata (TheoremĀ 59).
The mutual interpretability results of TableĀ 2
also allows us to obtain a completeness result for MSO.
Recall that āØPosDetā© is defined in DefinitionĀ 5.6.1,
§5.6.1.
We then get the following corollary to TheoremĀ 79.
Corollary 80**.**
For each closed formula Ļ of MSO,
[TABLE]
Proof 8.1**.**
Consider a closed MSO-formula Ļ.
Assume FSO+(PosDet)ā¢Ļā.
Let PosDet(Piā,Oiā,niā) (i=1,ā¦,k)
be the instances of (PosDet) used in the proof, so that
[TABLE]
ByĀ (6) (PropositionĀ 20),
we get
[TABLE]
and since (ā)ā commutes over propositional connectives,
by TheoremĀ 19 we obtain
[TABLE]
Moreover, since Ļā is HF-closed, we can assume
the HF-terms Piā, Oiā and niā to be closed.
It follows that there are constants for HF-sets
PĖiā, OĖiā and nĖiā (i=1ā¦,k)
such that
each formula āØPosDet(Piā,Oiā,niā)ā©
is syntactically identical to
āØPosDet(PĖiā,OĖiā,nĖiā)ā©.
We thus obtain
[TABLE]
which implies that MSO+āØPosDetā© proves Ļ.
If FSO+(PosDet) does not prove Ļā,
TheoremĀ 79 gives
FSO+(PosDet)ā¢Ā¬(Ļā)
and we conclude similarly.
In particular, it follows from PropositionĀ 46
that FSO+(PosDet) completely axiomatizes the standard
model T of D-ary trees.
Corollary 81**.**
For each closed formula Ļ of FSO,
[TABLE]
For each closed formula Ļ of MSO,
[TABLE]
Remark 82**.**
Note that it follows from RemarkĀ 9
that TheoremĀ 79 together with CorollaryĀ 81
implies the decidability of FSO over its standard model T.
By LemmaĀ 18 (see TableĀ 2)
we thus obtain a proof of Rabinās Tree TheoremĀ [Rab69],
namely the decidability of MSO over T.
However, even if provability in FSO is semi-recursive,
the axiom set of FSO is not recursive and the interpretation
of HF-Functions is not computable
(see RemarksĀ 9 andĀ 10
in §3.4.4,
as well as Remark 16 in §3.6.1).
We further elaborate on this in §8.5.
We will actually deduce TheoremĀ 79
via PropositionĀ 20,
(6)
(see TableĀ 2)
from the following.
Theorem 83**.**
For each closed formula Ļ of MSO,
[TABLE]
The proof of TheoremĀ 83
proceeds as expected via a translation of MSO-formulae
to automata.
As usual, such translations are easier to define when one starts from a version
of MSO with a purely relational and individual-free language.
We perform a translation of MSO to such a language in §8.2.
Then, the translation of formulae to automata is presented in §8.3.
It relies on the constructions of §6.
We thus arrive at PropositionĀ 87,
namely that
for each closed formula Ļ of MSO
there is an HF-closed parity automaton A over the
singleton alphabet 1
such that
[TABLE]
In order to obtain TheoremĀ 83,
it remains to show that
FSO actually decides the emptiness of such automata:
[TABLE]
This is PropositionĀ 88.
Its proof relies on the fact that the acceptance games of (A:1)
are actually generated from closed HF-Sets.
We call such games reduced parity games.
SectionĀ 8.4 is devoted to defining reduced parity games
and to showing that FSO decides winning for them
(TheoremĀ 93).
This essentially amounts to
a version of the Büchi-Landweber Theorem [BL69]
(see also e.g.Ā [Tho97, PP04]),
the effective determinacy
of parity games on finite graphs,
which is obtained thanks to the completeness of FSO[<Ėā]Ļ (§7).
TheoremĀ 93 then follows from the lifting of FSO[<Ėā]Ļ
to the paths of FSO (PropositionĀ 78).
8.2. Restricted Languages for MSODā
For the translation of formulae to automata, it is
useful and customary to work with formulae in a slightly different syntax,
based on a purely relational, individual-free vocabulary.
8.2.1. Restriction to a Relational Language
We first restrict to a purely relational vocabulary,
based on the defined formulae
[TABLE]
The relational formulae Ļ,ĻāĪDRā
are built from atomic formulae Xy and Sdā(x,y)
by means of ¬, āØ, āx and āX.
To each MSO-formula ĻāĪ
we associate a formula ĻR as follows.
For t a term of MSO,
define the formula (zāt) by structural induction on t:
[TABLE]
Note that
[TABLE]
Then, ĻR is obtained from Ļ
by replacing each atomic formula Xt, where t is not a variable,
by (āz)[(zāt)ā§Xz], where z is a fresh variable.
Lemma 84**.**
For every MSO-formula Ļ, we have
MSOā¢ĻāĻR.
8.2.2. Restriction to an Individual-Free Language
The next step is to get rid of individual quantifiers.
Consider the defined formulae:
[TABLE]
The individual-free formulae
Ļ,ĻāĪDIFā
are built from atomic formulae
(XāĖāY)
and Sdā(X,Y)
by means of negation, disjunction and
second-order monadic quantification āX only.
Let ĻāĪR
with free variables among x1ā,ā¦,xpā,Y1ā,ā¦,Yqā.
We inductively associate to Ļ a formula ĻIFāĪIF
with free variables among
X1ā,ā¦,Xpā,Y1ā,ā¦,Yqā
as follows.
Let
[TABLE]
where
[TABLE]
The other inductive cases are given as follows:
[TABLE]
Lemma 85**.**
For every formula ĻāĪR
with free variables among x,Y,
we have
[TABLE]
By composing the translations
(ā)R:ĪāĪR
and
(ā)IF:ĪRāĪIF,
we obtain:
Corollary 86**.**
For every closed MSO-formula Ļ,
there is a closed formula ĻāĪIF
such that MSOā¢ĻāĻ.
8.3. From Formulae to Automata
We are now going to associate to each formula ĻāĪIF
with free variables among X1ā,ā¦,Xpā
an HF-closed parity automaton A(Ļ):2p
such that
[TABLE]
Note that the correctness of A(Ļ) w.r.t. Ļ
is proved in FSO using the translation
(ā)ā:MSOāFSO
of §3.6.2.
Recall that (ā)ā replaces each monadic variable Xiā of Ļ
by a Function variable (FXiāā:2).
The construction of A(Ļ) from Ļ
is done by induction on Ļ
using the operations on automata devised in §6
(see TableĀ 1).
The base cases are provided by
the automata A(XiāāĖāXjā) and A(Sdā(Xiā,Xjā))
discussed in §8.3.1 below
for the atomic formulae of ĪIF.
The inductive cases are performed as follows,
where we implicitly apply substitutions (cf. §6.2)
when necessary:
[TABLE]
In particular, if Ļ is closed then A(Ļ)
is an automaton over the singleton alphabet 1,
whence by CorollaryĀ 86
we have:
Proposition 87**.**
For each closed formula Ļ of MSO
there is an HF-closed parity automaton (A:1)
such that
[TABLE]
In order to obtain TheoremĀ 83 from PropositionĀ 87,
it remains to show that FSO actually decides the emptiness
of L(A) for an HF-closed parity automaton A over the singleton
alphabet 1.
Proposition 88**.**
Given an HF-closed parity automaton (A:1),
[TABLE]
Proposition 88 is proved in §8.4 below.
8.3.1. Automata for Atomic Formulae
We provide HF-closed parity automata for the atomic formulae (X1āāĖāX2ā)
and Sdā(X1ā,X2ā) of the individual-free syntax
ĪIF of MSO.
The automaton A(X1āāĖāX2ā) over 2Ć2
has state set B={tt,ff}, with tt initial,
transitions given by
[TABLE]
and coloring C:Bto2
given by
[TABLE]
For dāD,
the automaton A(Sdā(X1ā,X2ā)) over 2Ć2
has state set QSā:=B+{w},
with ff initial,
transitions given by
[TABLE]
and with coloring given by
[TABLE]
Remark 89**.**
Recall from §8.2.2
that the formula Sdā(X,Y) of the individual-free syntax
ĪIF amounts in MSO to the formula
(āx)(āy)[Xxā§Yyā§yāSdā(x)].
So the automaton A(Sdā(X,Y)) only looks for some
xāX and yāY such that y is the d-successor of x,
but is does not check whether X and Y are singletons.
Lemma 90**.**
FSO* proves that*
[TABLE]
8.4. Reduced Parity Games
The goal of this Section is to prove PropositionĀ 88,
namely that for
an HF-closed parity automaton A
over the singleton alphabet 1,
[TABLE]
Consider an HF-closed automaton A over the singleton alphabet 1={0}.
Then for any (F:1)
the game G:=G(A,F) has edge relations induced by functions
[TABLE]
given (following RemarkĀ 49)
by
[TABLE]
So in particular the edge relations of G(A,F)
are independent from F.
But also,
since
[TABLE]
the whole game G(A,F)
is actually generated from HF-Sets.
In this Section, we discuss games generated from HF-Sets,
that we call reduced games.
We show that for reduced parity games, winning can actually be defined
within FSO[<Ėā]Ļ.
Thanks to the completeness of FSO[<Ėā]Ļ w.r.t. its standard model
(§7),
this implies that FSO[<Ėā]Ļ itself decides winning in such games.
This essentially amounts to a version of the Büchi-Landweber Theorem [BL69]
using the completeness of MSO[<Ėā]Ļ over its standard model.
Using PropositionĀ 78
we can then lift this result to FSO.
In §8.4.1 and §8.4.2
we repeat some material of §5,
but for the slightly different setting of reduced games.
We then obtain that FSO[<Ėā]Ļ decides winning in reduced parity games,
and we lift this to FSO in Theorem 93, §8.4.3.
This directly entails PropositionĀ 88.
8.4.1. Reduced Games as HF-Sets
The purpose of this Section is to give
adaptations of the notions of §5
to those parity games which are entirely generated from HF-Sets.
All the formulae of this Section are HF-formulae
in the sense of DefinitionĀ 3.4.4.
Hence, thanks to the Axioms of HF-Sets
(Remark 11, §3.4.4)
their closed instances are provable (both in FSO and FSO[<Ėā]Ļ)
if and only if they hold in VĻā.
{defi}
[Reduced Games]
A reduced game G
is given by HF-terms P,O,ePā,eOā
which satisfy the following formula
[TABLE]
We often write Game0ā(G) for
Game0ā(P,O,ePā,eOā).
Moreover, when no ambiguity arises, we abbreviate
G=(P,O,ePā,eOā) as
G=(P,O,e(G)).
{defi}
[Reduced Subgame]
We say that Gā²=(Pā²,Oā²,ePā²ā,eOā²ā)
is a reduced subgame of G=(P,O,ePā,eOā) whenever the following
formula holds
[TABLE]
{defi}
[Reduced Strategies]
Let G=(P,O,ePā,eOā)
where P,O,ePā,eOā are HF-variables.
- (1)
A reduced P-strategy on G
is an HF-set s
which satisfies the formula
[TABLE]
2. (2)
A reduced O-strategy on G is an HF-set
s
which satisfies the formula
[TABLE]
{defi}
[Reduced Subgame induced by a Reduced Strategy]
Given a player J (either P or O)
and a J-strategy s on G,
we let
[TABLE]
where
[TABLE]
and where {s}JāāeJā
is defined
(following the method of RemarkĀ 49)
to be the function
taking kāGJā
to the singleton {s(k)}.
Whenever possible, we write Gā¾{s}
or even just s for Gā¾{s}Jā.
8.4.2. Reduced Games in FSO[<Ėā]Ļ
In §8.4.1 we gave notions
of reduced parity games and reduced strategies.
In this Section, we work within FSO[<Ėā]Ļ and show
that this setting suffices to define winning
for reduced parity games.
Thanks to the completeness of FSO[<Ėā]Ļ w.r.t. the standard model of Ļ-words
(§7),
we obtain that FSO[<Ėā]Ļ decides winning in such games.
This is essentially the Büchi-Landweber Theorem [BL69].
We use the following FSO[<Ėā]Ļ-formula:
[TABLE]
{defi}
[Infinite Plays in Reduced Games]
Working in FSO[<Ėā]Ļ,
let G=(P,O,ePā,eOā),
where P,O,ePā,eOā are HF-variables.
Given an HF set K and a Function (V~:P),
we say that
V~ is an infinite play in G from K when the following
formula Play[<Ėā](G,K,V~) holds:
[TABLE]
Note that in DefinitionĀ 8.4.2 above,
we use the notation V~ for a play
in a reduced games,
to mark the difference with the notion of
plays (and more generally sets of game positions)
in the setting of §4.
{defi}
[Parity Conditions for Reduced Games]
Working in FSO[<Ėā]Ļ,
let G=(P,O,ePā,eOā),
where P,O,ePā,eOā are HF-variables.
- (1)
A coloring is given by Function C and an HF-set n
satisfying the following formula
[TABLE]
2. (2)
We define the following formula:
[TABLE]
{defi}
[Winning of Reduced Parity Games]
Working in FSO[<Ėā]Ļ,
let G=(P,O,ePā,eOā),
where P,O,ePā,eOā are HF-variables.
Furthermore let C be a Function variable and n be an HF-variable.
- (1)
We define the following formulae.
[TABLE]
2. (2)
Given a player J (either P or O),
we say that a J-strategy s is
winning in (G,C,n) from K
if the game (G{s}Jā,Par[<Ėā](C,n,ā)) is won by J from K,
i.e. if
the following formula holds
[TABLE]
Note that in DefinitionĀ 8.4.2,
we have denoted strategies in reduced games with a lower case roman s.
This notation contrasts with our notation Ļ for games
in the sense of §5 in order to insist on the fact that
strategies on reduced games are HF-sets.
Consider now G=(P,O,ePā,eOā)
where P, O, ePā and eOā are closed HF-terms
such that
[TABLE]
Assume also given closed HF-terms n and C
such that
[TABLE]
Then the positional determinacy of parity games (cf.Ā [EJ91])
implies
that for every HF-set ĪŗāP,
the following holds in the standard model N
of FSO[<Ėā]Ļ:
For some player J (either P or O)
there an HF-set s such that
[TABLE]
Thanks to the completeness of FSO[<Ėā]Ļ w.r.t. N
(TheoremĀ 74 and PropositionĀ 75),
we obtain the following result,
that may be viewed as a formulation of the Büchi-Landweber Theorem [BL69]
(see also e.g.Ā [Tho97, PP04]).
Recall that StratJ0ā(G,s) holds in
N (resp. FSO[<Ėā]Ļ, FSO) if and only if it holds
in VĻā.
Proposition 91**.**
Assume given closed HF-terms G=(P,O,ePā,eOā), n and C such that
[TABLE]
Then for every ĪŗāP,
there is a player J (either P or O)
and an HF-set s such that
[TABLE]
PropositionĀ 78,
namely
[TABLE]
(for Ļ a closed FSO[<Ėā]Ļ-formula)
moreover gives the following.
Proposition 92**.**
Assume given closed HF-terms G=(P,O,ePā,eOā), n and C such that
[TABLE]
Then for every ĪŗāP,
there is a player J (either P or O)
and an HF-set s such that
[TABLE]
8.4.3. Reduced Games in FSO
We now come back to FSO.
In this Section, we show, using PropositionĀ 92,
that FSO decides winning for parity games
induced from reduced parity games
(TheoremĀ 93).
This directly gives PropositionĀ 88.
A reduced game G=(P,O,ePā,eOā)
induces a game G=(P,O,EPā,EOā) in the sense
of DefinitionĀ 5.1,
where
[TABLE]
are defined using
HF-Bounded Choice for Product Types (TheoremĀ 22)
as
[TABLE]
Similarly, a strategy s in a reduced game G induces
a strategy Ļ in G in the sense of DefinitionĀ 5.3,
with
[TABLE]
As for colorings, from (C:Pto[0,n]) we define
C^:Gto[0,n] as in DefinitionĀ 47:
[TABLE]
We clearly have the following:
[TABLE]
Theorem 93**.**
Assume given closed HF-terms G=(P,O,ePā,eOā), n and C such that
[TABLE]
Then for every ĪŗāP,
[TABLE]
In the statement of TheoremĀ 93,
G(ā“) refers to the the game of RemarkĀ 32
(see also RemarkĀ 45).
Remark 94**.**
The crucial differences between TheoremĀ 93
and the axiom (PosDet)
are the following.
On one hand, TheoremĀ 93
allows us to derive (PosDet) for games on finite graphs only,
while (PosDet) speaks about arbitrary FSO-definable games
(in the sense of §5).
On the other hand,
TheoremĀ 93
says that FSO decides winning for games on finite graphs,
while (PosDet) is a statement of determinacy, i.e.Ā that one of the players wins,
but not which player wins.
Proof 8.2** (Proof of TheoremĀ 93).**
Fix G, n, C and Īŗ as in the statement.
Let J and s be given by PropositionĀ 92,
and let Ļ be induced from s as above.
We are going to show that Ļ is winning in G from position Īŗ:
[TABLE]
So let V:Gto2 be an infinite play of Ļ from Īŗ.
Our plan is to obtain Par(G,C^,n,V)
from PropositionĀ 92.
By Comprehension for Product Types (TheoremĀ 23),
let ā£Vā£:Dāto2
be the set of all xāDā such that
(x,k)āV for some kāP.
Note that TPath(ā£Vā£) holds in FSO.
PropositionĀ 92
then gives
[TABLE]
Note that
[TABLE]
and similarly for
WinStrat[<Ėā]Oā£Vā£ā(G,s,Īŗ,C,n).
By HF-Bounded Choice for Functions (§3.4.5),
let V~:ā£Vā£toP
take xāā£V⣠to the unique kāP
such that (x,k)āV.
Then we are done as soon as we show
Claim 95**.**
[TABLE]
Proof 8.3** (Proof of Claim 95).**
The property on parity conditions follows from the fact that
for all mā[0,n] we have
[TABLE]
As for Play[<Ėā]ā£Vā£(s,Īŗ,V~),
note that it unfolds to
[TABLE]
where
[TABLE]
But this directly follows from the definition of Ļ from s
together with the fact that V is a play of Ļ from Īŗ.
This concludes the proof of TheoremĀ 93.
We are now ready to prove PropositionĀ 88,
thus completing the proof of TheoremĀ 83.
Proof 8.4** (Proof of PropositionĀ 88).**
We have to show that for
an HF-closed parity automaton (A:1),
[TABLE]
For any (F:1),
the game G(A,F) is generated as above from the edge
relationsĀ (18).
Moreover, recall from DefinitionĀ 47
that the winning condition of G(A,F)
is generated, as in the statement of TheoremĀ 93,
by the game G(A,F)(ā“) of RemarkĀ 32.
We then conclude by TheoremĀ 93,
and this completes the proof of PropositionĀ 88.
8.5. Remarks on Recursiveness
We noted in RemarkĀ 82
that
the completeness of FSO+(PosDet) indeed allows us
to decide FSO and MSO formulae in the standard model T of §3.5.
This however comes with two apparent defects.
The first one is that the interpretation [[ā]] of HF-terms fixed
in ConventionĀ 3.4.4 is not computable
(see RemarksĀ 10 andĀ 15),
because provability in Sk(ZFCā) is not decidable
(as this theory contains the Ī 10ā fragment of arithmetic).
The second one is that, although the axiom set MSO+āØPosDetā©
is even polynomial-time recognizable (recall that āØPosDetā© is defined in
Definition 5.6.1, §5.6.1),
the interpretation āØāā© for HF-terms relies on ConventionĀ 3.4.4
(fixing the interpretation of HF-Functions),
and is thus not computable.
We discuss here a workaround for this involving a slightly different setting for FSO.
We chose to not officially work in that setting because we found it less uniform
and elegant than the current presentation of FSO,
which nonetheless still allows us to derive Rabinās Tree TheoremĀ [Rab69].
Rather than taking all the axioms on HF-sets
of §3.4.4, in particular considering
the whole theory Sk(ZFCā) there, we may work in systems
parametrized by chosen sets of HF-Functions.
A way to implement this would be to consider systems FSO(SK),
where the parameter SK specifies some interpretations
gn,mā for constants gĖān,mā
such thatĀ (2) is assumed to hold.
Concretely, a specification SK consists of a set SKāNĆN
together with functions
[TABLE]
Given a set SKāNĆN,
we let ZFCā(SK) consist of ZFCā augmented with
the axioms
[TABLE]
We say that SK is a specification if
[TABLE]
where,
for each (n,m)āSK,
gn,mā
is a computable function VĻnāāVĻā, and
for each each gĖānā²,mā²ā occurring in Ļn,mā,
we have (nā²,mā²)āSK, and
ZFCā(SK)ā¢(āk1ā,ā¦,knā)(ā!ā)Ļn,mā,
and
VĻāāØ(āk1ā,ā¦,knā)Ļn,mā[gn,mā(k1ā,ā¦,knā)/ā]
Given a specification SK, one can fix the interpretation
of all constants (gĖān,mā)n,māNā
by taking for gĖān,mā with (n,m)ā/SK
the function VĻnāāVĻā
with constant value ā
.
For the formal definition of FSO(SK),
instead of the Axioms on HF-Sets of §3.4.4, one has the following.
For each (n,m)āSK, and for all HF-terms K=K1ā,ā¦,Knā,
the axiom
[TABLE]
For each closed HF-formula Ļ such that VĻāāØĻ,
the axiom
[TABLE]
Given a specification SK, the interpretations [[ā]]
and āØāā© are computable.
All results of this paper
hold for sufficiently large specifications.
Theorem 96**.**
Let SK be a specification defining all the HF-Functions
ofĀ 1ā8, §3.4.4,
as well as those of ConventionĀ 5.5,
§5.5.
Then all the results stated in §8
hold for FSO(SK) instead of FSO.
9. The Simulation Theorem
This Section is devoted to the proof of the
Simulation Theorem, cf.Ā [EJ91, MS95].
Theorem 97** (Simulation TheoremĀ 56).**
For each HF-closed parity automaton A:Ī£
there is a non-deterministic HF-closed parity automaton
ND(A):Ī£
such that
[TABLE]
We assume that A is HF-closed in TheoremĀ 97
because we rely on McNaughtonās TheoremĀ [McN66],
in the standard model for Ļ-words,
which we import into FSO thanks to PropositionĀ 78.
Before a detailed exposition, let us explain the main idea
behind TheoremĀ 97.
We momentarily work in the usual mathematical universe
(i.e. not in the formal theory FSO).
Recall that in a non-deterministic automaton N, O can only explicitly choose
tree directions, since for each possible γNā in the image of āNā,
if (d,q),(d,qā²)āγNā then q=qā², by definition.
In order to obtain a non-deterministic automaton N
from an alternating automaton A,
the idea is to perform a subset construction,
such that each γNā in the image of āNā is of the form
[TABLE]
where each Sdā²ā gathers states q such that (d,q)āγAā
with γAā in the image of āAā.
More precisely, assuming SāPāā(QAā), one may consider functions
[TABLE]
Each such f induces
[TABLE]
and we can let
[TABLE]
Then, for each γNā(f) in the image of āNā
and for each tree direction dāD, the set Sdā²ā
is unique such that (d,Sdā²ā)āγNā(f),
and N satisfies the property asked in DefinitionĀ 6.4
to non-deterministic automata.
There is however a difficulty in the definition
of the acceptance condition of N.
We follow here the construction ofĀ [Wal02]
where the states of N, rather than being simply sets of states, are
sets of pairs of states SāP(QAāĆQAā).
Then an infinite sequence of states S0ā,S1ā,ā¦āQNā
induces a set of traces q0ā,q1ā,ā¦āQAā
with (qiā,qi+1ā)āSi+1ā.
For (Snā)nāNāāQNĻā to be accepting, one may then require
all its traces (qnā)nāNāāQAĻā
to be accepting.
We may obtain a parity condition for N
by noticing that its acceptance condition is Ļ-regular
(i.e. definable in MSO over Ļ-words).
This allows us to apply McNaughtonās TheoremĀ [McN66],
and to obtain a deterministic Ļ-word parity automaton D
whose language is the set of accepting sequences
(Snā)nāNāāQNĻā.
A suitable product of N with D then gives a non-deterministic
parity automaton equivalent to A.
The organization of this Section follows the above construction.
Working in FSO, consider a parity automaton A:Ī£.
We will build a non-deterministic automaton
ND(A):Ī£ with the same language.
The automaton ND(A) will be defined in three steps:
- (1)
We first define in §9.1 a non-deterministic automaton \ocA
in the sense of DefinitionĀ 6.1.
The acceptance condition of \ocA will be given by an FSO-formula
with a free Function variable
(intended to be range over infinite plays) rather than a parity condition.
2. (2)
For an HF-closed parity automaton A,
the formula describing the acceptance condition of \ocA
is then transformed in §9.2 to a FSO[<Ėā]Ļ formula
relativized to infinite rooted tree paths
(see §7).
This construction relies,
via PropositionĀ 78,
on
PropositionĀ 75
(i.e. PropositionĀ 20)
which requires the manipulation of closed (and in particular HF-closed)
objects.
3. (3)
Using the tools of §7,
and relying on McNaughtonās TheoremĀ [McN66]
(see also e.g.Ā [Tho97, PP04]),
in §9.3
we will then turn \ocA into an equivalent non-deterministic
parity automaton ND(A),
in the sense of DefinitionĀ 47.
\opt
draftnotes
In this Section, it is convenient
to work with the following games.
{defi}
Given an automaton A:Ī£, we let G(A) be the game with
[TABLE]
and with transitions defined by
HF-Bounded Choice for Product Types (TheoremĀ 22)
and Comprehension for HF-Sets (RemarkĀ 3.7.3) as
[TABLE]
As for winning,
we will consider the game G(A) as being equipped
with the winning condition Ī©Aā in the sense of §5.4.
Note that for F:Ī£, the acceptance game G(A,F)
is a subgame of G(A) in the sense of Def.Ā 31.
Remark 98**.**
Note that if Aut(A) then Σ is non-empty,
so we indeed have Game(G(A)).
For each F:Ī£,
the acceptance game
G(A,F) is a subgame of G(A)
(in the sense of Def.Ā 31).
In particular infinite plays in G(A,F) are infinite plays in G(A).
Moreover, it is easy to see that (winning) strategies on G(A,F)
are (winning) strategies on G(A).
Furthermore, note that the game G(A)(ā“) induced by RemarkĀ 31
from DefinitionĀ 9
is precisely the game G(A)(ā“) ofĀ (12).
It follows that in the case of a parity automaton A,
we unambiguously extend the notation of DefinitionĀ 47
and write
Par(A,C^Aā,nAā,U)
or
Par(A,U)
for the formula
Par(G(A)(ā“),C^Aā,nAā,U).
9.1. The Construction of \ocA.
Consider an alternating parity automaton A,
in the sense of DefinitionĀ 47.
So we have
A=(QAā,qAιā,āAā,CAā,nAā)
where
[TABLE]
We define the state set and the initial state of \ocA as:
[TABLE]
The transition function of \ocA is defined as follows,
using RemarkĀ 49.
For aāĪ£ and SāQ\ocAā
we let \ocγāā\ocAā(S,a)
if and only if there is some HF-set
[TABLE]
such that
\ocγ={(d,Sdā²ā)\leavevmodeĀ ā£\leavevmodeĀ dāDā§Sdā²āī =ā
},
where
[TABLE]
and where Ļ2ā
is a projection HF-Function of §3.4.4.6.
Remark 99**.**
We indeed have
[TABLE]
since for SāQ\ocAā=Pāā(QAāĆQAā),
by
HF-Bounded Choice for HF-Sets
(§3.4.5)
there is always some fāPāā(DĆQAā)Ļ2ā(S)
with āqāĻ2ā(S)(f(q)āāAā(q,a)),
and moreover such that
Sdā²ā is non-empty for at least one dāD.
Note our unusual choice of taking non-empty sets as states of \ocA.
It would have been more natural to allow the empty set as a state,
in particular because it would have allowed us to strengthen
CorollaryĀ 55 to an āexists uniqueā statement.
This could also have worked in our setting where games are assumed to
have no dead ends, and in which transitions of alternating automata
range over non-empty sets of non-empty subsets of DĆQAā.
However, the empty state would have appeared in the transitions of
\ocA only in case there is some tree direction dāD
which is not available to O at some stage.
Since the empty state of \ocA
would have been unconditionally winning for P,
this would have lead to an additional case to handle in
the proof of completeness of \ocA
(PropositionĀ 101 below).
So far we have defined for \ocA a state set (with an initial state)
and a transition function.
As explained above, we will not directly equip it with a parity condition.
Instead, we will define its acceptance condition via an FSO-formula
W\ocAā,
in the sense of DefinitionĀ 6.1.
Consider first V:G(\ocA)to2
and T:G(A)to2.
We say that T is a trace in V if the following
formula Trace(T,V) holds,
[TABLE]
where we use the following formula:
[TABLE]
The formula W\ocAā(V) is defined to be:
[TABLE]
Recall our notation Par(A,C^Aā,nAā,ā)
from RemarkĀ 98.
Note that W\ocAā
requires no condition
w.r.t. the transitions of G(A).
We are now going to show that \ocA has the same language asĀ A.
Theorem 100**.**
Fix a parity automaton A:Ī£ and consider the automaton
\ocA:Ī£ as defined above.
Then FSODā proves that for all F:Ī£,
\ocA accepts F if and only if A accepts F.
The proof of TheoremĀ 100
is split into PropositionsĀ 101 andĀ 102 below.
{conv}
In PropositionsĀ 101 andĀ 102,
for fixed automata A and \ocA,
we let
[TABLE]
Proposition 101**.**
Fix a parity automaton A:Ī£ and consider the automaton
\ocA:Ī£ as defined above.
Then FSODā proves that for all F:Ī£,
if A accepts F then \ocA accepts F.
Proof 9.2**.**
Let Ļ be a winning P-strategy in G(A,F).
We define a winning P-strategy Ļ in G(\ocA,F).
Note that
[TABLE]
First, given a P-position (x,S) in G(\ocA,F),
we define a conjunction
[TABLE]
as follows.
Definition of γ(x,S)ā.
For each qāĻ2ā(S), Ļ(x,q)
gives some γqāāāAā(q,F(x)).
HF-Bounded HF-Choice (§3.4.5)
then gives
[TABLE]
By HF-Comprehension (RemarkĀ 3.7.3), we then let γ(x,S)ā
be {(d,Sdā²ā)\leavevmodeĀ ā£\leavevmodeĀ dāDā§Sdā²āī =ā
}
where each Sdā²ā is defined as inĀ (20).
We now define the P-strategy Ļ on G(\ocA,F).
By HF-Bounded Choice for Functions (§3.4.5),
we let
[TABLE]
We have StratPā(G(\ocA,F),Ļ) directly by definition of
ā\ocAā.
It remains to check that Ļ is winning in G(\ocA,F).
Consider an infinite play of Ļ, that is some
V:G(\ocA)to2
such that
Play(Ļ,ι\ocā,V).
Since Ļ is winning in G(A,F),
by definition of W\ocAā
and by RemarksĀ 48 andĀ 98,
we are done if we show that:
[TABLE]
Assume Trace(T,V).
By HF-Comprehension for Product Types,
we let U:G(A)to2
be such that UPā=TPā
and such that
UOā consists of the {(x,Ļ(x,q))} for (x,q)āUPā.
Note that we actually have U:Ļto2.
It remains to check that
[TABLE]
We apply LemmaĀ 39,
whence it remains to show:
[TABLE]
Note that Path(G(A),ι,T) since Trace(T,V).
Proof 9.3** (Proof ofĀ (21)).**
We obviously have
ιāUPā=TPā.
Also, given uāU,
if uāUPā=TPā then ιā“G(A)āu,
and if uāUOā, then vā¶Ļāu for some
vāUPā=TPā, so that
ιā“G(A)āvā²G(A)āu.
Moreover, for each uāUPā, we have
uā¶Ļāv for some vāUOā,
and we get sG(A)ā²ā(u,v) by PropositionĀ 33.
It remains to show that U is linearly ordered w.r.t. ā“G(A)ā.
For UPā this follows from the same property for TPā.
Now let uāUPā and vā²āUOā.
Hence vā² is of the form (x,Ļ(x,q)) with v:=(x,q)āUPā=TPā.
If uā“G(A)āv then
uā²G(A)āvā² and we are done.
Otherwise, vā²G(A)āu.
But by definition of ā“G(A)ā, this implies u=(y,qā²)
with x<Ėāy, so that vā²ā²G(A)āu.
Consider now uā²,vā²āUOā
and let u,vāUPā be their immediate predecessors.
If uā²G(A)āv then uā²ā²G(A)āvā² and we are done.
Otherwise, without loss of generality we have that u=v.
But then uā²=vā² by definition of U.
Proof 9.4** (Proof ofĀ (22)).**
Assume first uāUPā.
In this case,
u is of the form (x,q) with (x,q)āTPā,
and uā² is of the form (x,Ļ(x,qā²))
with (x,qā²)āTPā.
But T is linearly ordered w.r.t. ā“G(A)ā,
so that q=qā².
It follows that uā¶Ļāuā².
Assume now that uāUOā.
In this case,
u is of the form (x,(q,γAā)) with (x,q)āUPā=TPā
and (q,γAā)=Ļ(x,q).
Moreover, uā²āUPā=TPā is of the form
(Sdā(x),qā²).
We thus get uā¶Ļāuā² as soon as
[TABLE]
Since Trace(T,V)
and since V is a play of Ļ,
there are unique S,Sā²
with (x,S),(Sdā(x),Sā²)āVPā
and such that
qāĻ2ā(S) and qā²āĻ2ā(Sā²).
Moreover, we necessarily have
(d,Sā²)āγ(x,S)ā
for (S,γ(x,S)ā)=Ļ(x,S).
But Trace(T,V) implies (q,qā²)āSā²,
and it follows
that (d,qā²)āγAā
by definition of γ(x,S)ā.
*This concludes the proof of PropositionĀ 101.
*
Proposition 102**.**
Fix a parity automaton A:Ī£ and consider the automaton
\ocA:Ī£ as defined above.
Then FSODā proves that for all F:Ī£,
if \ocA accepts F then A accepts F.
Proof 9.5**.**
Let Ļ be a winning P-strategy in G(\ocA,F).
We will define a winning P-strategy Ļ in G(A,F).
To this end, we invoke CorollaryĀ 55,
which tells us that since \ocA is non-deterministic,
for each xāDā there is at most one SāQ\ocAā
such that (x,S) belongs to an infinite play of Ļ.
Moreover,
using RemarkĀ 12,
for each SāQ\ocAā
we fix a well-order āŖÆ on Pāā(DĆQAā)Ļ2ā(S).
We now define the strategy Ļ.
Definition of Ļ.
We apply HF-Bounded Choice for Product Types (TheoremĀ 22).
Consider (x,q)āG(A,F)Pā.
We first assign to (x,q) an SāQ\ocAā such that qāĻ2ā(S).
If there exists such an S where furthermore (x,S)
belongs to an infinite play of Ļ, then this S is unique
and we choose that one.
Otherwise,
by Comprehension for HF-Sets (RemarkĀ 3.7.3),
we define an ad hoc SāQ\ocAā with qāĻ2ā(S).
Let now (S,γ(x,S)ā):=Ļ(x,S).
By definition of γ(x,S)ā
there is some
[TABLE]
such that
γ(x,S)ā={(d,Sdā²ā)\leavevmodeĀ ā£\leavevmodeĀ dāDā§Sdā²āī =ā
}
where each Sdā²ā is as inĀ (20).
Consider the āŗ-least such f.
We let
[TABLE]
It remains to show that Ļ is winning.
To this end, given an infinite play T of Ļ,
we will define an infinite play V of Ļ such that:
[TABLE]
Since Ļ is assumed to be winning,
thanks to
RemarksĀ 48 andĀ 98,
this will imply that Ļ
is also winning.
Assume Play(Ļ,ι,T).
We define V using the Recursion Theorem (PropositionĀ 26).
Let Ļ(V,v) be a FSO-formula stating that:
either v=ι\ocā,
or v=(x,Ļ(x,S)) with (x,S)āV,
or v=(Sdā(x),Sdā²ā) and
for some qā²āQAā we have (Sdā(x),qā²)āT,
and for some SāQ\ocAā, we have
(x,S)āV and Ļ(x,S)=(S,γ(x,S)ā) with (d,Sdā²ā)āγ(x,S)ā.
Note that Ļ(V,v) indeed satisfies the assumptions of the
Recursion Theorem (PropositionĀ 26), since
in the second clause we always have (x,S)ā²G(\ocA)ā(x,Ļ(x,S)),
and Ļ(x,S) is uniquely determined from (x,S);
in the last clause,
we always have (x,S)ā²G(\ocA)ā(Sdā(x),Sdā²ā).
Note also that since T is a play of Ļ, there is at most one dāD
such that (Sdā(x),q)āT for some qāQAā,
and Sdā²ā is uniquely determined from d and Ļ(x,S)
by construction of \ocA.
So by the Recursion Theorem (PropositionĀ 26) we indeed let
V:G(\ocA)to2 be unique such that
[TABLE]
We begin with a series of easy claims on V.
Claim 103**.**
For every xāDā, there is at most one SāQ\ocAā
such that (x,S)āV.
Proof 9.6** (Proof of ClaimĀ 103).**
We apply the Induction Axiom of FSO (§3.4.2).
The property holds for εĖ, since (εĖ,S)āV
implies S=q\ocAιā by definition of V.
Now assume the property for x and let us show it for Sdā(x).
So assume (Sdā(x),Sdā²ā),(Sdā(x),S~dā²ā)āV.
By definition of V, there are (x,S),(x,S~)āV
such that (d,Sdā²ā)āγ(x,S)ā
and (d,S~dā²ā)āγ(x,S~)ā
where
(S,γ(x,S)ā)=Ļ(x,S)
and
(S~,γ(x,S~)ā)=Ļ(x,S~).
But by induction hypothesis we get S=S~,
which implies γ(x,S)ā=γ(x,S~)ā.
This in turn implies Sdā²ā=S~dā²ā by construction of \ocA.
Claim 104**.**
For every uāV, the set {vāV\leavevmodeĀ ā£\leavevmodeĀ vā“G(\ocA)āu}
is linearly ordered w.r.t. ā¶Ļāā.
Proof 9.7** (Proof of ClaimĀ 104).**
We reason by ā²-Induction (TheoremĀ 25).
So let uāV be such that the property holds for all wā²G(\ocA)āu.
Assume first that uāVOā.
In this case, we must have u=(x,Ļ(x,S)) with (x,S)āV.
By induction hypothesis, the set
{vāV\leavevmodeĀ ā£\leavevmodeĀ vā“G(\ocA)ā(x,S)}
is linearly ordered w.r.t. ā¶Ļāā.
On the other hand, it follows from ClaimĀ 103
that (x,S) is the only immediate ā¶Ļā-predecessor of u in V.
Since (x,S)ā¶Ļāu,
we get the result by PropositionĀ 33.
Assume now that uāVPā.
If u=ι\ocā then the result is trivial.
Otherwise, u is of the form (Sdā(x),Sdā²ā)
and its membership to V is given by the last clause defining V.
Let S be such that (x,S)āV and such that
Ļ(x,S)=(S,γ(x,S)ā) with (d,Sdā²ā)āγ(x,S)ā.
Since (x,Ļ(x,S))ā¶Ļāu with (x,Ļ(x,S))āV,
by induction hypothesis
the set
{v\leavevmodeĀ ā£\leavevmodeĀ vā“G(\ocA)ā(x,Ļ(x,S))}
is linearly ordered w.r.t. ā¶Ļāā.
In order to obtain the result for
{v\leavevmodeĀ ā£\leavevmodeĀ vā“G(\ocA)ā(Sdā(x),Sdā²ā)}
we need to show that (x,Ļ(x,S)) is the unique
immediate ā¶Ļā-predecessor of (Sdā(x),Sdā²ā) in V.
But if (x,Ļ(x,S~))āV
then we should have (x,S~)āV,
so that S~=S by ClaimĀ 103.
Claim 105**.**
For every uāV, there is an infinite play U of Ļ
such that:
[TABLE]
Proof 9.8** (Proof of ClaimĀ 105).**
Let uāV.
First, by LemmaĀ 38
there is an infinite play U0ā in the game G(\ocA)ā¾{Ļ}
such that uāU0ā
and uā¶Ļāāv for all vāU0ā.
By Comprehension for Product Types (TheoremĀ 23)
we let
[TABLE]
We then get Play(Ļ,ι\ocā,U)
from ClaimĀ 104
and Play(Ļ,u,U0ā).
Claim 106**.**
Let (x,S)āV, and assume (x,q),(Sdā(x),qā²)āT
with qāĻ2ā(S).
Then there is some Sdā²āāQ\ocAā such that (Sdā(x),Sdā²ā)āV
and (q,qā²)āSdā²ā.
Moreover, we have (d,Sdā²ā)āγ(x,S)ā for (S,γ(x,S)ā)=Ļ(x,S).
Proof 9.9** (Proof of Claim 106).**
Since T is a play of Ļ, we have (d,qā²)āγ
for (q,γ)=Ļ(x,q).
Moreover, by ClaimĀ 105,
(x,S) belongs to an infinite play of Ļ.
Since qāĻ2ā(S), by definition of Ļ
this implies that there is some Sdā²ā such that
(d,Sdā²ā)āγ(x,S)ā for (S,γ(x,S)ā)=Ļ(x,S)
and (q,qā²)āSdā²ā.
We then obtain (Sdā(x),Sdā²ā)āV by definition of V.
We now proceed to show:
[TABLE]
We begin with Trace(T,V).
First, we have
Path(G(A),ι,T)
since T is a play of Ļ.
Moreover
Claim 107**.**
[TABLE]
Proof 9.10** (Proof of Claim 107).**
Using the Induction Axiom of FSO
(§3.4.2), we show
[TABLE]
*For the base case x=εĖ, if (x,q)āT then we must have
q=qAιā, so qāĻ2ā(q\ocAιā).
Assume now the property for x, and consider Sdā(x) and q,qā²āQAā
such that (x,q)āT and (Sdā(x),qā²)āT.
Furthermore, by induction hypothesis, let SāQ\ocAā
such that (x,S)āV and qāĻ2ā(S).
By ClaimĀ 106,
we then get (Sdā(x),Sdā²ā)āV for some Sdā²āāQ\ocAā
with qā²āĻ2ā(Sdā²ā).
*
We can now show the last required property for Trace(T,V),
namely:
Claim 108**.**
[TABLE]
Proof 9.11** (Proof of Claim 108).**
*Let (x,q),(y,qā²)āT
and Sā²āQ\ocAā
such that
(x,q)ā²G(A)P;Oā(y,qā²)
and
(y,Sā²)āV.
Then by definition of ā²G(A)ā we must have y=Sdā(x)
for some dāD.
Moreover, by ClaimĀ 107
there is some SāQ\ocAā such that (x,S)āV
and qāĻ2ā(S).
By ClaimĀ 106,
we then have (Sdā(x),Sdā²ā)āV for some Sdā²āāQ\ocAā
with (q,qā²)āSdā²ā.
It follows from ClaimĀ 103
that Sā²=Sdā²ā
so that (q,qā²)āSā²
and we are done.
*
We now turn to showing
Play(Ļ,ι\ocā,V).
Since ι\ocāāV,
thanks to PropositionĀ 35
it remains to show:
[TABLE]
First, we easily have:
Claim 109**.**
[TABLE]
Proof 9.12** (Proof of Claim 109).**
The result follows from ClaimĀ 105,
but it can be proved directly,
without the inductions underlying ClaimĀ 105.
Indeed, if v=(x,Ļ(x,S)), with (x,S)āV, then the result
directly follows from the definitions of V and of
the game G(\ocA)ā¾{Ļ}.
Otherwise, we have v=(Sdā(x),Sdā²ā),
and there is (x,S)āV such that
Ļ(x,S)=(S,γ(x,S)ā) with (d,Sdā²ā)āγ(x,S)ā.
But (x,S)āV implies
(x,Ļ(x,S))āV, and again the result
directly follows from the definition of G(\ocA)ā¾{Ļ}.
It then easily follows that:
Claim 110**.**
[TABLE]
Proof 9.13** (Proof of Claim 110).**
First, we have ι\ocāāV by definition
of V.
Moreover, given uāV
we have either ι\ocāā¶Ļāāu
or uā¶Ļāāι\ocā
by ClaimĀ 104.
The result then follows from
PropositionĀ 33.
It remains to show:
[TABLE]
To this end, we first show:
Claim 111**.**
[TABLE]
Proof 9.14** (Proof of Claim 111).**
Using the Induction Axiom of FSO
(§3.4.2), we show
[TABLE]
For the base case x=εĖ, if (x,S)āV then we must have
S=q\ocAιā.
Then we are done since ιāT
and qAιāāĻ2ā(S).
Assume the property for x, and consider Sdā(x) and S,Sā²āQ\ocAā
such that (x,S),(Sdā(x),Sā²)āV.
Furthermore, by induction hypothesis, let qāQAā
such that (x,q)āT and qāĻ2ā(S).
By definition of V, we have (Sdā(x),qā²)āT for some qā²āQAā.
It then follows from ClaimĀ 106
that qā²āĻ2ā(Sdā²ā) for some Sdā²āāQ\ocAā
such that (Sdā(x),Sdā²ā)āV.
But ClaimĀ 103
implies Sā²=Sdā²ā
so that qā²āĻ2ā(Sā²)
and we are done.
We can now proveĀ (23).
Proof 9.15** (Proof ofĀ (23)).**
If u=(x,S)āV, then v=(x,Ļ(x,S))āV and is unique such that
uā¶Ļāv.
Otherwise, u=(x,Ļ(x,S)) for some (x,S)āV,
and we have to show that there are some unique
dāD and Sdā²āāQ\ocAā such that
(Sdā(x),Sdā²ā)āV.
First, by ClimĀ 111
there is some qāQAā such that (x,q)āT
and qāĻ2ā(S).
Moreover, since T is a play of Ļ, with have (Sdā(x),qā²)āT
for some unique dāD and qā²āQAā.
It then follows from ClaimĀ 106
that there is some Sdā²āāQ\ocAā
such that (Sdā(x),Sdā²ā)āV
and uā¶Ļā(Sdā(x),Sdā²ā).
The uniqueness of Sdā²ā follows from
ClaimĀ 103.
This concludes the proof of PropositionĀ 102.
In the proof of
PropositionĀ 102 above,
we have used ClaimĀ 111
in order to show that V is a play of Ļ.
Let us state here for the record that this has a more general converse:
ClaimĀ 111
holds whenever T is a trace in V for V a play
in G(\ocA):
Lemma 112**.**
Given V:G(\ocA)to2 and T:G(A)to2,
in FSODā we have
[TABLE]
whenever
[TABLE]
Proof 9.16**.**
Using the Induction Axiom of FSO
(§3.4.2), we show
[TABLE]
For the base case x=εĖ, if (x,S)āV,
since
Play(G(\ocA),(εĖ,q\ocAιā),V)
we must have
S=q\ocAιā, so qAιāāĻ2ā(S).
Assume now the property for x, and consider
dāD and S,Sā²āQ\ocAā
such that (x,S)āV and (Sdā(x),Sā²)āV.
Furthermore, by induction hypothesis, let qāQAā
such that (x,q)āT and qāĻ2ā(S).
It follows from Path(G(A),(εĖ,qAιā),T)
that (Sdā²ā(x),qā²)āT for some dā²āD
and some qā²āQAā.
Moreover, Trace(T,V) implies
qā²āĻ2ā(Sā²ā²) for some Sā²ā² such that
(Sdā²ā(x),Sā²ā²)āV.
But
Play(G(\ocA),(εĖ,q\ocAιā),V)
implies dā²=d and Sā²ā²=Sā² and we are done.
9.2. Reformulating the Acceptance Condition of \ocA.
For an automaton A which we now assume to be HF-closed
(in the sense of DefinitionĀ 6.1),
we are going to formulate the FSO-formula W\ocAā
as a parity condition, which will allow us to obtain a parity automaton ND(A)
in §9.3.
In order to obtain a parity condition from W\ocAā we note
(followingĀ [Wal02]) that (when read in the standard model) it defines
an Ļ-regular condition, which can thus
by McNaughtonās TheoremĀ [McN66]
(see also e.g.Ā [Tho97, PP04])
be formulated with a deterministic parity automaton on Ļ-words.
We are actually not going to formalize McNaughtonās Theorem in our setting.
Rather, we will apply PropositionĀ 78,
which allows us to import in FSO any true FSO-formula on the infinite
paths of Dā.
Our way to the application of
PropositionĀ 78
proceeds with constructions similar to some of those in the proof of
TheoremĀ 93.
Consider some V:G(\ocA)to2
such that:
[TABLE]
By Comprehension for Product Types (TheoremĀ 23),
let ā£Vā£:Dāto2
be the set of all xāDā such that
(x,S)āV for some SāQ\ocAā.
Note that TPath(ā£Vā£)
(recall that TPath is defined inĀ (16)).
Furthermore, by HF-Bounded Choice for Functions (§3.4.5),
let V~:ā£Vā£toQ\ocAā
take xāā£V⣠to the unique SāQ\ocAā
such that (x,S)āV.
In FSO we have that W\ocAā
is equivalent to the following formula
W[<Ėā]\ocAā£Vā£ā(V~):
[TABLE]
where
the formula
Trace[<Ėā]ā£Vā£(T~,V~)
is
[TABLE]
with
[TABLE]
and, for C:QAāto[0,n],
the formula
Par[<Ėā]ā£Vā£(C,n,T~)
is (using ConventionĀ 5.5):
[TABLE]
Let us first note the following simple property.
Recall from DefinitionĀ 47
that CAā:QAāto[0,nAā]
is a coloring of the states of A,
while C^Aā colors the positions of G(A),
by taking for P-positions (x,q)
the color given by CAā to q and for O-positions the maximal color
nAā.
Lemma 113**.**
Assume given V and ā£V⣠as above.
Let T:G(A)to2
and T~:ā£Vā£toQAā
such that
[TABLE]
Then:
[TABLE]
Lemma 114**.**
Given
V, ā£V⣠and V~ as above,
FSODā proves that
[TABLE]
Proof 9.17**.**
Recall that the formula W\ocAā
requires no condition
w.r.t. the transitions of G(A).
We proceed as follows:
Assume first W\ocAā(V), and let
T~:ā£Vā£toQAā such that
Trace[<Ėā]ā£Vā£(T~,V~).
Using RemarkĀ 12,
let āŗ be a well-order on Pāā(DĆQAā).
By Comprehension for Product Types
(TheoremĀ 23),
let T:G(A)to2
such that
for all (x,q)āG(A)Pā, we have
[TABLE]
and such that (x,γ)āTOā iff
γāPāā(DĆQAā) is āŖÆ-minimal
such that T~(Sdā(x))=q for some (d,q)āγ.
Since
V is an infinite play of G(\ocA) from
(εĖ,q\ocAιā),
we may conclude by LemmaĀ 113
as soon as we show:
[TABLE]
We obviously have Path(G(A),T)
as well as (εĖ,qAιā)ā“G(A)āu
for all uāT.
Moreover we have:
[TABLE]
To see this, let (x,q)āT, so that T~(x)=q.
So by assumption we have qāĻ2ā(V~(x)),
and we are done since (x,V~(x))āV(x).
Finally we have
[TABLE]
To see this,
given (x,q),(y,qā²)āT
such that
(x,q)ā²G(A)P;Oā(y,qā²)
we necessarily have
S<Ėāā(x,y),
so that (q,qā²)āV~(y)
since T~(x)=q and T~(y)=qā².
But then we are done since V~(y) is the unique
SāQ\ocAā such that (y,S)āV.
Conversely, assume
W[<Ėā]\ocAā£Vā£ā(V~)
and let T:G(A)to2
such that Trace(T,V).
Since
V is an infinite play of G(\ocA) from
(εĖ,q\ocAιā),
LemmaĀ 112
implies:
[TABLE]
It follows that for all xāā£V⣠there is qāQAā
such that (x,q)āT, and this defines
T~:ā£Vā£toQAā
by HF-Bounded Choice for Functions (§3.4.5).
Note that we have:
[TABLE]
We can then conclude by LemmaĀ 113
as soon as we show:
[TABLE]
To see this,
first, for all xāā£Vā£, we have (x,T~(x))āT,
so that T(x)āĻ2ā(V~(x)) by definition of V~.
Moreover, given x,yāā£Vā£
with S<Ėāā(x,y),
we have
[TABLE]
*so that (T~(x),T~(y))āV~(y)
since Trace(T,V).
*
This concludes the proof of LemmaĀ 114.
We are now going to show that
W[<Ėā]\ocAā£Vā£ā(V~)
is equivalent in FSO to a parity automaton on Ļ-words.
This relies on McNaughtonās TheoremĀ [McN66]
applied in the usual standard model N of Ļ-words,
and, via PropositionĀ 78, on the completeness of FSO[<Ėā]Ļ.
In order to apply PropositionĀ 78,
we rewrite
W[<Ėā]\ocAā£Vā£ā(V~)
as the relativization to ā£V⣠of the FSO[<Ėā]Ļ-formula
[TABLE]
where
Par[<Ėā](C,n,T~) is the formula of
DefinitionĀ 8.4.2,
and where
[TABLE]
Note that
W[<Ėā]\ocAā£Vā£ā(V~) is the relativization
to ā£V⣠of
W[<Ėā]\ocAā(V~):
[TABLE]
Since A is HF-closed, the formula
W[<Ėā]\ocAā(V~) is also HF-closed,
and we can look at it
in the standard model N of Ļ-words (see §7).
By McNaughtonās TheoremĀ [McN66]
(see also e.g.Ā [Tho97, PP04]),
there is a deterministic parity Ļ-word automaton
D=(QDā,qDιā,āDā,cDā)
over Q\ocAā,
which
accepts V~ exactly when:
[TABLE]
It then follows
that in N,
for all V~:Q\ocAā,
the formula
W[<Ėā]\ocAā(V~)
is equivalent to
[TABLE]
PropositionĀ 78 then implies that FSO
proves that for V~:ā£Vā£toQ\ocAā,
the formula
W[<Ėā]\ocAā£Vā£ā(V~)
is equivalent to
[TABLE]
9.3. Definition of the Parity Automaton ND(A).
Consider an alternating parity tree automaton A:Ī£
as in the beginning of §9,
and assume it to be HF-closed.
Let \ocA:Σ be defined as in §9.1.
Moreover, let D:Q\ocAā be the parity
deterministic Ļ-word automaton
of §9.2.
We then let
[TABLE]
where:
the transition function
[TABLE]
takes ((S,q),a)
to the set of all γāPāā(Pāā(DĆ(Q\ocAāĆQDā)))
such that for some γ\ocAāāā\ocAā(S,a),
[TABLE]
the coloring
CND(A)ā:Q\ocAāĆQDāto[0,nDā]
takes (S,q) to CDā(q).
Note that ND(A):Ī£ is HF-closed by
RemarkĀ 49.
We shall now show that ND(A) is equivalent to A,
thus completing the proof of the Simulation TheoremĀ 97.
The proof is split into
PropositionsĀ 115
andĀ 116.
As expected, we invoke TheoremĀ 100, that FSODā proves the equivalence of !A and A.
{conv}
In PropositionsĀ 115 andĀ 116,
for fixed automata \ocA and ND(A),
we let
[TABLE]
Proposition 115**.**
Fix an HF-closed automaton A:Ī£ and consider
ND(A):Ī£ as defined above.
Then FSODā proves that for all F:Ī£,
if A accepts F then ND(A) accepts F.
Proof 9.18**.**
Thanks to TheoremĀ 100,
we are done if we show
that ND(A) accepts F whenever \ocA acceptsĀ F.
Let Ļ:G(\ocA,F)PātoOG(\ocA,F)ā
be the winning P-strategy in G(\ocA,F).
We define a strategy
Ļ:G(ND(A),F)PātoOG(ND(A),F)ā
as follows.
Definition of Ļ.*
By HF-Bounded Choice for Functions (§3.4.5),
we let Ļ(x,(S,qDā))
be ((S,qDā),γ),
where
γāPāā(Pāā(DĆ(Q\ocAāĆQDā)))
is defined by Comprehension for HF-Sets
(RemarkĀ 3.7.3)
as the set of all (d,(Sdā²ā,āDā(qDā,S)))
such that (d,Sdā²ā)āγ\ocAā,
where Ļ(x,S)=(S,γ\ocAā).*
It remains to show that Ļ is winning.
So let T such that
[TABLE]
By Comprehension for Product Types
(TheoremĀ 23),
let ā£ā£Uā£ā£:DāĆQAāto2
consist of the (x,q\ocAā)
for which there is qDāāQDā
such that (x,(q\ocAā,qDā))āT.
By HF-Bounded Choice for Functions (§3.4.5),
now let U~:ā£ā£Uā£ā£toQDā
take (x,q\ocAā)āā£ā£Uā£ā£ to
(the necessarily unique) qDā such that
(x,(q\ocAā,qDā))āT.
We have:
[TABLE]
It then follows from LemmaĀ 114
that we are done if we show that
ā£ā£Uā£ā£ is the set of all (x,qAā)āVPā
for some V:G(\ocA)to2
such that:
[TABLE]
But this is immediate from Comprehension for Product Types (TheoremĀ 23)
by letting V
be the union of ā£ā£Uā£ā£ with the set of
all (x,Ļ(x,q\ocAā)) for (x,q\ocAā)āā£ā£Uā£ā£.
When proving that
L(ND(A))āL(A)
in PropositionĀ 116 below,
in order to apply
PropositionĀ 102,
we have to extract a P-strategy on G(\ocA,F)
from a P-strategy on G(ND(A),F).
But ND(A) has more states than \ocA,
so we have to resort to CorollaryĀ 55,
stating that in plays of strategies on non-deterministic automata,
states are uniquely determined from tree positions.
Proposition 116**.**
Fix an HF-closed automaton A:Ī£ and consider ND(A):Ī£ as defined above.
Then FSODā proves that for all F:Ī£,
if ND(A) accepts F then A accepts F.
Proof 9.19**.**
Thanks to TheoremĀ 100,
we are done if we show
\ocA accepts F
whenever
ND(A) accepts F.
Let
Ļ:G(ND(A),F)PātoOGā(ND(A),F)
be the winning P-strategy in G(ND(A),F).
We are going to define a winning strategy
Ļ:G(\ocA,F)PātoOGā(\ocA,F)
in G(\ocA,F).
Note that ND(A) has more states than \ocA
and that,
[TABLE]
whereas we need to define:
[TABLE]
As mentioned, we resort to
CorollaryĀ 55.
The strategy Ļ is defined by HF-Bounded Choice for
Functions (§3.4.5) as follows.
Let (x,S)āDāĆQ\ocAā.
Assume that there is a play U of Ļ
such that
[TABLE]
Then it follows from
CorollaryĀ 55
there is a unique qDā such that
[TABLE]
In this case, we let
Ļ(x,S) be (S,γ\ocAā) where,
by Comprehension for HF-Sets (RemarkĀ 3.7.3),
γ\ocAā is the set of all (d,Sdā²ā)
such that there is some qDā²āāQDā
with (d,(Sdā²ā,qDā²ā))āγND(A)ā
for ((S,qDā),γND(A)ā)=Ļ(x,(S,qDā)).
Otherwise, we let Ļ(x,S)
be (S,γ\ocAā) where,
by Comprehension for HF-Sets (RemarkĀ 3.7.3),
γ\ocAā is the set of all (d,Sdā²ā)
such that there is some qDāāQDā
with (d,(Sdā²ā,qDā))āγND(A)ā
for ((S,qDιā),γND(A)ā)=Ļ(x,(S,qDιā)).
We are now going to show that Ļ is winning.
To this end, consider an infinite play of Ļ, that is some
V:G(\ocA)to2
such that
[TABLE]
We are going to define an infinite play of Ļ, that is some
U:G(ND(A))to2
with
[TABLE]
First, note that we are done if U satisfies the following property:
[TABLE]
Indeed, by Comprehension (TheoremĀ 23),
let ā£Vā£:Dāto2
be the set of all xāDā such that
(x,S)āV for some (necessarily unique) SāQ\ocAā.
Moreover,
by HF-Bounded Choice for Functions (§3.4.5),
let V~:ā£Vā£toQ\ocAā
take xāā£V⣠to the unique SāQ\ocAā
such that (x,S)āV.
By HF-Bounded Choice for Functions (§3.4.5),
let now U~:ā£Vā£toQDā
take xāā£V⣠to the unique qDāāQDā
such that (x,(V~(x),qDā))āU.
Since
Par(G(ND(A)),C^ND(A)ā,nND(A)ā,U),
we have
Par[<Ėā]ā£Vā£(CDā,nDā,U~),
so that
W[<Ėā]\ocAā£Vā£ā(V~)
and we conclude by LemmaĀ 114.
We now define an infinite play U of Ļ
satisfyingĀ (24),
for which we appeal to the
Recursion Theorem (PropositionĀ 26).
Let Ļ(U,u) be a FSO formula
stating the disjunction of the following:
u=ιNDā; or
u=(x,Ļ(x,(S,qDā)))* with
(x,(S,qDā))āU; or*
u=(Sdā(x),(Sdā²ā,qDā²ā)),
where
(Sdā(x),Sdā²ā)āV, and
for some qDāāQDā
and some SāQ\ocAā such that
(x,S)āV and (x,(S,qDā))āU,
we have
qDā²ā=āDā(qDā,S).
By the Recursion Theorem (PropositionĀ 26) we let
U:G(ND(A))to2 be unique such that:
[TABLE]
We need to showĀ (24)
and:
[TABLE]
We first show
that U is a play of Ļ.
Since ιNDāāU,
by PropositionĀ 35
it suffices to show:
[TABLE]
We proceed similarly to the proof of
PropositionĀ 102.
First, we prove:
Claim 117**.**
[TABLE]
Proof 9.20** (Proof of Claim 117).**
The result directly follows from the definition of Ļ
and the definition of
G(ND(A))ā¾{Ļ} (DefinitionĀ 5.3).
If v=(x,Ļ(x,(S,qDā))), with (x,(S,qDā))āU, then the result
is trivial.
Otherwise, we have v=(Sdā(x),(Sdā²ā,qDā²ā)),
and there is (x,(S,qDā))āU such that
(x,S)āV and qDā²ā=āDā(qDā,S).
Note that (x,(S,qDā))āU implies
(x,Ļ(x,(S,qDā)))āU,
and similarly, that (x,S)āV implies (s,Ļ(x,S))āV.
By definition of Ļ, we have Ļ(x,S)=(S,γ\ocAā)
where γ\ocAā is the set of all (d~,Sd~ā²ā)
such that (d~,(Sd~ā²ā,qDā²ā))āγND(A)ā,
where
((S,qDā),γND(A)ā)=Ļ(x,(S,qDā)).
But then we are done since we indeed have:
[TABLE]
Now we prove:
Claim 118**.**
[TABLE]
Proof 9.21** (Proof of Claim 118).**
We proceed by ā²-Induction
(TheoremĀ 25).
So let uāU s.t.
ιNDāā¶Ļāāv
for all vā²u with vāU.
The result is trivial if u=ιNDā.
Otherwise, by ClaimĀ 117,
there is vāU such that vā¶Ļāu.
But vā²u by PropositionĀ 33,
so we have
ιNDāā¶Ļāāv
by induction hypothesis and we conclude by PropositionĀ 33,
again.
It remains to show
[TABLE]
We first prove:
Claim 119**.**
[TABLE]
Proof 9.22** (Proof of Claim 119).**
The property follows from a case analysis according
to the following usual consequence of Induction
(see Proposition 6, §3.4.3):
[TABLE]
In the case of xāεĖ, if (x,(S,qDā))āU then we must have
S=q\ocAιā, so that (x,S)āV.
Consider now the case of xāSdā(y).
If u=(x,(S,qDā))āU, then it follows from
Ļ(U,u) that we have (x,S)āV and we are done.
We can now proveĀ (24).
Proof 9.23** (Proof ofĀ (24)).**
If u=(x,(S,qDā)), then (x,Ļ(x,(S,qDā)))
is the unique successor of u in U.
Assume u=(x,Ļ(x,(S,qDā))).
It then follows from ClaimĀ 117
that (x,(S,qDā))āU,
and by ClaimĀ 119
we also get (x,S)āV.
Since (x,S)āV, we have (Sdā(x),Sdā²ā)āV
for some unique dāD and Sdā²āāQ\ocAā.
It follows from Ļ(U,u)
that v=(Sdā(x),(Sdā²ā,qDā²ā))āU,
where qDā²ā=āDā(qDā,S).
It remains to show that v is unique such :
[TABLE]
Uniqueness follows from Ļ(U,u) and the fact that V is a play,
so it remains to show
uā¶Ļāv.
Note that (x,(S,qDā))āU implies
(x,Ļ(x,(S,qDā)))āU,
and similarly, that (x,S)āV implies (s,Ļ(x,S))āV.
By definition of Ļ, we have Ļ(x,S)=(S,γ\ocAā)
where γ\ocAā is the set of all (d~,Sd~ā²ā)
such that (d~,(Sd~ā²ā,qDā²ā))āγND(A)ā,
where
((S,qDā),γND(A)ā)=Ļ(x,(S,qDā)).
This finishes the proof since we indeed have:
[TABLE]
Finally, we proveĀ (24),
that is:
[TABLE]
Proof 9.24** (Proof ofĀ (24)).**
Using the Induction Axiom of FSO
(§3.4.2), we show
[TABLE]
For the base case xāεĖ,
if (x,S)āV then we must have S=q\ocAιā,
and we indeed obtain (x,(S,qDιā))āU.
Assume now the property for x, and consider some dāD
and Sdā²ā such that (Sdā(x),Sdā²ā)āV.
Since V is a play, it follows from
the Predecessor LemmaĀ 37 for Infinite Plays
(applied twice)
that (x,S)āV for some SāQ\ocAā.
It follows by induction hypothesis that (x,(S,qDā))āU
for some qāQDā.
But now, taking qDā²ā=āDā(qDā,S),
we have
(Sdā(x),(Sdā²ā,qDā²ā))āU and we are done.
This concludes the proof of PropositionĀ 116.
10. Conclusion
In this paper, we proposed for each non-empty (hereditarily) finite
set D the theory FSODā of
Functional (Monadic) Second-Order Logic
on the full (infinite) D-ary tree.
The theory FSODā (henceforth FSO) is
a uniform extension of MSO on the full D-ary tree
with hereditarily finite sets.
We formalized in FSO a basic theory of (alternating) tree automata
and (acceptance) games.
This allowed us, in the theory of FSO
augmented with an axiom (PosDet) of positional determinacy of parity games,
to formalize a translation of MSO-formulae to automata
adapted fromĀ [Wal02].
We then deduced the completeness of FSO+(PosDet)
thanks to a variant of the Büchi-Landweber Theorem [BL69],
stating that MSO decides winning for (definable) games of finite graphs
(and obtained thanks to the completeness of MSO over
Ļ-wordsĀ [Sie70]).
By naive proof enumeration, this gives a proof
of Rabinās Tree TheoremĀ [Rab69],
the decidability of MSO on infinite trees.
Moreover, since the formal theory FSO is conservative
(w.r.t. the faithful translation (ā)ā:MSOāFSO)
over a natural set of axioms for MSO,
we also get a complete axiomatization of MSO on infinite trees, namely MSODā+āØPosDetā© (cf.Ā DefinitionĀ 5.6.1, §5.6.1).
10.1. Proof theoretic strength of complementation
The present paper does not discuss proof theoretic strength.
In the context of second-order arithmetic
(in the sense ofĀ [Sim10]), it is known that
complementation of tree automata is between Ī 31ā and
Ī31ā-comprehensionĀ [KM16].
As far as only games are concerned
(as opposed to proving the correctness of
an internal function for complementation), only Ī 21ā-comprehension
is required for the positional determinacy of (each level of)
parity gamesĀ [KM15, Lemma 4.6].
10.2. Clarifying the status of āØPosDetā©
A problem arising from this work is whether the axiom schema āØPosDetā© is indeed independent of MSO. The latter may be seen as the monadic fragment of PA2 (over the appropriate language) and, as we have mentioned, is complete when restricted to infinite words.
While it might therefore be natural to suspect that MSO is already complete without āØPosDetā©, we point out that the axiomatization of Weak MSO
over infinite trees given inĀ [Sie78] also augments the natural fragment of Peano arithmetic by an axiom of induction over finite trees.
As we mentioned in the Introduction, the completeness of MSODā was erroneously claimed in the preliminary version of this work [DR15].
10.3. On the notion of proof for MSO
One outcome of this work is that our complete deduction
system for MSO
gives a new decision algorithm.
Of course, the naive decision algorithm by proof enumeration is
not very sophisticated,
and it is worth
restating that its correctness is itself driven by the usual automata-theoretic argument.
Such an algorithm, nonetheless, makes no mention of automata and so can be
adapted and improved purely in the setting of proof theory.
In this sense, the algorithm is the first of its kind:
a decision procedure for MSO on infinite trees that remains internal to the language, rather than requiring intermediate translations to automata.
A basic motivation for such algorithms
is that, even if Rabinās Tree Theorem proves the existence
of decision procedures for MSO on infinite trees, there is
(as far as we know) no working implementation of such procedures.333To our knowledge, the Mona tool
(https://www.brics.dk/mona/) only handles Weak MSO.
Our axiomatization instead allows the targeting of
(semi) automatic approaches, for instance based on proof assistants.
As we mentioned in the Introduction, our axiomatization is polynomial-time recognizable and so indeed yields a meaningful notion of āproof certificateā: a proof of a theorem may be easily checked, without having to reprove the theorem again.
10.4. Constructive systems and proof interpretations.
A further direction of research is to look for constructive interpretations of MSO.
In the case of Ļ-words, preliminary steps were made
inĀ [PR19].
The general idea is to proceed along the following steps:
- (1)
Determine the relevant computational information one should be able to extract
from constructive proofs.
2. (2)
Devise constructive variants of MSO
(together with suitable proof interpretations),
which are correct and complete
for the chosen class of functions
w.r.t. to their provable āā-sentences.
A realizability model for MSO has been proposed inĀ [Rib20],
in which the underlying logic is not only constructive but also
linear (in the sense ofĀ [Gir87]).
Of course, similar approaches may also be considered in more
traditional settings for constructive interpretations of
proofsĀ [TvD88, Koh08].