Slashdot Mirror

"Constructs mathematics from scratch, starting from ZFC set theory axioms. Over 4,000 proofs"

http://metamath.org/

Thing is, there are working implementations of the proof checker in a couple of hundred lines of code. You could write one in a functional language or whatnot and prove its correctness by hand. This is a gazillion times more reliable than man-made proof checking. The only problem is that it is quite a tedious task to write a proof in it. Most proofs in mathematical literature are not "proofs" in a formal sense, but more like informal sketches of a proof that are checked by hand. It can take months to figure out if a particular proof is correct. With an automated proof checker, a couple of milliseconds.

*(Click on "2+2=4 Trivia" or add "#trivia" to URL - slashcode is changing "#" to "%23" so I took "#trivia" off of the URL)

As I mentioned in another post above, I was mistaken not to qualify my statement as "essentially all of mathematics" instead of the rhetorical "all of mathematics" (which I in my haste to post I figured would be simpler for nonmathematicians to understand, but in retrospect it was a judgmental error).

But you are mistaken about the power of the ZF language. Please read the bottom half of page xiv (14 of 192) in the Preface of the "Metamath" book. This will explain how ZFC, with the addition of just one more axiom to result in Tarski-Grothendieck set theory, can do category theory. That this axiom isn't typically included with ZF has nothing to do with it being a hack - it is actually quite beautiful - but has more to do with tradition and the historical definition of what axioms ZF set theory happens to include. Mathematically there's nothing to prevent having the additional axiom all the time as part of the "standard" axiom set, and the mizar.org project does just this. From what I can tell there is nothing that Tarski-Grothendieck set theory can't do that category theory can do.

On the other hand no one, to my knowledge, has come up with a foundational set of category theory axioms that are anywhere near as convenient to work with as ZF-type axioms. In fact even finding them explicitly, precisely, and plainly displayed as a simple axiom system to plonk on top of first-order logic is something I have never seen. (I have seen a couple of systems claimed as such, but they were riddled with problems such as ambiguous rules and implicit definitions that weren't made clear if you actually wanted to start working with them mechanically.) So if category theorists want to have a myth "stomped out of existence" they'll have to do better in terms of making it simply accessible in the same way ZF-type axioms are.

In that case, I believe it consists of :
{} = 0
{{}} = 1

As pure mathematicians like to claim, all of mathematics is derived from the empty set.

That is cute. However you can't get very far with these two axioms. You need some more axioms that will let you build more complex structures starting from the empty set, such as combining them to form pairs, unions, powersets, and so on. You also need to postulate the existence of an infinite set. A quick overview of some of the history behind the axioms, and why they are needed, is given on the Russell paradox page.

The answer is simple. The most beautiful equations, hands down, are those from which all of mathematics can be derived. These are the axioms of ZFC set theory. What could possibly be more beautiful or more important than that? And it's a shame so few people know about them. See Zermelo-Fraenkel Axioms and Metamath Proof Explorer.

The answer is simple. The most beautiful equations, hands down, are those from which all of mathematics can be derived. These are the axioms of ZFC set theory. What could possibly be more beautiful or more important than that? And it's a shame so few people know about them. See Zermelo-Fraenkel Axioms and Metamath Proof Explorer.

If you think 2+2=4 is simple, then you haven't seen this!

From the site:

Mathematical Proofs Set to Music I added this web page just for fun. While looking at some proofs, it occurred to me that their structure resembled musical scores, so as an experiment I decided to see what they sounded like. Essentially, the musical notes correspond to the depth of the proof tree as the proof is constructed by the proof verifier. A fast higher note is produced for each step in the construction of a formula. A sustained lower note is produced when the formula is matched to a previous theorem or earlier proof step, to result in a new proof step (which corresponds to a proof step displayed on the Metamath Proof Explorer page that shows the theorem's proof).

Some proof-verification languages require verification programs that are rather large. For example, it has been estimated that a minimal verifier for HOL (a relatively light verification language) would require about 3000 lines of Python code for a verifier. Two projects that have significantly more modest requirements for their checking code are Ghilbert (currently in its early stages) and Metamath (more mature but with the drawback that new definitions can only be introduced as new axioms and therefore must be manually checked for soundness). A proof verifier has been written for the latter with only 300 lines of Python code.

Some proof-verification languages require verification programs that are rather large. For example, it has been estimated that a minimal verifier for HOL (a relatively light verification language) would require about 3000 lines of Python code for a verifier. Two projects that have significantly more modest requirements for their checking code are Ghilbert (currently in its early stages) and Metamath (more mature but with the drawback that new definitions can only be introduced as new axioms and therefore must be manually checked for soundness). A proof verifier has been written for the latter with only 300 lines of Python code.

Readers (or rather web surfers) might also enjoy the Metamath web site. Try the "Metamath Proof Explorer" which "constructs mathematics from scratch" quite literally, up through Cantor's infinity and beyond.

While the "Public Domain Dedication" at http://creativecommons.org/licenses/publicdomain/ seems reasonable, I created my own version which you can see at the bottom of my page http://us.metamath.org/symbols/symbols.html . Although I think it is OK as it is, I welcome comments.

I provide the md5 sum of my public domain file archive. While this may seem nitpicky, it allows the work to be identified unambigously, eliminating the possibility of accidentally using a modified version of that file that someone else has copyrighted. This is one of the dangers of public domain - for example, a photograph of a public-domain painting can be copyrighted, even though it may be visually indistinguishable from another one that has been released to public domain.

Also, I explicitly mention some of the things that can be done with a public domain work to educate the reader. I see many misguided pronouncements making things "public domain" with restrictions attached - for example, "public domain as long as you keep any derivative work public domain", "public domain but you must acknowledge me as the author", or "public domain for educational use". These are really copyright licenses, which is fine if that's what the authors want, but they misunderstand the term "public domain".

What is my personal motivation for making something public domain? For me there is a certain kind of satisfaction I get from old books and images with expired copyright, in that I am completely unencumbered to do whatever I wish with them, without any concern about possible consequences of copying, quoting, sharing, building on, or otherwise using the words, images, and ideas contained therein. I don't have to obsess with keeping track of and chasing down credits and permissions for every little piece of every little image that I might use.

Because I like the feeling of this kind of complete freedom, it is my desire that others experience it with respect to certain work of my own. If by my example some other people are encouraged to do the same, that would benefit me.

Public domain can also make things more practical. Since it can be so time-consuming to track down the copyrights for all the images you want to use on a web page, that often it is more efficient just to reinvent the wheel, taking your own photos of the same thing and redrawing your own versions of the same figures. Royalty-free collections can satisfy the need to a certain extent, but you still have to be careful to understand the licensing terms when using them - for example, do they allow your final work, and therefore any of their images contained in it, to be released to public domain if some day you should decide to do so?

In the end, under public domain I accept that someone may "steal" my work and call it their own. But honorable people give credit where credit makes sense, and for me life is too short to give a hoot about the others. So far it has not been a problem; instead, people have thanked me for making it public domain, and that makes me feel good.