Back to comment hit list
Back to comment hit list





Metamath Solitaire

Rating: 5 stars
Used in Course: Not used in course
Submitted by: Kannan Nambiar (Faculty), Jan 12, 2003
Comment: Many scientists believe in, what is called pantheism, the idea that the complex
working of the nature around us is the only palpable God we can deal with. For
this reason, Reality is the name used by philosophers to discuss God, so that
the highly emotional content that goes with the word God can be avoided. From
this it should be clear that reality is the same as metamathematics. Most
philosophers agree that contemplation of Reality is the highest form of
happiness. So, if you want happiness, play Metamath Solitaire all by yourself.

Technical Remarks:

The applet Metamath Solitaire lets you build simple mathematical proofs from
axioms in logic and set theory. This applet is based on a program called
Metamath, which can express theorems in abstract mathematics, accompanied by
proofs that can be verified by a computer program. Looking at Metamath, confirms
many of my beliefs. Beauty, simplicity, and rigor are the same. You can trust a
computer more than a mathematician. You must accept the four color conjecture,
instead of quibbling about it. All proofs of all mathematics can be arranged in
the lexical order in The Book, the amount of paper available being the only
limitation (see White Hole, Black Whole and The Book, in Merlot, Foundations of
Mathematics).This means that you can read The Book and collect as many theorems
as you want, but don't ask for a solution to your conjecture. There is no good
mathematics that a good high school student cannot understand. Any problem which
has a solution, has a simple solution. It is not enough to define empty set,
you must define the Void, when not even the empty set is there, of course, Void
is not a set, but we need the name. If we have Void, we can call a Dedekind cut
a Void. If we have Void, we can answer the uncomfortable question, What was
there before the Big Bang?, the answer is of course Void. It is not enough to
define cardinals, we want the Absolute, which contains all the cardinals. Of
course, Absolute is not a set (fortunately for us, Cantor has accepted this