Prove: Impossible to express "There are at least 7 objects" by quantifying over only 6 variables

[UPDATE: A comment in this post (Is it legitimate to quantify a variable twice? led me to a pdf of a book on Finite Model Theory by Libkin, and the issue here seems to be connected to the general concept of FO-inexpressibility. Chapter 3 on Erhrenfeucht-Fraisse games seems to contain relevant info, but it's WAY beyond introductory. I also turned up the phrase "Beth Definability Theorem", which seems related (cf. https://encyclopediaofmath.org/wiki/Beth_definability_theorem). Given all this, I doubt Barwise & Etchemendy expect anyone in their textbook audience to pursue this question successfully on their own...)

Question #14.8 in Language, Proof, & Logic by Barwise & Etchemendy says:

"It is impossible to express the sentence There are at least seven objects using only = and the six variables available in [the accompanying computer program] Tarski's World, no matter how many quantifiers you use. Try to prove this [Warning: This is true, but it is very challenging to prove]"

I'm hoping for only a hint -- NOT a solution (at least not immediately...)-- since the closest thing I was able to find here was this post( First-order definability of structures of at least $n$ elements), and further searches on definability/size of first-order structures led to much more complicated issues.

I don't want to clutter up the board with fruitless speculation, so I'll just briefly state a couple strategies I was playing around with:

General method: Proof by contradiction -- Assume we can express the target sentence with only 6 variables, call it $$\phi$$

Idea 1: Recognize that the target sentence can be expressed with either 6 or 7 quantified variables, and try to derive a contradiction out of the possible quantifier type/order

Idea 2: Try to show that assuming $$\phi$$ makes it possible to express "There are at least 6 objects" with only 5 variables. Induct down to "There is one object" with no variables. Attempt this by recognizing that each variable appears only a finite number of times in $$\phi$$. So pick, say, $$x_1$$ and in every instance replace it with $$x_2$$ except when an "=" already has $$x_2$$ in it, in which case replace it with $$x_3$$.

Idea 3: Consider the algebraic structure of, and relationship between, sets of wffs expressing the "at least n objects" property, where each set contains only wffs with a fixed number of variables.

Do any of these rough sketches seem like the right direction, or am I completely out to sea?

• Essentially idea 2, I suppose: If $\phi$ uses $n$ variables and is true for every model with $> n$ objects, show that it is also true with $n$ objects. Do so by both structrural induction (is $\phi$ of the form $\phi_1\land\phi_2$, $\phi_1\lor\phi_2$, ...?) and induction on $n$ (when $\phi$ is of the form $\exists x\phi_1$ or $\forall x\phi_1$) Commented Jun 25, 2021 at 5:06
• Whichever statement $\varphi$ is, you'd want to prove that $\varphi$ is true in some structure that has at most six objects. That would mean $\varphi$ cannot express that at least seven objects exist. Commented Jun 25, 2021 at 22:24

There are easier ways of doing this, but I suggest looking into Ehrenfeucht–Fraïssé games, as they're a good way of getting intuition for the expressiveness of first order logic. Rosenstein's Linear Orderings has a good introduction.

Two players, Spoiler and Duplicator, take turns picking elements of two structures A and B.

On turn $$i$$, Spoiler goes first and picks any element of either structure. Duplicator then picks an an element of the other structure to match it to. Call these $$a_i$$ and $$b_i$$ regardless of who picked what.

If at any point there is a basic formula (not involving boolean logic or quantifiers, so in your case only involving $$=$$) which is true of the $$a_i$$ but not true of the corresponding $$b_i$$, then Duplicator loses.

If Duplicator can avoid losing by turn $$n$$, then all formulas with $$n$$ variables which are true of one structure are true of the other. Duplicator can exploit this similarity to avoid losing.

Conversely, if Spoiler has a strategy to win in $$n$$ turns, there is a formula with $$n$$ variables which is true of one structure but not the other. Spoiler can exploit this difference to win.

If you want to bound the number of variables $$(\leq n)$$ and allow quantifying over the same variable multiple times, you need to bound the number of $$a_i$$ and $$b_i$$ ($$\leq n$$), but allow Spoiler to move a previous turn's $$a_j$$ ($$b_j$$) to which Duplicator responds by repositioning the correspoinding $$b_j$$ ($$a_j$$).

• Thank you! It further helps that you gave a nicely intuitive description of E-F games, since it's now crystal clear that that's what the computer program that goes with Barwise/Etchemendy's LPL text is doing. Commented Jun 28, 2021 at 16:45