This is a substantial revision of the original question, to cut out material that turned out to be irrelevant. Most of the comments and answers and comments-to-answers relate to the O.P. so are no longer applicable.
The question was triggered by a bald sub-heading in this informal write-up
A Problem With First Order Logic
The author doesn't say what specific example he was working with, but gives a simpler case
$$ S(x,y,a,b) \text{ could be } (a^2 = x) \wedge (b^2 = y) $$
He wants to express $\forall x, y ... [S(x, y, a, b)]$ in which $a$ is dependent purely on $x$, $b$ dependent purely on $y$; and those (in)dependencies is what he wants to express in the $...$.
That simpler case using roots is expressible in FOL, so is too over-simplified to illustrate anything.
He goes on to introduce 'Henkin' aka 'Branching' quantifiers. So his general case could be expressed as
$$ \pmatrix{\forall x \exists a\\ \forall y \exists b}S(x, y, a, b) $$
Although this appears to involve quantifying only over individuals, its semantics are in fact given in (a restricted form of) Second-Order. So the sub-heading's 'Problem with First Order Logic' is that it is not Second Order. Nothing to see here; move right along.
Some relevant resources: wikipedia branching quantifier; Stanford Encyclopedia Dependence logic; a critique of so-called 'Hintikka sentences' with their claim of non-expressibility in FOL. I found math.stackexchange had very little, hence this question. Google has lots of hits but mostly about Henkin's contributions to logic in general.
Then the nub of my question (before I realised a Henkin quantifier is merely Second-Order in sheep's clothing) was: I just don't get what the examples in those write-ups are trying to say that can't be said in FOL.
tl;dr: some Second-Order formulas (including some using Henkin quantification) can be equivalently expressed in FOL; some can't. Again nothing to see here. The literature (including in the Stanford Encyclopedia) mostly shows examples that in fact can be expressed in FOL. Again perhaps over-simplifying for the sake of explanation.
@Noah's answer below brings forward an example entailing an infinitary model; it is substantially more complex than the natural language examples in the literature.
A note for non-maths readers: I came at this from Dependency Theory in the database Relational Model, which is entirely equivalently expressible in FOL. That's a different sense of "Dependenc/y".
EDIT: Based on the comments below, let me explain in detail the key point:
Proof: Suppose $\theta$ is a first-order sentence true in exactly the infinite structures. We'll consider its negation, $\neg\theta$; by our assumption on $\theta$, $\neg\theta$ is true in exactly the finite structures.
So what? Well, we use the compactness theorem. This is in my opinion the most important basic result in logic, and is definitely the first thing you want to master to understand first-order logic and its extensions. The compactness theorem says that if $\Gamma$ is a set of first-order sentences, and every finite subset of $\Gamma$ has a model, then $\Gamma$ itself has a model.
For $n\in\mathbb{N}$, let $\chi_n$ be the sentence $$\exists x_1\exists x_2...\exists x_n(\bigwedge_{i<j\le n} x_i\not=x_j).$$ Each $\chi_n$ is a first-order sentence which is true in exactly those structures with at least $n$ elements. Now let's think about the set of sentences $$\Gamma=\{\chi_n:n\in\mathbb{N}\}\cup\{\neg\theta\}.$$
Any finite subset $\Gamma_0\subseteq\Gamma$ is satisfiable: if we let $k\in\mathbb{N}$ be large enough so that no $\chi_m$ is in $\Gamma_0$ for $m\ge k$ (note that such a $k$ exists since $\Gamma_0$ is finite!), we see that any structure of size at least $k$ satisfies $\Gamma_0$. But $\Gamma$ itself has no model: any model of $\{\chi_n: n\in\mathbb{N}\}$ must be infinite, but no infinite structure is a model of $\neg\theta$. So we have our contradiction. $\quad\Box$
Note that we can write this as a direct proof instead, showing:
(Above, take $\neg\theta$ to be $\eta$.)
The two crucial facts we've used about first-order logic are:
The compactness theorem, and
the fact that first-order logic has negation.
It turns out, surprisingly, that the latter is the issue with dependence(-style) logic(s)! But that's something we should look at only after we understand the basic argument above in detail.
The bulk of this question I find difficult to follow; let me address the main question:
I think it's easier to just do an explicit example: a sentence $\varphi$ using a Henkin quantifier, in the empty language, which is true exactly if the ambient domain is infinite. Namely, $$\varphi\equiv\exists zQ(x, y; a, b)[a\not=z\wedge (x\not=y\iff a\not=b)].$$ (Here I'm writing "$Q(x, y; a, b)$" to denote "for all $x, y$ there are $a, b$ depending only on $x, y$ respectively such that.")
OK, it's probably not clear what $\varphi$ means, so let's take it apart.
The semantics of branching quantifiers is best described, in my opinion, in terms of Skolem functions. According to this semantics we can express $\varphi$ in second-order logic as $$\hat{\psi}\equiv\exists F_1, F_2, z\forall x, y[(F_1(x)\not=z)\wedge (F_1(x)=F_2(y)\iff x=y)].$$ However, I claim we can do one better, and express it as $$\psi\equiv \exists z, F\forall x, y(F(x)\not=z\wedge (x\not=y\implies F(x)\not=F(y))).$$ (Note that here "$\iff$" isn't needed since we're only using one function symbol now - "$x=y\implies F(x)=F(y)$" is a tautology.) Clearly we have $\psi\implies\hat{\psi}$ (take $F_1=F_2=F$); conversely, the point is that in order for a pair of Skolem functions $F_1, F_2$ to witness that $\hat{\psi}$ is true we must have $F_1=F_2$ (if $F_1(a)\not=F_2(a)$ for $a$ in the domain, then $x=a, y=a$ would give a counterexample to $\psi$).
Now looking at $\psi$, we see that $\psi$ asserts the existence of an injection from the model to itself (namely, $F$) which is not surjective (it misses $z$). So $\psi$ is a sentence true in every infinite structure but false in every finite structure, and by the compactness theorem (and the argument above) this can't happen in a first-order way.
Let me try to give a quick "moral" of the story. The crucial point of difference between first-order and dependence sentences here is:
E.g. the Skolemized version of the first-order sentence $$\forall x\forall y\exists z\forall u\exists v(\theta(x, y, z, u, v))$$ is $$\exists F\exists G\forall x\forall y\forall u(\theta(x, y, F(x, y), u, G(x, y, u))).$$
By contrast, in a dependence sentence we have more freedom with regard to how the Skolem functions are "entangled," and we've seen that in play above.
Now let me try to explain the claim that dependence logic only involves quantifying over individuals (a claim, incidentally, that I disagree with). What dependence logic does is argue that general expressions of the form $$\mbox{[second-order existential quantifiers](first-order formula)}$$ form a natural generalization of first-order sentences while staying in the realm of quantification over individuals, since all the new power we get this way really just comes down to expressing dependencies. (These are in fact essentially the sentences expressible in dependence logic.)
I haven't treated here the question of whether dependence logic is in fact more first-order or more second-order. Vaanaanen has written at length in defense of the former position; personally, I take the latter view. But you asked specifically for something expressible using dependencies which isn't first-order expressible, and I've done that above. So hopefully this is helpful.