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

Question

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?

Answer 1

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

Answer 2

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.

Answer 3

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

Answer 4

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