|
|
Metamath Solitaire (Java Applet) | |
| Mirrors > Home > Metamath Solitaire | ||
|
|
Because of security issues with Java applets, several browsers have removed the ability to run Java applets, and the above links will not work. However, it is possible to run the applet independent of any browser. On Windows 7, the following instructions worked as of 14-Mar-2018. (I expect Windows 10 will be similar but haven't tried it. If someone wishes to work out the instructions for Windows 10, MacOS, or Linux, let me know and I will post the information here.)1. In the Windows Start menu, in the "Search programs and files" box, type "Programs and Features". The "Programs and Features" control panel should open. Uninstall any existing versions of Java.
2. Go to http://www.oracle.com/technetwork/java/javase/downloads/jdk8-downloads-2133151.html [accessed 4-Aug-2018]. Check "Accept" the license. Click on jdk-8u161-windows-i586.exe to download it. In the download folder, double-click on jdk-8u161-windows-i586.exe; follow the instructions to install Java, accepting all defaults. Note that this is the 32-bit version of Java, which you must install even if your computer is 64 bits. (The ability to run applets was removed from the 64-bit version of Java.)
3. In the Windows Start menu, select All Programs, then Java, then Configure Java. The Java Control Panel will open. Click the Security tab. Check "Enable Java content for browser and Web Start applications". Check the "High" security level (not "Very High"). Next to the "Exception Site List", click on "Edit Site List...", then "Add". Enter "http://us.metamath.org" then click OK. "http://us.metamath.org" should appear in the "Exception Site List". Click OK at the bottom of the Java Control Panel.
4. In the Windows Start menu, in the "Search programs and files" box, type "command". A Command Prompt window will open. In the Command Prompt window, type exactly (or copy/paste) the following, including the quotes:
"C:\Program Files (x86)\Java\jdk1.8.0_161\bin\appletviewer" http://us.metamath.org/mmsolitaire/mmsviewer.html
(To paste into the Command Prompt window, click on the upper left "C:\." icon, select Edit, then Paste.) The Metamath Solitaire applet should run.
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 [accessed 20-Jul-2020]. You can also download the compiled applet.
Some interesting places to start are A home page for THE AXIOM OF CHOICE [accessed 20-Jul-2020] and and Infinite Ink's Mathematics Page [accessed 20-Jul-2020]. If you know of other good pages, let me know.
Almost anything you could imagine is available at Math Forum Internet Mathematics Library [accessed 20-Jul-2020]. Logic calculators can be found at Frank Potter's Science Gems - Mathematics [accessed 20-Jul-2020] and Logic Calculator [accessed 20-Jul-2020].
The Database of Existing Mechanized Reasoning Systems [accessed 20-Jul-2020] 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.
| This
page was last updated on 17-Oct-2020. Your comments are welcome: Norman Megill  Copyright terms: Public domain |
W3C HTML validation [external] |