{'fraction_non_alphanumeric': 0.06435710793633549, 'fraction_numerical': 0.009587701667662556, 'mean_word_length': 3.6441094853683147, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 52, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Complete Axiomatizations of Fragments of Monadic Second-Order Logic on Finite Trees

We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., each formula that is valid on all finite trees is provable using our axioms. As a backdrop to our positive results, on arbitrary structures, the logics that we study are known to be non-recursively axiomatizable.


Introduction
In this paper, we develop a uniform method for obtaining complete axiomatizations of fragments of MSO on finite trees. In particular, we obtain a complete axiomatization for MSO, FO(TC 1 ), and FO(LFP 1 ) on finite node-labeled sibling-ordered trees. We take inspiration from Kees Doets, who proposed in [12] complete axiomatizations of FO-theories in particular on the class of node-labeled finite trees without sibling-order (see Section 4, where we discuss his work in more details). A similar result for FO on node-labeled finite trees with sibling order was shown in [2] in the context of model-theoretic syntax and in [9] in the context of XML query languages. We use the signature of [9] and extend the set of axioms proposed there to match the richer syntax of the logics we consider.
Finite trees are basic and ubiquitous structures that are of interest at least to mathematicians, computer scientists (e.g. tree-structured documents) and linguists (e.g. parse trees). The logics we study are known to be very well-behaved on this particular class of structures and to have an interestingly high expressive power. In particular, they all allow to express reachability, but at the same time, they have the advantage of being decidable on trees.
As XML documents are tree-structured data, our results are relevant to XML query languages. Declarative query languages fro both relational and XML data are based on logical languages. In [11] and [16], MSO and FO(TC 1 ) have been proposed as a yardstick of expressivity of navigational query languages for XML. It is known that FO(LFP 1 ) has the same expressive power as MSO on trees, but the translations between the two are nontrivial, and hence it is not clear whether an axiomatization for one language can be obtained from an axiomatization for the other language in any straightforward way. One important and well-studied problem for XML query languages, as well as for database query languages in general, is query optimization. Typically, a query can be expressed in many equivalent ways, and the execution time of a query depends strongly on the way it is expressed. A common approach to database query optimization is by means of a set of rewrite rules, allowing one to transform a query expression into another equivalent one, together with a cost model that predicts the execution time of a query expression on a given database [1]. In [10], a sound and complete set of rewrite rules for the XML path language Core XPath 2.0 was obtained from a complete axiomatization of the first-order theory of finite trees, exploiting the fact that Core XPath 2.0 is expressively complete for first-order logic. We expect that the results we present here can be used in order to obtain sound and complete sets of rewrite rules for dialects of Core XPath that are expressively complete for FO(TC 1 ) and for MSO, such as the ones presented in [7,11].
In applications to computational linguistics, finite trees are used to represent the grammatical structure of natural language sentences. In the context of model theoretic syntax, Rogers advocates in [27] the use of MSO in order to characterize derivation trees of context free grammars. Kepser also argues in [21] that MSO should be used in order to query treebanks. A treebank is a text corpus in which each sentence has been annotated with its syntactic structure (represented as a tree structure). In [22] and [30] Kepser and Tiede propose to consider various transitive closure logics, among which FO(TC 1 ), arguing that they constitute very natural formalisms from the logical point of view, allowing concise and intuitive phrasing of parse tree properties.
The remainder of the paper is organized as follows: in Section 2 we present the concept of finite tree and the logics we are interested in together with their standard interpretation. Section 3 merely state our three axiomatizations. In Section 4, we introduce non standard semantics called Henkin semantics for which our axiomatizations are easily seen to be complete. We prove in detail the FO(LFP 1 ) Henkin completeness proof. Section 5 introduces operations on Henkin structures: substructure formation and a general operation of Henkin structures combination. We obtain Feferman-Vaught theorems for this operation by means of Ehrenfeucht-Fraïssé games. This section contains in particular the definitions and adequacy proofs of the Ehrenfeucht-Fraïssé games that we also use there to prove our Feferman-Vaught theorems. In Section 6, we prove real completeness (that is, on the more Proof. Indeed, suppose there is a finite sequence of points a 1 . . . a n such that g(u) = a 1 , g(v) = a n , and for each i < n, M, g[x/a i ; y/a i+1 ] |= ϕ(x, y). Then for any subset A closed under ϕ and containing a 1 , we can show by induction on the length of the sequence a 1 . . . a n that a n belongs to A. Now, on the other hand, suppose that there is no finite sequence like described above. To show that there is a subset A of the required form, we simply take A to be the set of all points that can be reached from u via ϕ by a finite sequence. By assumption, v does not belong to this set and the set is closed under ϕ.
Intuitively this means that for a formula of the form [TC xy ϕ](u, v) to hold on a standard structure, there must be a finite "ϕ path" between the points that are named by the variables u and v.
Finally we will also be interested in monadic least fixed-point logic FO(LFP 1 ), which extends FO with set variables and an explicit monadic least fixed point operator. Consider a FO(LFP 1 )-formula ϕ(X, x) and a structure M together with a valuation g. This formula induces an operator F ϕ taking a set A ⊆ dom(M) to the set {a : M, g[a/x, A/X] |= ϕ}. FO(LFP 1 ) is concerned with least fixed points of such operators. If ϕ is positive in X (a formula is positive in X whenever X only occurs in the scope of an even number of negations), the operator F ϕ is monotone (i.e. X ⊆ Y implies F ϕ (X) ⊆ F ϕ (Y )). Monotone Definition 2.5 (Syntax and semantics of FO(LFP 1 )). Let At stand for a first-order atomic formula (of the form R( x)), x = y, or ⊤), X a set variable, x, y FO-variables, ψ, ξ FO(LFP 1 )formulas and ϕ(x, X) a FO(LFP 1 )-formula positive in X (besides x and X, ϕ(x, X) possibly contains other free variables). The set of FO(LFP 1 ) formulas is given by the following recursive definition: We use ∀xψ as shorthand for ¬∃x¬ψ. We define the quantifier depth of a FO(LFP 1 )-formula as the maximal number of nested first-order quantifiers and LF P operators. Again, we can interpret FO(LFP 1 )-formulas in first-order structures. The notion of assignment and the truth of atomic formulas are defined similarly as in the MSO case. The truth of compound formulas is defined by induction, with the same clauses as in FO and an additional one: M, g |= [LF P Xx ϕ]y iff for all A ⊆ dom(M), if for all a ∈ dom(M), M, g[a/x, A/X] |= ϕ(x, X) implies a ∈ A, then g(y) ∈ A.
Remark 2.6. In practice we will use an equivalent (less intuitive but often more convenient) rephrasing: M, g |= [LF P Xx ϕ]y iff for all A ⊆ dom(M), if g(y) / ∈ A, then there exists a ∈ dom(M) such that a / ∈ A and M, g[a/x, A/X] |= ϕ(x, X).

Expressive Power.
There is a recursive procedure, transforming any FO(LFP 1 )formula ϕ into a MSO-formula ϕ ′ such that M, g |= ϕ iff M, g |= ϕ ′ . The interesting clause is ([LF P Xx ϕ(x, X)]y) ′ = ∀X(∀x(ϕ(x, X) ′ → Xx) → Xy). (The other ones are all of the same type, e.g. (ϕ ∧ ψ) ′ = (ϕ ′ ∧ ψ ′ ).) This procedure can easily be seen adequate by considering the semantical clause for the LF P operator. Now there is also a recursive procedure transforming any FO(TC 1 ) formula ϕ into a FO(LFP 1 ) formula ϕ ′′ such that M, g |= ϕ iff M, g |= ϕ ′′ . The interesting clause is ([T C xy ϕ](u, v)) ′′ = [LF P Xy y = u ∨ ∃x((Xx ∧ ϕ(x, y) ′′ ))]v. Let us give an argument for this claim. By Proposition 2.4 it is enough to show that [LF P Xy y = u∨∃x(Xx∧ϕ(x, y) ′′ )]v holds if and only if there is a finite ϕ ′′ path from u to v. For the right to left direction, suppose there is such a path a 1 . . . a n with g(u) = a 1 and g(v) = a n . Then, for any subset A of the domain, we can show by induction on i that if for all a i (1 ≤ i ≤ n), a i = u ∨ ∃x((Ax ∧ ϕ(x, a i ) ′′ ) implies a i ∈ A, then v ∈ A, i.e., [LF P Xy y = u ∨ ∃x((Xx ∧ ϕ(x, y) ′′ ))]v holds. Now for the left to right direction, suppose there is no such ϕ ′′ path. Consider the set A of all points that can be reached from u by a finite ϕ ′′ path. By assumption, ¬Av and it holds that ∀y((y = u ∨ ∃x(Ax ∧ ϕ(x, y) ′′ )) → Ay), i.e., ¬[LF P Xy y = u ∨ ∃x(Xx ∧ ϕ(x, y) ′′ )]v.
It is known that on arbitrary structures FO(TC 1 ) < FO(LFP 1 ) < MSO (see [13] or [24]) and on trees FO(TC 1 ) < trees FO(LFP 1 ) = trees MSO (see [11] and [28]). It is also known that the (not FO definable) class of finite trees is already definable in FO(TC 1 ) (see for 6 A. GHEERBRANT AND B. TEN CATE instance [22]), which is the weakest of the logics studied here. We provide additional detail in Section 6.3.

The Axiomatizations
where ϕ is atomic and ψ is obtained from ϕ by replacing x in zero or more (but not necessarily all) places by y.
⊢ ∀Xϕ → ϕ[X/T ], where T (which is either a set variable or a set predicate) is substitutable in ϕ for X.
⊢ ϕ → ∀Xϕ, where X does not occur free in ϕ MSO Generalization if ⊢ ϕ, then ⊢ ∀Xϕ where ψ is any FO(TC 1 ) formula As many arguments in this paper equally hold for MSO, FO(TC 1 ) and FO(LFP 1 ), we let Λ ∈ {MSO, FO(TC 1 ), FO(LFP 1 )} and use Λ as a symbol for any one of them. The axiomatization of Λ on finite trees consists of three parts: the axioms of first-order logic, the specific axioms of Λ, and the specific axioms on finite trees.
To axiomatize FO, we adopt the infinite set of logical axioms and the two rules of inference given in Figure 1 (like in [14], except from the fact that we use a generalization rule). Here, as in [14], by a propositional tautology, we mean a formula can be obtained from a valid propositional formula (also known as the sentential calculus) by uniformly substituting formulas for the proposition letters). Alternatively, FO1 may be replaced by where ψ is any FO(LFP 1 ) formula and ϕ(x, ψ) is the result of the replacement in ϕ(x, X) of each occurrence of X by ψ (renaming variables when needed) ) → P (y)), Generalization and P positive in ϕ does not occur in ξ, then ⊢ ξ → [LF P Xx ϕ](y) there is a least sibling T10. ∀x∀y((x ≺ y ∨ y ≺ x) ↔ (∃z(z < ch x ∧ z < ch y) ∧ x = y)) linearly ordered siblings where ϕ(x) ranges over Λ-formulas in one free variable x, and x < ch y is shorthand for x < y ∧ ¬∃z(z < y ∧ x < z), x ≺ ns y is shorthand for x ≺ y ∧ ¬∃z(x ≺ z ∧ z ≺ y)  Figure 2 are added to the axiomatization of FO and we call the resulting system ⊢ MSO . COMP stands for "comprehension" by analogy with the comprehension axiom of set theory. MSO1 plays a similar role as FO2, MSO2 as FO3 and MSO3 as FO4. To axiomatize FO(TC 1 ), the axiom and rule of Figure 3 are added to the axiomatization of FO and we call the resulting system ⊢ FO(TC 1 ) . To axiomatize FO(LFP 1 ), the axiom and rule of Figure  4 are added to the axiomatization of FO and we call the resulting system ⊢ FO(LFP 1 ) . We are interested in axiomatizing Λ on the class of finite trees. For that purpose, we restrict the class of considered structures by adding to ⊢ Λ the axioms given in Figure 5 and we call the resulting system ⊢ tree Λ . Note that the induction scheme in Figure 5 allows to reason by induction on properties definable in Λ only. Proof. It follows from the truth of T1, T2 and T5 that (M, <) is a tree. Note that T3 and T4 are valid consequences of T1, T2, T5 on finite structures. Furthermore, T6, T7 and T10 imply that ≺ linearly orders the children of each node (and that ≺ only relates to each other nodes that are siblings). Note again that T8 and T9 follow from T6, T7 and T10 on finite structures.
We refer for basic definitions (e.g., proof by which we mean formal deduction, or axiomatization by which we mean deductive calculus) to [14] and sometimes only sketch or even omit classical arguments. E.g., we assume the notion of being substitutable in a formula to be clear for both objects and set variables. For details on such basic notions and technics, we refer to the material extensively developed in [14] and in particular, to the proof of the FO completeness theorem presented there. The Henkin completeness proofs provided in Section 4 are built on this classical material.
We end this Section by spelling out some definitions that are specific to our paper.
Definition 3.2. We say that a Λ-formula ϕ is Λ-provable if ⊢ Λ ϕ occurs (as the last line) in some Λ-proof and we say that it is Λ-consistent if its negation is not Λ-provable. Let Γ be a set of Λ-formulas and ϕ a Λ-formula. By Γ ⊢ Λ ϕ we will always mean that there are ψ 1 , . . . , ψ n ∈ Γ such that ⊢ Λ (ψ 1 ∧ . . . ∧ ψ n ) → ϕ. Whenever Γ ⊢ Λ ¬ϕ does not hold, we say that ϕ is Γ-consistent. We say that Γ is Λ-consistent if ⊤ is Γ-consistent. Finally, we say that Γ is a maximal consistent set of Λ-formulas if Γ is consistent, and for each formula φ ∈ Λ, either φ ∈ Γ or ¬φ ∈ Γ. Now the main result of this paper is that on standard structures, the Λ theory of finite trees is completely axiomatized by ⊢ tree Λ . In the remaining sections we will progressively build a proof of it.

Henkin Completeness
As it is well known, MSO, FO(TC 1 ) and FO(LFP 1 ) are highly undecidable on arbitrary standard structures and hence not recursively enumerable (by arbitrary, we mean when there is no restriction on the interpretation of the relation symbols from the signature, unlike in the case of, e.g., trees). So in order to show that our axiomatizations ⊢ tree Λ are complete on finite trees, we refine a trick used by Kees Doets in his PhD thesis [12]. We proceed in two steps (the second step being the one inspired by Kees Doets). First, we show completeness theorems, based on a non-standard (so called Henkin) semantics for MSO, FO(TC 1 ) and FO(LFP 1 ) (on the general topic of Henkin semantics, see [18], the original paper by Henkin and also [26]). Each semantics respectively extends the class of standard structures with non standard (Henkin) MSO, FO(TC 1 ) and FO(LFP 1 )-structures. By the Henkin completeness theorems, our axiomatic systems ⊢ tree Λ naturally turn out to be complete on the wider class of their Henkin-models. But we will see that compactness also follows from these completeness results and some of these Henkin models are infinite. As a second step, we show in Section 6 that no Λ-sentence can distinguish between standard and non-standard Λ-Henkin-models among models of our axioms. Every finite Henkin model being also a standard model, this entails that our axioms are complete on the class of (standard) finite trees, i.e., each Λ-sentence valid on this class is provable using the system ⊢ tree Λ . Now let us point out that Kees Doets was interested in complete axiomatizations of monadic "Π 1 1 -theories" of various classes of linear orders and trees. Considering such theories in fact amounts to considering first-order theories of such structures extended with finitely many unary predicates. Thus, he was relying on the FO completeness theorem and if he was working with non-standard models of particular FO-theories, he was not concerned with non standard Henkin-structures in our sense. In particular, he used Ehrenfeucht-Fraïssé games in order to show that "definably well-founded" node-labeled trees have well-founded n-equivalents for all n. In Section 6.2, Lemma 6.4, which is the key lemma to our main completeness result, establishes a similar result for definably well-founded Henkin-models of the Λ-theory of finite node-labeled sibling-ordered finite trees. Hence, what makes the originality of the method developed in this paper is its use of Henkin semantics: we first create a Henkin model and then "massage" it in order to obtain a model that is among our intended ones. Similar methods are commonly used to show completeness results in modal logic, where "canonical models" are often transformed in order to obtain intended models (see [3]). Remarkably, the completeness proof for the µ-calculus on finite trees given in [8], which is directly inspired by the methods used here, proceeds in that way. There are numerous examples of that sort in modal logic (and especially, in temporal logic), but there is also one notable example in classical model theory. In 1970, Keisler provided a complete axiomatization of FO extended with the quantifier "there exist uncountably many" (see [20]). His completeness proof, which is established for standard models, is surprisingly simple, it relies on the construction of an elementary chain of Henkin structures and then uses the omitting types theorem. Hence all in all, these structures seem to provide a particularly convenient tool, not only for simple Henkin completeness proofs, but also for more refined completeness proofs with respect to interesting subclasses of Henkin models like standard models.
Let us now introduce Henkin structures formally. Such structures are particular cases among structures called frames (note that such frames are unrelated to "Kripke frames") and it is convenient to define frames before defining Henkin-structures. In our case, a frame is simply a relational structure together with some subset of the powerset of its domain called its set of admissible subsets. A Henkin structure is a frame whose set of admissible subsets satisfies some natural closure conditions. Whenever A M = ℘(dom(M)), M can be identified to a standard structure. Assignments g into M are defined as in standard semantics, except that if X is a set variable, then we require that g(X) ∈ A M . Definition 4.2 (Interpretation of Λ-formulas in frames). Λ-formulas are interpreted in frames as in standard structures, except for the three following clauses. The set quantifier clause of MSO becomes: The T C clause of FO(TC 1 ) becomes: then g(v) ∈ A. And finally the LF P clause of FO(LFP 1 ) becomes: then g(y) ∈ A.  We do not detail here the MSO proof, as it is a special case of the proof of completeness for the theory of types given in [26]. We focus only on the FO(LFP 1 ) case, as the FO(TC 1 ) case is very similar, except that there is no need to consider set variables. Up to now we have been working with purely relational vocabularies. Here we will be using individual constants in the standard way, but only for the sake of readability (we could dispense with them and use FO variables instead). Also, whenever this is clear from the context, we will use ⊢ as shorthand for ⊢ FO(LFP 1 ) . Let us now begin the Henkin completeness proof for FO(LFP 1 ). This will achieve the proof of Theorem 4.5. Proof. We refer the reader to the proof for FO given by Enderton in [14, page 117]. The same proof applies for FO(LFP 1 ) (as well as MSO and FO(TC 1 )).
Definition 4.7. We say that a set of FO(LFP 1 ) formulas ∆ contains FO(LFP 1 ) Henkin witnesses if and only if the two following conditions hold. First, for every formula ϕ, if ¬∀xϕ ∈ ∆, then ¬ϕ[x/t] ∈ ∆ for some term t and if ¬[LF P Xx ϕ]y ∈ ∆, then ¬P y ∧ ¬∃x(¬P x ∧ ϕ(P, x)) ∈ ∆ for some monadic predicate P . Second, if ϕ ∈ ∆ and x is a free variable of ϕ, then ∀x(P x ↔ ϕ(x)) ∈ ∆ for some monadic predicate P .
The originality of the FO(LFP 1 ) case essentially lies in the notion of FO(LFP 1 )-Henkin witness of Definition 4.7. In order to use this notion in the proof of Lemma 4.9, we also need the following lemma: Lemma 4.8. Let Γ be a consistent set of FO(LFP 1 )-formulas and θ a FO(LFP 1 )-formula of the form ∀x(ϕ ↔ P x) with P a fresh monadic predicate (i.e. not appearing in Γ). Then Γ ∪ {θ} is also consistent.
Proof. Suppose Γ ∪ {∀x(ϕ ↔ P x)} is inconsistent, so there is some proof of ⊥ from formulas in Γ ∪ {∀x(ϕ ↔ P x)}. We first rename all bound variables in the proof with variables which had no occurrence in the proof or in ∀x(ϕ ↔ P x) (this is possible since proofs are finite objects and we have a countable stock of variables). Also, whenever in the proof the FO(LFP 1 ) generalization rule is applied on some unary predicate P , we make sure that this P is different from the unary predicate that we want to substitute by ϕ and which does not appear in the proof; this is always possible because we have a countable set of unary predicates. Now, we replace in the proof all occurrences of P x by ϕ (as we renamed bound variables, there is no accidental binding of variables by wrong quantifiers). Then, every occurrence of ∀x(ϕ ↔ P x) in the proof becomes an occurrence of ∀x(ϕ ↔ ϕ), i.e., we have obtained a proof of ⊥ from Γ ∪ {∀x(ϕ ↔ ϕ)}, i.e., from Γ (∀x(ϕ ↔ ϕ) is provable, as it can be obtained by FO generalization from a propositional tautology). It entails that Γ is already inconsistent, which contradicts the consistency of Γ. Now it remains to show that the replacement procedure of all occurrences of P x by ϕ is correct, so that we still have a proof of ⊥ after it. Every time the replacement occurs in an axiom (or its generalization, which is still an axiom as we defined it), then the result is still an instance of the given axiom schema (even for FO(LFP 1 ) generalizations, because we took care that P is never used in the proof for a FO(LFP 1 ) generalization). Also, as replacement is applied uniformly in the proof, every application of modus ponens stays correct: consider ψ → ξ and ψ. Obviously the result ψ * of the substitution will allow to derive the result ξ * of the substitution from ψ * → ξ * and ψ * . Also ⊥ * is simply ⊥, so the procedure gives us a proof of ⊥. Lemma 4.9. (FO(LFP 1 ) Lindenbaum Lemma) Let σ be a countable vocabulary and let σ * = σ ∪ {c n | ∈ N} ∪ {P n | n ∈ N} with c i , P i / ∈ σ. If a set Γ of FO(LFP 1 )-formulas in vocabulary σ is consistent, then there exists a maximal consistent set Γ * of σ * formulas such that Γ ⊆ Γ * and Γ * contains FO(LFP 1 )-Henkin witnesses.
Proof. Let Γ be a consistent set of well formed FO(LFP 1 )-formulas in a countable vocabulary σ. We expand σ to σ * by adding countably many new constants and countably many new monadic predicates. Then Γ remains consistent as a set of well formed formulas in the new language. We fix an enumeration of all tuples consisting of two FO variables, one set variable and one formula of σ * : . . (this is possible since the language is countable), where the ϕ i are formulas, the x i , x ′ i are FO variables and the X i are set variables.
• Let θ 3n−2 be ¬∀x n ϕ n → ¬ϕ n [x n /c l ], where c l is the first of the new constants neither occurring in ϕ n nor in θ k with k < 3n − 2. • Let θ 3n−1 be ¬[LF P x ′ n Xn ϕ n ]x n → (¬P l x n ∧ ¬∃x(¬P l x ∧ ϕ n (P l , x))), where P l is the first of the new monadic predicates neither occurring in ϕ n nor in θ k with k < 3n − 1. • Let θ 3n be ∀x n (ϕ n ↔ P l x n ), where P l is the first of the new monadic predicates neither occurring in ϕ n nor in θ k with k < 3n. Call Θ the set of all the θ i . If not, then because deductions are finite, for some m ≥ 0, Γ ∪ {θ 1 , . . . , θ m , θ m+1 } is inconsistent. Take the least such m. Then, by the definition of consistency and the axioms of propositional logic, Γ ∪ {θ 1 , . . . , θ m } ⊢ ¬θ m+1 . Now there are three cases: Since c does not appear in any formula on the left, by Lemma 4.6, Γ ∪ {θ 1 , . . . , θ m } ⊢ ∀xϕ, which contradicts the minimality of m (or the consistency of Γ if m = 0).
Since P does not appear in any formula on the left, by FO( which contradicts the minimality of m (or the consistency of Γ whenever m = 0). (3) θ m+1 is of the form ∀x(ϕ ↔ P x). By Lemma 4.8, this is not possible. We extend Γ ∪ Θ to a maximal consistent set Γ * in the standard way (see for instance [14, page 137]).
We will now show that if Γ * is a maximal consistent set that contains FO(LFP 1 )-Henkin witnesses, then Γ * has a FO(LFP 1 )-Henkin model M Γ * . Definition 4.11. Let Γ * ⊆ F ORM (σ) be maximal consistent and contain FO(LFP 1 )-Henkin witnesses. We define an equivalence relation on the set of FO terms, by letting We denote the equivalence class of a term t by |t|. Definition 4.13. We define M Γ * (together with a valuation g Γ * ) out of Γ * .
Proof. By construction of Γ * which contains FO(LFP 1 )-Henkin witnesses, this is immediate (we introduced a monadic predicate for each parametrically definable subset).
Proof. By induction on ϕ.
Proof. First turn Γ into a FO(LFP 1 ) maximal consistent set Γ * with FO(LFP 1 )-Henkin witnesses in a possibly richer signature (with extra individual constants and monadic predicates) σ * . Then build a structure M Γ * out of this Γ * . Then the structure M Γ * satisfies Γ * under the valuation g Γ * and hence it satisfies also Γ (Γ being a subset of Γ * ).
Compactness follows directly from Definition 3.2 and Theorem 4.5, i.e., a possibly infinite set of Λ-sentences has a Λ-Henkin model if and only if every finite subset of it has a Λ-Henkin model. It also follows directly from Theorem 4.5 that ⊢ tree Λ is complete on the class of its Λ-Henkin-models. Nevertheless, by compactness the axioms of ⊢ tree Λ also have infinite models. We overcome this problem by defining a slightly larger class of Henkin structures, which we will call definably well-founded Λ-quasi-trees. 1 Definition 4.17. A Λ-quasi-tree is any Λ-Henkin structure (T, <, ≺, P 1 , . . . , P n , A T ) (where A T is the set of admissible subsets of T ) satisfying the axioms T1-T10 of Figure 5. A Λ-quasi-tree is definably well founded if, in addition, it satisfies all Λ-instances of the induction scheme Ind of Figure 5.
With this definition, we obtain from Theorem 4.5 the following:

Operations on Henkin-Structures
Let Λ ∈ {MSO, FO(TC 1 ), FO(LFP 1 )}. As noted in Remark 4.4, every finite Λ-Henkin structure is also a standard structure. Hence, when working in finite model theory, it is enough to rely on the usual FO constructions to define operations on structures. On the other hand, even though our main completeness result concerns finite trees, inside the proof we need to consider infinite (Λ-Henkin) structures and operations on them. In this context, methods for forming new structures out of existing ones have to be redefined carefully. We first propose a notion of substructure of a Λ-Henkin-structure generated by one of its parametrically definable admissible subsets: Note that in the case of MSO and FO(LFP 1 ), we could also have defined A M↾A in an alternative way: Proposition 5.2. Take M and A as previously and consider the structure The second condition holds because both B ′ and A are parametrically definable in M, so their intersection also is ( Now, in order to show that Λ-substructures are Λ-Henkin-structures, we introduce a notion of relativization and a corresponding relativization lemma. This lemma establishes that for every Λ-Henkin-structure M and Λ-substructure M ↾ A of M (with A a set parametrically definable in M), if a set is parametrically definable in M ↾ A then it is also parametrically definable in M. This result will be useful again in Section 6.2.
Definition 5.3 (Relativization mapping). Given two Λ-formulas ϕ, ψ having no variables in common and given a FO variable x occurring free in ψ, we define REL(ϕ, ψ, x) by induction on the complexity of ϕ and call it the relativization of ϕ to ψ: where ψ[y/x] is the formula obtained by replacing in ψ every occurrence of x by y and similarly for ψ[z/x].
Hence for instance, REL(∃yP (y), Q(x), x) = ∃y(P (y) ∧ Q(y)), which is satisfied in any model M of which the submodel induced by Q contains an element satisfying P .
Lemma 5.4 (Relativization lemma). Let M be a Λ-Henkin-structure, g a valuation on M, ϕ, ψ Λ-formulas having no variable in common and A = {x | M, g |= ψ}. If g(y) ∈ A for every variable y occurring free in ϕ and g(Y ) ∈ A M↾A for every set variable Y occurring free in ϕ, then M, g |= REL(ϕ, ψ, x) ⇔ M ↾ A, g |= ϕ.
Proof. By induction on the complexity of ϕ. Let g be an assignment satisfying the required conditions. Base case: ϕ is an atom and REL(ϕ, ψ, x) = ϕ. So M, g |= ϕ ⇔ M ↾ A, g |= ϕ (by hypothesis, g is a suitable assignment for both models). Inductive hypothesis: the property holds for every ϕ of complexity at most n. Now consider ϕ of complexity n + 1.
• ϕ :≈ ϕ 1 ∧ ϕ 2 and REL(ϕ 1 ∧ ϕ 2 , ψ, x) :≈ REL(ϕ 1 , ψ, x) ∧ REL(ϕ 2 , ψ, x). By induction hypothesis, the property holds for ϕ 1 and for ϕ 2 . By the semantics of ∧, it also holds for Hence, by the semantics of ∃ and by definition of Hence, by the semantics of ∃ and by definition of . By definition of T C, the following are equivalent: By inductive hypothesis, for all a, b ∈ A, ∈ C, which, by the semantics of T C, is equivalent to: . Now by our assumptions on g and by definition of A, g[a/y, b/z] only assigns points in A.
By definition of LF P , the following are equivalent: then g(z) ∈ C, which, by the semantics of LF P , is equivalent to: As REL(χ, ψ, x) is positive in X and X does not occur in ψ, M, g[a/y, C/X] |= REL(χ, ψ, x)∧ ψ[y/x]. Also by hypothesis a ∈ C. Now as M, g[a/y] |= ψ[y/x], by definition of A, a ∈ A. So a ∈ A ∩ C, i.e, a ∈ B and since we proved it for arbitrary a ∈ dom(M), by 4., g(z) ∈ B. As B ⊆ C, it follows that g(z) ∈ C. Proof. Take B parametrically definable in M ↾ A, i.e., there is a Λ-formula ϕ(y) and an assignment g such that Assume without loss of generality that ϕ and ψ have no variables in common. We define an assignment g * by letting g * (z) = g ′ (z) for every variable z occurring in ψ and g * (z) = g(z) otherwise. The situation with set variables is symmetric. Now by Lemma 5.4 There is, in model theory, a whole range of methods to form new structures out of existing ones. Standard references on the matter are [15,25], written in a very general algebraic setting. Familiar constructions like disjoint unions of relational structures are redefined as particular cases of a new notion of generalized product of FO-structures and abstract properties of such products are studied. In particular, an important theorem now called the Feferman-Vaught theorem for FO is proven in [15]. We are particularly interested in one of its corollaries, which establishes that generalized products of relational structures preserve elementary equivalence. We show an analogue of this result for a particular case of generalized product of Λ-Henkin-structures that we call fusion, this notion being itself a generalization of a notion of disjoint union of Λ-Henkin-structures defined below. That is:  = ∅ for every i = j. In this sense, disjoint union as we defined it above can be seen as a special case of fusion.
We show preservation results involving f -fusions of Λ-Henkin-structures. Hence we deal with analogues of elementary equivalence for these logics and we refer to Λ-equivalence. Let us recall that by quantifier depth of a Λ-formula, we mean the maximal number of nested quantifiers in the formula (by "quantifier", we mean FO and MSO-quantifiers, as well as T C or LF P -operators).
Definition 5.8. Given two Λ-Henkin-structures M and N, we write M ≡ Λ N and say that M and N are Λ-equivalent if they satisfy the same Λ-sentences. Also, for any natural number n, we write M ≡ n Λ N and say that M and N are n-Λ-equivalent if M and N satisfy the same Λ-sentences of quantifier depth at most n. In particular, M ≡ Λ N holds iff, for all n, M ≡ n Λ N holds. Now we are ready to introduce the "Feferman-Vaught theorems" that we will show in Section 5.2 and which establish that f -fusions of Λ-Henkin-structures preserve Λ-equivalence, that is: We will also show in this section that every f -fusion of Λ-Henkin-structures is a Λ-Henkin-structure. Comparable work had already been done by Makowski in [25] for extensions of FO, but an important difference is that he only considered standard structures, whereas we need to deal with Λ-Henkin-structures. Our proofs make use of Ehrenfeucht-Fraïssé games for each of the logics Λ.

Ehrenfeucht-Fraïssé Games on Henkin-Structures.
Let Λ ∈ {MSO, FO(TC 1 ), FO(LFP 1 )}. We survey Ehrenfeucht-Fraïssé games for FO, MSO, FO(TC 1 ), and FO(LFP 1 ) which are suitable to use on Henkin structures. We also provide an adequacy proof for the FO(TC 1 ) game. The MSO game is a rather straightforward extension of the FO case and has already been used by other authors (see for instance [23]). The FO(LFP 1 ) game is borrowed from Uwe Bosse [4]. It also applies to Henkin structures, as careful inspection shows. The FO(TC 1 ) game has already been mentioned in passing by Erich Grädel in [17] as an alternative to the game he used and we show that it is adequate for Henkin semantics. It looks also similar to a system of partial isomorphisms given in [6]. However it is important to note that this game is very different from the FO(TC 1 ) game which is actually used in [17]. The two games are equivalent when played on standard structures, but not when played on FO(TC 1 )-Henkin structures. This is so because the game used in [6] relies on the alternative semantics for the T C operator given in Proposition 2.4, so that only finite sets of points can be chosen by players ; whereas the game we use involves choices of not necessarily finite admissible subsets. These are not equivalent approaches. Indeed, on FO(TC 1 )-Henkin structures a simple compactness argument shows that the semantical clause of Proposition 2.4 (defined in terms of existence of a finite path) is not adequate.
Let us first introduce basic notions connected to these games. One rather trivial sufficient condition for Λ-equivalence is the existence of an isomorphism. Clearly isomorphic structures satisfy the same Λ-formulas. A more interesting sufficient condition for Λ-equivalence is that of Duplicator having a winning strategy in all Λ Ehrenfeucht-Fraïssé games of finite length. To define this, we first need this notion: Definition 5.10 (Finite Partial Isomorphism). A finite partial isomorphism between structures M and N is a finite relation {(a 1 , b 1 ), . . . , (a n , b n )} between the domains of M and N such that for all atomic formulas ϕ(x 1 , . . . , x n ), M |= ϕ [a 1 , . . . , a n ] iff N |= ϕ [b 1 , . . . , b n ]. Since equality statements are atomic formulas, every finite partial isomorphism is (the graph of) a injective partial function.
We will also need the following lemma: Lemma 5.11 (Finiteness Lemma). Fix any set x 1 , . . . , x k , X k+1 , . . . , X m . In a finite relational vocabulary, up to logical equivalence, with these free variables, there are only finitely many Λ-formulas of quantifier depth ≤ n.
Proof. This can be shown by induction on k. In a finite relational vocabulary, with finitely many free variables, there are only finitely many atomic formulas. Now, any Λ-formula of quantifier depth k + 1 is equivalent to a Boolean combination of atoms and formulas of quantifier depth k prefixed by a quantifier. Applying a quantifier to equivalent formulas preserves equivalence and the Boolean closure of a finite set of formulas remains finite, up to logical equivalence. Now, as we are concerned with extensions of FO, every Λ-game will be defined as an extension of the classical FO game, that we recall here:  N)) is as follows. There are two players, Spoiler and Duplicator. The game has n rounds, each of which consists of a move of Spoiler followed by a move of Duplicator. Spoiler's moves consist of picking an element from one of the two structures, and Duplicator's responses consist of picking an element in the other structure. In this way, Spoiler and Duplicator build up a finite binary relation between the domains of the two structures: initially, the relation is empty; each round, it is extended with another pair. The winning conditions are as follows: if at some point of the game the constructed binary relation is not a finite partial isomorphism, then Spoiler wins immediately. If after each round the relation is a finite partial isomorphism, then the game is won by Duplicator. The proof for the first order case is classic. We refer the reader to the proof given in [13] or to the one in [24].
For technical convenience in the course of inductive proofs, we extend the notion of FO parameter by considering set parameters, i.e., instead of interpreting a set variable as a name of the admissible set A, we can add a new monadic predicate A to the signature. The new predicates and the sets they name are called set parameters. (This is similar to the FO 20 A. GHEERBRANT AND B. TEN CATE notion that can be found in [19].) We will work with parametrized (or expanded) Henkinstructures, that is, structures considered together with partial valuations. This means that the assignment is possibly non empty at the beginning of the game, which can start with some "handicap" for Duplicator, i.e., some preliminary set of already "distinguished objects and sets".
We first define a necessary and sufficient condition for MSO equivalence by extending Ehrenfeucht-Fraïssé games from FO to MSO. This game has already been defined in the literature, see for instance [23].  We omit the proof, because it parallels the FO case. The proof works regardless whether MSO is interpreted in the standard or in the Henkin way. What matters here is that the game-theoretic meaning of a "quantification" over a given "domain", lies in the choice of an element from that domain (including one consisting of "higher-order elements", e.g., sets). The FO(TC 1 ) game that we will be introducing now had been already mentioned in passing by Erich Grädel in [17] as an alternative to the game he used. We will show that it is adequate on Henkin-structures.  N,b)) of length n on expanded structures (M,ā) and (N,b) is defined as for the first-order case, except that each time she chooses a structure, Spoiler can either choose only one element or an admissible subset together with two elements of its domain. In the first case we say that she plays an ∃ (or point) move and in the second case, a T C-move (which we will define more precisely below). Each point move results in an extension of the assignment {ā →b} with elements a s+1 ∈ dom(M), b s+1 ∈ dom(N). Each T C-move results in an extension of the assignment {ā →b} with elements a s+1 , a s+2 ∈ dom(M), b s+1 , b s+2 ∈ dom(N). At each round, Spoiler chooses the kind of move to be played.
The ∃ move is defined as in the FO case. The T C-move is as follows: Spoiler considers two pebbles (a i , b i ) and (a j , b j ) on the board (i.e., corresponding couples of parameters taken in each structure) and depending on the structure that he chooses to consider, he plays: • either a set A ∈ A M with a i ∈ A and a j / ∈ A. Duplicator then answers with a set B ∈ A N such that b i ∈ B and b j / ∈ B. Spoiler now picks b s+1 ∈ B, b s+2 / ∈ B and Duplicator answers with a s+1 ∈ A, a s+2 / ∈ A. • or a set B ∈ A N with b i ∈ B and b j / ∈ B. Duplicator then answers with a set A ∈ A M such that a i ∈ A and a j / ∈ A. Spoiler now picks a s+1 ∈ A, a s+2 / ∈ A and Duplicator answers with b s+1 ∈ B, b s+2 / ∈ B. In each T C-move, the assignment is extended with a s+1 → b s+1 , a s+2 → b s+2 . After n moves, Duplicator has won if the constructed assignmentā →b is a partial isomorphism (i.e. the game continues with the two new pebbles in each structure, but the sets A and B are forgotten). By induction on n. Base step: With 0 round the initial match between distinguished objects must have failed to be a partial isomorphism for Spoiler to win. This implies that (M,ā) and (N,b) disagree on some atomic formula.
Inductive step: The induction hypothesis says that for every two structures, if Spoiler can win their comparison game over n rounds, then the structures disagree on some FO(TC 1 )-formula of quantifier depth n. Assume that for some structures (M,ā), (N,b), Spoiler has a winning strategy for the game over n + 1 rounds. Let us reason on Spoiler's first move in the game. It can either be a T C or an ∃ move.
If it is an ∃ move, then it means that Spoiler picks an element a in one of the two structures, so that no matter what element b Duplicator picks in the other, Spoiler has an n-round winning strategy. But then we can use the induction hypothesis, and find for each such b a formula ϕ b (x) that distinguishes (M,ā, a) from (N,b, b). In fact we can assume that in each case the respective formula is true of (M,ā, a) and false of (N,b, b) (by negating the formula if needed). Now take the big conjunction ϕ(x) of all these formulas (which is equivalent to a finite formula according to Lemma 5.11) and prefix it with an existential quantifier. Then the resulting formula is true in (M,ā) but false in (N,b). It is true in (M,ā) if we pick a for the existentially quantified variable. And no matter which element we pick in (N,b), it will always falsify one of the conjuncts in the formula, by construction. So, the new formula is false in (N,b). I.e., ∃xϕ(x) of quantifier depth n + 1 distinguishes (M,ā) and (N,b).
If Spoiler's first move is a T C-move, then it means that Spoiler picks a subset in one structure, let say A ∈ A M (with a i ∈ A and a j ∈ A), so that no matter which B ∈ A N (with b i ∈ B and b j ∈ B) Duplicator picks in the other structure, Spoiler can pick b k ∈ B, b k+1 ∈ B such that no matter which a k ∈ A, a k+1 ∈ A Duplicator picks, Spoiler has an n-round winning strategy. For each B that might be chosen by Duplicator, Spoiler's given strategy gives a fixed couple b k , b k+1 . For each response a k , a k+1 of Duplicator, we thus obtain by inductive hypothesis a discriminating formula ϕ B,a k ,a k+1 (x, y) that we can assume to be true in (N,b) for b k , b k+1 and false in (M,ā) for a k , a k+1 . Now for each B, let us take the big conjunction Φ B (x, y) of all these formulas (which is finite, by Lemma 5.11). We can then construct the big disjunction Φ(x, y) (again finite, by the same lemma) of all the formulas Φ B (x, y).
Considering the first round in the game together with the inductive hypothesis, note that the MSO formula ∃X(a i ∈ X ∧ a j ∈ X ∧ ∀xy((x ∈ X ∧ y ∈ X) → ¬Φ(x, y))) holds in (M,ā). Indeed, by induction hypothesis, any couple a k ∈ A, a k+1 ∈ A that Duplicator might choose in dom(M) will always falsify at least one of the conjuncts of each Φ B (x, y). Finally, the formula Φ(x, y) being constructed as the disjunction of all the formulas Φ B (x, y), any such couple a k , a k+1 will also falsify Φ(x, y). Now the MSO formula ∃X(a i ∈ X ∧ a j ∈ X ∧ ∀xy((x ∈ X ∧ y ∈ X) → ¬Φ(x, y))) is equivalent to ∃X(a i ∈ X ∧ a j ∈ X ∧ ¬∃xy(x ∈ X ∧ Φ(x, y) ∧ y ∈ X)), which means that On the other hand for the same reasons, note that it holds in (N,b) that ∀X((b i ∈ X ∧ b j ∈ X) → ∃xy(x ∈ X ∧ y ∈ X ∧ Φ(x, y))). Indeed, by induction hypothesis, for each B that Duplicator might choose in A N Spoiler will always be able to find a couple b k ∈ B, b k+1 ∈ B satisfying all the conjuncts of the corresponding formulas Φ B (x, y). Finally, the formula Φ(x, y) being constructed as the disjunction of all the formulas Φ B (x, y), such a couple a k , a k+1 will also satisfy Φ(x, y). Now ∀X((b i ∈ X ∧ b j ∈ X) → ∃xy(x ∈ X ∧ y ∈ X ∧ Φ(x, y))) is equivalent to ∀X(b i ∈ X ∨ b j ∈ X ∨ ∃xy(x ∈ X ∧ y ∈ X ∧ Φ(x, y))), which means that (N Let u be a name for the parameters a i , b i and v for b i , b j . [T C xy Φ(x, y)](u, v) of quantifier depth n + 1 distinguishes (N,ā) and (M,b). ⇐ From the existence of a FO(TC 1 ) formula of quantifier depth n distinguishing (M,ā) and (N,b) we will infer the existence of a winning strategy for Spoiler in the game EF n F O+T C ((M,ā), (N,b)). By induction on n.
Base step: Doing nothing is a strategy for Spoiler. Inductive step: The inductive hypothesis says that, for every two structures, if they disagree on some FO(TC 1 ) formula of quantifier depth n, then Spoiler has a winning strategy in the n-round game. Now, assume that some expanded structures (M,ā), (N,b) disagree on some FO(TC 1 ) formula χ of quantifier depth n + 1. Any such formula must be equivalent to a Boolean combination of formulas of the form ∃xψ(x) and [T C xy ϕ(x, y)](u, v) with ψ, ϕ of quantifier depth at most n. If χ distinguishes the two structures, then there is at least one component of this Boolean combination which suffices for distinguishing them.
Let us first suppose that it is of the form ∃xψ(x). We may assume without loss of generality that (M,ā) |= ∃xψ(x) whereas (N,b) |= ∃xψ(x). Then it means that there exists an object a ∈ dom(M) such that (M,ā) |= ψ(a) whereas for every object b ∈ dom(N), (N,b) |= ψ(b). But then we can use our induction hypothesis and find for each such b a winning strategy for Spoiler in EF n FO(TC 1 ) ((M,ā, a), (N,b, b)). We can infer that Spoiler has a winning strategy in EF n+1 FO(TC 1 ) ((M,ā), (N,b)). His first move consists in picking the object a in dom(M) and for each response b in dom(N) of Duplicator, the remaining of his winning strategy is the same as in EF n FO(TC 1 ) ((M,ā, a), (N,b, b)). We now suppose that [T C xy ϕ(x, y)](u, v) of quantifier depth n+1 distinguishes the two structures. We may assume without loss of generality that (M,ā) |= [T C xy ϕ(x, y)](u, v) i.e. it holds in (M,ā) that ∀X((a i ∈ X ∧ a j ∈ X) → ∃xy(x ∈ X ∧ y ∈ X ∧ ϕ(x, y))), . We want to show that Spoiler has a winning strategy in EF n+1 FO(TC 1 ) ((M,ā), (N,b)). Let us describe her first move. She first chooses (N,b) By definition of T C, such a set exists. Duplicator has to respond by picking a set A in A M containing a i and not a j . Spoiler then picks a k ∈ A and a k+1 ∈ A such that (M,ā) |= ϕ(a k , a k+1 ). This is possible because by definition of T C, for any possible choice A of Duplicator (i.e., any set A containing a i and not a j ) we have ∃xy(x ∈ A ∧ y ∈ A ∧ ϕ(x, y)). But that means that Duplicator is now stuck and has to pick b k ∈ B and b k+1 ∈ B such that (N,b) |= ϕ(b k , b k+1 ). Consequently, we have (N,b, b k , b k+1 ) |= ϕ(x, y), whereas (M,ā, a k , a k+1 ) |= ϕ(x, y). As ϕ(x, y) is of quantifier depth n, by induction hypothesis, Spoiler has a winning strategy in EF n FO(TC 1 ) ((M,ā, a k , a k+1 ), (N,b, b k , b k+1 )). The remaining of Spoiler's winning strategy in EF n+1 FO(TC 1 ) ((M,ā), (N,b)) (i.e. after her first move, that we already accounted for) is consequently as in EF n FO(TC 1 ) ((M,ā, a k , a k+1 ), (N,b, b k , b k+1 )). Let us finally consider the FO(LFP 1 ) case. There are two classical equivalent syntactic ways of defining the syntax of FO(LFP 1 ): the one we used in Section 2.2 and another one, dispensing with restrictions to positive formulas, but allowing negations only in front of atomic formulas and introducing a greatest fixed-point operator as the dual of the least fixed-point operator (also ∀ cannot be defined using ∃ and has to be introduced separately, similarly for the Boolean connectives). This second way of defining FO(LFP 1 ) turns out to be more convenient to define an adequate Ehrenfeucht-Fraïssé game. The game is suitable to use on Henkin structures because the semantics on which it relies is merely a syntactical variant of the one given in Section 4. Now the FO(LFP 1 )-formulas [LF P Xx ϕ(x, X)]y and [GF P Xx ϕ(x, X)]y, stating that a point belongs to the least fixed-point, or respectively, to the greatest fixed-point induced by the formula ϕ satisfy the following equations: [LF P Xx ϕ(x, X)]y ↔ ∀X(¬Xy → ∃x(¬Xx ∧ ϕ(x, X))) [GF P Xx ϕ(x, X)]y ↔ ∃X(Xy ∧ ∀x(Xx → ϕ(x, X))) Note that this holds no matter whether we be concerned with FO(LFP 1 ) and MSO on standard structures or on Henkin structures. The consideration of these equations is the In each fixed-point move the assignment is extended by A r+1 → B r+1 , a s+1 → b s+1 .
After n moves, Duplicator has won if the constructed element assignmentā →b is a partial isomorphism and for the subset assignmentĀ →B, for any 1 ≤ j ≤ r and i ≤ s: We call an assignment with these properties a posimorphism. For a proof in the case of standard structures, we refer the reader to Uwe Bosse [4]. As pointed out earlier, the same argument works as well in the case of Henkin structures.

Fusion Theorems on Henkin-Structures.
Let Λ ∈ {MSO, FO(TC 1 ), FO(LFP 1 )}. We show our analogues of Feferman-Vaught theorem for fusions of Λ-Henkin-structures. We will refer to them as Λ-fusion Theorems, even though they will sometimes be formally first stated as corollaries. What we show is, more precisely, that fusion of Λ-Henkin-structures preserve Λ-equivalence for all fixed quantifier-depths.
In order to give inductive proofs for MSO and FO(LFP 1 ), it will be more convenient to consider parametrized Λ-Henkin-structures where the set of set parameters is closed under union, this notion being defined below. This is safe because whenever two parametrized structures (M,Ā,ā) and (N,B,b) are n-Λ-equivalent, it follows trivially that M and N considered together with a subset of this set of parameters are also n-Λ-equivalent.
. Proof. We define a winning strategy for Duplicator in the game out of her winning strategies in the games EF n MSO ((M i ,Ā i ,ā i ), (N i ,B i ,b i )) by induction on n.
Base step: n = 0, doing nothing is a strategy for Duplicator. We need to show that agree on all atomic formulas. Now in the fusion structures, each atomic formula is defined by f in terms of a σ * -quantifier free formula that is evaluated in the corresponding disjoint union structure. So it is enough to show that the disjoint union structures agree on all atomic σ * -formulas and on their Boolean combinations. The initial match between the distinguished objects in (M i ,Ā i ,ā i ) and (N i ,B i ,b i ) is a partial isomorphism for every 1 ≤ i ≤ k, so it is also one for 1≤i≤k M i ,ā 1 , . . . ,ā k and 1≤i≤k N i ,b 1 , . . . ,b k i.e. the two disjoint union structures extended with FO parameters agree on all σ * -atomic formulas. We still need to show that it is also one for 1≤i≤k M i , (Ā 1 , . . . ,Ā k ) ∪ ,ā 1 , . . . ,ā k and 1≤i≤k N i , (B 1 , . . . ,B k ) ∪ ,b 1 , . . . ,b k i.e. the two disjoint union structures extended with FO parameters and the closure under union of set parameters agree on all σ * -atomic formulas. It is enough to point that for every parameter a i j , for every I ⊆ {i 1 , . . . , i m ′ , . . . , k 1 , k m ′ } by construction of i∈I A i in (Ā 1 , . . . ,Ā k ) ∪ , the following are equivalent: Similarly for every parameter b i j , by construction of i∈I B i in (B 1 , . . . ,B k ) ∪ , the following are equivalent: But by Duplicator's winning strategy in the small structure games, we know that the following are equivalent: So the following are also equivalent: So the two extended disjoint union structures agree on all σ * -atomic formulas. Now relying on the semantics of Boolean connectives, it can be shown by induction on the complexity of quantifier free sentences that they also agree on all Boolean combinations of atomic σ * -sentences.
Inductive step: the inductive hypothesis says that whenever Duplicator has a winning strategy in EF n We want to show that this also holds when the length of the games is n + 1. Suppose Duplicator has a winning strategy in the game EF n+1 We describe Duplicator's answer to Spoiler's first move in the game EF n+1 MSO (( f 1≤i≤k M i ,Ā 1 , . . . ,Ā k ,ā 1 , . . . ,ā k ), ( f 1≤i≤k N i ,B 1 , . . . ,B k ,b 1 , . . . ,b k )). It will then follow by induction hypothesis, that he has a winning strategy in the remaining n-length game.
• Spoiler's first move is a point move. Suppose Spoiler picks a in f 1≤i≤k M i . Then a belongs to dom(M i ) for some 1 ≤ i ≤ k. So Duplicator uses his winning strategy in EF n+1 ). By induction hypothesis he also has one in the remaining n-length MSO game between the following two structures: • Spoiler's first move is a set move. Suppose Spoiler chooses a set A in the set of admissible subsets of f 1≤i≤k M i . Then A is necessarily of the form A 1 ∪ . . . ∪ A k , with A i an admissible subset of M i . We now define locally his response B = B 1 ∪ . . . ∪ B k , using his winning strategies in the small structures, so that he still has a winning strategy in By induction hypothesis, he also has one in the remaining n-length MSO game between the following two structures: Now an analogue of this result for disjoint unions can easily be derived as a corollary of Theorem 5.23. For the convenience of the reader, we provide here the detailed argument: a sequence of first-order parameters of the form a i 1 , . . . , a im with m ∈ N andĀ i a sequence of set parameters of the form A i 1 , . . . , A i m ′ with m ′ ∈ N, similarly for theb i andB i ), then Now consider a mapping f such that for every n-ary predicate P ∈ σ * , f (P ) = P x 1 . . . x n . By Theorem 5. 23 we have that  Proof. First note that the following are equivalent: • for some n, there is a finite sequence of parametersā,Ā such that B is defined by a MSO formula ϕ of quantifier depth n usingā,Ā, • for some n, for every two points a, a ′ ∈ dom(M), if they are MSO n-indistinguishable usingā,Ā, then a ∈ B iff a ′ ∈ B. Now suppose for the sake of contradiction that there is Proof. Analogous to the proof of Corollary 5.25 (as A f Let us now consider the FO(TC 1 ) case. As T C moves can only be played when there are already two pebbles on the board, it is more convenient to show first a version of our FO(TC 1 ) fusion theorem in which each small structure comes with at least two parameters. This allows us to define Duplicator's answer to a T C move played in a big structure, by means of his winning strategies in the corresponding small structures. We then derive as a corollary the fusion theorem for non-parametrized structures.
Theorem 5.27 (Fusion Theorem for FO(TC 1 )). Let M i and N i be FO(TC 1 )-Henkin structures, where 1 ≤ i ≤ k. Furthermore, for 1 ≤ i ≤ k, letā i ,b i be sequences of first-order parameters of the form a i 1 , . . . , a im , b i 1 , . . . , b im (where m ∈ N may depend on i), where each sequenceā i (orb i ) contains at least two distinct elements, unless the structure M i (respectively, N i ) has only one element. Whenever Proof. We define a winning strategy for Duplicator in the game out of her winning strategies in the games EF n FO(TC 1 ) ((M i ,ā i ), (N i ,b i )) by induction on n. Base step: n = 0, doing nothing is a strategy for Duplicator. We need to show that the f 1≤i≤k M i ,ā 1 , . . . ,ā k and f 1≤i≤k N i ,b 1 , . . . ,b k agree on all atomic formulas. Now in the fusion structures, each atomic formula is defined by f in terms of a σ * -quantifier free formula that is evaluated in the corresponding disjoint union structure. So it is enough to show that the disjoint union structures agree on all atomic σ * -formulas and on their Boolean combinations. The initial match between the distinguished objects in (M i ,ā i ) and (N i ,b i ) is a partial isomorphism for every 1 ≤ i ≤ k, so it is also one for 1≤i≤k M i ,ā 1 , . . . ,ā k and 1≤i≤k N i ,b 1 , . . . ,b k i.e. the two disjoint union structures agree on all σ * -atomic formulas. Now relying on the semantics of Boolean connectives, it can be shown by induction on the complexity of quantifier free sentences that they also agree on all Boolean combinations of atomic σ * -sentences.
Inductive step: the inductive hypothesis says that whenever Duplicator has a winning strategy in the game EF n FO(TC 1 ) ((M i ,ā i ), (N i ,b i )) for some (M i ,ā i ), (N i ,b i ) satisfying the required conditions on parameters and 1 ≤ i ≤ k, he also has one in the game EF n FO(TC 1 ) (( f 1≤i≤k M i ,ā 1 , . . . ,ā k ), ( f 1≤i≤k N i ,b 1 , . . . ,b k )). We want to show that this also holds whenever the length of the game is n + 1. Suppose Duplicator has a winning strategy in the game EF n+1 FO(TC 1 ) ((M i ,ā i ), (N i ,b i )) for all 1 ≤ i ≤ k. We describe Duplicator's answer to Spoiler's first move in the game EF n+1 ). It will then follow by induction hypothesis, that he has a winning strategy in the remaining n-length game.  a) in dom(M i ), there is a distinguished object inside, but also outside A i , so Duplicator considers A i together with these two parameters and constructs B i by using his winning strategy in EF n+1 , so Duplicator considers any one of these distinguished objects, say a j , and looks at A i \{a j } together with some parameter inside A i . Then he can use his winning strategy in EF n+1 to construct an answer that we call , only distinguished objects exist outside A i , 4 so Duplicator similarly considers some distinguished object a j and looks at A i ∪ {a j } together with some other parameter outside A i , so that he can construct an answer that we call B ′ i by using his winning strategy in EF n+1 . . ∪ B k has been constructed, Spoiler picks two points b ∈ B and b ′ / ∈ B. There are two cases: 1. b and b ′ belong to the domain of one and the same small structure N i ; now dom(M i ) is as previously described in a), b), c) (but not d)), because two distinct points cannot belong to one and the same single point structure) and in each case Duplicator does the following: a) He uses his winning strategy in the game EF n+1 to answer with a, a ′ , so that he still has a winning strategy in EF n FO( ). By induction hypothesis he also has one in the remaining n length game b) Suppose initially that b ′ = b j . Now Duplicator considers A i \{a j } together with a j and some other parameter inside this set. Then he uses his winning strategy in EF n+1 FO(TC 1 ) ((M i ,ā i ), (N i ,b i )) to pick corresponding a, a ′ in M i , so that he still has a winning strategy in EF n FO(TC 1 ) ((M i ,ā i , a, a ′ ), (N i ,b i , b, b ′ )). By induction hypothesis he also has one in the remaining n length game Next, suppose b = b j . Then we choose a = a j . The parameter a j already matches b i.e., Duplicator has a winning strategy in ) that he may use to pick a ′ , thus answering as if it was a point move (i.e., a ′ has to be n-equivalent to b ′ ). Therefore Duplicator still has a winning strategy in . By induction hypothesis he also has one in the remaining n length game This works, except that there is the additional condition a ′ / ∈ A i that Duplicator must also maintain in order to respect the rules of the game. A slightly more refined argument shows, however that there has to be an n-equivalent point to b ′ which is outside A i . Indeed, instead of b, Spoiler could have picked any other point b * ∈ B i together with b ′ / ∈ B i and Duplicator's winning strategy would have provided a correct answer a * ∈ A i , a ′ / ∈ A i , which means that Duplicator would have found some point a ′ which is at least n-equivalent to b ′ and lies outside A i (because if Duplicator has a winning strategy in EF n ) as well, and consequently also in with a j and with some other parameter outside this set and uses his winning strategy in EF n+1 , so that he still has a winning strategy in . By induction hypothesis he also has one in the remaining n length game otherwise b ′ = b j , then a ′ = a j because the parameter a j already matches b ′ i.e., Duplicator has a winning strategy in ), so we can show by a similar argument as above that he can use it to pick a ∈ A i , so that he still has a winning strategy in EF n FO(TC 1 ) ((M i ,ā i , a, a ′ ), (N i ,b i , b, b ′ )). By induction hypothesis he also has one in the remaining n length game we can again use a similar argument to show that Duplicator can use his winning strategy in and EF n+1 FO(TC 1 ) ((M j ,ā j ), (N j ,b j )) to pick a, a ′ in the right part of the structure (that is, inside or outside A i ), so that he still has a winning strategy in the games EF n FO(TC 1 ) ((M i ,ā i , a), (N i ,b i , b)) and EF n FO(TC 1 ) ((M j ,ā j , a ′ ), (N j ,b j , b ′ )) (in the special case where for instance, M j is a single point structure, Duplicator picks the only available point in the other structure). By induction hypothesis he also has one in the 32 A. GHEERBRANT AND B. TEN CATE remaining n length game We now show a corollary of the preceding lemma, in which the small structures do not come with any distinguished objects: Proof. We know that Spoiler's first two moves in the FO(TC 1 )-game of length n + 1 between Similarly, for every j = i such that 1 ≤ j ≤ k, fix some random point a j 1 coming from the domain of M j , Spoiler could have played this point and so Duplicator would have had an adequate answer b j 1 such that (M j , a j 1 ) ≡ n FO(TC 1 ) (N j , b j 1 ). Now for the second round in the game, some point a ′ = a l 2 or b ′ = b l 2 coming from the domain of respectively M l or N l will be played by Spoiler and Duplicator will be able to answer so that (M l , a l 1 , a l 2 ) ≡ n−2 FO(TC 1 ) (N l , b l 1 , b l 2 ). Similarly, for each M j such that j = l, we can find points such that (M j , a j 1 , a j 2 ) ≡ n−2 FO(TC 1 ) (N i , b j 1 , b j 2 ). Now as for all 1 ≤ i ≤ k, Duplicator has a winning strategy in EF n−2 FO(TC 1 ) ((M i , a i 1 , a i 2 ), (N i , b i 1 , b i 2 )), by the previous lemma, he has one in so he also has one in EF n−2 Proof. Analogous to the proof of Corollary 5.26.
In the FO(LFP 1 ) case, the situation parallels the FO(TC 1 ) case. As LF P moves can only be played when there is already one pebble on the board, it is more convenient to show first a version of our FO(LFP 1 ) fusion theorem in which each small structure comes with at least one FO parameter. This allows us to define Duplicator's answer to a LF P move played in the big structure, by means of his winning strategies in the small structures. We then derive as a corollary the fusion theorem for non-parametrized structures.
Theorem 5.32 (Fusion Theorem for FO(LFP 1 )). Letā i ,b i be non empty sequences of firstorder parameters of the form a i 1 , . . . , a im , b i 1 , . . . , b im , with m ∈ N andĀ i ,B i sequences of set parameters of the form Proof. We proceed by induction on n, defining a winning strategy for Duplicator in the game ). Base step: n = 0, doing nothing is a strategy for Duplicator (this can be justified by a similar argument as in the MSO case).
• Spoiler's first move is an ∃ move.
Same argument as for MSO and FO(TC 1 ). • Spoiler's first move is a ∀ move.
Symmetric. • Spoiler's first move is a GFP move.
Suppose Spoiler chooses a set A in the set of admissible subsets of f 1≤i≤k M i with some pebble a i j ∈ A. Then A is necessarily of the form A 1 ∪. . .∪A k , with A i an admissible subset of M i . Her response B = B 1 ∪ . . . ∪ B k can now be defined locally for each B i using her winning strategies in the small structures. So let Spoiler choose A = A 1 ∪ . . . ∪ A k . Keeping in mind that each small structure comes with at least one parameter, there are four cases: 1) in dom(M i ), there is a distinguished object inside A i and A i = dom(M i ), so Duplicator considers A i together with this parameter and constructs B i by using his winning strategy in EF n+1 2) in dom(M i ), there are only distinguished objects outside A i = ∅, so Duplicator considers any a j among those and looks at A i ∪ {a j }, so that he can use his winning strategy in EF n+1 to construct an answer that we call This is a correct answer, because the (posimorphism) condition to be maintained (see Definition 5.20) is that for every pebble a l on the board at the end of the game, a l ∈ A i ⇒ b l ∈ B i . But by Duplicator's winning strategy in EF n+1 , we know already that for every such pebble, a l ∈ A i ∪ {a j } ⇒ b l ∈ B ′ i , so also a l ∈ A i ⇒ b l ∈ B ′ i \{b j }, since the winning conditions will assure that a l = a j if and As pebbles are only chosen using Duplicator's winning strategies in the small structures, the posimorphism condition will be maintained. 4) B i = ∅. So A i = ∅. As no pebble can belong to this set, the posimorphism condition will be maintained. Now that B = B 1 ∪. . .∪B k has been constructed, Spoiler picks a new element b ∈ B which belongs to the domain of one particular small structure N i (so b ∈ B i ) and dom(M i ) is as previously described either in 1, 2 or 3 (but not 4), because b cannot belong to the empty set) and in each case Duplicator does the following: 1) Duplicator answers with a according to his winning strategy in ; 2) Duplicator again considers A i ∪ {a j } and answers according to his winning strategy in EF n+1 . This is safe, because the pebble to be chosen may be assumed to be fresh, so it won't be a j ; 3) Duplicator picks a random pebble a j ∈ dom(M i ) and considers dom(M i )\{a j }. His winning strategy provides him with a correct answer. So in any of these cases (either 1, 2 or 3), Duplicator has a winning strategy in the game . Now for all j = i, 1 ≤ j ≤ k, he also has one in EF n FO(LFP 1 ) ((M j ,Ā j , A j ,ā j ), (N j ,B j , B j ,b j )). So by induction hypothesis, he has one in the remaining n-length FO(LFP 1 ) game between the following two structures: • Spoiler's first move is a LF P move. Symmetric.
Proof. We know that Spoiler's first move in EF n+1 FO(LFP 1 ) ( f 1≤i≤k M i , f 1≤i≤k N i ) must be a FO quantifier move, because the LF P move can only be played once there is a pebble on the board. Let us look at the first move. Suppose Spoiler plays a point a ∈ dom( f 1≤i≤k M i ). So a ∈ dom(M i ) for some 1 ≤ i ≤ k. By Duplicator's winning strategy in EF n FO(LFP 1 ) (M i , N i ), he has an answer b ∈ dom(N i ) such that (M i , a) ≡ n FO(LFP 1 ) (N i , b). Let us rename a with a i and b with b i . Similarly, for every j = i such that 1 ≤ j ≤ k, fix some random point a j coming from the domain of M j , Spoiler could have played this point and so Duplicator would have had an adequate answer b j such that (M j , a j ) ≡ n FO(LFP 1 ) (N j , b j ). Now as for all 1 ≤ i ≤ k, Duplicator has a winning strategy in EF n−1 FO(LFP 1 ) ((M i , a i ), (N i , b i )), by the previous lemma, he has one in EF n−1 FO(LFP 1 ) ( f 1≤i≤k M i , a 1 , . . . , a k ), ( f 1≤i≤k N i , b 1 , . . . , b k )), so he also has one in EF n−1   Proof. Analogous to the proof of Corollary 5.26.

6.
Putting it Together: Completeness on Finite Trees 6.1. Forests and Operations on Forests. In Section 6.2, we will prove that no Λsentence can distinguish Λ-Henkin-models of ⊢ tree Λ from standard models of ⊢ tree Λ . More precisely, we will show that for each n, every definably well-founded Λ-quasi-tree is n-Λequivalent to a finite tree. In order to give an inductive proof, it will be more convenient to consider a stronger version of this result concerning a class of finite and infinite Henkin structures that we call quasi-forests. In this section, we give the definition of quasi-forest and we show how they can be combined into bigger quasi-forests using the notion of fusion from Section 5. Whenever quasi forests are finite, we simply call them finite forests. As a simple example, consider a finite tree and remove the root node, then it is no longer a finite tree. Instead it is a finite sequence of trees, whose roots stand in a linear (sibling) order. 5 It does not have a unique root, but it does have a unique left-most root. For technical reasons it will be convenient in the definition of quasi forests to add an extra monadic predicate R labeling the roots. Definition 6.1 (Λ-quasi-forest). Let T = (dom(T ), <, ≺, P 1 , . . . , . . . P n , A T ) be a Λ-quasitree. Given a node a in T , consider the Λ-substructure of T generated by the set {x | ∃z(a z ∧ z ≤ x)}, which is the set formed by a together with all its siblings to the right and their descendants. The Λ-quasi-forest T a is obtained by labeling each root in this substructure with R (Rx ⇔ def ¬∃y y < x). Whenever T is a tree, we simply call T a a forest.
We will show in our main proof of completeness that for each n and for each node a in a definably well-founded Λ-quasi-tree, the Λ-quasi-forest T a is n-Λ-equivalent to a finite forest. Our proof will use a notion of composition of Λ-quasi-forests which is a special case of fusion. Given a single node forest F 1 and two Λ-quasi-forests F 2 and F 3 , we construct a new Λ-quasi-forest f △ (F 1 , F 2 , F 3 ) by letting the unique element in F 1 be the left-most root, the roots of F 2 become the children of this node and the roots of F 3 become its siblings to the right. We then derive a corollary of the Λ-fusion theorem for compositions of Λ-quasi-forests and use it in Section 6.2.
Definition 6.2. Let σ = {<, ≺, R, P 1 , . . . , P n }, be a relational vocabulary with only monadic predicates except < and ≺. Given three additional monadic predicates Q 1 , Q 2 , Q 3 , we define a mapping f △ from σ to quantifier-free formulas over σ ∪ {Q 1 , Q 2 , Q 3 } by letting Corollary 6.3. Let F 1 be a single node forest and F 2 , F 3 Λ-quasi forests. If F 2 ≡ n Λ F ′ 2 and Figure 6: A composition of forests using the mapping f △ Figure 6 represents a composition of three forests F 1 , F 2 , F 3 which uses the mapping f △ . Only new < ch -arrows are represented, linking the unique node in F 1 to the root nodes in F 2 . But new -links have also been added and the roots in F 3 have became the siblings to the right of the root in F 1 . This is implicitly indicated by the left to right organization of the picture.

Main Proof of Completeness.
Lemma 6.4. For all n ∈ N, every definably well-founded Λ-quasi-tree of finite signature is n-Λ-equivalent to a finite tree. In particular, a Λ-sentence is valid on definably well-founded Λ-quasi-trees iff it is valid on finite trees.

Finite Linear Orders
Let us note that a simplified version of this method can be used in order to show the completeness of MSO, FO(TC 1 ) and FO(LFP 1 ) on finite node-labeled linear orders (i.e., finite node-labeled trees in which every node has at most one child). The relevant simpler axioms are the ones listed in Figures 1, 7 and respectively, Figures 2, 3 and 4.
∃x∀y¬(y < x) there is a root L5.
∀xy(x = y ∨ x < y ∨ y < x) < is total Ind. ∀x(∀y((x < y → ϕ(y)) → ϕ(x)) → ∀xϕ(x) where ϕ(x) ranges over Λ-formulas in one free variable x and x < ch y is shorthand for x < y ∧ ¬∃z(z < y ∧ x < z) In this paper, taking inspiration from Kees Doets [12] we developed a uniform method for obtaining complete axiomatizations of fragments of MSO on finite trees. For that purpose, we had to adapt classical tools and notions from finite model theory to the specificities of Henkin semantics. The presence of admissible subsets called for some refinements in model theoretic constructions such as formation of substructure or disjoint union. Also, we noticed that not every Ehrenfeucht-Fraïssé game that has been used for FO(TC 1 ) was suitable to use on Henkin-structures. We focused on a game which does not seem to have been used previously in the literature. We also established analogues of the FO Feferman-Vaught theorem for MSO, FO(TC 1 ) and FO(LFP 1 ) on Henkin-structures (let us recall that related work for the case of standard structures can be found in [25]). We considered fusions, a particular case of the Feferman-Vaught notion of generalized product and obtained results for Henkin-structures which might be interesting to generalize and use in other contexts. We applied our method to MSO, FO(TC 1 ) and FO(LFP 1 ), but it would be worth also examining other fragments of MSO or logics such as monadic deterministic transitive closure logic (FO(DTC 1 ), which was advocated in [30] as particularly relevant in the context of applications to model-theoretic syntax) or monadic alternating transitive closure logic (FO(ATC 1 )), see also [6].
An important feature of our main completeness argument (the idea of which was borrowed from Kees Doets) is the way we used the inductive scheme of Figure 5. Hence, extending our approach to another class of finite structures would involve finding a comparable scheme. We also know that we should focus on a logic which is decidable on this class, as on finite structures recursive enumerability is equivalent to decidability (as long as the model-checking is decidable). This suggests that other natural candidates would be fragments of MSO on classes of finite structures with bounded treewidth. Finally, let us notice that MSO is also known to be decidable over infinite trees and over linear orders of order type ω. It would be interesting to look for a model-theoretic argument which would work on a Henkin model and produce an intended model of one of these theories in a way comparable to what we did here or to what Keisler did in [20]. Note that related complete axiomatizations of monadic theories of classes of infinite structures can be found in [5], [29] and [31], but that instead of relying on Henkin-semantics, the completeness proofs there are based on automata-theoretic techniques.