April 27th, 2007 uber-rigorous math

I recently discovered a wonderful website: http://www.metamath.org

The website is a project to derive all of math from set theory (The ZFC axioms to be more precise). Of course, formalists have been espousing the view that all of math is essentially a game of logic since the beginning. While this view is held “in principle”, an attempt to actually carry through with this seemingly ginormous task has been largely ignored since Russell’s Principia Mathematica. Of course the Principia is a bit outdated, and doesn’t explicity use the ZFC axioms. Hence, this web project is a long-needed one in my opinion. In addition, the database uses symbolic logic exclusively, hence the rigor of the approach is never in question. Plus, this allows anyone who has looked at the ZFC axioms to understand the proofs (actually parsing out what the proof and the theorem mean is entirely another matter).

Another cool thing about this project is that a computer program has been written that checks the proofs automatically! Of course automated theorem proving is something that has divided mathematicians. Some claim it removes the beauty and the “Art” of mathematics while others see it as the only way to do truly rigorous math.

A fun thing to do is to just browse the various theorems that are in the site’s archives. Some of them are extremely interesting. For example, there is a proof for the principal of equality (that x=x). While many think this is an axiom (the axiom of equality), it can actually be derived from the ZFC axioms, which do not include the equality principle. I think this is completely mind-blowing. Something as seemingly trivial as equality can actually be proven rigorously!

If I had more time, I might want to work on becoming conversant in symbolic logic so I can actually read this stuff.