A More Complex Example

If given the premise that

\(1+2^{2}=5\)

one can prove that

\(1\in \epsilon[\lambda z \, z+2^{2} =5]\)

For it follows from our premise (by \(\lambda\)-Abstraction) that:

\([\lambda z \, z+2^{2}=5]1\)

Independently, by the logic of identity, we know:

\(\epsilon[\lambda z \, z+2^{2}=5] = \epsilon[\lambda z \, z+2^{2}=5]\)

So we may conjoin this fact and the result of \(\lambda\)-Abstraction to produce:

\(\epsilon[\lambda z \, z+2^{2}=5] \eqclose \epsilon[\lambda z \, z+2^{2}=5] \amp [\lambda z \, z+2^{2}=5]1\)

Then, by existential generalization on the concept \([\lambda z \, z+2^{2}=5]\), it follows that:

\(\exists G[\epsilon[\lambda z \, z+2^{2}=5] \eqclose \epsilon G \amp G1]\)

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

\(1\in\epsilon[\lambda z \, z+2^{2}=5]\),

which is what we were trying to prove.

Return to Frege's Theorem and Foundations for Arithmetic