1.Introduction
We consider the succinctness of defining words. More precisely, if we allow formulas of size up to n in some logic, we want to know the length of the longest word definable by such formulas.
This question is not very interesting for all formalisms. An example where this is the case is given by regular expressions. There is no smaller regular expression that defines a word than the word itself. This result is spelled out at least in the survey [3]. However, the situation is completely different for monadic second-order logic MSO over words with linear order and unary predicates for the letters. Even though MSO has the same expressive power as regular expressions over words, it is well-known that MSO is non-elementarily more succinct. This follows from the results in the PhD thesis [16] of Stockmeyer. In fact, he proved that the problem whether the language defined by a given star-free generalized regular expression has non-empty complement is of non-elementary complexity with respect to the length of the expression. Since star-free generalized expressions can be polynomially translated into first-order logic FO, it follows that already FO is non-elementarily more succinct than regular expressions. In the article [15], Reinhardt uses a variation of Stockmeyer’s method for proving similar non-elementary succinctness gaps between finite automata and the logics MSO and FO.
In this paper our focus is in the definability of words in MSO and FO. As far as we know, this aspect of succinctness has not been considered previously in the context of words. We show that these logics can define words of non-elementary length via formulas of polynomial size.
In order to argue about definability via formulas of bounded size, we define the size n fragments FO[n] and MSO[n] that include only formulas of size up to n. We also define similar quantifier rank k fragments FOk and MSOk and use them to prove our upper bounds. Both of these types of fragments are essentially finite in the sense that they contain only a finite number of non-equivalent formulas. We call the length of the longest word definable in a fragment the definability number of that fragment. Using this concept, our initial question is reframed as studying the definability numbers of FO[n] and MSO[n].
The definability number of a fragment is closely related to the Löwenheim–Skolem and Hanf numbers of the fragment. The Löwenheim–Skolem number of a fragment is the smallest number m such that each satisfiable formula in the fragment has a model of size at most m. The Hanf number is the smallest number l such that any formula with a model of size greater than l has arbitrarily large models. These were originally defined for extensions of first-order logic in the context of model theory of infinite structures, but they are also meaningful in the context of finite structures. For a survey on Löwenheim–Skolem and Hanf numbers both on infinite and finite structures see [2]. For previous research on finite Löwenheim–Skolem type results see [5] and [6].
We also consider the definability numbers of quantifier rank k fragments of first-order logic with two variables FO2. In the context of words, the number of variables is an important parameter for first-order logic. Over words, three variables suffice to define any first-order definable property [9]. On the other hand, one variable offers very limited expressive power. Thus, two variables is naturally a very interesting and well-studied case. The expressive power of two variables over words has been shown to be the same as unary temporal logic [4] as well as one quantifier alternation in FO [17]. By combining the results of [17] with those of [14], we see that two variables also corresponds to unambiguous regular languages.
Aside from what we have already mentioned, related work includes the article [12] of Pikhurko and Verbitsky, where they consider the complexity of single finite structures. They study the minimal quantifier rank in FO of both defining a single finite structure and separating it from other structures of the same size. In [11] the same authors and Spencer consider quantifier rank and formula size required to define single graphs in FO. The survey [13] by Pikhurko and Verbitsky covers the above work and more on the logical complexity of single graphs in FO. By logical complexity they mean minimal quantifier rank, number of variables and length of a defining formula as functions of the size of the graph. They give an extensive account of these measures and relate them to each other, the Ehrenfeucht–Fraïssé game and the Weisfeiler–Lehman algorithm. An important difference between our approach and theirs is that we take formula size as the parameter and look for the longest definable word, whereas they do the opposite.
Our contributions are upper and lower bounds for the definability, Löwenheim–Skolem and Hanf numbers of the size n fragments of FO and MSO on words. The upper bounds in Section 3 are obtained by counting types with respect to the quantifier rank n/2 fragment. The upper bounds for both FO and MSO are expressions containing exponential towers of height n/2+2. The lower bounds in Sections 4 and 5 are given by concrete polynomial size formulas that define words of non-elementary length based on the cumulative hierarchy of sets. The lower bounds are exponential towers of height n/c5 for FO and n/c for MSO, respectively.
An anonymous referee pointed out that lower bounds similar to ours can be obtained by adapting the method used by Reinhardt in [15], which in turn is based on the work of Stockmeyer [16]. However, our formulas are based on the cumulative hierarchy of sets instead of the binary counters used in Stockmeyer and Reinhardt. Furthermore, we emphasize defining single words and relate the bounds to Löwenheim–Skolem and Hanf numbers.
Note that our results only apply in the context of words. If finite structures over arbitrary finite vocabularies are allowed, then there are no computable upper bounds for the Löwenheim–Skolem or Hanf numbers of the size n fragments of FO. For the Löwenheim–Skolem number, this follows from Trakhtenbrot’s theorem11 (see, e.g., [10]), and for the Hanf number, this follows from a result of Grohe in [5]. Clearly the same applies for the size n fragments of MSO as well.
This paper is an extended version of the conference contribution [7]. In this version we have obtained tighter upper bounds on the numbers of types and thus definability numbers of FO and MSO in Section 3. For FOk, the upper bound in [7] was tower(k+1,k2+k), using the modified exponential tower notation defined in this version. The new bound of tower(k+2) gets rid of the polynomial on top of the tower and introduces a square root. For MSOk the bound in [7] was tower(k+1,(k+1)2). The new bound of 14tower(k+1,k+2)3 reduces the top polynomial to a linear one and introduces a third root. In addition, we have added the entirely new Section 6, where we investigate the definability numbers of two variable logics FOk2.
2.Preliminaries
The logics we consider in this paper are first-order logic FO and monadic second-order logic MSO and their (typically finite) fragments. The syntax and semantics of these are standard and well known. We direct the reader to [1] and [10] for in-depth introductions of these logics. In terms of structures we limit our consideration to words of the two letter alphabet Σ={a,b}.
When we say that a word satisfies a logical sentence, we mean the natural corresponding word model does. A word model is a finite structure with linear order and unary predicates Pa and Pb for the two symbols. Since we only consider words over the two letter alphabet Σ, we will tacitly assume that all formulas of MSO are in the vocabulary {<,Pa,Pb} of the corresponding word models (and similarly for FO-formulas). We denote the length of a word w∈Σ∗ by |w|. We will also assume that all word models w with |w|=n have domain [n]:={1,…,n}. We will use the notation [n] also elsewhere.
For w∈Σ∗ and a∈Σ, an a-chain is a maximal subword of w that consists of consecutive letters a. Since we operate on the two letter alphabet {a,b}, we have a-chains and b-chains, which we also collectively refer to as chains. For example, the word aabbba consists of three chains: two a-chains of lengths 2 and 1, with a b-chain of length 3 in between.
To work with formulas of FO and MSO with free variables, we define the notion of an (r,s)-interpretation (w,P¯,p¯), where w∈Σ∗, P¯=(P1,…,Pr) is a tuple of sets of points in w, and p¯=(p1,…,ps) is a tuple of points in w. Naturally if w is the empty word ε, then s=0 and no points can be interpreted. For a formula φ∈MSO with second-order variables X¯=(X1,…,Xr) and first-order variables x¯=(x1,…,xs), we also define the truth relation (w,P¯,p¯)⊧φ as w⊧φ[P¯/X¯,p¯/x¯], where the operator / denotes interpreting the variables on the right as the values on the left. For FO we similarly define s-interpretations (w,p¯) and the truth relation (w,p¯)⊧φ.
Definition 2.1.
The size sz(φ) of a formula φ∈MSO is defined recursively as follows:
For
n∈N the size
n fragment of
MSO, denoted
MSO[n], consists of the formulas of
MSO with size at most
n. Size as well as size
n fragments are defined in the same way for
FO.
Definition 2.2.
The quantifier rank qr(φ) of a formula φ∈MSO is defined recursively as follows:
qr(φ)=0 for atomic φ,
qr(¬ψ)=qr(ψ),
qr(ψ∧θ)=qr(ψ∨θ)=max{qr(ψ),qr(θ)},
qr(∃xψ)=qr(∀xψ)=qr(∃Uψ)=qr(∀Uψ)=qr(ψ)+1.
For
k∈N, the quantifier rank
k fragment of
MSO, denoted
MSOk, consists of the formulas
φ∈MSO with
qr(φ)⩽k. The quantifier rank
k fragment of
FO is defined in the same way and denoted
FOk.
Note that both size n fragments and quantifier rank k fragments are essentially finite in the sense that they contain only finitely many non-equivalent formulas.
Definition 2.3.
For each (finite) fragment L of MSO or FO, we define the relation ≡L on nonempty Σ-words as
w≡Lv,if w and v agree on all L-sentences.
Clearly ≡L is an equivalence relation on Σ+. We denote the set Σ+/≡L of equivalence classes of ≡L shortly by Σ+/L and define a notation for the number of these classes.
Definition 2.4.
For each (finite) fragment L of MSO or FO, we denote the number of equivalence classes of ≡L by NL, i.e.
NL:=|Σ+/L|.
Note that each equivalence class of ≡L is uniquely determined by a subset tpL(w)={φ∈L|w⊧φ} of L-sentences, which we call the L-type of w.
For quantifier rank fragments FOk and MSOk we define similar concepts also for formulas with free variables.
Definition 2.5.
We define the relation ≡MSOk on (r,s)-interpretations as
(w,P¯,p¯)≡MSOk(v,Q¯,q¯),if (w,P¯,p¯) and (v,Q¯,q¯) agree on all MSOk formulaswith free variables X¯=(X1,…,Xr) and x¯=(x1,…,xs).
The relation
≡FOk is defined in the same way for
s-interpretations.
The set of equivalence classes of ≡MSOk over (r,s)-interpretations is denoted by Mkr,s and the number of these classes is denoted by Mkr,s=|Mkr,s|. Furthermore, the set of equivalence classes of ≡FOk over s-interpretations is denoted by Fks and the number of these classes is denoted by Fks=|Fks|.
Note that Mk0,0=NMSOk+1 and Fk0=NFOk+1, since the empty word ε is taken into account in Mk0,0 and Fk0, but not in NMSOk and NFOk.
We also consider two-variable first order logic FO2. The syntax and semantics of this logic are defined identically to FO with the exception that only two variables, x and y, are used. For some of the proofs we utilize a standard Ehrenfeucht–Fraïssé or pebble game found in the literature, see [1,10]. The game has two players, whom we call Spoiler and Duplicator. The parameters of the game are the quantifier rank k∈N and two word models w and v.
The two-pebble EF-game is denoted by GFOk2(w,v). The game is played for k rounds and features two pairs of pebbles that start the game off the board. In each round, Spoiler picks up one of either pair of pebbles and moves it on a point p in w or q in v. Duplicator responds by moving the other pebble of the pair to a point q in v or p in w, respectively. After a round, let p1, p2 and q1, q2 be the points with pebbles on them. Duplicator wins if after each round, the map (p1,p2)↦(q1,q2) is a partial isomorphism between w and v. Otherwise Spoiler wins.
The game GFOk2(w,v) characterizes the equivalence of structures for FO2 formulas up to quantifier rank k. Using our notation of quantifier rank fragments, we get the following theorem.
Theorem 2.6.
Duplicator has a winning strategy for GFOk2(w,v) if and only if w≡FOk2v.
In order to discuss words of non-elementary length and make our bounds precise, we define the exponential tower function tower(n) as well as the modified exponential tower function tower(k,ℓ), where the number ℓ is on top of the tower. Note that the modified exponential tower is essentially one level higher than the ordinary one since the 1 on top of the ordinary tower is not considered for the height.
Definition 2.7.
The exponential tower function tower:N→N is defined recursively by setting tower(0):=1 and tower(n+1):=2tower(n). The modified exponential tower function tower(k,ℓ):N×N→N is defined recursively by setting tower(0,ℓ):=ℓ and tower(n+1,ℓ):=2tower(n,ℓ).
2.1.Definability, Löwenheim–Skolem and Hanf numbers
Löwenheim–Skolem and Hanf numbers were originally introduced for studying the behaviour of extensions of first-order logic on infinite structures. See the article [2] of Ebbinghaus for a nice survey on the infinite case. As observed in [5], with suitable modifications, it is possible to give meaningful definitions for these numbers also on finite structures. We will now give such definitions for finite fragments L of FO and MSO, and in addition, we introduce the closely related definability number of L.
Definition 2.8.
We say that a sentence φ∈MSO defines a word w∈Σ+ if w⊨φ and v⊭φ for all v∈Σ+∖{w}. For a fragment L of MSO or FO, we denote by Def(L) the set of words definable in L, i.e.
Def(L):={w∈Σ+| there is φ∈L s.t. φ defines w}.
Let φ be a sentence in MSO over Σ-words. If it has a model, we denote by μ(φ) the minimal length of a model of φ: μ(φ)=min{|w||w∈Σ+,w⊧φ}. If φ has no models, we stipulate μ(φ)=0. Furthermore, we denote by ν(φ) the maximum length of a model of φ, assuming the maximum is well-defined. If the maximum is not defined, i.e., if φ has no models or has arbitrarily long models, we stipulate ν(φ)=0.
Definition 2.9.
Let L be a finite fragment of MSO or FO with Def(L)≠∅.
(a) The definability number of L is DN(L)=max{|w||w∈Σ+,w∈Def(L)}.
(b) The Löwenheim–Skolem number of L is LS(L)=max{μ(φ)|φ∈L}.
(c) The Hanf number of L is H(L)=max{ν(φ)|φ∈L}.
Thus, DN(L) is the length of the longest L-definable word. Note further that LS(L) is the smallest number m such that every φ∈L that has a model, has a model of length at most m. Similarly H(L) is the smallest number ℓ such that if φ∈L has a model of length greater than ℓ, then it has arbitrarily long models.
Since every sentence φ of MSO defines a regular language over Σ, and there is an effective translation from MSO to equivalent finite automata, it is clear that we can compute the numbers μ(φ) and ν(φ) from φ. Consequently, for any finite fragment L of MSO, LS(L) and H(L) can be computed from L.
As we mentioned in the Introduction, LS(FO[n]) and H(FO[n]) are not computable from n if we consider arbitrary finite models instead of words. Clearly the same holds also for the fragments FOk, MSO[n] and MSOk.
It follows immediately from Definition 2.9 that the definability number of any finite fragment of MSO is bounded above by its Löwenheim–Skolem number and its Hanf number:
Proposition 2.10.
If L is a finite fragment of MSO, then DN(L)⩽LS(L),H(L).
Proof.
It suffices to observe that if w∈Def(L), then μ(φ)=ν(φ)=|w|, where φ∈L is the sentence that defines w. □
Note that all three cases for the relationship between LS(L) and H(L) are possible. In fact, for any positive integers m and n there is a finite fragment L of FO such that LS(L)=m and H(L)=n, as we show in the next example.
Example 2.11.
Let ψm be the sentence ∃x1…∃xm⋀1⩽i<j⩽m¬xi=xj, and let θn be the sentence ∀x1…∀xn+1⋁1⩽i<j⩽n+1xi=xj. Then clearly μ(ψm)=m, ν(ψm)=0, μ(θn)=1, and ν(θn)=n. Thus, LS(L)=m and H(L)=n for the fragment L:={ψm,θn}.
3.Numbers of types and upper bounds
In this section we estimate the number of types for quantifier rank fragments FOk and MSOk. Using these estimates we obtain upper bounds for definability numbers, Löwenheim–Skolem numbers and Hanf numbers of both quantifier rank k fragments and size n fragments FO[n] and MSO[n].
3.1.Definability and types
To count types we must work with (r,s)-interpretations. Let (w,P¯,p¯) be an (r,s)-interpretation and let (v,Q¯,q¯) be an (r,s′)-interpretation. We assume these interpretations have the same second-order variables and no common first-order variables. We define the catenation of (w,P¯,p¯) and (v,Q¯,q¯) as the (r,s+s′)-interpretation (w,P¯,p¯)·(v,Q¯,q¯)=(wv,P∪Q′‾,p¯q¯′), where (P∪Q′)i=Pi∪Qi′, Qi′={q+|w||q∈Qi} and qi′=qi+|w| for each i∈[s′]. Note that for interpretations with different second-order variables we can interpret all missing variables as empty sets before applying this definition.
It is well-known that equivalence of words up to a quantifier rank is preserved in catenation. We formulate this for formulas with free variables:
Theorem 3.1.
Let L∈{FOk,MSOk} for some k∈N.
If(w,P¯,p¯)≡L(w′,P¯′,p¯′)and(v,Q¯,q¯)≡L(v′,Q¯′,q¯′),then(w,P¯,p¯)·(v,Q¯,q¯)≡L(w′,P¯′,p¯′)·(v′,Q¯′,q¯′).
In particular, if w≡Lw′ and v≡Lv′, then wv≡Lw′v′.Proof.
The claim is proved by a straightforward Ehrenfeucht-Fraïssé game argument similarly to Proposition 3.1.4 in [1]. □
Using Theorem 3.1, we get the following upper bounds for the numbers μ(φ) and ν(φ) in terms of the quantifier rank of φ:
Proposition 3.2.
Let L∈{FOk,MSOk} for some k∈N. If φ is a sentence of L, then μ(φ),ν(φ)⩽NL.
Proof.
If |w|⩽NL for all words w∈Σ+ such that w⊧φ, the claim is trivial. Assume then that w⊧φ and |w|>NL. Then there are two initial segments u and u′ of w such that |u|<|u′| and u≡Lu′. Let v and v′ be the corresponding end segments, i.e., w=uv=u′v′. Then by Theorem 3.1, uv′≡Lu′v′=w, and similarly u′v≡Luv=w, and hence uv′⊧φ and u′v⊧φ.
Since |uv′|<|w|, we see that w is not the shortest word satisfying φ. The argument applies to any word w with |w|>NL, and hence we conclude that μ(φ)⩽NL. On the other hand |u′v|>|w|, and hence w is neither the longest word satisfying φ. Applying this argument repeatedly, we see that φ is satisfied in arbitrarily long words, and hence ν(φ)=0⩽NL. □
From Propositions 2.10 and 3.2 we immediately obtain the following upper bound for the definability numbers of quantifier rank fragments of MSO:
Corollary 3.3.
Let k∈N and L∈{FOk,MSOk}. Then LS(L),H(L)⩽NL, and consequently DN(L)⩽NL.
This NL upper bound for the definability, Löwenheim–Skolem and Hanf numbers shows that the quantifier rank fragments L of FO and MSO behave quite tamely on words: Clearly every union of equivalence classes of ≡L is definable by a sentence of L and every sentence defines a union of equivalence classes. Hence the number of non-equivalent sentences in L is 2NL. Thus, any collection of representatives of non-equivalent sentences of L necessarily contains sentences of size close to NL. However, in spite of this, it is not possible to define words that are longer than NL by sentences of L.
This shows that quantifier rank is not a good starting point if we want to prove interesting succinctness results for definability. Hence we turn our attention to the size n fragments FO[n] and MSO[n]. Note first that for any n∈N, FO[n] is trivially contained in FOn, and similarly, MSO[n] is contained in MSOn. A simple argument shows that this can be improved by a factor of 2:
Lemma 3.4.
For any n∈N, FO[2n]⩽FOn and MSO[2n]⩽MSOn.
Proof.
Let φ∈FO[2n] with qr(φ)⩾n+1. Thus at least n+1 of the size of φ comes from quantifiers, leaving at most n−1 for the rest of the formula. We may assume all variables are different. For n+1 variables to occur at least once in an atomic subformula of φ, it would take at least (n+1)/2 atomic formulas x<y and (n+1)/2−1 connectives ∧ or ∨ between them. In total, this would require φ to be of size at least 2n+1. Thus, only n variables of φ occur in some atomic formula. Removing the quantifications of the rest of the variables gives an equivalent formula of quantifier rank n.
The same argument works for MSO as second-order variables P must also occur in atomic formulas P(x) to have an effect on the semantics of the formula. □
Note that we have not tried to be optimal in the formulation of Lemma 3.4. We believe that with a more careful analysis, 2n could be replaced with 3n, and possibly with an even larger number.
Corollary 3.5.
For any n∈N, DN(FO[2n]),LS(FO[2n]),H(FO[2n])⩽NFOn=Fn0−1 and DN(MSO[2n]),LS(MSO[2n]),H(MSO[2n])⩽NMSOn=Mn0,0−1.
3.2.Number of FOk-types
As we have seen in the previous subsection, the numbers of FOk-types and MSOk-types give upper bounds for the corresponding definability, Löwenheim–Skolem and Hanf-numbers. It is well known that on finite relational structures, for FOk this number is bounded above by an exponential tower of height k+1 with a polynomial, that depends on the vocabulary, on top (see, e.g., [13] for the case of graphs). It is straightforward to generalize this type of upper bound to MSOk. In this subsection and the next one, we carry out a more careful analysis and obtain tighter bounds on the class of Σ-words.
Recall that Fk0 denotes the number of ≡FOk-types of Σ-words w, where we include the case w=ε. To obtain upper bounds for Fk0, we also need to consider the number Fk1 of ≡FOk-types of 1-interpretations (w,p). We start by showing that FOk-equivalence of 1-interpretations reduces to FOk-equivalence of corresponding initial and end segments of the words, and FOk+1-equivalence of words reduces to FOk-equivalence of 1-interpretations arising from the words.
Let w=a1…aℓ be a Σ-word, and let p∈[ℓ]. We denote the initial segment a1…ap−1 of w by w<p and the end segment ap+1…aℓ by w>p. Furthermore, we denote the single letter word ap by w(p).
Lemma 3.6.
Assume that k∈N, w∈Σℓ, v∈Σm, p∈[ℓ], and q∈[m]. Then
(a) (w,p)≡FOk(v,q) if and only if w<p≡FOkv<q, w>p≡FOkv>q, and w(p)=v(q).
(b) w≡FOk+1v if and only if for every p∈[ℓ] there is q∈[m] such that (w,p)≡FOk(v,q), and vice versa, for every q∈[m] there is p∈[ℓ] such that (w,p)≡FOk(v,q).
Proof.
(a) Assume first that the conditions
hold. Then
(w,p)=w<p·(w(p),1)·w>p,
(v,q)=v<q·(v(q),1)·v>q, and trivially
(w(p),1)≡FOk(v(q),1), and hence by Theorem
3.1,
(w,p)≡FOk(v,q).
On the other hand, if w<p≢FOkv<q, then w<p⊧φ and v<q⊭φ for some sentence φ∈FOk. This means that (w,p)⊧ψ(x) and (v,q)⊭ψ(x), where ψ(x) is the relativization of φ to the set of elements smaller than x, i.e., ψ(x) is obtained from φ by replacing each existential subformula ∃yθ by ∃y(y<x∧θ), and each universal subformula ∀yθ by ∀y(y<x→θ). Since the quantifier rank of ψ is the same as that of φ, we see that (w,p)≢FOk(v,q). Similarly, if w>p≢FOkv>q, then (w,p)≢FOk(v,q). It is also immediately clear that if w(p)≠v(q), then (w,p)≢FOk(v,q). Thus, if (∗) does not hold, then (w,p)≢FOk(v,q).
Claim (b) is just the standard back-and-forth characterization for ≡FOk+1 (see [1] Theorem 2.3.3). □
We consider next the number of equivalence classes of words with respect FO0, FO1 and FO2. In the proof of the following lemma, we denote the set of letters α∈Σ that occur in a word w∈Σ∗ by l(w). Thus, e.g., l(aa)={a} and l(abba)={a,b}.
Lemma 3.7.
F00=1, F10=4, and F20⩽97.
Proof.
Clearly all words are equivalent with respect to FO0, as there are no quantifier-free sentences. Hence F00=1. Furthermore, it is easy to see that two words w,v∈Σ∗ are equivalent with respect to FO1 if and only if l(w)=l(v). Thus, F10=|P(Σ)|=4. (Note that ∅ corresponds to the equivalence class containing only the empty word.)
To prove that F20⩽97 we give a list of 97 Σ-words, and show that every word w∈Σ∗ is FO2-equivalent with one of the words in the list. We list the words in groups based on the total number of chains.
(0) the empty word ε (the unique word without a- or b-chains)
(1) ar and br for r∈[3]
(2) arbs and bras for r,s∈[3]
(3) arbsat and brasbt for r,t∈[2] and s∈[3]
(4) arbsatbu and brasbtau for r,s,t,u∈[2]
(5) arbsabat and brasbabt for r,s,t∈[2].
Clearly group (1) contains 6 words, group (2) contains 18 words, group 3 contains 24 words, group (4) contains 32 words, and group (5) contains 16 words. Thus there are
1+6+18+24+32+16=97 words in the list.
Our goal is now to prove that for any w∈Σ∗ there is a word v in the list such that w≡FO2v. We divide the proof into cases according to the total number of chains in w. By the obvious symmetry, we can omit cases where the first letter of w is b.
In the proof we use the following observations. By Lemma 3.6, to prove that w∈Σℓ and v∈Σm are FO2-equivalent it suffices to show that there is a relation R⊆[ℓ]×[m] such that dom(R)=[ℓ], ran(R)=[m], and the condition
holds for any pair
(p,q)∈R. We say that the relation is
total on w and v if
dom(R)=[ℓ] and
ran(R)=[m].
Moreover, as noted above, two words w′ and v′ are FO1-equivalent if an only if l(w′)=l(v′). Thus, the condition (∗) above can be replaced with the condition
Assume now that w∈Σ∗. We have the following cases based on the number of chains in w.
(0) The case w=ε is trivial.
(1) Assume that w=ak for some k⩾1. If k⩽3, then w is in the list, and hence the claim holds. If k>3, we let v=a3. Then the following hold:
(a) w(p)=v(q)=a for all p∈[k] and q∈[3],
(b) for any p∈[k], w<p=ap−1 and w>p=ak−p,
(c) for any q∈[3], v<q=aq−1 and v>q=a3−q.
(2) Assume next that w=akbℓ for some k,ℓ⩾1. Let v=arbs, where r=min{k,3} and s=min{ℓ,3}. Then v is in group (2), and by case (1), ak≡FO2ar and bℓ≡FO2bs. Hence w≡FO2v follows from Theorem 3.1.
(3) Assume then that w=akbℓam for some k,ℓ,m⩾1. Let v=arbsat, where r=min{k,2}, s=min{ℓ,3} and t=min{m,2}. Then v is in group (3). Let R⊆[k+ℓ+m]×[r+s+t] consist of pairs (p,q) of points that are in corresponding positions in corresponding chains, i.e., R=R1∪R2∪R3, where
R1={(1,1)}∪{(p,r)|1<p⩽k},
R2={(k+1,r+1),(k+ℓ,r+s)}∪{(p,r+2)|k+1<p<k+ℓ},
R3={(k+ℓ+m,r+s+t)}∪{(p,r+s+1)|k+ℓ<p<k+ℓ+m}.
Clearly R is total on w and v. We show now that (⋆) holds for all pairs in R. For all pairs (p,q)∈R it is obvious that w(p)=v(q), as R respects the correspondence between chains. For the pair (1,1)∈R1 we have l(w<1)=l(v<1)=∅ and l(w>1)=l(v>1)={a,b}. For pairs (p,r) in the second part of R1 we have l(w<p)=l(v<r)={a} and l(w>p)=l(v>r)={a,b}; these are also the values of l(w<p), l(v<q), l(w>p), l(v>q) for the first pair (p,q)=(k+1,r+1) in R2, unless ℓ=s=1, in which case l(w>p)=l(v>q)={a}. The case (p,q)=(k+ℓ,r+s) is symmetric to the previous one, and for pairs (p,q) in the second part of R2 we have l(w<p)=l(v<q)=l(w>p)=l(v>q)={a,b}. Finally, the pairs in R3 are handled symmetrically to those in R1.
(4) Assume then that w=akbℓambn for some k,ℓ,m,n⩾1. Let v=arbsatbu, where r=min{k,2}, s=min{ℓ,2}, t=min{m,2} and u=min{n,2}. Then v is in group (4). Using the same idea as in case (3), we relate the first points in the first chains ak and bℓ with the first elements of ar and bs, respectively, and the rest of the points in these chains (if any) with the second elements in ar and bs. The points in the last two chains am, bn, at and bu are related in a symmetric way. Thus, we define R=R1∪R2∪R3∪R4⊆[k+ℓ+m+n]×[r+s+t+u] by setting
R1={(1,1)}∪{(p,r)|1<p⩽k},
R2={(k+1,r+1)}∪{(p,r+s)|k+1<p⩽k+ℓ},
R3={(k+ℓ+m,r+s+t)}∪{(p,r+s+1)|k+ℓ<p<k+ℓ+m},
R4={(k+ℓ+m+n,r+s+t+u)}∪{(p,r+s+t+1)|k+ℓ+m<p<k+ℓ+m+n}.
(5) Assume then that w=akbℓambnao for some k,ℓ,m,n,o⩾1. This time we let v=arbsabat, where r=min{k,2}, s=min{ℓ+n−1,2}, and t=min{o,2}. Then v is in group (5). We define again relations R1, R2, R3, R4 and R5 between the corresponding chains with a similar idea as in the previous cases:
R1={(1,1)}∪{(p,r)|1<p⩽k},
R2={(k+1,r+1)}∪{(p,r+s)|k+1<p⩽k+ℓ},
R3={(p,r+s+1)|k+ℓ<p⩽k+ℓ+m},
R4={(k+ℓ+m+n,r+s+2)},
R5={(k+ℓ+m+n+o,r+s+2+t)}∪{(p,r+s+3)|k+ℓ+m+n<p<r+s+2+t}.
(6+) Assume then that w=ak1bℓ1…akebℓe, where e⩾3 and ki,ℓi⩾1 for all i∈[e]. By case (4), it suffices to show that w≡FO2w′, where w′=ak1bmanbℓe, m=ℓ1+⋯+ℓe−1 and n=k2+⋯+ke. To show this we let R be the bijection that maps the j-th a in w to the j-th a in w′ and the j-th b in w to the j-th b in w′. Then R is total on w and w′, and it is easy to verify that (⋆) holds for all pairs (p,q)∈R.
The case in which w is of the form ak1bℓ1…akebℓeake+1 for some e⩾3 is handled in the same way by reducing to case (5).
□
Remark 3.8.
In fact we can show that all the words listed in (0)–(5) in the proof above are non-equivalent, and thus F20=97. We did not include the straightforward (but tedious) proof here, as we only need the upper bound.
Lemma 3.7 serves as the basis in proving a recursive upper bound for the numbers Fk0 in Theorem 3.11. In the next two lemmas, we provide the recursion formula for these numbers needed in the induction step.
Lemma 3.9.
For any k∈N, Fk1=2(Fk0)2.
Proof.
Let w∈Σℓ, v∈Σm, p∈[ℓ], and q∈[m]. By Lemma 3.6(a), (w,p)≡FOk(v,q) if and only if w<p≡FOkv<q, w>p≡FOkv>q, and w(p)=v(p). Clearly this means that there is a one-to-one correspondence between the set Fk1 and the set Fk0×Σ×Fk0, and consequently we get Fk1=|Fk0×Σ×Fk0|=2(Fk0)2. □
Let w be a Σ-word with |w|=ℓ. We denote the set of all ≡FOk-equivalence classes of pairs (w,p), p∈[ℓ], by Fk1(w). Note that Fk1(w)⊆Fk1.
Lemma 3.10.
For any k∈N, Fk+10⩽22(Fk0)2.
Proof.
Let w and v be Σ-words. It follows from Lemma 3.6(b) that if Fk1(w)=Fk1(v), then w≡FOk+1v. In other words, the FOk+1-type of w is uniquely determined by the set Fk1(w)⊆Fk1. Hence Fk+10⩽|P(Fk1)|=2Fk1=22(Fk0)2. □
Theorem 3.11.
For any k∈N, Fk0⩽tower(k+2). Hence also NFOk=Fk0−1⩽tower(k+2).
Proof.
By Lemma 3.7, F00=1 and F10=4. On the other hand, tower(2)=4=2 and tower(3)=16=4. Hence the claim holds for k=0 and k=1.
For k⩾2, we prove the stronger claim
by induction on
k. In the case
k=2 we have
Fk0⩽97 by Lemma
3.7, and
12tower(k+2)−1=12216−1=27−1=127, and hence
(‡) holds.
Assume then that k⩾2, and the claim (‡) holds for k. Using Lemma 3.10 we get the following estimates:
Fk+10⩽22(Fk0)2⩽212tower(k+2)−2tower(k+2)+2⩽212tower(k+2)−2=14(2tower(k+2))12⩽12tower(k+3)−1.
Thus, the claim
(‡) holds for
k+1. □
As a corollary to the above result on the number of types, we obtain upper bounds on the definability, Löwenheim–Skolem and Hanf numbers of FOk.
Corollary 3.12.
For any k∈N, DN(FOk),LS(FOk),H(FOk)⩽tower(k+2).
Via Corollary 3.5 we obtain similar upper bounds for the same numbers of size n fragments FO[n].
Corollary 3.13.
For any n∈N, DN(FO[n]),LS(FO[n]),H(FO[n])⩽tower(n/2+2).
3.3.Number of MSOk-types
In this subsection we prove an upper bound for the number of MSOk-types of Σ-words. Recall that we denote by Mkr,0 the number of MSOk-types of interpretations of the form (w,P1,…,Pr), and by Mkr,1 the number of MSOk-types of interpretations (w,P1,…,Pr,p). We proceed with similar steps as in the previous subsection: we compute first the numbers M0r,0 and M1r,0. Then we prove a recursion formula for Mk+1r,0 in terms of Mkr+1,0. This proof is based on reducing Mkr,1 to Mkr,0 and Mk+1r,0 to Mkr+1,1, in analogue with Lemmas 3.9 and 3.10.
Lemma 3.14.
For any r∈N, M0r,0=1 and M1r,0=22r+1.
Proof.
All (r,0)-interpretations (w,B¯) are equivalent with respect to MSO0, as there are no formulas that do not contain any first-order variables. Hence M0r,0=1.
To prove the second claim, we introduce first some auxiliary notions. Let (w,P¯,p)=(w,P1,…,Pr,p) be an (r,1)-interpretation. The atomic profile of p in (w,P¯) is pr(w,P¯,p):={i∈[r+1]|p∈Pi}, where Pr+1:=Pa. Note that here the letter a is treated via the predicate Pa and the letter b is then handled as the complement of Pa. Furthermore, the total atomic profile of (w,P¯) is Pr(w,P¯):={pr(w,P¯,p)|p∈[ℓ]}, where ℓ=|w|.
Observe now that two (r,0)-interpretations (w,P¯) and (v,Q¯) cannot be separated in MSO1 by any formula starting with a second-order quantifier. Thus, (w,P¯) and (v,Q¯) are equivalent with respect to MSO1 if and only if for every p in w there is q in v (and vice versa, for every q in v there is p in w) such that (w,P¯,p)≡MSO0(v,Q¯,q). Clearly (w,P¯,p)≡MSO0(v,Q¯,q) holds if and only if pr(w,P¯,p)=pr(v,Q¯,q). Thus we see that (w,P¯)≡MSO1(v,Q¯) if and only if Pr(w,P¯)=Pr(v,Q¯). In other words, the set Pr(w,P¯)⊆P([r+1]) uniquely determines the ≡MSO1-equivalence class of (w,P¯). Note further that for any subset X⊆P([r+1]) there exists an (r,0)-interpretation (w,P¯) such that Pr(w,P¯)=X. Thus we conclude that M1r,0=|P(P([r+1]))|=22r+1. □
We prove next the analogue of Lemma 3.9 for MSOk. In the proof we use the following notation: if (w,P¯)=(w,P1,…,Pr) is an (r,0)-interpretation and p∈[ℓ] for ℓ=|w|, then P<p,i:=Pi∩[p−1] for each i∈[r], and P¯<p=(P<p,1,…,P<p,r). The notations P>p,i and P¯>p are defined analogously.
Lemma 3.15.
For any k,r∈N, Mkr,1=2r+1(Mkr,0)2.
Proof.
Assume that (w,P¯,p) and (v,Q¯,q) are (r,1)-interpretations. With a similar argument as in the proof of Lemma 3.6(a), we see that (w,P¯,p)≡MSOk(v,Q¯,q) if and only if the condition
(†)(w<p,P¯<p)≡MSOk(v<q,Q¯<q),(w>p,P¯>p)≡MSOk(v>q,Q¯>q),w(p)=v(q),and{i∈[r]|p∈Pi}={i∈[r]|q∈Qi}
holds. Thus, we see that there is a one-to-one correspondence between the sets
Mkr,1 and
Mkr,0×Σ×P([r])×Mkr,0, and hence
Mkr,1=2·|P([r])|·(Mkr,0)2=2r+1(Mkr,0)2. □
Next we prove the recursion formula for the numbers Mkr,0; note that while the subscript k+1 reduces to k on the right hand side, the superscript r increases to r+1. Fortunately this is not a problem, as we will see in the proof of Theorem 3.17.
Let (w,P¯) be an (r,0)-interpretation with |w|=ℓ. We denote the set of all ≡MSOk-equivalence classes of (r,1)-interpretations (w,P¯,p), p∈[ℓ], by Mkr,1(w,P¯) and the set of all ≡MSOk-equivalence classes of (r+1,0)-interpretations (w,P¯Q), Q⊆[ℓ], by Mkr+1,0(w,P¯). Note that Mkr,1(w,P¯)⊆Mkr,1 and Mkr+1,0(w,P¯)⊆Mkr+1,0.
Lemma 3.16.
For any k⩾1, Mk+1r,0⩽2(Mkr+1,0)3.
Proof.
Let (w,P¯) and (v,Q¯) be interpretations, where |w|=ℓ and |v|=m. Using again the standard back-and-forth argument, (w,P¯)≡MSOk+1(v,Q¯) if and only if the following conditions hold:
for every p∈[ℓ] there is q∈[m] such that (w,P¯,p)≡MSOk(v,Q¯,q),
for every q∈[m] there is p∈[ℓ] such that (w,P¯,p)≡MSOk(v,Q¯,q),
for every R⊆[ℓ] there is S⊆[m] such that (w,P¯R)≡MSOk(v,Q¯S), and
for every S⊆[m] there is R⊆[ℓ] such that (w,P¯R)≡MSOk(v,Q¯S).
(This is a straightforward generalization for
MSO of the back-and-forth argument of
FO in Theorem 2.3.3 of [
1].)
Thus, if Mkr,1(w,P¯)=Mkr,1(v,Q¯) and Mkr+1,0(w,P¯)=Mkr+1,0(v,Q¯), then (w,P¯)≡MSOk+1(v,Q¯). This means that the MSOk+1-type of (w,P¯) is uniquely determined by the two sets Mkr,1(w,P¯) and Mkr+1,0(w,P¯), and consequently Mk+1r,0⩽|P(Mkr,1)×P(Mkr+1,0)|=2Mkr,1·2Mkr+1,0 which is equal to 22r+1(Mkr,0)2+Mkr+1,0 by Lemma 3.15.
Clearly Mkr,0⩽Mkr+1,0, and hence Mk+1r,0⩽2(2r+1+1)(Mkr+1,0)2. The claim follows from this since by Lemma 3.14, 2r+1+1⩽M1r+1,0 and clearly M1r+1,0⩽Mkr+1,0 for any k⩾1. □
Theorem 3.17.
For any k∈N and r∈N, Mkr,0⩽14tower(k+1,k+r+2)3. In particular, NMSOk=Mk0,0−1⩽14tower(k+1,k+2)3.
Proof.
We prove that the claim holds for any r by induction on k. By Lemma 3.14, we have M0r,0=1 and M1r,0=22r+1. On the other hand, we have 14tower(1,r+2)3=(142r+2)1/3=2r/3⩾1 and 14tower(2,r+3)3=(1422r+3)1/3=213(2r+3−2)⩾22r+1, since 13(2r+3−2)⩾13(342r+3)=2r+1. Thus, the claim holds for k=0 and k=1.
Assume then that k⩾1, and the claim holds for k and any r. Using Lemma 3.16 we get the following estimates:
Mk+1r,0⩽2(Mkr+1,0)3⩽214tower(k+1,k+r+3)⩽213(tower(k+1,k+r+3)−2)=(142tower(k+1,k+r+3))13=14tower(k+2,k+r+3)3.
Thus, the claim holds for
k+1. □
We can now formulate the upper bounds for definability, Löwenheim–Skolem and Hanf numbers for quantifier rank k fragments of MSO.
Corollary 3.18.
For any k∈N, DN(MSOk),LS(MSOk),H(MSOk)⩽14tower(k+1,k+2)3.
Using Corollary 3.5 we get the following upper bounds of the same numbers for the size n fragments of MSO.
Corollary 3.19.
For any n∈N, DN(MSO[n]),LS(MSO[n]),H(MSO[n])⩽14tower(n/2+1,n/2+2)3.
In the next two sections we will prove lower bounds for the definability numbers of FO[n] and MSO[n] by providing explicit polynomial size sentences that define words that are of exponential tower length.
4.Lower bounds for FO
In order to obtain a lower bound for DN(FO[n]) we need a relatively small FO-formula that defines a long word. The long word we define has to do with the cumulative hierarchy of finite sets.
The finite levels Vi of the cumulative hierarchy are defined by V0=∅ and Vi+1=P(Vi). We represent finite sets as words using only braces { and } in a straightforward fashion. For example V0 is encoded as {} and V1 as {{}}. V2 has two possible encodings: {{}{{}}} and {{{}}{}}. It is well known that |Vi+1|=tower(i). Thus the encodings of Vi+1 have length at least tower(i). We will define one such word via an FO-formula of polynomial size with respect to i.
For the encoding, we will consider a to be the left brace { and b the right brace }. For readability, we define formulas L(x):=Pa(x) and R(x):=Pb(x) that say x is a left or right brace, respectively. We also define S(x,y):=x<y∧¬∃z(x<z<y) that says y is the successor of x.
As each set in the encoding can be identified by its outermost braces, the formula mostly operates on pairs of variables. For readability we adopt the convention x‾:=(x1,x2), and similarly for different letters, to denote these pairs. To ensure that our formula defines a single encoding of Vi, we also define a linear order on encoded sets and require that the elements are in that order.
We define our formula recursively in terms of many subformulas. We briefly list the meanings and approximate sizes of each subformula involved:
core(x‾,θ(s,t)): the common core formula used in the formulas seti and oseti defined below. States that every brace y between x1 and x2 has a pair z such that the pair satisfies θ. In practice, θ will be another step of a similar recursion. The variables s and t are used to deal with both cases y<z and z<y at once, making the formula smaller.
core(x‾,θ(s,t)):=x1<x2∧L(x1)∧R(x2)∧∀y(x1<y<x2→∃z(x1<z<x2∧y≠z∧∃s∃t((y<z→(s=y∧t=z))∧(z<y→(s=z∧t=y))∧θ(s,t))))
seti(x‾): x‾ correctly encodes a set in Vi+1, possibly with repetition. Size linear in i.
set0(x‾):=L(x1)∧R(x2)∧S(x1,x2)seti+1(x‾):=core(x‾,seti(s,t))
x‾∈iy‾: x‾ is an element of y‾. Size linear in i. Assumes that x‾ encodes a set in Vi+1 and y‾ encodes a set in Vi+2. The part with z‾ is used to ensure that x‾ is an element of y‾ and not for example an element of an element.
x‾∈iy‾:=y1<x1<x2<y2∧¬∃z‾(seti(z‾)∧y1<z1<x1∧x2<z2<y2)
x‾∼iy‾: x‾ and y‾ encode the same set, possibly in a different order. Size O(i2). Assumes x‾ and y‾ encode sets in Vi+1. The two implications on the second line are used to deal with the symmetry of x‾ and y‾ at once, making the formula smaller.
x‾∼0y‾:=⊤x‾∼i+1y‾:=∀a‾(seti(a‾)→∃b‾(seti(b‾)∧(a‾∈ix‾→b‾∈iy‾)∧(a‾∈iy‾→b‾∈ix‾)∧a‾∼ib‾))
x‾≺iy‾: the ≺i−1-greatest element of the symmetric difference of x‾ and y‾ is in y‾. Size O(i3). Defines a linear order for encoded sets in Vi+1. The set z‾ is in y‾, is not in x‾ and is larger than any a‾ that is in x‾ but not in y‾.
x‾≺0y‾:=⊥x‾≺i+1y‾:=∃z‾(seti(z‾)∧z‾∈iy‾∧∀a‾((seti(a‾)∧a‾∈ix‾)→(a‾≁iz‾∧(∃b‾(seti(b‾)∧b‾∈iy‾∧a‾∼ib‾)∨a‾≺iz‾))))
oseti(x‾): x‾ correctly encodes a set in Vi+1 with no repetition and with the elements in the linear order given by the formula x‾≺iy‾. Size O(i4). Ensures that only a singular word satisfies our formula.
oset0(x‾):=L(x1)∧R(x2)∧S(x1,x2)oseti+1(x‾):=core(x‾,oseti(s,t))∧∀a‾∀b‾((seti(a‾)∧seti(b‾)∧a‾∈ix‾∧b‾∈ix‾∧a1<b1)→a‾≺ib‾)
addi(x‾,y‾,z‾): States that x‾=y‾∪{z‾}. Size O(i2). Assumes x‾ and y‾ encode sets in Vi+1 and z‾ encodes a set in Vi. The first line states that y‾⊆x‾, the second line states z‾∈x‾ and the two final lines state x‾∖{z‾}⊆y‾.
addi+1(x‾,y‾,z‾):=∀a‾((seti(a‾)∧a‾∈iy‾)→∃b‾(seti(b‾)∧b‾∈ix‾∧a‾∼ib‾))∧∃c‾(seti(c‾)∧c‾∈ix‾∧c‾∼iz‾∧∀d‾((seti(d‾)∧d‾∈ix‾∧d1≠c1)→∃e‾(seti(e‾)∧e‾∈iy‾∧e‾∼id‾)))
Vi(x‾): x‾ encodes the set Vi. Size O(i5). States that x‾ is an ordered encoding, ∅∈x‾, Vi−1∈x‾ and for all c‾∈x‾ and d‾∈Vi−1, we have c‾∪{d‾}∈x‾.
V0(x‾):=set0(x‾)Vi+1(x‾):=oseti+1(x‾)∧∃a‾(V0(a‾)∧S(x1,a1))∧∃b‾(Vi(b‾)∧S(b2,x2)∧∀c‾∀d‾((seti(c‾)∧c‾∈ix‾∧seti−1(d‾)∧d‾∈i−1b‾)→∃e‾(seti(e‾)∧e‾∈ix‾∧addi(e‾,c‾,d‾))))
ψi: the entire word is the ordered encoding of the set Vi. Size O(i5).
ψi:=∃x∃y∀z(x⩽z∧z⩽y∧Vi(x,y))
The formula ψi+1 defines a word w that, as an encoding of the set Vi+1, has length at least tower(i). The size of ψi+1 is O((i+1)5) and thus O(i5). Let c be a constant such that sz(ψi+1)⩽c·i5 so w∈Def(FO[c·i5]). As we want to relate the length of w to the size of ψi, we set n=c·i5 and obtain the following result:
Theorem 4.1.
For some constant c∈N there are infinitely many n∈N satisfying
DN(FO[n])⩾tower(⌊n/c5⌋).
Proposition 2.10 immediately gives the same bound for the Hanf number.
Corollary 4.2.
For some constant c∈N there are infinitely many n∈N satisfying
H(FO[n])⩾tower(⌊n/c5⌋).
By omitting the subformula oseti+1 from the above we get a formula of size O(i3) that is no longer satisfied by only one word but still only has large models. With this formula we obtain a lower bound for the Löwenheim–Skolem number.
Corollary 4.3.
For some c∈N there are arbitrarily large n∈N satisfying
LS(FO[n])⩾tower(⌊n/c3⌋).
5.Lower bounds for MSO
In this section, we define a similar formula for MSO as we did above for FO. The formula again defines an encoding of Vi but for MSO our formula is of size O(i2) compared to the O(i5) of FO. We achieve this by quantifying a partition of so called levels Dj for the braces and thus the encoded sets and using a different method to define only a single encoding. The monadic predicates Dj are used throughout the formulas and only quantified at the beginning of the recursion.
The level Dj of the entire encoded set will be equal to the maximum depth of braces inside the set. The level of an element of a set will always be one less than the level of the parent set. This means that there will be instances of the same set with different levels in our encoding. For example in the encoding {{}{{}}} the outermost braces are in D2, both of the elements are in D1 and the empty set in the second element is in D0.
We again define our formula in terms of many subformulas and briefly list the meaning and size of each subformula:
seti(x‾): x‾ encodes a set of level i. Size constant. Here we only require that there are no braces of the same level between x1 and x2, leaving the rest to the formula levelsi below.
set0(x‾):=S(x1,x2)∧L(x1)∧R(x2)∧D0(x1)∧D0(x2)seti(x‾):=x1<x2∧L(x1)∧R(x2)∧Di(x1)∧Di(x2)∧∀y(x1<y<x2→¬Di(y))
levelsi: The relations Dj define the levels of sets as intended and there are no odd braces without pairs. Size O(i2). States that every brace has a level, no brace has two different levels, every set encloses only braces of lower levels and every brace has a pair of the same level to form a set.
levelsi:=∀x(⋁j=0iDj(x)∧⋀j,k∈{0,…,i}j≠k¬(Dj(x)∧Dk(x))∧∀x‾(⋀j=0i(setj(x‾)→∀y(x1<y<x2→⋁k=0j−1Dk(y))))∧∀x1(⋀j=0i((L(x1)∧Dj(x1))→∃x2setj(x1,x2))∧⋀j=0i(R(x1)∧Dj(x1))→∃x2setj(x2,x1))
x‾∈y‾: x‾ is an element of y‾. Size constant. Assumes x‾ encodes a set of level i and y‾ encodes a set of level i−1.
x‾∈y‾:=y1<x1∧x2<y2
x‾∼iy‾: x‾ and y‾ encode the same set. Size linear in i. Assumes x‾ and y‾ encode sets of level i. Similar to the FO case.
x‾∼0y‾:=⊤x‾∼i+1y‾:=∀a‾(seti(a‾)→∃b‾(seti(b‾)∧(a‾∈x‾→b‾∈y‾)∧(a‾∈y‾→b‾∈x‾)∧a‾∼ib‾))
addi(x‾,y‾,z‾): States that x‾=y‾∪{z‾}. Size linear in i. Assumes x‾ and y‾ encode sets of level i and z‾ encodes a set of level i−1. Similar to the FO case.
addi+1(x‾,y‾,z‾):=∀a‾((seti(a‾)∧a‾∈y‾)→∃b‾(seti(b‾)∧b‾∈x‾∧a‾∼ib‾))∧∃c‾(seti(c‾)∧c‾∈x‾∧c‾∼iz‾∧∀d‾((seti(d‾)∧d‾∈x‾∧d1≠c1)→∃e‾(seti(e‾)∧e‾∈y‾∧e‾∼id‾)))
Vi(x‾): x‾ encodes the set Vi. Size O(i2). Assumes the level partition is given. Similar to the FO case with no ordering.
V0(x‾):=set0(x‾)Vi+1(x‾):=seti+1(x‾)∧∃a‾(seti(a‾)∧a‾∈x‾∧S(a1,a2))∧∃b‾(Vi(b‾)∧b‾∈x‾∧∀c‾∀d‾((seti(c‾)∧c‾∈x‾∧seti−1(d‾)∧d‾∈b‾)→∃e‾(seti(e‾)∧e‾∈x‾∧addi(e‾,c‾,d‾))))
φi(x,y): Quantifies the level partition and states the subword from x to y encodes Vi. Size O(i2).
φi(x,y):=∃D0…∃Di(levelsi∧Vi(x,y)))
We now have a formula φi(x,y) that says the subword from x to y encodes the set Vi. There are still multiple words that satisfy this formula, since different orders of the sets and even repetition are still allowed. To pick out only one such word, we use a lexicographic order, where a shorter word always precedes a longer one.
Let φi′ be the formula obtained from φi by replacing each occurrence of L(x) with P1(x) and R(x) with P2(x). We define the final formula ψi of size O(i2) that says the entire word model is the least word in the lexicographic order that satisfies the property of φi. We check that no lexicographically smaller word satisfies φi by quantifying the word under consideration on top of the same word model using the variables P1 and P2 for the two letters. We first ensure that P1 and P2 partition the model and then use y′ as the cut-off point for the possibly shorter word we want to quantify. If y′=y we check the lexicographic order with z as the first different symbol. Finally we state that the quantified word does not satisfy φi.
ψi:=∃x∃y(∀z(x⩽z∧z⩽y)∧φi(x,y)∧∀P1∀P2(∀z((P1(z)∨P2(z))∧¬(P1(z)∧P2(z)))∧∀y′((y′<y∨∃z(∀a(a<z→(L(a)↔P1(a)∧R(a)↔P2(a)))∧(P1(z)∧R(z)))→¬φi′(x,y′))))
We have used the lexicographic order here to select only one of the possible words that satisfy our property. Note that this can be done for any property. The size of such a formula will depend polynomially on the size of the alphabet, as well as linearly on the size of the formula defining the property in question.
We obtain the lower bound for the definability number as in the FO case.
Theorem 5.1.
For some constant c∈N there are infinitely many n∈N satisfying
DN(MSO[n])⩾tower(⌊n/c⌋).
We get the same bounds for LS(MSO[n]) and H(MSO[n]) via Proposition 2.10.
Corollary 5.2.
For some constant c∈N there are infinitely many n∈N satisfying
LS(MSO[n]),H(MSO[n])⩾tower(⌊n/c⌋).
6.Two-variable logic
In this section we prove upper and lower bounds on the definability numbers of quantifier rank k fragments of first-order logic with two variables FO2.
For the upper bound on DN(FOk2) we use the k-round, 2-pebble EF-game GFOk2. For details on the game, see for example [1]. We prove two separate lemmas that together allow us to show that a long enough word cannot be separated from a shorter one with two variables and quantifier rank k.
Lemma 6.1.
Let a∈Σ and let w∈Σ∗ contain an a-chain of length at least 2k and let v∈Σ∗ be obtained from w by removing from such a chain all other letters but the first k and the last k−1 letters. Then w≡FOk2v.
Proof.
We consider the k-round 2-pebble EF-game GFOk2(w,v). If w and v are as in the claim, then each point i∈[|v|] has a directly corresponding point in w as v is obtained by removing points from w. We denote this corresponding point by f(i). Note that for the shortened chain, the correspondence is between the first k letters and the last k−1 letters of the chain in each word. We denote the subword of w consisting of only the long a-chain of the claim with u. With m⩽k fixed we call the part of u excluding the first m letters and the last m−1 letters the middle part of u. When Spoiler moves one of the pebbles we call the other pair of pebbles that is not moved the stationary pebbles.
We describe a strategy for Duplicator in GFOk2(w,v). We show that the strategy maintains both partial isomorphism and the following conditions with m rounds left in the game:
(1) If the stationary pebbles are not in the middle part of u on either side, then they are on a pair (f(i),i).
(2) Otherwise, the stationary pebbles are in the middle part of u on both sides.
Note that the above conditions hold in the starting position as there are no stationary pebbles.
Consider the next move in a k-round 2-pebble game with words w and v as in the claim with m⩽k rounds left to play and assume the conditions above hold.
If Spoiler moves on a stationary pebble, then Duplicator responds with the point, where the other stationary pebble is. This clearly maintains partial isomorphism. Below we assume that Spoiler always moves on a different point.
If Spoiler moves anywhere but the middle part of u, then Duplicator responds with the corresponding point according to f, resulting in a pair (f(i),i). This along with the conditions clearly maintains partial isomorphism.
For the rest of the proof, assume Spoiler moves in the middle part of u in w or v. If m=k, then there are no stationary pebbles. Duplicator responds with the k-th letter of u in the opposite word. Partial isomorphism clearly holds.
Assume m<k and the stationary pebbles are on the pair (f(i),i), where i is the m-th letter of the chain u in v. Now Duplicator responds with the m−1-th letter from the end of u in the opposite word. The new pair is to the right of the old one in both words so partial isomorphism is maintained.
If m<k and the stationary pebbles are on a pair (f(i),i), where i is not the m-th letter of the chain u in v, then Duplicator moves to the m-th letter of u in the opposite word. This clearly maintains partial isomorphism.
Finally assume m<k and that the stationary pebbles are in the middle part of u in both words. Now if the move of Spoiler is to the left of the stationary pebble in one of the words, Duplicator responds with the m-th letter of u in the opposite word. If the move of Spoiler is to the right of the stationary pebble, Duplicator responds with the m−1-th letter from the end of u in the opposite word. Clearly this maintains partial isomorphism.
It remains to show that conditions 1 and 2 are maintained by this strategy. When Spoiler picks up a pebble for the next move, condition 1 clearly holds as Duplicator has respected the correspondence f. For condition 2 we see that Duplicator has responded to moves in the middle part of u with either the m-th letter of u or the m−1-th letter from the end of u. In the following position with m−1 rounds left, these points are in the middle part of u in both words. Thus conditions 1 and 2 are maintained.
Since Duplicator has a winning strategy for the game GFOk2(w,v), by Theorem 2.6, we obtain w≡FOk2v. □
Lemma 6.2.
Let Σ={a,b} and let w∈Σ∗ with at least 2k+2 chains. If v∈Σ∗ is obtained from w by removing all other chains except the first k and the last k chains, then w≡FOk2v.
Proof.
We again consider GFOk2(w,v). If w starts and ends with the same letter c∈{a,b}, then we remove the last c-chain from w and use the resulting w′ and corresponding v′ for the proof instead. When we have obtained w′≡FOk2v′, we can use Theorem 3.1 to obtain w≡FOk2v. By symmetry we assume that w starts with a and ends with b.
For words w and v as in the claim, each point i∈[|v|] has a directly corresponding point in w as v was obtained by shortening w. We denote this point by f(i). When Spoiler moves one of the pebbles we call the other pair of pebbles that is not moved the stationary pebbles.
We describe a strategy for Duplicator in GFOk2(w,v). We show that the strategy maintains both partial isomorphism and the following conditions with m rounds left in the game:
(1) If one stationary pebble is on a point f(i)∈[|w|] within the first or last m chains of w, then the corresponding pebble is on i∈[|v|].
(2) Otherwise, neither of the stationary pebbles is within the first and last m chains of w or v, that is, the stationary pebbles are in the middle part of w and v.
Note that the above conditions hold in the starting position as there are no stationary pebbles.
Consider the next move in an k-round 2-pebble game with words w and v as in the claim with m⩽k rounds left to play and assume the conditions hold.
If Spoiler moves on a stationary pebble, then Duplicator responds with the point, where the other stationary pebble is. This clearly maintains partial isomorphism. Below we assume that Spoiler always moves on a different point.
If Spoiler moves within the first or last m chains in w or v, then Duplicator responds with the corresponding point, resulting in a pair (f(i),i). If the stationary pebbles follow the correspondence f, then clearly partial isomorphism holds. Otherwise the stationary pebbles are in the middle part of both w and v and partial isomorphism holds because the corresponding points i and f(i) are both either on the left or the right side of the words.
For the rest of the proof, assume Spoiler moves on a letter c∈{a,b} in the middle part of t∈{w,v}, that is, not within the first or last m chains. Let u∈{w,v}, be the opposite word, where Duplicator moves. If m=k, then there are no stationary pebbles and Duplicator moves in the k-th chain in u. Partial isomorphism trivially holds.
If m<k and the stationary pebbles are on a pair (f(i),i), where i is in the m-th chain in v, then Duplicator moves to the m-th chain from the end in u. Now partial isomorphism holds as the pair (f(i),i) is to the left of the middle part of t and the last m chains of u.
If m<k and the stationary pebbles are on a pair (f(i),i), where i is not in the m-th chain in v, then Duplicator moves to the m-th chain in u. This clearly maintains partial isomorphism.
Finally assume m<k and that the stationary pebbles are somewhere in the middle part of both w and v as in condition 2. Now if the move of Spoiler is to the left of the stationary pebble in t, then Duplicator moves to the m-th chain in u. If the move is to the right of the stationary pebble in t, then Duplicator moves to the m-th chain from the end of u. Clearly this maintains partial isomorphism.
It remains to show that conditions 1 and 2 still hold, when Spoiler picks up a pebble in the following position. Clearly condition 1 holds since Duplicator has respected the correspondence f. For condition 2 we see that Duplicator has responded to moves in the middle part of either word by playing in the m-th chain counting from the beginning or end of the other word. In the following position with m−1 rounds left, these pebbles are not within the m−1 first and last chains of w or v. Thus the conditions 1 and 2 are maintained by this strategy.
Since Duplicator has a winning strategy for the game GFOk2(w,v), by Theorem 2.6, we obtain w≡FOk2v. □
The two above lemmas allow us to prove the following theorem as a lower bound to the Löwenheim–Skolem number, Hanf number and definability number of FOk2.
Theorem 6.3.
For any k∈N, LS(FOk2)⩽4k2−1, H(FOk2)⩽4k2−6k+2 and hence also DN(FOk2)⩽4k2−6k+2.
Proof.
Let w∈Σ∗ be a word with |w|>4k2−1. Since 4k2−1=(2k−1)·(2k+2−1), by the pigeonhole principle there is a chain with length at least 2k or at least 2k+2 chains. Now by Lemmas 6.1 and 6.2, there is a shorter word v∈Σ∗ with w≡FOk2v. Recall that for a formula φ, μ(φ) is the length of the shortest model of φ. We obtain μ(φ)⩽4k2−1 for all φ∈FOk2 and therefore LS(FOk2)⩽4k2−1.
For the Hanf number, consider a word v∈Σ∗ with |v|>4k2−6k+2. Since 4k2−6k+2=(2k−2)·(2k−1), there is a chain with length at least 2k−1 or at least 2k chains. In the first case, by increasing the length of this long chain one can obtain words w with arbitrary length that are by Lemma 6.1 equivalent with v. In the second case, by increasing the number of chains one can again obtain words w of arbitrary length that are by Lemma 6.2 equivalent with v. Thus H(FOk2)⩽4k2−6k+2. □
For the lower bound on DN(FOk2) we give a formula that defines a word of quadratic length. We begin with some auxiliary formulas. Our target word starts with a and ends with b and this is reflected in the formulas. We define all auxiliary formulas with the free variable x and the understanding that the roles of x and y can be switched in nested formulas, when necessary.
chlt⩾1a(x):=Pa(x)chlt⩾ma(x):=Pa(x)∧∃y(y<x∧chlt⩾m−1b(y)),for m>1chlt⩾1b(x):=Pb(x)chlt⩾mb(x):=Pb(x)∧∃y(y<x∧chlt⩾ma(y)),for m>1
The formula chlt⩾ma(x) states that x is in an a-chain that is at least the m-th one from the left. Similarly, the formula chlt⩾mb(x) states that x is in at least the m-th b-chain. Our target word starts with a and this causes some differences between the two formulas.
chlt⩽1a(x):=Pa(x)∧∀y(y<x→Pa(y))chlt⩽ma(x):=Pa(x)∧∀y(y<x∧Pb(y)→chlt⩽m−1b(y)),for m>1chlt⩽mb(x):=Pb(x)∧∀y(y<x∧Pa(y)→chlt⩽ma(y)),for m⩾1
As a counterpart to the above, the formula chlt⩽ma(x) states that x is in at most the m-th a-chain from the left. The formula chlt⩽mb(x) says the same for b.
chlt=ma(x):=chlt⩾ma(x)∧chlt⩽ma(x),for m⩾1chlt=mb(x):=chlt⩾mb(x)∧chlt⩽mb(x),for m⩾1
By combining the above formulas we obtain the formula chlt=ma(x) which states that the point x is in the m-th a-chain of the word.
We also define corresponding formulas chrt⩾ma(x), chrt⩽ma(x) and chrt=ma(x) that say the point x is in the m-th a-chain from the right, or the end of the word. These formulas are obtained from the chltb-formulas by switching the roles of a and b as well as the direction of each instance of the linear order. Formulas chrt⩾mb(x), chrt⩽mb(x) and chrt=mb(x) are obtained in the same way by switching in the chlta-formulas the roles of a and b as well as the direction of the linear order.
The quantifier rank of the formulas chlt=ma(x) and chrt=mb(x) is 2m−1, while for the formulas chlt=mb(x) and chrt=ma(x) it is 2m.
We move on to formulas that specify the length of each chain in the word.
poslt1,1a(x):=Pa(x)∧¬∃y(y<x)posltm,1a(x):=chlt=ma(x)∧∀y(y<x→¬chlt=ma(y)),for m>1posltm,ℓa(x):=chlt=ma(x)∧∃y(y<x∧posltm,ℓ−1a(y)),for m⩾1,l>1
The formula posltm,ℓa(x) states that x is the ℓ-th symbol in the m-th a-chain from the left. The formulas posltm,ℓb(x), posrtm,ℓa(x) and posrtm,ℓb(x) are defined in the same way, using the appropriate subformulas for a or b and left or right.
lenltm,ℓa(x):=posltm,ℓa(x)∧∀y(y>x→¬chlt=ma(y)),for m⩾1,l⩾1
The formula lenltm,ℓa(x) states that x is in the m-th a-chain of the word, which has length ℓ. In fact x is the last letter of the chain but we do not use this going forward.
We define in the same way the formulas lenltm,ℓb(x) for b-chains as well as lenrtm,ℓa(x) and lenrtm,ℓb(x) for the m-th chain from the end of the word. The quantifier rank of the formulas lenltm,ℓa(x) and lenrtm,ℓb(x) is 2m+l−1, while for the formulas lenltm,ℓb(x) and lenrtm,ℓa(x) it is 2m+l.
We are now ready to define the full formula φ of quantifier rank k, which defines a word w with k−3 chains of both a and b. For simplicity, we assume that k is even. The length of the chains decreases by one for each chain as they approach the middle of the word w.
φ:=∃x(lenltk/2−1,1a(x)∧lenrtk/2−1,1a(x))∧∃x(lenltk/2−1,1b(x)∧lenrtk/2−1,1b(x))∧⋀i=1k/2−2∃x(lenlti,k−2i−1a(x))∧⋀i=1k/2−2∃x(lenlti,k−2i−2b(x))∧⋀i=1k/2−2∃x(lenrti,k−2i−2a(x))∧⋀i=1k/2−2∃x(lenrti,k−2i−1b(x))
To see that
φ defines a single word
w, note that the first two lines fix the middle chains of both
a and
b as length one. The following lines set the length of each chain to the left and to the right of these middle chains. Thus all chains are fixed and only a single word satisfies
φ. Assuming
k is even, the length of the word
w that
φ defines is
k2−5k+6. This proves the following theorem:
Theorem 6.4.
For any even k∈N, DN(FOk2)⩾k2−5k+6.
7.Conclusion
We considered the definability number, the Löwenheim–Skolem number and the Hanf number on words in the size n fragments of first-order logic and monadic second-order logic. We obtained exponential towers of various heights as upper and lower bounds for each of these numbers.
For FO, we obtained the bounds
tower(⌊n/c5⌋)⩽DN(FO[n])⩽tower(n/2+2)
for some constant
c. As corollaries, we obtained the same bounds for
LS(FO[n]) and
H(FO[n]). In addition, by modifying the formula we used for the lower bounds, we obtained a slightly better lower bound of
tower(⌊n/c3⌋) for
LS(FO[n]).
In the case of MSO, the bounds are similarly
tower(⌊n/c⌋)⩽DN(MSO[n])⩽14tower(n/2+1,n/2+2)3
for a different constant
c. We again immediately obtained the same bounds for
LS(MSO[n]) and
H(MSO[n]).
The gaps between the lower bounds and upper bounds we have proved are quite big. In absolute terms, they are actually huge, as each upper bound is non-elementary with respect to the corresponding lower bound. However, it is more fair to do the comparison in the iterated logarithmic scale, which reduces the gap to be only polynomial. Nevertheless, a natural task for future research is to look for tighter lower and upper bounds.
For first-order logic with two variables, we obtained the following bounds for the definability numbers of the quantifier rank k fragments for even k∈Z+
k2−5k+6⩽DN(FOk2)⩽4k2−6k+2.
The same bounds hold also for the Hanf number, whereas for the Löwenheim–Skolem number the upper bound is
4k2−1. We see that the situation for
FO2 is completely different from full
FO or
MSO as the bounds are not even exponential, not to speak of exponential towers.
Finally, we remark that an exponential tower upper bound for the number of types in the quantifier rank fragments of some logic L can be obtained completely generically as in the Appendix of the pre-print [8]. The argument in [8] works in the same way irrespective of the type of quantifiers allowed in L. Thus, it can be applied for example in the case where L is the extension of FO with some generalized quantifier (or a finite set of generalized quantifiers). Assuming further that the quantifier rank fragments L of L satisfy Theorem 3.1, we can obtain this way an exponential tower upper bound for the numbers DN(L), LS(L) and H(L). On the other hand, note that if the quantifier rank fragments L satisfy Theorem 3.1, then each ≡L is an invariant equivalence relation, and hence L can only define regular languages. Therefore it seems that our technique for proving upper bounds cannot be used for logics with expressive power beyond regular languages.
