27 Aug 2002 raph   » (Master)

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.

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!