Is this a valid way of saying "exactly two..."? $\exists x \exists!y((x \ne y) \wedge P(x) \wedge P(y))$ So I have been looking at this question: How to convert an English sentence that contains "Exactly two" or "Atleast two" into predicate calculus sentence? And the way I would do this didn't really show up there.
So I would like to write "Exactly two..." like this:

Let $P(x)$ be a predicate, so to say exactly two terms satisfy $P$ I would write:
$$\exists x \exists!y((x \ne y) \wedge P(x) \wedge P(y))$$

Now, this would ensure that $x \ne y $ and since $=$ is an equivalence relation, it ensures that there is only one such $x$ and $y$.
Would this be a right way to write it? I'm not a mathematican, so I was unsure If I can provide this as an answer, but it got me curious as my notation is much shorter than the ones proposed in the linked question.
 A: Your expression translates to something like:

There exists an element $x$, and a unique element $y$ distinct from $x$, such that $P(x)$ and $P(y)$ are true.

This is equivalent to saying that there are exactly two elements making $P$ true, so is correct.
You can generalise your characterisation to define quantifiers $\exists^n$ for $n \ge 1$ meaning 'there exist exactly $n$' in the following way:

*

*Define $\exists^1 x\, P(x)$ to mean $\exists! x\, P(x)$;

*Define $\exists^{n+1}x\, P(x)$ to mean $\exists x\, \exists^n y\, (x \ne y \wedge P(x) \wedge P(y))$
Note that the recursive definition of $\exists^2$ collapses to precisely the definition you made.
A: Exactly two terms satify $ P$ can be written as
$$\exists !(x,y) \;:\; x\ne y \wedge P(x) \wedge P(y)$$
or also
$$\exists x\exists y \; : \; x\ne y \wedge  P(x) \wedge P(y) \wedge \Bigl( \forall z \; (z\ne x\wedge z\ne y \; \implies \;\lnot P(z))\Bigr)$$
A: Perhaps a more standard definition of $P$ (with a biconditional) and easier to work with would be:

For distinct $a$ and $b$, we have $P(c)$ being true if and only if $c=a$ or $c=b$.
$\exists a: \exists b: [a\neq b \land \forall c: [P(c) \iff c=a \lor c=b]]~~~$


FYI: Using the notation of set theory, $P$ might instead be a set such that
$~~~P=\{a, b\}$, $~a\neq b$
Or, more formally,
$~~~\exists a ~\exists b~ [a\neq b \land \forall c~[c\in P \iff c=a \lor c=b]]$
Here, "$c\in P$" has simply replaced "$P(c)$" in this case.
A: Exactly two:
$$\exists x \exists y(Px \land Py \land x \neq y \land \forall z(Pz \implies (z =x \lor z=y)))$$
