Defining long words succinctly in FO and MSO

Abstract

We consider the length of the longest word definable in FO and MSO via a formula of size n. For both logics we obtain as an upper bound for this number an exponential tower of height linear in n. We prove this by counting types with respect to a fixed quantifier rank. As lower bounds we obtain for both FO and MSO an exponential tower of height in the order of a rational power of n. We show these lower bounds by giving concrete formulas defining word representations of levels of the cumulative hierarchy of sets. For the two-variable fragment of FO we obtain quadratic lower and upper bounds for the definability numbers of quantifier rank k fragments. In addition, we consider the Löwenheim–Skolem and Hanf numbers of these logics on words and obtain similar bounds for these as well.

Keywords

Logic on words monadic second-order logic succinctness

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 ${FO}_{k}$ and ${MSO}_{k}$ 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 ${FO}^{2}$ . 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 $\sqrt[5]{n / c}$ for FO and $\sqrt{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 theorem1

¹
Trakhtenbrot’s theorem states that the finite satisfiability problem of FO is undecidable. Hence there cannot exist any computable upper bound for the size of models that need to be checked to see whether a given formula is satisfiable.

(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 ${FO}_{k}$ , the upper bound in [7] was $tower (k + 1, k^{2} + k)$ , using the modified exponential tower notation defined in this version. The new bound of $\sqrt{tower (k + 2)}$ gets rid of the polynomial on top of the tower and introduces a square root. For ${MSO}_{k}$ the bound in [7] was $tower (k + 1, {(k + 1)}^{2})$ . The new bound of $\sqrt[3]{\frac{1}{4} tower (k + 1, k + 2)}$ 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 ${FO}_{k}^{2}$ .

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 $P_{a}$ and $P_{b}$ 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 ${<, P_{a}, P_{b}}$ of the corresponding word models (and similarly for $FO$ -formulas). We denote the length of a word $w \in Σ^{*}$ by $| w |$ . We will also assume that all word models w with $| w | = n$ have domain $[n] : = {1, \dots, n}$ . We will use the notation $[n]$ also elsewhere.

For $w \in Σ^{*}$ and $a \in Σ$ , 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 $a a b b b a$ 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, \bar{P}, \bar{p})$ , where $w \in Σ^{*}$ , $\bar{P} = (P_{1}, \dots, P_{r})$ is a tuple of sets of points in w, and $\bar{p} = (p_{1}, \dots, p_{s})$ 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 $φ \in MSO$ with second-order variables $\bar{X} = (X_{1}, \dots, X_{r})$ and first-order variables $\bar{x} = (x_{1}, \dots, x_{s})$ , we also define the truth relation $(w, \bar{P}, \bar{p}) ⊧ φ$ as $w ⊧ φ [\bar{P} / \bar{X}, \bar{p} / \bar{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, \bar{p})$ and the truth relation $(w, \bar{p}) ⊧ φ$ .

Definition 2.1.
The size $sz (φ)$ of a formula $φ \in MSO$ is defined recursively as follows:
$sz (φ) = 1$ for atomic φ,

$sz (\neg ψ) = sz (ψ) + 1$ ,

$sz (ψ \land θ) = sz (ψ \lor θ) = sz (ψ) + sz (θ) + 1$ ,

$sz (\exists x ψ) = sz (\forall x ψ) = sz (\exists U ψ) = sz (\forall U ψ) = sz (ψ) + 1$ .
For $n \in 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 $φ \in MSO$ is defined recursively as follows:
$qr (φ) = 0$ for atomic φ,

$qr (\neg ψ) = qr (ψ)$ ,

$qr (ψ \land θ) = qr (ψ \lor θ) = max {qr (ψ), qr (θ)}$ ,

$qr (\exists x ψ) = qr (\forall x ψ) = qr (\exists U ψ) = qr (\forall U ψ) = qr (ψ) + 1$ .
For $k \in N$ , the quantifier rank k fragment of $MSO$ , denoted ${MSO}_{k}$ , consists of the formulas $φ \in MSO$ with $qr (φ) ⩽ k$ . The quantifier rank k fragment of $FO$ is defined in the same way and denoted ${FO}_{k}$ .

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 $\equiv_{L}$ on nonempty Σ-words as $\begin{matrix} w \equiv_{L} v, if w and v agree on all L -sentences . \end{matrix}$

Clearly $\equiv_{L}$ is an equivalence relation on $Σ^{+}$ . We denote the set $Σ^{+} / \equiv_{L}$ of equivalence classes of $\equiv_{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 $\equiv_{L}$ by $N_{L}$ , i.e. $\begin{matrix} N_{L} : = | Σ^{+} / L | . \end{matrix}$

Note that each equivalence class of $\equiv_{L}$ is uniquely determined by a subset ${tp}_{L} (w) = {φ \in L | w ⊧ φ}$ of L-sentences, which we call the L-type of w.

For quantifier rank fragments ${FO}_{k}$ and ${MSO}_{k}$ we define similar concepts also for formulas with free variables.
Definition 2.5.
We define the relation $\equiv_{{MSO}_{k}}$ on $(r, s)$ -interpretations as $\begin{aligned} (w, \bar{P}, \bar{p}) \equiv_{{MSO}_{k}} (v, \bar{Q}, \bar{q}), if (w, \bar{P}, \bar{p}) and (v, \bar{Q}, \bar{q}) agree on all {MSO}_{k} formulas \\ with free variables \bar{X} = (X_{1}, \dots, X_{r}) and \bar{x} = (x_{1}, \dots, x_{s}) . \end{aligned}$ The relation $\equiv_{{FO}_{k}}$ is defined in the same way for s-interpretations.

The set of equivalence classes of $\equiv_{{MSO}_{k}}$ over $(r, s)$ -interpretations is denoted by $M_{k}^{r, s}$ and the number of these classes is denoted by $M_{k}^{r, s} = | M_{k}^{r, s} |$ . Furthermore, the set of equivalence classes of $\equiv_{{FO}_{k}}$ over s-interpretations is denoted by $F_{k}^{s}$ and the number of these classes is denoted by $F_{k}^{s} = | F_{k}^{s} |$ .

Note that $M_{k}^{0, 0} = N_{{MSO}_{k}} + 1$ and $F_{k}^{0} = N_{{FO}_{k}} + 1$ , since the empty word ε is taken into account in $M_{k}^{0, 0}$ and $F_{k}^{0}$ , but not in $N_{{MSO}_{k}}$ and $N_{{FO}_{k}}$ .

We also consider two-variable first order logic ${FO}^{2}$ . 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 \in N$ and two word models w and v.

The two-pebble EF-game is denoted by ${GFO}_{k}^{2} (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 $p_{1}$ , $p_{2}$ and $q_{1}$ , $q_{2}$ be the points with pebbles on them. Duplicator wins if after each round, the map $(p_{1}, p_{2}) \mapsto (q_{1}, q_{2})$ is a partial isomorphism between w and v. Otherwise Spoiler wins.

The game ${GFO}_{k}^{2} (w, v)$ characterizes the equivalence of structures for ${FO}^{2}$ 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 ${GFO}_{k}^{2} (w, v)$ if and only if $w \equiv_{{FO}_{k}^{2}} v$ .

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 \to N$ is defined recursively by setting $tower (0) : = 1$ and $tower (n + 1) : = 2^{tower (n)}$ . The modified exponential tower function $tower (k, ℓ) : N \times N \to N$ is defined recursively by setting $tower (0, ℓ) : = ℓ$ and $tower (n + 1, ℓ) : = 2^{tower (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 $φ \in MSO$ defines a word $w \in Σ^{+}$ if $w ⊨ φ$ and $v ⊭ φ$ for all $v \in Σ^{+} ∖ {w}$ . For a fragment L of $MSO$ or $FO$ , we denote by $Def (L)$ the set of words definable in L, i.e. $\begin{matrix} Def (L) : = {w \in Σ^{+} | there is φ \in L s.t. φ defines w}. \end{matrix}$

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 \in Σ^{+}, 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) \neq \emptyset$ .
The definability number of L is $DN (L) = max {| w | | w \in Σ^{+}, w \in Def (L)}$ .

The Löwenheim–Skolem number of L is $LS (L) = max {μ (φ) | φ \in L}$ .

The Hanf number of L is $H (L) = max {ν (φ) | φ \in 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 $φ \in L$ that has a model, has a model of length at most m. Similarly $H (L)$ is the smallest number ℓ such that if $φ \in 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 ${FO}_{k}$ , $MSO [n]$ and ${MSO}_{k}$ .

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 \in Def (L)$ , then $μ (φ) = ν (φ) = | w |$ , where $φ \in 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 $\exists x_{1} \dots \exists x_{m} ⋀_{1 ⩽ i < j ⩽ m} \neg x_{i} = x_{j}$ , and let $θ_{n}$ be the sentence $\forall x_{1} \dots \forall x_{n + 1} ⋁_{1 ⩽ i < j ⩽ n + 1} x_{i} = x_{j}$ . 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 ${FO}_{k}$ and ${MSO}_{k}$ . 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, \bar{P}, \bar{p})$ be an $(r, s)$ -interpretation and let $(v, \bar{Q}, \bar{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, \bar{P}, \bar{p})$ and $(v, \bar{Q}, \bar{q})$ as the $(r, s + s^{'})$ -interpretation $(w, \bar{P}, \bar{p}) \cdot (v, \bar{Q}, \bar{q}) = (w v, \overline{P \cup Q^{'}}, \bar{p} {\bar{q}}^{'})$ , where ${(P \cup Q^{'})}_{i} = P_{i} \cup Q_{i}^{'}$ , $Q_{i}^{'} = {q + | w | | q \in Q_{i}}$ and $q_{i}^{'} = q_{i} + | w |$ for each $i \in [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 \in {{FO}_{k}, {MSO}_{k}}$ for some $k \in N$ . $\begin{aligned} If (w, \bar{P}, \bar{p}) \equiv_{L} (w^{'}, {\bar{P}}^{'}, {\bar{p}}^{'}) and (v, \bar{Q}, \bar{q}) \equiv_{L} (v^{'}, {\bar{Q}}^{'}, {\bar{q}}^{'}), \\ then (w, \bar{P}, \bar{p}) \cdot (v, \bar{Q}, \bar{q}) \equiv_{L} (w^{'}, {\bar{P}}^{'}, {\bar{p}}^{'}) \cdot (v^{'}, {\bar{Q}}^{'}, {\bar{q}}^{'}) . \end{aligned}$ In particular, if $w \equiv_{L} w^{'}$ and $v \equiv_{L} v^{'}$ , then $w v \equiv_{L} w^{'} 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 \in {{FO}_{k}, {MSO}_{k}}$ for some $k \in N$ . If φ is a sentence of L, then $μ (φ), ν (φ) ⩽ N_{L}$ .
Proof.
If $| w | ⩽ N_{L}$ for all words $w \in Σ^{+}$ such that $w ⊧ φ$ , the claim is trivial. Assume then that $w ⊧ φ$ and $| w | > N_{L}$ . Then there are two initial segments u and $u^{'}$ of w such that $| u | < | u^{'} |$ and $u \equiv_{L} u^{'}$ . Let v and $v^{'}$ be the corresponding end segments, i.e., $w = u v = u^{'} v^{'}$ . Then by Theorem 3.1, $u v^{'} \equiv_{L} u^{'} v^{'} = w$ , and similarly $u^{'} v \equiv_{L} u v = w$ , and hence $u v^{'} ⊧ φ$ and $u^{'} v ⊧ φ$ .

Since $| u v^{'} | < | w |$ , we see that w is not the shortest word satisfying φ. The argument applies to any word w with $| w | > N_{L}$ , and hence we conclude that $μ (φ) ⩽ N_{L}$ . 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 ⩽ N_{L}$ . □

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 \in N$ and $L \in {{FO}_{k}, {MSO}_{k}}$ . Then $LS (L), H (L) ⩽ N_{L}$ , and consequently $DN (L) ⩽ N_{L}$ .

This $N_{L}$ 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 $\equiv_{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 $2^{N_{L}}$ . Thus, any collection of representatives of non-equivalent sentences of L necessarily contains sentences of size close to $N_{L}$ . However, in spite of this, it is not possible to define words that are longer than $N_{L}$ 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 \in N$ , $FO [n]$ is trivially contained in ${FO}_{n}$ , and similarly, $MSO [n]$ is contained in ${MSO}_{n}$ . A simple argument shows that this can be improved by a factor of 2:
Lemma 3.4.
For any $n \in N$ , $FO [2 n] ⩽ {FO}_{n}$ and $MSO [2 n] ⩽ {MSO}_{n}$ .
Proof.
Let $φ \in FO [2 n]$ 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 $2 n + 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, $2 n$ could be replaced with $3 n$ , and possibly with an even larger number. Corollary 3.5.
For any $n \in N$ , $DN (FO [2 n]), LS (FO [2 n]), H (FO [2 n]) ⩽ N_{{FO}_{n}} = F_{n}^{0} - 1$ and $DN (MSO [2 n]), LS (MSO [2 n]), H (MSO [2 n]) ⩽ N_{{MSO}_{n}} = M_{n}^{0, 0} - 1$ .

3.2. Number of ${FO}_{k}$ -types

As we have seen in the previous subsection, the numbers of ${FO}_{k}$ -types and ${MSO}_{k}$ -types give upper bounds for the corresponding definability, Löwenheim–Skolem and Hanf-numbers. It is well known that on finite relational structures, for ${FO}_{k}$ 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 ${MSO}_{k}$ . 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 $F_{k}^{0}$ denotes the number of $\equiv_{{FO}_{k}}$ -types of Σ-words w, where we include the case $w = ε$ . To obtain upper bounds for $F_{k}^{0}$ , we also need to consider the number $F_{k}^{1}$ of $\equiv_{{FO}_{k}}$ -types of 1-interpretations $(w, p)$ . We start by showing that ${FO}_{k}$ -equivalence of 1-interpretations reduces to ${FO}_{k}$ -equivalence of corresponding initial and end segments of the words, and ${FO}_{k + 1}$ -equivalence of words reduces to ${FO}_{k}$ -equivalence of 1-interpretations arising from the words.

Let $w = a_{1} \dots a_{ℓ}$ be a Σ-word, and let $p \in [ℓ]$ . We denote the initial segment $a_{1} \dots a_{p - 1}$ of w by $w_{< p}$ and the end segment $a_{p + 1} \dots a_{ℓ}$ by $w_{> p}$ . Furthermore, we denote the single letter word $a_{p}$ by $w (p)$ .

Lemma 3.6.
Assume that $k \in N$ , $w \in Σ^{ℓ}$ , $v \in Σ^{m}$ , $p \in [ℓ]$ , and $q \in [m]$ . Then
$(w, p) \equiv_{{FO}_{k}} (v, q)$ if and only if $w_{< p} \equiv_{{FO}_{k}} v_{< q}$ , $w_{> p} \equiv_{{FO}_{k}} v_{> q}$ , and $w (p) = v (q)$ .

$w \equiv_{{FO}_{k + 1}} v$ if and only if for every $p \in [ℓ]$ there is $q \in [m]$ such that $(w, p) \equiv_{{FO}_{k}} (v, q)$ , and vice versa, for every $q \in [m]$ there is $p \in [ℓ]$ such that $(w, p) \equiv_{{FO}_{k}} (v, q)$ .

Proof.
(a) Assume first that the conditions
$w_{< p} \equiv_{{FO}_{k}} v_{< q}$ , $w_{> p} \equiv_{{FO}_{k}} v_{> q}$ , and $w (p) = v (q)$
hold. Then $(w, p) = w_{< p} \cdot (w (p), 1) \cdot w_{> p}$ , $(v, q) = v_{< q} \cdot (v (q), 1) \cdot v_{> q}$ , and trivially $(w (p), 1) \equiv_{{FO}_{k}} (v (q), 1)$ , and hence by Theorem 3.1, $(w, p) \equiv_{{FO}_{k}} (v, q)$ .

On the other hand, if $w_{< p} ≢_{{FO}_{k}} v_{< q}$ , then $w_{< p} ⊧ φ$ and $v_{< q} ⊭ φ$ for some sentence $φ \in {FO}_{k}$ . 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 $\exists y θ$ by $\exists y (y < x \land θ)$ , and each universal subformula $\forall y θ$ by $\forall y (y < x \to θ)$ . Since the quantifier rank of ψ is the same as that of φ, we see that $(w, p) ≢_{{FO}_{k}} (v, q)$ . Similarly, if $w_{> p} ≢_{{FO}_{k}} v_{> q}$ , then $(w, p) ≢_{{FO}_{k}} (v, q)$ . It is also immediately clear that if $w (p) \neq v (q)$ , then $(w, p) ≢_{{FO}_{k}} (v, q)$ . Thus, if $()$ does not hold, then $(w, p) ≢_{{FO}_{k}} (v, q)$ .

Claim (b) is just the standard back-and-forth characterization for $\equiv_{{FO}_{k + 1}}$ (see [1] Theorem 2.3.3). □

We consider next the number of equivalence classes of words with respect ${FO}_{0}$ , ${FO}_{1}$ and ${FO}_{2}$ . In the proof of the following lemma, we denote the set of letters $α \in Σ$ that occur in a word $w \in Σ^{}$ by $l (w)$ . Thus, e.g., $l (a a) = {a}$ and $l (a b b a) = {a, b}$ .
Lemma 3.7.
$F_{0}^{0} = 1$ , $F_{1}^{0} = 4$ , and $F_{2}^{0} ⩽ 97$ .
Proof.
Clearly all words are equivalent with respect to ${FO}_{0}$ , as there are no quantifier-free sentences. Hence $F_{0}^{0} = 1$ . Furthermore, it is easy to see that two words $w, v \in Σ^{}$ are equivalent with respect to ${FO}_{1}$ if and only if $l (w) = l (v)$ . Thus, $F_{1}^{0} = | P (Σ) | = 4$ . (Note that ∅ corresponds to the equivalence class containing only the empty word.)

To prove that $F_{2}^{0} ⩽ 97$ we give a list of 97 Σ-words, and show that every word $w \in Σ^{}$ is ${FO}_{2}$ -equivalent with one of the words in the list. We list the words in groups based on the total number of chains.
the empty word ε (the unique word without a- or b-chains)

$a^{r}$ and $b^{r}$ for $r \in [3]$

$a^{r} b^{s}$ and $b^{r} a^{s}$ for $r, s \in [3]$

$a^{r} b^{s} a^{t}$ and $b^{r} a^{s} b^{t}$ for $r, t \in [2]$ and $s \in [3]$

$a^{r} b^{s} a^{t} b^{u}$ and $b^{r} a^{s} b^{t} a^{u}$ for $r, s, t, u \in [2]$

$a^{r} b^{s} a b a^{t}$ and $b^{r} a^{s} b a b^{t}$ for $r, s, t \in [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 \in Σ^{}$ there is a word v in the list such that $w \equiv_{{FO}_{2}} v$ . 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 \in Σ^{ℓ}$ and $v \in Σ^{m}$ are ${FO}_{2}$ -equivalent it suffices to show that there is a relation $R \subseteq [ℓ] \times [m]$ such that $dom (R) = [ℓ]$ , $ran (R) = [m]$ , and the condition
$w_{< p} \equiv_{{FO}_{1}} v_{< q}$ , $w_{> p} \equiv_{{FO}_{1}} v_{> q}$ , and $w (p) = v (q)$
holds for any pair $(p, q) \in 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 ${FO}_{1}$ -equivalent if an only if $l (w^{'}) = l (v^{'})$ . Thus, the condition $()$ above can be replaced with the condition
$l (w_{< p}) = l (v_{< q})$ , $l (w_{> p}) = l (v_{> q})$ , and $w (p) = v (q)$ .

Assume now that $w \in Σ^{}$ . We have the following cases based on the number of chains in w.
The case $w = ε$ is trivial.

Assume that $w = a^{k}$ for some $k ⩾ 1$ . If $k ⩽ 3$ , then w is in the list, and hence the claim holds. If $k > 3$ , we let $v = a^{3}$ . Then the following hold:
$w (p) = v (q) = a$ for all $p \in [k]$ and $q \in [3]$ ,

for any $p \in [k]$ , $w_{< p} = a^{p - 1}$ and $w_{> p} = a^{k - p}$ ,

for any $q \in [3]$ , $v_{< q} = a^{q - 1}$ and $v_{> q} = a^{3 - q}$ .
Thus defining $R : = {(1, 1), (k, 3)} \cup {(p, 2) | 1 < p < k}$ , we see that $l (w_{< p}) = l (v_{< q})$ , $l (w_{> p}) = l (v_{> q})$ and $w (p) = v (q)$ whenever $(p, q) \in R$ . Hence we have $w \equiv_{{FO}_{2}} v$ .

Assume next that $w = a^{k} b^{ℓ}$ for some $k, ℓ ⩾ 1$ . Let $v = a^{r} b^{s}$ , where $r = min {k, 3}$ and $s = min {ℓ, 3}$ . Then v is in group (2), and by case (1), $a^{k} \equiv_{{FO}_{2}} a^{r}$ and $b^{ℓ} \equiv_{{FO}_{2}} b^{s}$ . Hence $w \equiv_{{FO}_{2}} v$ follows from Theorem 3.1.

Assume then that $w = a^{k} b^{ℓ} a^{m}$ for some $k, ℓ, m ⩾ 1$ . Let $v = a^{r} b^{s} a^{t}$ , where $r = min {k, 2}$ , $s = min {ℓ, 3}$ and $t = min {m, 2}$ . Then v is in group (3). Let $R \subseteq [k + ℓ + m] \times [r + s + t]$ consist of pairs $(p, q)$ of points that are in corresponding positions in corresponding chains, i.e., $R = R_{1} \cup R_{2} \cup R_{3}$ , where
$R_{1} = {(1, 1)} \cup {(p, r) | 1 < p ⩽ k}$ ,

$R_{2} = {(k + 1, r + 1), (k + ℓ, r + s)} \cup {(p, r + 2) | k + 1 < p < k + ℓ}$ ,

$R_{3} = {(k + ℓ + m, r + s + t)} \cup {(p, r + s + 1) | k + ℓ < p < k + ℓ + m}$ .
Thus, $R_{1}$ relates the first a in the chain $a^{k}$ to the first a in $a^{r}$ , and the rest of the a’s in $a^{k}$ to the second a in $a^{r}$ (note however, that if $k = r = 1$ , then the second part in $R_{1}$ is empty.) Similarly, $R_{2}$ relates the first and last b in the chain $b^{ℓ}$ to the first and last b, resp., in $b^{s}$ , and all other b’s in $b^{ℓ}$ to the second b in $b^{s}$ . Finally, $R_{3}$ is similar to $R_{1}$ , except that the last a’s in the chains $a^{m}$ and $a^{t}$ are related.

Clearly R is total on w and v. We show now that $(⋆)$ holds for all pairs in R. For all pairs $(p, q) \in R$ it is obvious that $w (p) = v (q)$ , as R respects the correspondence between chains. For the pair $(1, 1) \in R_{1}$ we have $l (w_{< 1}) = l (v_{< 1}) = \emptyset$ and $l (w_{> 1}) = l (v_{> 1}) = {a, b}$ . For pairs $(p, r)$ in the second part of $R_{1}$ 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 $R_{2}$ , 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 $R_{2}$ we have $l (w_{< p}) = l (v_{< q}) = l (w_{> p}) = l (v_{> q}) = {a, b}$ . Finally, the pairs in $R_{3}$ are handled symmetrically to those in $R_{1}$ .

Assume then that $w = a^{k} b^{ℓ} a^{m} b^{n}$ for some $k, ℓ, m, n ⩾ 1$ . Let $v = a^{r} b^{s} a^{t} b^{u}$ , 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 $a^{k}$ and $b^{ℓ}$ with the first elements of $a^{r}$ and $b^{s}$ , respectively, and the rest of the points in these chains (if any) with the second elements in $a^{r}$ and $b^{s}$ . The points in the last two chains $a^{m}$ , $b^{n}$ , $a^{t}$ and $b^{u}$ are related in a symmetric way. Thus, we define $R = R_{1} \cup R_{2} \cup R_{3} \cup R_{4} \subseteq [k + ℓ + m + n] \times [r + s + t + u]$ by setting
$R_{1} = {(1, 1)} \cup {(p, r) | 1 < p ⩽ k}$ ,

$R_{2} = {(k + 1, r + 1)} \cup {(p, r + s) | k + 1 < p ⩽ k + ℓ}$ ,

$R_{3} = {(k + ℓ + m, r + s + t)} \cup {(p, r + s + 1) | k + ℓ < p < k + ℓ + m}$ ,

$R_{4} = {(k + ℓ + m + n, r + s + t + u)} \cup {(p, r + s + t + 1) | k + ℓ + m < p < k + ℓ + m + n}$ .
Clearly R is total on w and v, and with a similar argument as in case (3), we can verify that $(⋆)$ holds for all pairs $(p, q) \in R$ .

Assume then that $w = a^{k} b^{ℓ} a^{m} b^{n} a^{o}$ for some $k, ℓ, m, n, o ⩾ 1$ . This time we let $v = a^{r} b^{s} a b a^{t}$ , 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 $R_{1}$ , $R_{2}$ , $R_{3}$ , $R_{4}$ and $R_{5}$ between the corresponding chains with a similar idea as in the previous cases:
$R_{1} = {(1, 1)} \cup {(p, r) | 1 < p ⩽ k}$ ,

$R_{2} = {(k + 1, r + 1)} \cup {(p, r + s) | k + 1 < p ⩽ k + ℓ}$ ,

$R_{3} = {(p, r + s + 1) | k + ℓ < p ⩽ k + ℓ + m}$ ,

$R_{4} = {(k + ℓ + m + n, r + s + 2)}$ ,

$R_{5} = {(k + ℓ + m + n + o, r + s + 2 + t)} \cup {(p, r + s + 3) | k + ℓ + m + n < p < r + s + 2 + t}$ .
However, this time we need one more relation that does not respect corresponding chains: if $n ⩾ 2$ , we need to relate the $n - 1$ first b’s in the chain $b^{n}$ to the second b in $b^{s}$ . Thus we define
$R_{6} = {(p, r + s) | k + ℓ + m < p < k + ℓ + m + n}$ .
We leave it to the reader to verify that the relation $R = R_{1} \cup R_{2} \cup R_{3} \cup R_{4} \cup R_{5} \cup R_{6}$ is total on w and v, and all pairs $(p, q) \in R$ satisfy the condition $(⋆)$ .

Assume then that $w = a^{k_{1}} b^{ℓ_{1}} \dots a^{k_{e}} b^{ℓ_{e}}$ , where $e ⩾ 3$ and $k_{i}, ℓ_{i} ⩾ 1$ for all $i \in [e]$ . By case (4), it suffices to show that $w \equiv_{{FO}_{2}} w^{'}$ , where $w^{'} = a^{k_{1}} b^{m} a^{n} b^{ℓ_{e}}$ , $m = ℓ_{1} + \dots + ℓ_{e - 1}$ and $n = k_{2} + \dots + k_{e}$ . 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) \in R$ .

The case in which w is of the form $a^{k_{1}} b^{ℓ_{1}} \dots a^{k_{e}} b^{ℓ_{e}} a^{k_{e + 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 $F_{2}^{0} = 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 $F_{k}^{0}$ 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 \in N$ , $F_{k}^{1} = 2 {(F_{k}^{0})}^{2}$ .
Proof.
Let $w \in Σ^{ℓ}$ , $v \in Σ^{m}$ , $p \in [ℓ]$ , and $q \in [m]$ . By Lemma 3.6(a), $(w, p) \equiv_{{FO}_{k}} (v, q)$ if and only if $w_{< p} \equiv_{{FO}_{k}} v_{< q}$ , $w_{> p} \equiv_{{FO}_{k}} v_{> q}$ , and $w (p) = v (p)$ . Clearly this means that there is a one-to-one correspondence between the set $F_{k}^{1}$ and the set $F_{k}^{0} \times Σ \times F_{k}^{0}$ , and consequently we get $F_{k}^{1} = | F_{k}^{0} \times Σ \times F_{k}^{0} | = 2 {(F_{k}^{0})}^{2}$ . □

Let w be a Σ-word with $| w | = ℓ$ . We denote the set of all $\equiv_{{FO}_{k}}$ -equivalence classes of pairs $(w, p)$ , $p \in [ℓ]$ , by $F_{k}^{1} (w)$ . Note that $F_{k}^{1} (w) \subseteq F_{k}^{1}$ .
Lemma 3.10.
For any $k \in N$ , $F_{k + 1}^{0} ⩽ 2^{2 {(F_{k}^{0})}^{2}}$ .
Proof.
Let w and v be Σ-words. It follows from Lemma 3.6(b) that if $F_{k}^{1} (w) = F_{k}^{1} (v)$ , then $w \equiv_{{FO}_{k + 1}} v$ . In other words, the ${FO}_{k + 1}$ -type of w is uniquely determined by the set $F_{k}^{1} (w) \subseteq F_{k}^{1}$ . Hence $F_{k + 1}^{0} ⩽ | P (F_{k}^{1}) | = 2^{F_{k}^{1}} = 2^{2 {(F_{k}^{0})}^{2}}$ . □
Theorem 3.11.
For any $k \in N$ , $F_{k}^{0} ⩽ \sqrt{tower (k + 2)}$ . Hence also $N_{{FO}_{k}} = F_{k}^{0} - 1 ⩽ \sqrt{tower (k + 2)}$ .
Proof.
By Lemma 3.7, $F_{0}^{0} = 1$ and $F_{1}^{0} = 4$ . On the other hand, $\sqrt{tower (2)} = \sqrt{4} = 2$ and $\sqrt{tower (3)} = \sqrt{16} = 4$ . Hence the claim holds for $k = 0$ and $k = 1$ .

For $k ⩾ 2$ , we prove the stronger claim
$F_{k}^{0} ⩽ \frac{1}{2} \sqrt{tower (k + 2)} - 1$
by induction on k. In the case $k = 2$ we have $F_{k}^{0} ⩽ 97$ by Lemma 3.7, and $\frac{1}{2} \sqrt{tower (k + 2)} - 1 = \frac{1}{2} \sqrt{2^{16}} - 1 = 2^{7} - 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: $\begin{aligned} F_{k + 1}^{0} & ⩽ 2^{2 {(F_{k}^{0})}^{2}} \\ ⩽ 2^{\frac{1}{2} tower (k + 2) - 2 \sqrt{tower (k + 2)} + 2} \\ ⩽ 2^{\frac{1}{2} tower (k + 2) - 2} \\ = \frac{1}{4} {(2^{tower (k + 2)})}^{\frac{1}{2}} \\ ⩽ \frac{1}{2} \sqrt{tower (k + 3)} - 1 . \end{aligned}$ 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 ${FO}_{k}$ .
Corollary 3.12.
For any $k \in N$ , $DN ({FO}_{k}), LS ({FO}_{k}), H ({FO}_{k}) ⩽ \sqrt{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 \in N$ , $DN (FO [n]), LS (FO [n]), H (FO [n]) ⩽ \sqrt{tower (n / 2 + 2)}$ .

3.3. Number of ${MSO}_{k}$ -types

In this subsection we prove an upper bound for the number of ${MSO}_{k}$ -types of Σ-words. Recall that we denote by $M_{k}^{r, 0}$ the number of ${MSO}_{k}$ -types of interpretations of the form $(w, P_{1}, \dots, P_{r})$ , and by $M_{k}^{r, 1}$ the number of ${MSO}_{k}$ -types of interpretations $(w, P_{1}, \dots, P_{r}, p)$ . We proceed with similar steps as in the previous subsection: we compute first the numbers $M_{0}^{r, 0}$ and $M_{1}^{r, 0}$ . Then we prove a recursion formula for $M_{k + 1}^{r, 0}$ in terms of $M_{k}^{r + 1, 0}$ . This proof is based on reducing $M_{k}^{r, 1}$ to $M_{k}^{r, 0}$ and $M_{k + 1}^{r, 0}$ to $M_{k}^{r + 1, 1}$ , in analogue with Lemmas 3.9 and 3.10.

Lemma 3.14.
For any $r \in N$ , $M_{0}^{r, 0} = 1$ and $M_{1}^{r, 0} = 2^{2^{r + 1}}$ .
Proof.
All $(r, 0)$ -interpretations $(w, \bar{B})$ are equivalent with respect to ${MSO}_{0}$ , as there are no formulas that do not contain any first-order variables. Hence $M_{0}^{r, 0} = 1$ .

To prove the second claim, we introduce first some auxiliary notions. Let $(w, \bar{P}, p) = (w, P_{1}, \dots, P_{r}, p)$ be an $(r, 1)$ -interpretation. The atomic profile of p in $(w, \bar{P})$ is $pr (w, \bar{P}, p) : = {i \in [r + 1] | p \in P_{i}}$ , where $P_{r + 1} : = P_{a}$ . Note that here the letter a is treated via the predicate $P_{a}$ and the letter b is then handled as the complement of $P_{a}$ . Furthermore, the total atomic profile of $(w, \bar{P})$ is $\Pr (w, \bar{P}) : = {pr (w, \bar{P}, p) | p \in [ℓ]}$ , where $ℓ = | w |$ .

Observe now that two $(r, 0)$ -interpretations $(w, \bar{P})$ and $(v, \bar{Q})$ cannot be separated in ${MSO}_{1}$ by any formula starting with a second-order quantifier. Thus, $(w, \bar{P})$ and $(v, \bar{Q})$ are equivalent with respect to ${MSO}_{1}$ 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, \bar{P}, p) \equiv_{{MSO}_{0}} (v, \bar{Q}, q)$ . Clearly $(w, \bar{P}, p) \equiv_{{MSO}_{0}} (v, \bar{Q}, q)$ holds if and only if $pr (w, \bar{P}, p) = pr (v, \bar{Q}, q)$ . Thus we see that $(w, \bar{P}) \equiv_{{MSO}_{1}} (v, \bar{Q})$ if and only if $\Pr (w, \bar{P}) = \Pr (v, \bar{Q})$ . In other words, the set $\Pr (w, \bar{P}) \subseteq P ([r + 1])$ uniquely determines the $\equiv_{{MSO}_{1}}$ -equivalence class of $(w, \bar{P})$ . Note further that for any subset $X \subseteq P ([r + 1])$ there exists an $(r, 0)$ -interpretation $(w, \bar{P})$ such that $\Pr (w, \bar{P}) = X$ . Thus we conclude that $M_{1}^{r, 0} = | P (P ([r + 1])) | = 2^{2^{r + 1}}$ . □

We prove next the analogue of Lemma 3.9 for ${MSO}_{k}$ . In the proof we use the following notation: if $(w, \bar{P}) = (w, P_{1}, \dots, P_{r})$ is an $(r, 0)$ -interpretation and $p \in [ℓ]$ for $ℓ = | w |$ , then $P_{< p, i} : = P_{i} \cap [p - 1]$ for each $i \in [r]$ , and ${\bar{P}}_{< p} = (P_{< p, 1}, \dots, P_{< p, r})$ . The notations $P_{> p, i}$ and ${\bar{P}}_{> p}$ are defined analogously.
Lemma 3.15.
For any $k, r \in N$ , $M_{k}^{r, 1} = 2^{r + 1} {(M_{k}^{r, 0})}^{2}$ .
Proof.
Assume that $(w, \bar{P}, p)$ and $(v, \bar{Q}, q)$ are $(r, 1)$ -interpretations. With a similar argument as in the proof of Lemma 3.6(a), we see that $(w, \bar{P}, p) \equiv_{{MSO}_{k}} (v, \bar{Q}, q)$ if and only if the condition $\begin{aligned} (†) & (w_{< p}, {\bar{P}}_{< p}) \equiv_{{MSO}_{k}} (v_{< q}, {\bar{Q}}_{< q}), (w_{> p}, {\bar{P}}_{> p}) \equiv_{{MSO}_{k}} (v_{> q}, {\bar{Q}}_{> q}), w (p) = v (q), \\ and {i \in [r] | p \in P_{i}} = {i \in [r] | q \in Q_{i}} \end{aligned}$ holds. Thus, we see that there is a one-to-one correspondence between the sets $M_{k}^{r, 1}$ and $M_{k}^{r, 0} \times Σ \times P ([r]) \times M_{k}^{r, 0}$ , and hence $M_{k}^{r, 1} = 2 \cdot | P ([r]) | \cdot {(M_{k}^{r, 0})}^{2} = 2^{r + 1} {(M_{k}^{r, 0})}^{2}$ . □

Next we prove the recursion formula for the numbers $M_{k}^{r, 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, \bar{P})$ be an $(r, 0)$ -interpretation with $| w | = ℓ$ . We denote the set of all $\equiv_{{MSO}_{k}}$ -equivalence classes of $(r, 1)$ -interpretations $(w, \bar{P}, p)$ , $p \in [ℓ]$ , by $M_{k}^{r, 1} (w, \bar{P})$ and the set of all $\equiv_{{MSO}_{k}}$ -equivalence classes of $(r + 1, 0)$ -interpretations $(w, \bar{P} Q)$ , $Q \subseteq [ℓ]$ , by $M_{k}^{r + 1, 0} (w, \bar{P})$ . Note that $M_{k}^{r, 1} (w, \bar{P}) \subseteq M_{k}^{r, 1}$ and $M_{k}^{r + 1, 0} (w, \bar{P}) \subseteq M_{k}^{r + 1, 0}$ .
Lemma 3.16.
For any $k ⩾ 1$ , $M_{k + 1}^{r, 0} ⩽ 2^{{(M_{k}^{r + 1, 0})}^{3}}$ .
Proof.
Let $(w, \bar{P})$ and $(v, \bar{Q})$ be interpretations, where $| w | = ℓ$ and $| v | = m$ . Using again the standard back-and-forth argument, $(w, \bar{P}) \equiv_{{MSO}_{k + 1}} (v, \bar{Q})$ if and only if the following conditions hold:
for every $p \in [ℓ]$ there is $q \in [m]$ such that $(w, \bar{P}, p) \equiv_{{MSO}_{k}} (v, \bar{Q}, q)$ ,

for every $q \in [m]$ there is $p \in [ℓ]$ such that $(w, \bar{P}, p) \equiv_{{MSO}_{k}} (v, \bar{Q}, q)$ ,

for every $R \subseteq [ℓ]$ there is $S \subseteq [m]$ such that $(w, \bar{P} R) \equiv_{{MSO}_{k}} (v, \bar{Q} S)$ , and

for every $S \subseteq [m]$ there is $R \subseteq [ℓ]$ such that $(w, \bar{P} R) \equiv_{{MSO}_{k}} (v, \bar{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 $M_{k}^{r, 1} (w, \bar{P}) = M_{k}^{r, 1} (v, \bar{Q})$ and $M_{k}^{r + 1, 0} (w, \bar{P}) = M_{k}^{r + 1, 0} (v, \bar{Q})$ , then $(w, \bar{P}) \equiv_{{MSO}_{k + 1}} (v, \bar{Q})$ . This means that the ${MSO}_{k + 1}$ -type of $(w, \bar{P})$ is uniquely determined by the two sets $M_{k}^{r, 1} (w, \bar{P})$ and $M_{k}^{r + 1, 0} (w, \bar{P})$ , and consequently $M_{k + 1}^{r, 0} ⩽ | P (M_{k}^{r, 1}) \times P (M_{k}^{r + 1, 0}) | = 2^{M_{k}^{r, 1}} \cdot 2^{M_{k}^{r + 1, 0}}$ which is equal to $2^{2^{r + 1} {(M_{k}^{r, 0})}^{2} + M_{k}^{r + 1, 0}}$ by Lemma 3.15.

Clearly $M_{k}^{r, 0} ⩽ M_{k}^{r + 1, 0}$ , and hence $M_{k + 1}^{r, 0} ⩽ 2^{(2^{r + 1} + 1) {(M_{k}^{r + 1, 0})}^{2}}$ . The claim follows from this since by Lemma 3.14, $2^{r + 1} + 1 ⩽ M_{1}^{r + 1, 0}$ and clearly $M_{1}^{r + 1, 0} ⩽ M_{k}^{r + 1, 0}$ for any $k ⩾ 1$ . □
Theorem 3.17.
For any $k \in N$ and $r \in N$ , $M_{k}^{r, 0} ⩽ \sqrt[3]{\frac{1}{4} tower (k + 1, k + r + 2)}$ . In particular, $N_{{MSO}_{k}} = M_{k}^{0, 0} - 1 ⩽ \sqrt[3]{\frac{1}{4} tower (k + 1, k + 2)}$ .
Proof.
We prove that the claim holds for any r by induction on k. By Lemma 3.14, we have $M_{0}^{r, 0} = 1$ and $M_{1}^{r, 0} = 2^{2^{r + 1}}$ . On the other hand, we have $\sqrt[3]{\frac{1}{4} tower (1, r + 2)} = {(\frac{1}{4} 2^{r + 2})}^{1 / 3} = 2^{r / 3} ⩾ 1$ and $\sqrt[3]{\frac{1}{4} tower (2, r + 3)} = {(\frac{1}{4} 2^{2^{r + 3}})}^{1 / 3} = 2^{\frac{1}{3} (2^{r + 3} - 2)} ⩾ 2^{2^{r + 1}}$ , since $\frac{1}{3} (2^{r + 3} - 2) ⩾ \frac{1}{3} (\frac{3}{4} 2^{r + 3}) = 2^{r + 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: $\begin{aligned} M_{k + 1}^{r, 0} & ⩽ 2^{{(M_{k}^{r + 1, 0})}^{3}} \\ ⩽ 2^{\frac{1}{4} tower (k + 1, k + r + 3)} \\ ⩽ 2^{\frac{1}{3} (tower (k + 1, k + r + 3) - 2)} \\ = {(\frac{1}{4} 2^{tower (k + 1, k + r + 3)})}^{\frac{1}{3}} \\ = \sqrt[3]{\frac{1}{4} tower (k + 2, k + r + 3)} . \end{aligned}$ 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 \in N$ , $DN ({MSO}_{k}), LS ({MSO}_{k}), H ({MSO}_{k}) ⩽ \sqrt[3]{\frac{1}{4} tower (k + 1, k + 2)}$ .

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 \in N$ , $DN (MSO [n]), LS (MSO [n]), H (MSO [n]) ⩽ \sqrt[3]{\frac{1}{4} tower (n / 2 + 1, n / 2 + 2)}$ .

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 $V_{i}$ of the cumulative hierarchy are defined by $V_{0} = \emptyset$ and $V_{i + 1} = P (V_{i})$ . We represent finite sets as words using only braces { and } in a straightforward fashion. For example $V_{0}$ is encoded as ${}$ and $V_{1}$ as ${{}}$ . $V_{2}$ has two possible encodings: ${{} {{}}}$ and ${{{}} {}}$ . It is well known that $| V_{i + 1} | = tower (i)$ . Thus the encodings of $V_{i + 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) : = P_{a} (x)$ and $R (x) : = P_{b} (x)$ that say x is a left or right brace, respectively. We also define $S (x, y) : = x < y \land \neg \exists 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 $\overline{x} : = (x_{1}, x_{2})$ , and similarly for different letters, to denote these pairs. To ensure that our formula defines a single encoding of $V_{i}$ , 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 (\overline{x}, θ (s, t))$ : the common core formula used in the formulas ${set}_{i}$ and ${oset}_{i}$ defined below. States that every brace y between $x_{1}$ and $x_{2}$ 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. $\begin{aligned} core (\overline{x}, θ (s, t)) & : = x_{1} < x_{2} \land L (x_{1}) \land R (x_{2}) \\ \land \forall y (x_{1} < y < x_{2} \to \exists z (x_{1} < z < x_{2} \land y \neq z \\ \land \exists s \exists t ((y < z \to (s = y \land t = z)) \\ \land (z < y \to (s = z \land t = y)) \land θ (s, t)))) \end{aligned}$

${set}_{i} (\overline{x})$ : $\overline{x}$ correctly encodes a set in $V_{i + 1}$ , possibly with repetition. Size linear in i. $\begin{aligned} {set}_{0} (\overline{x}) : = L (x_{1}) \land R (x_{2}) \land S (x_{1}, x_{2}) \\ {set}_{i + 1} (\overline{x}) : = core (\overline{x}, {set}_{i} (s, t)) \end{aligned}$

$\overline{x} \in_{i} \overline{y}$ : $\overline{x}$ is an element of $\overline{y}$ . Size linear in i. Assumes that $\overline{x}$ encodes a set in $V_{i + 1}$ and $\overline{y}$ encodes a set in $V_{i + 2}$ . The part with $\overline{z}$ is used to ensure that $\overline{x}$ is an element of $\overline{y}$ and not for example an element of an element. $\begin{aligned} \overline{x} \in_{i} \overline{y} & : = y_{1} < x_{1} < x_{2} < y_{2} \land \neg \exists \overline{z} ({set}_{i} (\overline{z}) \land y_{1} < z_{1} < x_{1} \land x_{2} < z_{2} < y_{2}) \end{aligned}$

$\overline{x} \sim_{i} \overline{y}$ : $\overline{x}$ and $\overline{y}$ encode the same set, possibly in a different order. Size $O (i^{2})$ . Assumes $\overline{x}$ and $\overline{y}$ encode sets in $V_{i + 1}$ . The two implications on the second line are used to deal with the symmetry of $\overline{x}$ and $\overline{y}$ at once, making the formula smaller. $\begin{aligned} \overline{x} \sim_{0} \overline{y} : = ⊤ \\ \begin{aligned} \overline{x} \sim_{i + 1} \overline{y} & : = \forall \overline{a} ({set}_{i} (\overline{a}) \to \exists \overline{b} ({set}_{i} (\overline{b}) \\ \land (\overline{a} \in_{i} \overline{x} \to \overline{b} \in_{i} \overline{y}) \land (\overline{a} \in_{i} \overline{y} \to \overline{b} \in_{i} \overline{x}) \land \overline{a} \sim_{i} \overline{b})) \end{aligned} \end{aligned}$

$\overline{x} ≺_{i} \overline{y}$ : the $≺_{i - 1}$ -greatest element of the symmetric difference of $\overline{x}$ and $\overline{y}$ is in $\overline{y}$ . Size $O (i^{3})$ . Defines a linear order for encoded sets in $V_{i + 1}$ . The set $\overline{z}$ is in $\overline{y}$ , is not in $\overline{x}$ and is larger than any $\overline{a}$ that is in $\overline{x}$ but not in $\overline{y}$ . $\begin{aligned} \overline{x} ≺_{0} \overline{y} : = ⊥ \\ \begin{aligned} \overline{x} ≺_{i + 1} \overline{y} & : = \exists \overline{z} ({set}_{i} (\overline{z}) \land \overline{z} \in_{i} \overline{y} \land \forall \overline{a} (({set}_{i} (\overline{a}) \land \overline{a} \in_{i} \overline{x}) \\ \to (\overline{a} ≁_{i} \overline{z} \land (\exists \overline{b} ({set}_{i} (\overline{b}) \land \overline{b} \in_{i} \overline{y} \land \overline{a} \sim_{i} \overline{b}) \lor \overline{a} ≺_{i} \overline{z})))) \end{aligned} \end{aligned}$

${oset}_{i} (\overline{x})$ : $\overline{x}$ correctly encodes a set in $V_{i + 1}$ with no repetition and with the elements in the linear order given by the formula $\overline{x} ≺_{i} \overline{y}$ . Size $O (i^{4})$ . Ensures that only a singular word satisfies our formula. $\begin{aligned} {oset}_{0} (\overline{x}) : = L (x_{1}) \land R (x_{2}) \land S (x_{1}, x_{2}) \\ \begin{aligned} {oset}_{i + 1} (\overline{x}) & : = core (\overline{x}, {oset}_{i} (s, t)) \land \forall \overline{a} \forall \overline{b} (({set}_{i} (\overline{a}) \land {set}_{i} (\overline{b}) \\ \land \overline{a} \in_{i} \overline{x} \land \overline{b} \in_{i} \overline{x} \land a_{1} < b_{1}) \to \overline{a} ≺_{i} \overline{b}) \end{aligned} \end{aligned}$

${add}_{i} (\overline{x}, \overline{y}, \overline{z})$ : States that $\overline{x} = \overline{y} \cup {\overline{z}}$ . Size $O (i^{2})$ . Assumes $\overline{x}$ and $\overline{y}$ encode sets in $V_{i + 1}$ and $\overline{z}$ encodes a set in $V_{i}$ . The first line states that $\overline{y} \subseteq \overline{x}$ , the second line states $\overline{z} \in \overline{x}$ and the two final lines state $\overline{x} ∖ {\overline{z}} \subseteq \overline{y}$ . $\begin{aligned} {add}_{i + 1} (\overline{x}, \overline{y}, \overline{z}) & : = \forall \overline{a} (({set}_{i} (\overline{a}) \land \overline{a} \in_{i} \overline{y}) \to \exists \overline{b} ({set}_{i} (\overline{b}) \land \overline{b} \in_{i} \overline{x} \land \overline{a} \sim_{i} \overline{b})) \\ \land \exists \overline{c} ({set}_{i} (\overline{c}) \land \overline{c} \in_{i} \overline{x} \land \overline{c} \sim_{i} \overline{z} \\ \land \forall \overline{d} (({set}_{i} (\overline{d}) \land \overline{d} \in_{i} \overline{x} \land d_{1} \neq c_{1}) \\ \to \exists \overline{e} ({set}_{i} (\overline{e}) \land \overline{e} \in_{i} \overline{y} \land \overline{e} \sim_{i} \overline{d}))) \end{aligned}$

$V_{i} (\overline{x})$ : $\overline{x}$ encodes the set $V_{i}$ . Size $O (i^{5})$ . States that $\overline{x}$ is an ordered encoding, $\emptyset \in \overline{x}$ , $V_{i - 1} \in \overline{x}$ and for all $\overline{c} \in \overline{x}$ and $\overline{d} \in V_{i - 1}$ , we have $\overline{c} \cup {\overline{d}} \in \overline{x}$ . $\begin{aligned} V_{0} (\overline{x}) : = {set}_{0} (\overline{x}) \\ \begin{aligned} V_{i + 1} (\overline{x}) & : = {oset}_{i + 1} (\overline{x}) \land \exists \overline{a} (V_{0} (\overline{a}) \land S (x_{1}, a_{1})) \land \exists \overline{b} (V_{i} (\overline{b}) \land S (b_{2}, x_{2}) \\ \land \forall \overline{c} \forall \overline{d} (({set}_{i} (\overline{c}) \land \overline{c} \in_{i} \overline{x} \land {set}_{i - 1} (\overline{d}) \land \overline{d} \in_{i - 1} \overline{b}) \\ \to \exists \overline{e} ({set}_{i} (\overline{e}) \land \overline{e} \in_{i} \overline{x} \land {add}_{i} (\overline{e}, \overline{c}, \overline{d})))) \end{aligned} \end{aligned}$

$ψ_{i}$ : the entire word is the ordered encoding of the set $V_{i}$ . Size $O (i^{5})$ . $\begin{array}{r} ψ_{i} : = \exists x \exists y \forall z (x ⩽ z \land z ⩽ y \land V_{i} (x, y)) \end{array}$

The formula $ψ_{i + 1}$ defines a word w that, as an encoding of the set $V_{i + 1}$ , has length at least $tower (i)$ . The size of $ψ_{i + 1}$ is $O ({(i + 1)}^{5})$ and thus $O (i^{5})$ . Let c be a constant such that $sz (ψ_{i + 1}) ⩽ c \cdot i^{5}$ so $w \in Def (FO [c \cdot i^{5}])$ . As we want to relate the length of w to the size of $ψ_{i}$ , we set $n = c \cdot i^{5}$ and obtain the following result:

Theorem 4.1.
For some constant $c \in N$ there are infinitely many $n \in N$ satisfying $\begin{matrix} DN (FO [n]) ⩾ tower (⌊ \sqrt[5]{n / c} ⌋) . \end{matrix}$

Proposition 2.10 immediately gives the same bound for the Hanf number.
Corollary 4.2.
For some constant $c \in N$ there are infinitely many $n \in N$ satisfying $\begin{matrix} H (FO [n]) ⩾ tower (⌊ \sqrt[5]{n / c} ⌋) . \end{matrix}$

By omitting the subformula ${oset}_{i + 1}$ from the above we get a formula of size $O (i^{3})$ 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 \in N$ there are arbitrarily large $n \in N$ satisfying $\begin{matrix} LS (FO [n]) ⩾ tower (⌊ \sqrt[3]{n / c} ⌋) . \end{matrix}$

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 $V_{i}$ but for MSO our formula is of size $O (i^{2})$ compared to the $O (i^{5})$ of FO. We achieve this by quantifying a partition of so called levels $D_{j}$ for the braces and thus the encoded sets and using a different method to define only a single encoding. The monadic predicates $D_{j}$ are used throughout the formulas and only quantified at the beginning of the recursion.

The level $D_{j}$ 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 $D_{2}$ , both of the elements are in $D_{1}$ and the empty set in the second element is in $D_{0}$ .

We again define our formula in terms of many subformulas and briefly list the meaning and size of each subformula:

${set}_{i} (\overline{x})$ : $\overline{x}$ encodes a set of level i. Size constant. Here we only require that there are no braces of the same level between $x_{1}$ and $x_{2}$ , leaving the rest to the formula ${levels}_{i}$ below. $\begin{aligned} {set}_{0} (\overline{x}) : = S (x_{1}, x_{2}) \land L (x_{1}) \land R (x_{2}) \land D_{0} (x_{1}) \land D_{0} (x_{2}) \\ \begin{aligned} {set}_{i} (\overline{x}) & : = x_{1} < x_{2} \land L (x_{1}) \land R (x_{2}) \land D_{i} (x_{1}) \land D_{i} (x_{2}) \\ \land \forall y (x_{1} < y < x_{2} \to \neg D_{i} (y)) \end{aligned} \end{aligned}$

${levels}_{i}$ : The relations $D_{j}$ define the levels of sets as intended and there are no odd braces without pairs. Size $O (i^{2})$ . 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. $\begin{aligned} {levels}_{i} & : = \forall x (⋁_{j = 0}^{i} D_{j} (x) \land \underset{\begin{array}{c} j, k \in {0, \dots, i} \\ j \neq k \end{array}}{⋀} \neg (D_{j} (x) \land D_{k} (x)) \\ \land \forall \overline{x} (⋀_{j = 0}^{i} ({set}_{j} (\overline{x}) \to \forall y (x_{1} < y < x_{2} \to ⋁_{k = 0}^{j - 1} D_{k} (y)))) \\ \land \forall x_{1} (⋀_{j = 0}^{i} ((L (x_{1}) \land D_{j} (x_{1})) \to \exists x_{2} {set}_{j} (x_{1}, x_{2})) \\ \land ⋀_{j = 0}^{i} (R (x_{1}) \land D_{j} (x_{1})) \to \exists x_{2} {set}_{j} (x_{2}, x_{1})) \end{aligned}$

$\overline{x} \in \overline{y}$ : $\overline{x}$ is an element of $\overline{y}$ . Size constant. Assumes $\overline{x}$ encodes a set of level i and $\overline{y}$ encodes a set of level $i - 1$ . $\begin{aligned} \overline{x} \in \overline{y} & : = y_{1} < x_{1} \land x_{2} < y_{2} \end{aligned}$

$\overline{x} \sim_{i} \overline{y}$ : $\overline{x}$ and $\overline{y}$ encode the same set. Size linear in i. Assumes $\overline{x}$ and $\overline{y}$ encode sets of level i. Similar to the FO case. $\begin{aligned} \overline{x} \sim_{0} \overline{y} : = ⊤ \\ \begin{aligned} \overline{x} \sim_{i + 1} \overline{y} & : = \forall \overline{a} ({set}_{i} (\overline{a}) \to \exists \overline{b} ({set}_{i} (\overline{b}) \\ \land (\overline{a} \in \overline{x} \to \overline{b} \in \overline{y}) \land (\overline{a} \in \overline{y} \to \overline{b} \in \overline{x}) \land \overline{a} \sim_{i} \overline{b})) \end{aligned} \end{aligned}$

${add}_{i} (\overline{x}, \overline{y}, \overline{z})$ : States that $\overline{x} = \overline{y} \cup {\overline{z}}$ . Size linear in i. Assumes $\overline{x}$ and $\overline{y}$ encode sets of level i and $\overline{z}$ encodes a set of level $i - 1$ . Similar to the FO case. $\begin{aligned} {add}_{i + 1} (\overline{x}, \overline{y}, \overline{z}) & : = \forall \overline{a} (({set}_{i} (\overline{a}) \land \overline{a} \in \overline{y}) \to \exists \overline{b} ({set}_{i} (\overline{b}) \land \overline{b} \in \overline{x} \land \overline{a} \sim_{i} \overline{b})) \\ \land \exists \overline{c} ({set}_{i} (\overline{c}) \land \overline{c} \in \overline{x} \land \overline{c} \sim_{i} \overline{z} \\ \land \forall \overline{d} (({set}_{i} (\overline{d}) \land \overline{d} \in \overline{x} \land d_{1} \neq c_{1}) \\ \to \exists \overline{e} ({set}_{i} (\overline{e}) \land \overline{e} \in \overline{y} \land \overline{e} \sim_{i} \overline{d}))) \end{aligned}$

$V_{i} (\overline{x})$ : $\overline{x}$ encodes the set $V_{i}$ . Size $O (i^{2})$ . Assumes the level partition is given. Similar to the FO case with no ordering. $\begin{aligned} V_{0} (\overline{x}) : = {set}_{0} (\overline{x}) \\ \begin{aligned} V_{i + 1} (\overline{x}) & : = {set}_{i + 1} (\overline{x}) \land \exists \overline{a} ({set}_{i} (\overline{a}) \land \overline{a} \in \overline{x} \land S (a_{1}, a_{2})) \\ \land \exists \overline{b} (V_{i} (\overline{b}) \land \overline{b} \in \overline{x} \land \forall \overline{c} \forall \overline{d} (({set}_{i} (\overline{c}) \land \overline{c} \in \overline{x} \land {set}_{i - 1} (\overline{d}) \land \overline{d} \in \overline{b}) \\ \to \exists \overline{e} ({set}_{i} (\overline{e}) \land \overline{e} \in \overline{x} \land {add}_{i} (\overline{e}, \overline{c}, \overline{d})))) \end{aligned} \end{aligned}$

$φ_{i} (x, y)$ : Quantifies the level partition and states the subword from x to y encodes $V_{i}$ . Size $O (i^{2})$ . $\begin{aligned} φ_{i} (x, y) & : = \exists D_{0} \dots \exists D_{i} ({levels}_{i} \land V_{i} (x, y))) \end{aligned}$

We now have a formula $φ_{i} (x, y)$ that says the subword from x to y encodes the set $V_{i}$ . 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 $P_{1} (x)$ and $R (x)$ with $P_{2} (x)$ . We define the final formula $ψ_{i}$ of size $O (i^{2})$ 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 $P_{1}$ and $P_{2}$ for the two letters. We first ensure that $P_{1}$ and $P_{2}$ 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}$ . $\begin{aligned} ψ_{i} & : = \exists x \exists y (\forall z (x ⩽ z \land z ⩽ y) \land φ_{i} (x, y) \\ \land \forall P_{1} \forall P_{2} (\forall z ((P_{1} (z) \lor P_{2} (z)) \land \neg (P_{1} (z) \land P_{2} (z))) \\ \land \forall y^{'} ((y^{'} < y \lor \exists z (\forall a (a < z \to (L (a) \leftrightarrow P_{1} (a) \land R (a) \leftrightarrow P_{2} (a))) \\ \land (P_{1} (z) \land R (z))) \to \neg φ_{i}^{'} (x, y^{'})))) \end{aligned}$

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 \in N$ there are infinitely many $n \in N$ satisfying $\begin{matrix} DN (MSO [n]) ⩾ tower (⌊ \sqrt{n / c} ⌋) . \end{matrix}$

We get the same bounds for $LS (MSO [n])$ and $H (MSO [n])$ via Proposition 2.10. Corollary 5.2.
For some constant $c \in N$ there are infinitely many $n \in N$ satisfying $\begin{matrix} LS (MSO [n]), H (MSO [n]) ⩾ tower (⌊ \sqrt{n / c} ⌋) . \end{matrix}$

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 ${FO}^{2}$ .

For the upper bound on $DN ({FO}_{k}^{2})$ we use the k-round, 2-pebble EF-game ${GFO}_{k}^{2}$ . 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 \in Σ$ and let $w \in Σ^{}$ contain an a-chain of length at least* $2 k$ and let $v \in Σ^{}$ 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 \equiv_{{FO}_{k}^{2}} v$ .
Proof.
We consider the k-round 2-pebble EF-game ${GFO}_{k}^{2} (w, v)$ . If w and v are as in the claim, then each point $i \in [| 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 ${GFO}_{k}^{2} (w, v)$ . We show that the strategy maintains both partial isomorphism and the following conditions with m rounds left in the game:
If the stationary pebbles are not in the middle part of u on either side, then they are on a pair $(f (i), i)$ .

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 ${GFO}_{k}^{2} (w, v)$ , by Theorem 2.6, we obtain $w \equiv_{{FO}_{k}^{2}} v$ . □
Lemma 6.2.
Let $Σ = {a, b}$ and let $w \in Σ^{}$ with at least* $2 k + 2$ chains. If $v \in Σ^{}$ is obtained from w by removing all other chains except the first k and the last k chains, then* $w \equiv_{{FO}_{k}^{2}} v$ .
Proof.
We again consider ${GFO}_{k}^{2} (w, v)$ . If w starts and ends with the same letter $c \in {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^{'} \equiv_{{FO}_{k}^{2}} v^{'}$ , we can use Theorem 3.1 to obtain $w \equiv_{{FO}_{k}^{2}} v$ . 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 \in [| 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 ${GFO}_{k}^{2} (w, v)$ . We show that the strategy maintains both partial isomorphism and the following conditions with m rounds left in the game:
If one stationary pebble is on a point $f (i) \in [| w |]$ within the first or last m chains of w, then the corresponding pebble is on $i \in [| v |]$ .

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 \in {a, b}$ in the middle part of $t \in {w, v}$ , that is, not within the first or last m chains. Let $u \in {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 ${GFO}_{k}^{2} (w, v)$ , by Theorem 2.6, we obtain $w \equiv_{{FO}_{k}^{2}} v$ . □

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 ${FO}_{k}^{2}$ .
Theorem 6.3.
For any $k \in N$ , $LS ({FO}_{k}^{2}) ⩽ 4 k^{2} - 1$ , $H ({FO}_{k}^{2}) ⩽ 4 k^{2} - 6 k + 2$ and hence also $DN ({FO}_{k}^{2}) ⩽ 4 k^{2} - 6 k + 2$ .
Proof.
Let $w \in Σ^{}$ be a word with $| w | > 4 k^{2} - 1$ . Since $4 k^{2} - 1 = (2 k - 1) \cdot (2 k + 2 - 1)$ , by the pigeonhole principle there is a chain with length at least $2 k$ or at least $2 k + 2$ chains. Now by Lemmas 6.1 and 6.2, there is a shorter word $v \in Σ^{}$ with $w \equiv_{{FO}_{k}^{2}} v$ . Recall that for a formula φ, $μ (φ)$ is the length of the shortest model of φ. We obtain $μ (φ) ⩽ 4 k^{2} - 1$ for all $φ \in {FO}_{k}^{2}$ and therefore $LS ({FO}_{k}^{2}) ⩽ 4 k^{2} - 1$ .

For the Hanf number, consider a word $v \in Σ^{}$ with $| v | > 4 k^{2} - 6 k + 2$ . Since $4 k^{2} - 6 k + 2 = (2 k - 2) \cdot (2 k - 1)$ , there is a chain with length at least $2 k - 1$ or at least $2 k$ 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 ({FO}_{k}^{2}) ⩽ 4 k^{2} - 6 k + 2$ . □

For the lower bound on $DN ({FO}_{k}^{2})$ 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. $\begin{aligned} {chlt}_{⩾ 1}^{a} (x) : = P_{a} (x) \\ {chlt}_{⩾ m}^{a} (x) : = P_{a} (x) \land \exists y (y < x \land {chlt}_{⩾ m - 1}^{b} (y)), for m > 1 \\ {chlt}_{⩾ 1}^{b} (x) : = P_{b} (x) \\ {chlt}_{⩾ m}^{b} (x) : = P_{b} (x) \land \exists y (y < x \land {chlt}_{⩾ m}^{a} (y)), for m > 1 \end{aligned}$

The formula ${chlt}_{⩾ m}^{a} (x)$ states that x is in an a-chain that is at least the m-th one from the left. Similarly, the formula ${chlt}_{⩾ m}^{b} (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. $\begin{aligned} {chlt}_{⩽ 1}^{a} (x) : = P_{a} (x) \land \forall y (y < x \to P_{a} (y)) \\ {chlt}_{⩽ m}^{a} (x) : = P_{a} (x) \land \forall y (y < x \land P_{b} (y) \to {chlt}_{⩽ m - 1}^{b} (y)), for m > 1 \\ {chlt}_{⩽ m}^{b} (x) : = P_{b} (x) \land \forall y (y < x \land P_{a} (y) \to {chlt}_{⩽ m}^{a} (y)), for m ⩾ 1 \end{aligned}$

As a counterpart to the above, the formula ${chlt}_{⩽ m}^{a} (x)$ states that x is in at most the m-th a-chain from the left. The formula ${chlt}_{⩽ m}^{b} (x)$ says the same for b. $\begin{aligned} {chlt}_{= m}^{a} (x) : = {chlt}_{⩾ m}^{a} (x) \land {chlt}_{⩽ m}^{a} (x), for m ⩾ 1 \\ {chlt}_{= m}^{b} (x) : = {chlt}_{⩾ m}^{b} (x) \land {chlt}_{⩽ m}^{b} (x), for m ⩾ 1 \end{aligned}$

By combining the above formulas we obtain the formula ${chlt}_{= m}^{a} (x)$ which states that the point x is in the m-th a-chain of the word.

We also define corresponding formulas ${chrt}_{⩾ m}^{a} (x)$ , ${chrt}_{⩽ m}^{a} (x)$ and ${chrt}_{= m}^{a} (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 ${chlt}^{b}$ -formulas by switching the roles of a and b as well as the direction of each instance of the linear order. Formulas ${chrt}_{⩾ m}^{b} (x)$ , ${chrt}_{⩽ m}^{b} (x)$ and ${chrt}_{= m}^{b} (x)$ are obtained in the same way by switching in the ${chlt}^{a}$ -formulas the roles of a and b as well as the direction of the linear order.

The quantifier rank of the formulas ${chlt}_{= m}^{a} (x)$ and ${chrt}_{= m}^{b} (x)$ is $2 m - 1$ , while for the formulas ${chlt}_{= m}^{b} (x)$ and ${chrt}_{= m}^{a} (x)$ it is $2 m$ .

We move on to formulas that specify the length of each chain in the word. $\begin{aligned} {poslt}_{1, 1}^{a} (x) : = P_{a} (x) \land \neg \exists y (y < x) \\ {poslt}_{m, 1}^{a} (x) : = {chlt}_{= m}^{a} (x) \land \forall y (y < x \to \neg {chlt}_{= m}^{a} (y)), for m > 1 \\ {poslt}_{m, ℓ}^{a} (x) : = {chlt}_{= m}^{a} (x) \land \exists y (y < x \land {poslt}_{m, ℓ - 1}^{a} (y)), for m ⩾ 1, l > 1 \end{aligned}$

The formula ${poslt}_{m, ℓ}^{a} (x)$ states that x is the ℓ-th symbol in the m-th a-chain from the left. The formulas ${poslt}_{m, ℓ}^{b} (x)$ , ${posrt}_{m, ℓ}^{a} (x)$ and ${posrt}_{m, ℓ}^{b} (x)$ are defined in the same way, using the appropriate subformulas for a or b and left or right. $\begin{aligned} {lenlt}_{m, ℓ}^{a} (x) & : = {poslt}_{m, ℓ}^{a} (x) \land \forall y (y > x \to \neg {chlt}_{= m}^{a} (y)), for m ⩾ 1, l ⩾ 1 \end{aligned}$

The formula ${lenlt}_{m, ℓ}^{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 ${lenlt}_{m, ℓ}^{b} (x)$ for b-chains as well as ${lenrt}_{m, ℓ}^{a} (x)$ and ${lenrt}_{m, ℓ}^{b} (x)$ for the m-th chain from the end of the word. The quantifier rank of the formulas ${lenlt}_{m, ℓ}^{a} (x)$ and ${lenrt}_{m, ℓ}^{b} (x)$ is $2 m + l - 1$ , while for the formulas ${lenlt}_{m, ℓ}^{b} (x)$ and ${lenrt}_{m, ℓ}^{a} (x)$ it is $2 m + 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. $\begin{aligned} φ & : = \exists x ({lenlt}_{k / 2 - 1, 1}^{a} (x) \land {lenrt}_{k / 2 - 1, 1}^{a} (x)) \\ \land \exists x ({lenlt}_{k / 2 - 1, 1}^{b} (x) \land {lenrt}_{k / 2 - 1, 1}^{b} (x)) \\ \land ⋀_{i = 1}^{k / 2 - 2} \exists x ({lenlt}_{i, k - 2 i - 1}^{a} (x)) \land ⋀_{i = 1}^{k / 2 - 2} \exists x ({lenlt}_{i, k - 2 i - 2}^{b} (x)) \\ \land ⋀_{i = 1}^{k / 2 - 2} \exists x ({lenrt}_{i, k - 2 i - 2}^{a} (x)) \land ⋀_{i = 1}^{k / 2 - 2} \exists x ({lenrt}_{i, k - 2 i - 1}^{b} (x)) \end{aligned}$ 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 $k^{2} - 5 k + 6$ . This proves the following theorem: Theorem 6.4.
For any even* $k \in N$ , $DN ({FO}_{k}^{2}) ⩾ k^{2} - 5 k + 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 $\begin{matrix} tower (⌊ \sqrt[5]{n / c} ⌋) ⩽ DN (FO [n]) ⩽ \sqrt{tower (n / 2 + 2)} \end{matrix}$ 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 (⌊ \sqrt[3]{n / c} ⌋)$ for $LS (FO [n])$ .

In the case of $MSO$ , the bounds are similarly $\begin{matrix} tower (⌊ \sqrt{n / c} ⌋) ⩽ DN (MSO [n]) ⩽ \sqrt[3]{\frac{1}{4} tower (n / 2 + 1, n / 2 + 2)} \end{matrix}$ 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 \in Z_{+}$ $\begin{matrix} k^{2} - 5 k + 6 ⩽ DN ({FO}_{k}^{2}) ⩽ 4 k^{2} - 6 k + 2 . \end{matrix}$ The same bounds hold also for the Hanf number, whereas for the Löwenheim–Skolem number the upper bound is $4 k^{2} - 1$ . We see that the situation for ${FO}^{2}$ 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 $\equiv_{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.

Footnotes

Acknowledgements

Miikka Vilander was supported by the Academy of Finland projects Explaining AI via Logic (XAILOG), grant number 345612 (Kuusisto) and Theory of computational logics, grant numbers 352419, 352420, 353027, 324435 and 328987. We would also like to thank an anonymous reviewer for an improvement on the results of Theorem as well as all of their other hard work.

References

Ebbinghaus and

Flum, Finite Model Theory, 2nd edn, Perspectives in Mathematical Logic, Springer, 1995. ISBN 978-3-540-60149-4.

H.-D.

Ebbinghaus, Löwenheim–Skolem theorems, in: Philosophy of Logic,

D.M.

Gabbay,

Thagard,

Woods and

Jacquette, eds, Handbook of the Philosophy of Science, Elsevier Science, 2006. ISBN 9780080466637.

Ellul,

Krawetz,

Shallit and

Wang, Regular expressions: New results and open problems, J. Autom. Lang. Comb.10(4) (2005), 407–437. doi:10.25596/jalc-2005-407.

Etessami,

M.Y.

Vardi and

Wilke, First-order logic with two variables and unary temporal logic, Inf. Comput.179(2) (2002), 279–295. doi:10.1006/inco.2001.2953.

Grohe, Some remarks on finite Löwenheim–Skolem theorems, Math. Log. Q.42 (1996), 569–571. doi:10.1002/malq.19960420145.

Grohe, Large finite structures with few

L^{k}

-types, Inf. Comput.179(2) (2002), 250–278. doi:10.1006/inco.2002.2954.

Hella and

Vilander, Defining long words succinctly in FO and MSO, in: Revolutions and Revelations in Computability – 18th Conference on Computability in Europe, CiE 2022, Proceedings, Swansea, UK, July 11–15, 2022,

Berger,

J.N.Y.

Franklin,

Manea and

Pauly, eds, Lecture Notes in Computer Science, Vol. 13359, Springer, 2022, pp. 125–138. doi:10.1007/978-3-031-08740-0_11.

Hella and

Vilander, Defining long words succinctly in FO and MSO, pre-print, 2022. doi:10.48550/arxiv.2202.10180.

Immerman and

Kozen, Definability with bounded number of bound variables, Inf. Comput.83(2) (1989), 121–139. doi:10.1016/0890-5401(89)90055-2.

10.

Libkin, Elements of Finite Model Theory, Texts in Theoretical Computer Science. An EATCS Series, Springer, 2004. ISBN 3-540-21202-7. doi:10.1007/978-3-662-07003-1.

11.

Pikhurko,

Spencer and

Verbitsky, Succinct definitions in the first order theory of graphs, Ann. Pure Appl. Log.139(1–3) (2006), 74–109. doi:10.1016/j.apal.2005.04.003.

12.

Pikhurko and

Verbitsky, Descriptive complexity of finite structures: Saving the quantifier rank, J. Symb. Log.70(2) (2005), 419–450. doi:10.2178/jsl/1120224721.

13.

Pikhurko and

Verbitsky, Logical complexity of graphs: A survey, in: Model Theoretic Methods in Finite Combinatorics – AMS-ASL Joint Special Session, Washington, DC, USA, January 5–8, 2009,

Grohe and

J.A.

Makowsky, eds, Contemporary Mathematics, Vol. 558, American Mathematical Society, 2009, pp. 129–180. doi:10.1090/conm/558/11050.

14.

Pin and

Weil, Ponynominal closure and unambiguous product, Theory Comput. Syst.30(4) (1997), 383–422. doi:10.1007/BF02679467.

15.

Reinhardt, The complexity of translating logic to finite automata, in: Automata, Logics, and Infinite Games: A Guide to Current Research [Outcome of a Dagstuhl Seminar, February 2001],

Grädel,

Thomas and

Wilke, eds, Lecture Notes in Computer Science, Vol. 2500, Springer, 2001, pp. 231–238. doi:10.1007/3-540-36387-4_13.

16.

L.J.

Stockmeyer, The complexity of decision problems in automata theory and logic, PhD thesis, Massachusetts Institute of Technology, 1974.

17.

Thérien and

Wilke, Over words, two variables are as powerful as one quantifier alternation, in: Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, Dallas, Texas, USA, May 23–26, 1998,

J.S.

Vitter, ed., ACM, 1998, pp. 234–240. doi:10.1145/276698.276749.