Equality implies Substitution
Theorem
Let $\phi ( x )$ denote a Well-Formed Formula which contains $x$ as a free variable.
- $\forall x: ( \phi ( x ) \iff \exists y: ( y = x \land \phi ( y ) ) )$
- $\forall x: ( \phi ( x ) \iff \forall y: ( y = x \implies \phi ( y ) ) )$
Note that when $y$ is substituted for $x$ in either formula, it is false in general.
A link to explain the above statement, which is I believe covered somewhere. Perhaps we ought to add it as a page in the "fallacies and mistakes" category.
You can help ProofWiki by explaining it.
To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
If you would welcome a second opinion as to whether your explanation is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
Proof
$\forall x: ( ( \exists y: y = x \land \forall y: ( y = x \implies \phi ( x ) ) ) \implies \exists y: ( y = x \land \phi ( x ) ) )$
- $\forall x: x = x$
$\implies \forall x: \exists y: y = x$
$\implies \forall x: ( \forall y: ( y = x \implies \phi ( x ) ) \implies \exists y: ( y = x \land \phi ( x ) ) )$ $\Box$
- $\forall x,y: ( ( y = x \land \phi ( y ) ) \implies \phi ( x ) )$
$\implies \forall x: ( \exists y: ( y = x \land \phi ( y ) ) \implies \phi ( x ) )$ $\Box$ (1)
From the first two lemmas, we can also derive the following statement. These two statements comprise one direction of the assertion:
- $\forall x: ( \forall y: ( y = x \implies \phi ( y ) ) \implies \phi ( x ) ) )$ (2)
Similarly:
- $\forall x,y: ( \phi ( x ) \implies ( y = x \implies \phi ( y ) ) )$
$\implies \forall x: ( \phi ( x ) \implies \forall y: ( y = x \implies \phi ( y ) ) )$ $\Box$ (3)
$\implies \forall x: ( \phi ( x ) \implies \exists y: ( y = x \land \phi ( y ) ) )$ (4)
The above two statements comprise the other direction of the biconditional assertions. Together, (1), (2), (3), and (4) prove the two assertions.
$\blacksquare$
Please fix formatting and $\LaTeX$ errors and inconsistencies.
It may also need to be brought up to our standard house style.
If you have done this or know it has been done, please remove {{Tidy}} from the code.
Source
- Willard Quine: Set Theory and Its Logic (1963): $\S 6.1$
- Willard Quine: Set Theory and Its Logic (1963): $\S 6.2$
