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?
 A: 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$).
