A More Complex Example

If given the premise that

1+2²=5

one can prove that

1 ∈ ε[λz z+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]

And, finally, By the definition of membership, we obtain:

1 ∈ ε[λz z+2²=5],

which is what we were trying to prove.

Return to Frege's Theorem and Foundations for Arithmetic