Is this a valid way of saying "exactly two..."? $\exists x \exists!y((x \ne y) \wedge P(x) \wedge P(y))$

Question

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.

Answer 1

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.

Answer 2

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)$$

Answer 3

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.

Answer 4

Exactly two:

$$\exists x \exists y(Px \land Py \land x \neq y \land \forall z(Pz \implies (z =x \lor z=y)))$$