First order logical formula for "one of x" Considering the following sentence:

Almost one of five women earn more money than her partner.

I can partly translate this to the following first order predicate logical formula:
(assuming that a partner ship is 'traditional')

$\exists x,y~|~Woman(x) \wedge Man(y) \wedge PartnerOf(x,y) \wedge MakesMore(x,y)$

But how can I introduce the "one of x" into this formula?
 A: Taking the meaning to of "one in $n$ satisfies $\varphi$" to be (among finite models) "the set of individuals satisfying $\phi$ is at least $\frac{1}{n}$ the size of the set of all individuals", there is no way to state this in first-order logic.
To simplify matters, assume we have a first-order language with only the unary predicate symbol $P$ as a nonlogical symbol, and suppose that $\psi$ is a sentence in this language meaning "one in $n$ satisfies $P$."
For each natural number $k$ we can construct sentences $\theta_k$ and $\sigma_k$ with the following meanings:


*

*$\theta_k$: at least $k$ distinct individuals satisfy $P$;

*$\sigma_k$: at least $k$ distinct individuals do not satisfy $P$.


A relatively easy compactness argument shows that both $$\Sigma_+ = \{ \psi , \theta_1 , \sigma_1 , \theta_2 , \sigma_2 , \ldots \}; \qquad
\Sigma_- = \{ \neg \psi , \theta_1 , \sigma_1 , \theta_2 , \sigma_2 , \ldots \}$$ are consistent.  Furthermore, by the Löwenheim–Skolem Theorem, both $\Sigma_+$ and $\Sigma_-$ have countably infinite models.  But it is easy to show that any two countable models of $\{ \theta_1 , \sigma_1 , \theta_2 , \sigma_2 , \ldots \}$ are isomorphic.
A: See Arthur's post for the answer to the problem. Take the following as a couple of failed attempts.

$\fbox{1}$ A natural way of doing it would be to quantify over subsets of the domain:

$\forall_{\langle 5, W, S\rangle}\phi(S)$ is true iff every set S of size 5 consisting of women (W) satisfies formula $\phi.$

The way this works is simple. Given a structure with domain $D$, predicate letter '$W$' has as its extension some subset of $D$, namely, the subset consisting of all women. The special quantifier selects every subset S of size 5 among that extension of $W$ and passes it to the second-order predicate $\phi$. All that is left is to define $\phi(X)$ s.t. it is true just in case there exists (at least, at most, a unique: all easily definable in terms of the standard quantifiers) someone in $X$ who earns more money than her husband (you already know how to approach this).

$\fbox{2}$ Since the language must be first-order, we can't quantify over subsets of the domain, so we can use iterations of standard quantifiers to do the job of the quantifier above, e.g. in the following way:

$\forall_{\langle 5, W, S\rangle}\phi(S) ~=_{df}~ \forall x_1, x_2, x_3, x_4, x_5 ((Wx_1 \land \ldots \land Wx_5) \rightarrow (\phi(x_1) \lor \ldots \lor \phi(x_5)))$

There's a natural way of generalizing this to any size and predicate. If you want "exactly" 5 or "at most" 5, you have to add more stuff to the consequent; this one only covers the "at least" 5 case.
