7
$\begingroup$

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?

$\endgroup$
12
$\begingroup$

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

$\endgroup$
5
$\begingroup$

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

$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$
    – CiaPan
    Aug 29 '17 at 7:20
2
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.