Metamath Home Metamath Solitaire (Java Applet)  
Mirrors  >  Home  >  Metamath Solitaire
Metamath HomeMetamath
Home
Metamath Solitaire (Java Applet)  

Run the applet in a popup window
Run the applet in main browser window

(Recent versions of Java will block this applet by default for security reasons. For instructions on how to allow it, see How can I configure the Exception Site List? [accessed 4-Nov-2015].)
Welcome to Metamath Solitaire, a Java applet that lets you build simple proofs in logic and set theory. You can play around with it for curiosity or fun, or if you're serious it will be the hardest "game" in the world! This is because built into it are the axioms of logic and ZFC (Zermelo-Fraenkel with Choice) set theory, which are generally held to encompass essentially all of mathematics. It's up to you to unlock its secrets!
  1. What is the goal of Metamath Solitaire?
  2. Can I make a mistake?
  3. I'm impatient and want to see something happen right away!
  4. I only see the axioms for propositional calculus. How do I get set theory?
  5. What do the symbols mean?
  6. How does the logic work?
  7. How can I prove x = x?
  8. How can I add my own theorems as additional axioms?
  9. How can I save my work?
  10. Can I see some more proofs?
  11. Will Metamath Solitaire help me do my set theory homework?
  12. Can I look at the source code?
  13. What other Web resources are there for set theory?
  14. Where can I find other math applets?
  15. (For logicians) Why do the axioms of Predicate Calculus look different from the ones I learned in school?
  16. (For logicians) Where can I find references for the other logics shown on the 'Select Logic Family' screen?

 

Most philosophers agree that contemplation of Reality is the highest form of happiness. So, if you want happiness, play Metamath Solitaire all by yourself.
—Prof. Kannan Nambiar (ret.), Jawaharlal Nehru Univ.

 

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.
—Nick Yee, Stanford Univ.

   New 2-Dec-2006    Berislav Žarnić has translated the Metamath Solitaire applet to Croatian [external].
   New 28-Mar-2006    Scott Fenton created the following Metamath Solitaire versions: mm.java.gz upgrades the mm.java file to use the features of Java 2 SDK 1.5, and mmsol-0.5.tar.gz is a standalone version (not an applet) that reads the axioms from external files rather than embedded in the applet. Note. The SDK 1.5 version of mm.java has not yet been made official because it is unclear if it will run in earlier versions of Internet Explorer. A volunteer with access to IE 5.50.4522.1800 (Windows 98 or NT 4.0), with Microsoft's (not Sun's) Java virtual machine version 3802, is needed to test it: when mousing over the area where the applet would be, make sure it doesn't flash an error message on the bottom of the screen saying, "load: class mm not found". SDK 1.4 had this problem, causing user complaints, so it is currently compiled using SDK 1.3.
   Updated 16-Feb-2013    An open challenge has been to beat the records for the shortest known proofs (text file) for the 193 theorems of propositional calculus in Whitehead and Russell's Principia Mathematica. (The instructions in the file tell you how to enter these in Metamath Solitaire applet, although the longer ones will require considerable patience.) Gregory Bush found shorter proofs for 67 of the 193 theorems, and Scott Fenton has found additional shortenings. Older versions: pmproofs-orig.txt pmproofs-2010-11-01.txt pmproofs-2012-01-23.txt.
   New 13-Apr-2001    Thanks to Marcello DeMarinis from Italy for upgrading this applet to Java 2.
1. What is the goal of Metamath Solitaire?

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.


2. Can I make a mistake?

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.


3. I'm impatient and want to see something happen right away!

There is a theorem of logic which states the trivial fact (P -> P) (read "P implies P"), 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 (P -> P). Select 'Proof Information' from the left-hand menu to see the details of the proof you built.


4. I only see the axioms for propositional calculus. How do I get set theory?

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.)


5. What do the symbols mean?

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:

  • -> (arrow): implies
  • -. (sideways backwards L): not
  • A. (upside down A): for all
  • = (equals sign): equals
  • e. (stylized epsilon): is an element of
  • ( and ) (left and right parentheses)
  • 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 P and Q are wff variables, and x and y are set variables. Then (P -> Q), -. P, A.xP, x = y, and x e. y 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 ph, ps,... instead of Roman letters P, Q,... 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:

  • <-> (double arrow): logically equivalent to
  • \/ (vee): or
  • /\ (wedge): and
  • E. (backwards E): exists
  • {x | P}: class abstraction (or class builder): the class of (sets) x such that (wff) P is true
  • (_ (underlined sideways U): is a subset of
  • u. (small sans-serif u): union of two classes
  • U. (large sans-serif U): union of a class
  • i^i (upside-down u): intersection of two classes
  • |^| (upside-down U): intersection of a class
  • (/) (circle with slash): empty set
  • 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 x is a class, a class abstraction {x | P} is a class, and the empty set (/) is a class. If A and B are variables representing classes, then (A u. B), (A i^i B), U.A, and |^|A 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 x is a set, P and Q are wffs, and A and B are classes, then (P <-> Q), (P \/ Q), (P /\ Q), E.xP, A = B, A e. B, and A (_ B 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 A can be eliminated from any theorem in which it occurs by replacing it with {x | P} where x and P are new set and wff variables not otherwise occurring in the theorem. Here is a sketch of how we transform A = A, for example, to a primitive wff: {x | P} = {x | P} becomes A.x(P <-> P) which finally becomes A.x-. ((P -> P) -> -. (P -> P)).

    Even with the new symbols, we can still only substitute set variables with other set variables. We can substitute set variable x for class variable A in the theorem A = A to conclude x = x, but we can't conclude A = A from x = x.

    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.


    6. How does the logic work?

    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, P and (P -> Q) (read "P implies Q"). It asserts that if we have proved two assertions, P and (P -> Q), we can infer a third assertion, namely Q. 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 (P -> Q) hypothesis of ax-mp, and the one under it must be matchable to P.

    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.)


    7. How can I prove x = x?

    Click on 'Select Logic Family' then 'Predicate Calculus'. Then select the following axioms in this order to prove x = x:

    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 x = x. 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 A = A 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.)


    8. How can I add my own theorems as additional axioms?

    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 (P -> Q) and (Q -> R) from which it asserts (P -> R). 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 x = x 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.)


    9. How can I save my work?

    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.


    10. Can I see some more proofs?

    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: ((P -> (Q -> R)) -> (Q -> (P -> R)))  Proof: (19 steps) 211m2mm11m22mm1m2mm

    Theorem: ((Q -> R) -> ((P -> Q) -> (P -> R)))  Proof: (7 steps) 121m2mm

    Theorem: ((P -> Q) -> ((Q -> R) -> (P -> R)))  Proof: (15 steps) 1121m2mm2m1m2mm

    Theorem: (P -> -. -. P)  Proof: (19 steps) 1131m2mm31m2mm2mm3m

    Theorem: (-. -. P -> P)  Proof: (17 steps) 1131m2mm31m2mm2mm

    Theorem: (-. P -> (P -> Q))  Proof: (7 steps) 131m2mm

    You can also find proofs of all 193 theorems of propositional calculus in Whitehead and Russell's Principia Mathematica here.


    11. Will Metamath Solitaire help me do my set theory homework?

    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.


    12. Can I look at the source code?

    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.


    13. What other Web resources are there for set theory?

    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.


    14. Where can I find other math applets?

    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.


    15. (For logicians) Why do the axioms of Predicate Calculus look different from the ones I learned in school?

    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 x and y are distinct individual variables" and "where x is an individual variable not occurring in wff P". 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 E.xx = y we may safely infer E.xx = x since we can prove the former without variable restrictions, but from x e. y -> A.zx e. y (which will have the restrictions z distinct from x and z distinct from y) we may not infer z e. y -> A.zz e. y. 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.


    16. (For logicians) Where can I find references for the other logics shown on the 'Select Logic Family' screen?
  • Implicational logic: Roger Hindley and David Meredith, Principal Type-Schemes and Condensed Detachment, J. Symb. Logic 55, 90-105 (1990).
  • Intuitionist propositional calculus: T. Thatcher Robinson, Independence of Two Nice Sets of Axioms for the Propositional Calculus, J. Symb. Logic 33, 265-270 (1968).
  • Modal logic [external]
  • Modal provability logic: George Boolos and Richard Jeffrey, Computability and Logic (1989), ch. 27.
  • Quantum logic: M. Pavicic, Nonordered Quantum Logic, Int. J. of Theoretical Physics 32, 1481-1505 (1993) and M. Pavicic, private communication (1997).
  • Euclidean geometry: A. Tarski, What is Elementary Geometry?, in The Axiomatic Method (ed. L. Henkin et. al.) (1959), pp. 16-29.
  • Weak D-complete logic: N. Megill and M. Bunder, Weaker D-Complete Logics [external], J. IGPL 4 (1996), pp. 215-225. PDF version. This is a specialized research logic that is mostly of interest to logicians.

  •   This page was last updated on 4-Nov-2015.
    Your comments are welcome: Norman Megill nm at alum dot mit dot edu
    Copyright terms: Public domain
    W3C HTML validation [external]