**Metamath**

I have more insight into the lambda definition yesterday. I believe that the definition of (lambda x x) is correct - it should be equivalent to the identity relation defined in Metamath. However, it is quite definitely a class and not a set. As a result, trying to use it as a function argument just yields the empty set.

This is probably a reasonable way out of the logic thicket. The problem is that the untyped lambda calculus is subject to the Russell set paradox.

I was talking about this with Bram, and he called ZF set theory a "hack." I more or less agree, but playing with it in the context of Metamath has led me to appreciate how powerful a hack it is. With a small number of relatively simple axioms, it gets you a rich set of infinities, but avoids the particular ones that bring the whole formal system crumbling down. You get integers, reals, tuples, sequences (finite and infinite), transfinites, and functions from set to set. You don't get untyped lambda calculus. Overall, it's probably a good tradeoff.