|Metamath Solitaire (Java Applet)|
|Mirrors > Home > Metamath Solitaire|
|Metamath Solitaire (Java Applet)|
Most philosophers agree that contemplation
of Reality is the highest form of happiness. So, if you want happiness,
play Metamath Solitaire all by yourself.
Dress a tedious task in the guise of a game, and there are players
who will spend hours and hours on end doing a task they wouldn't otherwise do.
Essentially everything that is possible to know in mathematics can be derived from a handful of axioms known as "Zermelo-Fraenkel set theory," which is the culmination of years of effort to isolate the essential nature of mathematics and is one of the most impressive achievements of humankind. Metamath Solitaire lets you play with these axioms to prove simple theorems, giving you a glimpse at how ultimately all of mathematics can be derived.
Metamath Solitaire is not a game with a score, where you win or lose. You could try to prove a specific theorem you have in mind (and if you succeed that would be winning), or you can just play around with it and see what happens as you experiment with different combinations of axioms, trying to come up with one that is unusual or aesthetically pleasing.
Metamath Solitaire makes it impossible to prove anything wrong. The only choices you are allowed at any point are legal ones and anything that results on the screen is a mathematically correct theorem, no matter how surprising or bizarre it might seem. Any theorem you stumble across, whether by accident or on purpose, will have a proof that is absolutely rigorous.
There is a theorem of logic which states the trivial fact (read " implies "), which means "if something is true, then it is true". From the 'Axioms:' (right-hand) menu, select in succession ax-1, ax-1, ax-2, ax-mp, and ax-mp. You will see the logic undergo transformations to result in . Select 'Proof Information' from the left-hand menu to see the details of the proof you built.
Choose 'Select Logic Family' from the left-hand menu then click on either 'ZFC Set Theory' or 'ZFC Set Theory + Definitions'. (Some other logic systems - implicational, intuitionist, modal, quantum, Euclidean geometry - are also available but are not discussed here; see the references at the end of this page.)
Mathematicians use symbols to state compactly and precisely what might take many words in English. In Metamath Solitaire, you can think of them as "game pieces" that you manipulate according to the rules of logic. A symbol can be either a constant, shown in black, or a variable, shown in color.
The primitive constant symbols (connectives) for logic and set theory are the following:There are two kinds of variables: wff (well-formed formula, pronounced "wiff") variables and set variables. Variables provide placeholders into which other expressions matching the type of the variable can be substituted. To make it easier to distinguish variables from the connectives, and to identify their type, we show them in color with a different color for each type. Suppose and are wff variables, and and are set variables. Then , , , , and are wffs and can be substituted for wff variables in an axiom or theorem. Set variables can only be substituted with other set variables.
[Note: Elsewhere on the Metamath site, we usually use Greek letters , ,... instead of Roman letters , ,... to represent wff variables, but the meaning is the same.]
For set theory, we introduce some definitions to make things a little more compact. The defined symbols are:Their definitions, which you can see on the 'Axiom Information' screen, introduce a new type of variable called a "class" shown in purple. A set is a class, a class abstraction is a class, and the empty set is a class. If and are variables representing classes, then , , , and are classes. Any expression qualifying as a class may be substituted for a class variable.
With our new symbols, we also extend the definition of a wff. If is a set, and are wffs, and and are classes, then , , , , , , and are wffs and may be substituted for wff variables.
You can see how we can build up complex expressions with these. Expressions qualifying as wffs can contain class variables, and expressions qualifying as classes can contain wff variables. All axioms (and theorems derived from them) are wffs.
Class variables are not part of the primitive language. A class variable can be eliminated from any theorem in which it occurs by replacing it with where and are new set and wff variables not otherwise occurring in the theorem. Here is a sketch of how we transform , for example, to a primitive wff: becomes which finally becomes .
Even with the new symbols, we can still only substitute set variables with other set variables. We can substitute set variable for class variable in the theorem to conclude , but we can't conclude from .
In set theory books, you will find many other definitions built up in a hierarchy starting from these. The theorem of arithmetic 2 + 2 = 4 is explained as follows in terms of set theory: 2, +, and 4 denote specific classes or sets (just as denotes the empty set); 2 + 2 is a class called an operation value (which combines 3 classes to form a new class); and 2 + 2 = 4 is a wff, connecting two classes with the = sign. The proof of 2 + 2 = 4 is very complex if you start with the axioms of set theory and beyond the scope of what you may easily do with Metamath Solitaire. You can see its complete proof in the Metamath Proof Explorer.
Propositional calculus, which is the simplest subset of logic, has four axioms: ax-1, ax-2, ax-3, and ax-mp. (Only this subset of logic shows up by default; you can add more logic and set theory from the left-hand menu.) Each axiom has one assertion and zero or more hypotheses. The first 3 have no hypotheses. The axiom ax-mp has 2 hypotheses and is usually called an "inference rule" rather than an axiom; "mp" stands for "modus ponens".
Modus ponens has two hypotheses, and (read " implies "). It asserts that if we have proved two assertions, and , we can infer a third assertion, namely . Example: If we know that "Bob is a man" and "If Bob is a man then Bob is a human", we can infer "Bob is a human". (To see the representation of modus ponens in Metamath Solitaire, select 'Axiom Information' from the left-hand menu then select 'ax-mp' from the right-hand menu.)
While you are proving a theorem, what you see on the screen is a list of theorems called a "stack". When you click on an axiom, the program figures out how to make variable substitutions into the hypotheses of the axiom and simultaneously into the top-most assertions on the stack so that the hypotheses match these assertions. This is called "unification". After unification, the unified hypotheses are removed from the stack, and the axiom's assertion, with substitutions made to it, is added to the stack. Note that the top of the stack must be matchable to the hypothesis of ax-mp, and the one under it must be matchable to .
If you click on ax-1, ax-2, or ax-3, there is no unification because they have no hypotheses. Instead, they are just added to the stack. All variables in the stack below the one you add are renamed to be unique, to allow future unifications to result in the most general possible theorem.
Your goal is to end up with a single entry in the stack, exhausting it with ax-mp as much as possible. Note that ax-mp won't show up as a choice if unification is not possible. (Using 'Delete Stack Top', you can also trim off failed experiments left dangling on the stack. However you don't have to do this; 'Proof Information' will show only what's needed to prove whatever is on the stack top, ignoring anything below it.)
Click on 'Select Logic Family' then 'Predicate Calculus'. Then select the following axioms in this order to prove :
ax-8 ax-1 ax-2 ax-mp ax-2 ax-2 ax-mp ax-mp ax-mp ax-16 ax-1 ax-mp ax-2 ax-mp ax-mp ax-gen ax-9 ax-mp
Watch carefully (then read about) the distinct variable requirement that appears at the tenth step, evolves during the rest of the proof, and vanishes at the end. 'Axiom Information' then 'ax-16' will show the axiom where this requirement originates; click 'Exit Axiom Information' to get back. After the proof is complete, you can select 'Proof Information' to see the final variable assignments back-substituted throughout the proof.
If we introduce set theory, there is a shorter proof of . Click on 'Select Logic Family' then 'ZFC Set Theory'. Then click on:
ax-1 ax-1 ax-2 ax-mp ax-mp ax-1 ax-1 ax-2 ax-mp ax-mp df-bi3 ax-mp ax-mp ax-gen ax-ext ax-mp
There, your first proof using an axiom of set theory!
To prove the more general for classes, click on 'Select Logic Family' then 'ZFC Set Theory + Definitions'. Then click on:
ax-1 ax-1 ax-2 ax-mp ax-mp ax-1 ax-1 ax-2 ax-mp ax-mp df-bi3 ax-mp ax-mp ax-gen df-ceq df-bi2 ax-mp ax-mp
Are you starting to get the idea now? (Your main goal should be to try to understand what what happens when you click on an axiom or rule, so you are convinced the result really follows from the sequence of steps. Don't be frustrated if you can't "see" how we came up with the sequence of steps in the first place - that does not come naturally and requires a lot of practice. Indeed, some of the above proofs were based on an exhaustive computer search to find the shortest sequence.)
Often a useful intermediate result tends to get used over and over again. Rather than prove it anew each time, you can add it as an additional axiom.
For example, a very useful rule is the syllogism inference. It has hypotheses and from which it asserts . Select 'Add Hypothesis' twice. Then select Axioms $hyp1, $hyp2, ax-1, ax-mp, ax-2, ax-mp, ax-mp. Click on 'Save as Axiom'. You will see it stored as 'user-1' on the 'Axiom Information' screen, and it will appear in the 'Axioms:' menu whenever it can be applied to the top 2 entries of the stack. After 'Save as Axiom', select 'Erase Stack' to start a new proof (and use your syllogism in it if you wish). Exercise: Use your syllogism to shorten the first proof of above to 14 steps. (Hint: look for the sequence ax-1, ax-mp, ax-2, ax-mp, ax-mp and replace it with user-1.)
Unfortunately, the applet does not have the ability to save your proofs in a disk file. You can save your work by clipping the proofs from the 'Proof Information' screen and putting them into an editor (or writing them down on a piece of paper if your browser doesn't support this). Everything will be erased when you exit the browser!
As a security feature, Java applets normally cannot write to the user's disk. As mentioned in the 28-Mar-2006 note at the top of this page, Scott Fenton has created a stand-alone version of the Metamath Solitaire Java program. If you are interested and know Java, this program could be enhanced to save and retrieve proofs.
For more serious proofs, you may want to learn how to use the Metamath program, which allows you to save your work and has a large database of already proved results to start from.
Here are a few more proofs in propositional calculus to get you started. To abbreviate the proofs, I've used 1, 2, 3, and m in place of ax-1, ax-2, ax-3, and ax-mp. If you find a clever proof, send it to me and maybe I'll post it here, with your name attached to it, of course!
Theorem: Proof: (19 steps) 211m2mm11m22mm1m2mm
Theorem: Proof: (7 steps) 121m2mm
Theorem: Proof: (15 steps) 1121m2mm2m1m2mm
Theorem: Proof: (19 steps) 1131m2mm31m2mm2mm3m
Theorem: Proof: (17 steps) 1131m2mm31m2mm2mm
Theorem: Proof: (7 steps) 131m2mm
You can also find proofs of all 193 theorems of propositional calculus in Whitehead and Russell's Principia Mathematica here.
Practically speaking, no. The axioms for set theory are presented in their raw form, and extensive logic manipulation is necessary to come up with even simple theorems of textbook set theory. For example, here are the lengths ('Axioms:' menu clicks) of some actual proofs: commutative law for logical OR, 177 clicks; existence of the empty set, 6,175,677 clicks; transfinite recursion, 24,326,750,185,446 clicks! Your instructor might not appreciate such proofs for your homework, whose printouts you would have to roll in with a wheelbarrow or possibly a fleet of tractor-trailer trucks. Proofs can be made much smaller by creating a hierarchy of reusable intermediate subtheorems with 'Save as Axiom'. For the first proof, with 10 subtheorems we can reduce the total number of 'Axioms:' clicks to 69; for the second, with 171 subtheorems we can reduce it to 1267 clicks; the third, transfinite recursion, 736 subtheorems and 7557 clicks - all possible in principle with the applet but hardly practical, especially since the applet cannot save and recall your work.
These proofs and thousands more are worked out in complete detail in the database for the Metamath software (which has a command-line interface) and are displayed on the web in the Metamath Proof Explorer. Topics in its database file include Russell's paradox, Cantor's theorem, Peano's postulates, the Burali-Forti paradox, transfinite induction and recursion, the Schröder-Bernstein theorem, Zermelo's well-ordering theorem, Zorn's Lemma, and the complete Dedekind-cut construction of real numbers.
For a more in-depth understanding of the Metamath program you'll want to look at the Metamath book (PDF file, 1.3 megabytes, 200 pp.), which also includes an easy-to-read informal discussion of abstract mathematics and computers and has references to other proof verifiers and automated theorem provers.
Yes, you may look at the source code. The program is copyrighted under the terms of the GNU General Public License [external]. You can also download the compiled applet.
Some interesting places to start are A home page for THE AXIOM OF CHOICE [external] and Set Theory Page [external] and Infinite Ink's Mathematics Page [external]. If you know of other good pages, let me know.
Almost anything you could imagine is available at Math Forum Internet Mathematics Library [external]. Over 15000 calculators can be found at Martindale's Calculators On-Line Center [external]. Logic calculators can be found at Christian Gottschall's Gateway to Logic [external] and Frank Potter's Science Gems - Mathematics [external] and Logic Calculator [external].
The Database of Existing Mechanized Reasoning Systems [external] has several reasoning tools executable via the Web.
The axioms (or more precisely, axiom schemes) are logically equivalent to the ones you learned. Specifically, they are equivalent to a Hilbert-style system of first-order logic with equality and a single binary predicate (stylized epsilon). It is easy to see that each axiom is a theorem scheme of standard classical predicate calculus. In addition, though, the set of axioms is metalogically complete, meaning that we can directly prove all possible simple metatheorems (not just theorems) with no additional metalogic beyond the simple metalogic built into the underlying formal framework. A simple metatheorem is a theorem scheme with metavariables that range over wffs and individual variables, along with zero or more restrictions of the forms "where and are distinct individual variables" and "where is an individual variable not occurring in wff ". These terms are explained in more detail in Remark 9.6 of this article (PDF file).
The algorithm that manipulates the axioms and inference rules is unification (a matching and substitution algorithm used by theorem provers) enhanced to obey any accompanying distinct variable restrictions. In the applet, this algorithm is performed by the "unify" method in the "Unification" class in mm.java, returning the :most general" unified scheme if it exists and if no distinct variable restrictions are violated (or null otherwise).
Although more axioms are needed for our system compared to standard systems, the underlying concepts involve only simple substitution of expressions for metavariables (subject to distinct variable restrictions). There are no primitive notions of free variable and proper substitution; these are defined concepts. Free and bound variables may be substituted with the same variable provided no distinct variable constraint is violated (and the unification algorithm does not permit you to violate it). For example, from we may safely infer since we can prove the former without variable restrictions, but from (which will have the restrictions distinct from and distinct from ) we may not infer . Each individual variable should be thought of as a metavariable of ordinary predicate calculus, and you will recognize these two examples as valid metatheorems.
This axiom system has been used to verify proofs of reasonably sophisticated theorems of elementary set theory as you can see in the Metamath Proof Explorer. For another discussion of the axioms see the Metamath Proof Explorer's note on the axioms.
page was last updated on 4-Nov-2015.
Your comments are welcome: Norman Megill
Copyright terms: Public domain
|W3C HTML validation [external]|