A counting quantifier is a quantifier that denotes how many elements satisfy a predicate. I will use the notation $\exists_n x \phi x$ to denote that there are $n$ elements $x$ such that $\phi x$.
I was thinking about how to define such a quantifier recursively and came up with the following:
$$\exists_0 x \phi x \Longleftrightarrow \neg \exists x \phi x $$
$$\exists_{n+1} x \phi x \Longleftrightarrow \exists x ( \phi x \land \exists_n y ( y \neq x \land \phi y ) ) $$
In plain language, there are $n+1$ elements that satisfy $\phi$ iff there is an element $x$ that satisfies $\phi$ and there are $n$ elements distinct from $x$ that also satisfy $\phi$.
In the case of $n = 1$, this reduces to
$$ \exists_1 x \phi x \Longleftrightarrow \exists x ( \phi x \land \neg \exists y ( y \neq x \land \phi y ) ) $$
which matches the uniqueness quantifier. In the case of $n=2$, this reduces to
$$ \exists_2 x \phi x \Longleftrightarrow \exists x ( \phi x \land \exists y ( y \neq x \land \phi y \land \neg \exists z ( z \neq y \land z \neq x \land \phi z ) ) ) $$
For finite sets, the set-theoretic concepts of cardinality and equinumerosity can then be defined by
$$ \lvert A \rvert = n \Longleftrightarrow \exists_n x (x \in A) $$
$$ \lvert A \rvert = \lvert B \rvert \Longleftrightarrow \exists n ( \exists_n x (x \in A) \land \exists_n x (x \in B) ) $$
My questions are the following:
- Why have I not seen set-theoretic cardinality or equinumerosity described in terms of counting quantifiers before? Is there some kind of limitation to this approach?
- Can the concept be rigorously extended to infinite cardinalities through a first-order infinitary logic (contradicting the statement here)? Or is this somehow circular?
Your cardinality schema is fine as long as it's just intended as a notational shorthand. The problems start when a) you seem to be regarding this schema as a single statement, rather than infinitely many and b) you quantify over $n$ in attempting to define equinumerosity.
In your cardinality schema, the $n$ on the right-hand side is part of a notational device (the counting quantifiers that you introduced); it's not a variable. On the left-hand side, it looks a bit like a variable, but of course it must have the same meaning on both sides, so it isn't. It's just a placeholder for a number external to the formal system, and only when you plug in some $n$ do you get a (true) statement of first-order logic. To assert equalities for all possible finite cardinalities in this manner, you need countably infinitely many statements.
That's OK as long as you're aware of it. Your attempt to define equinumerosity, on the other hand, makes no sense. There's no way to instantiate the schema you've written, because plugging in some value for $n$ would result in quantifying over a constant. Here you've used $n$ in two incompatible ways – both as a number external to the system in a notational shorthand (in the $C_n$ quantifiers) and in a way that only makes sense when $n$ is a variable (quantifying over it).