This is a file in the archives of the Stanford Encyclopedia of Philosophy.

If given the premise that

1 + 2² = 5

one can prove that

1 ( + 2² = 5)

For it follows from our premise (by

-Abstraction) that:

[z z + 2² = 5]1

Independently, by the logic of identity, we know:

([z z + 2² = 5]) = ([z z + 2² = 5])

So we may conjoin this fact and the result of

-Abstraction to produce:

([z z + 2² = 5]) = ([z z + 2² = 5]) & [z z + 2² = 5]1

Then, by existential generalization on the concept [

z z + 2² = 5], it follows that:

G[([z z + 2² = 5]) = G & G1]

By the definition of membership, we obtain:

1 ([z z + 2² = 5])

And, finally, by our Rewrite Rule, we establish what we set out to prove:

1 ( + 2² = 5)