Defining $a^n b^{n^2}$ with one existential SO binary relation

Is it possible to define the language:

$$L = \{ a^n \; b^{n^2} \}$$


using an existential second order sentence over strings (ordered structures with unary predicates $U_a(x), U_b(x)$) using only one binary relation?

The sentence should have this form: $\exists M ( \exists B_1,...,B_n ( \varphi ))$ where:

• $M$ is a binary relation

• $B_i$ are monadic

• $\varphi$ is first order with signature (available relations) $\sigma = \langle

If not, how to prove it? (or cite a textbook in which I can find similar exercises)

First off, I assume you also want to have a binary relation on the domain, acting as a linear order:

-
Those languages definable in MSO are exactly those that are definable in existential MSO (see for this Finite Model Theory by Ebbinghaus and Flum, thm 6.2.3)

-
Those languages definable in existential SO are those recognizable in NP, that's Fagin's theorem.

So you have that e-MSO matchs the regular languages. If you can prove that the different existential quantifiers in BET are necessary for recognizing a language and a binary relationvariable cannot encode the unaries, you are done.

A different approach (possibly more fruitful) is to argue the following way:
The constraint $a^2 = b$ is a meta constraint. You have to emulate this inside your language to get it in the object-world. Now im general SO over the empty signature is strong enough for such, but this is a different exercise. So you have to show two things:
Is your framework strong enough to emulate $x \mapsto x^2$ relative to the discrete order? Pay attention, Beth's Definability Theorem does fail in general in the finite, as does Craig's Interpolant Theorem (both for FO). This is also in above's book, 3.5.1.
If you succeed in doing so, you still have to following problem: You need to get the "meta-size" of $U_a$ and $U_b$ into the object language. This is possible if you allow existential quantifiers of the form "exists exactly n many x:", which is possible in FO. However, you can only do this for a fixed number, additionally, you cannot get the "object-size" into the meta language. You could employ counting to test for sizes. In the MSO setting, they are of the form "$C_n(X)$ which is satisfied iff $ X mod n = 0$. These are not possible to emulate with just a binary relationvariable and FO. Can you show that even using those, you cannot get enough?

Another edit: Lets consider the solution with two binary relations, $R$ and $S$. I'll furthermore use $\bot$ as the smallest element of the order, $\top$ as the largest.

• $\forall x, y: (x,y) \in R \implies U_a(x) \wedge U_b(y)$

• $\forall x: ((x,\top) \in R \iff x = \bot) \wedge ((\bot,x) \in R \iff x = \top)$

• $\forall x: \exists y: (x,y) \in R$

• $\forall y: \exists! x: (x,y) \in R$

• $\forall x_1, x_2, y_1, y_2: x_1

Well, $R$ does split $U_b$ into $|U_a|$ many equivalence classes, each of which is not empty and the smaller the values in $U_a$, the large the corresponding values in the factorized $U_b$. A model of this sentence can look like this (numbers being the elements in $U_a$ and letters being the elements in $U_b$ factorized by the equivalence relation induced by $R$.


w = 1-2-3-cc-bbbbbbb-a

What is left now is to make sure that the equivalence classes have the appropriate size. For this, note that we can indeed encode $x \mapsto x^2$ inside a binary relation (somewhat). See here that if $n = 1$, we have to append 1 element to the end and if $n = m + 1$, then for this one element more in $U_a$, we have to add as many elements to $U_b$ as we did for m, and two additional ones ($(n+1)^2 - n^2 - (n^2 - (n-1)^2) = 2$, aka when considering adding +1 repeatedly to $n$, one has to add 1, 3, 5, ... to $n^2$).

So, let's encode this behaviour with $S$:

• $\forall y_1, y_2: (y_1, y_2) \in S \implies U_b(y_1) \wedge U_b(y_2)$

• $\forall y: \neg (y, \top) \in S$ (probably redundant)

• $\forall y_1: (\exists y_2: (y_1, y_2) \in S) \implies (\exists! y_2: (y_1, y_2) \in S)$

• $\forall y_1: (\exists y_2: (y_2, y_1) \in S) \implies (\exists! y_2: (y_2, y_1) \in S)$

• $\forall y_1, y_2: (y_1, y_2) \in S \implies (\exists x_1, x_2: (x_1, y_1) \in R \wedge (x_2, y_2) \in R \wedge \neg \exists x_3: (x_1

• $\forall y_1: (\exists x_1, x_2: x_1

This asserts that $S$ acts only on $U_b$, that if it is defined, it'll be uniquely defined (an injective partial function so to say, I'll use it from now on as a function), nothing is mapped to the largest element and whenever "$y_2 = S(y_1)$", than $y_2$ is in the equivalence class induced by the direct successor of the inducer of the equivalence class of $y_1$. Furthermore, $S$ is defined for each element that is not member of the "least" equivalence class.

With the help of this auxiliary function, we can control the size of the equivalence classes produced by $R$:

• $\forall x: \bot

This formula expresses that for each element in $x \in U_a$, which is not the smallest one, there is a next smaller one $x'$. The elements which are paired with $x'$ in $R$ translated with $S$ are paired with $x$ in R, there are two additional elements which are not the image of any of those. Lastly, there are no elements paired with $x$) besides these two additionals and those that came from $x'$.

The following is now up to you:

• Prove that all models of this sentence are words of the form $a^nb^{n^2}$

• Prove that every word of the form $a^nb^{n^2}$ does satisfy this sentence

• Show that you can indeed encode the two relations into one

StackExchange Computer Science Q#116508, answer score: 3