# Problem with the compact version of the definition for "exactly one"

According to the definition, if we want to express that there is exactly one $x$ such that $P(x)$, we specify:

$\exists x (P(x) \wedge \forall y (P(y) \rightarrow y = x))$

By Existential Instantiation we can say that $P(a) \wedge \forall y (P(y) \rightarrow y = a)$.

Since we are not dealing with a biconditional, but just a conditional, we cannot infer the following from just the previous statement:

$\forall y (y = a \rightarrow P(y))$

Which is counter intuitive, for we would expect that any $y$ satisfying $P$ would precisely be $a$.

However, we find that there is a more compact definition of exactly one by stating it like this:

$\exists x \forall y (P(x) \leftrightarrow y = x)$

Once again, by Existential Instantiation we can write:

$\forall y (P(y) \leftrightarrow y = a)$

This time implying that $\forall y (y = a \rightarrow P(y))$.

Then... what just happened?

That's right that you cannot turn an implication without other justification. However there is justification here as we have also $P(a)$ in the statement. It's by the axiom of equality you have $y=a\rightarrow P(y)$ due to $P(a)$.

By Existential Instantiation we can say that $$P(a) \wedge \forall y (P(y) \rightarrow y = a)$$.

Since we are not dealing with a biconditional, but just a conditional, we cannot infer the following from just the previous statement:

$$\forall y (y = a \rightarrow P(y))$$

No, of course we can infer that.  We are not dealing with just a conditional, but rather with a conjunction and a conditional.   Since $$P(a)$$ therefore $$\forall y~(y{=}a\to P(y))$$, and hence$$P(a)\wedge \forall y~(P(y)\to y=a)\dashv\vdash \forall y~\Big(\big(y=a\to P(y)\big)~\wedge~\big(y\neq a\to\neg P(y)\big)\Big)$$

• You may use LaTeX / MathJax symbols \land and \lor for logical operators, so you get appropriate visual appearing while retaining the semantics in the source. Aug 29, 2017 at 7:20

For the first definition, with the equality axiom for formulas we can easily derive:

$P(x) \vdash y=x \to P(y)$.

In details:

1) $∃x \ (P(x) ∧ ∀y(P(y) → y=x))$ --- premise

2) $P(a) ∧ ∀y(P(y) → y=a)$ --- from 1) by Existential Instantiation (I would prefer to use $\exists$-Elim...)

3) $∀y(P(y) → y=a)$ --- from 2) by Conjunction Elimination

4) $P(y) → y=a$ --- from 3) by Universal Instantiation

5) $P(a)$ --- from 2) by Conjunction Elimination

6) $y=a$ --- assumed [*]

7) $\vdash y=a \to a=y$ --- symmetry: provable from equality axioms

8) $a=y$ --- from 6) and 7) by Modus Ponens ($\to$-Elimination)

9) $\vdash a=y \to (P(a) \to P(y))$ --- equality axiom

10) $P(a) \to P(y)$ --- from 8) and 9) by Modus Ponens

11) $P(y)$ --- from 5) and 10) by Modus Ponens

12) $y=a \to P(y)$ --- from 6) and 11) by Conditional Proof (or $\to$-Introduction), discharging assumption [*]

13) $P(y) \leftrightarrow y=a$ --- from 4) and 12) by $\leftrightarrow$-Introduction

14) $\forall y \ (P(y) \leftrightarrow y=a)$ --- from 13) by Generalization ($\forall$-Introduction)

15) $\exists x \ \forall y \ (P(y) \leftrightarrow y=x)$ --- from 14) by $\exists$-Introduction.

In conclusion, we have:

$∃x \ (P(x) ∧ ∀y(P(y) → y=x)) \vdash \exists x \ \forall y \ (P(y) \leftrightarrow y=x)$.

In a similar way we can prove the equivalence of the two definitions.

$$P(a) \wedge \forall y (P(y) \rightarrow y = a)$$.

Since we are not dealing with a biconditional, but just a conditional, we cannot infer the following from just the previous statement:

$$\forall y (y = a \rightarrow P(y))$$

Sure we can! Given that $$a$$ has property $$P$$, anything that is identical to $$a$$ will have to have property $$P$$ as well.

In other words, $$\forall y (y = a \rightarrow P(y))$$ logically follows from $$P(a)$$, and therefore also from $$P(a) \wedge \forall y (P(y) \rightarrow y = a)$$.

I am guessing that you thought it didn't, because you were too focused on the second conjunct.