See also:

Proof Assistant User Guide

ProofAssistantGUIQuickHOWTO.html

ProofAssistantGUIDetailedInfo.html

ProofAssistantGUIDeriveFeature.html

StepUnifier.html

PageLocalRef.mmp

WorkVariables.html

StepSelectorSearch.html

UnifyEraseAndRederiveFormulas.html

So, it is possible to emulate Metamath Solitaire with mmj2. And unlike the Metamath Solitaire applet, you can save a partially completed proof to continue to work on later. In addition, mmj2 not only can be used to create proofs forward as Metamath Solitaire does, it can also be used to create them backwards from the conclusion.

I'll start at the beginning, assuming you are using Windows, so you won't have to read the mmj2 documentation. Download the latest

`mmj2.zip`

and put it in `c:\mmj2.zip`

. Extract the Zip file to
create `c:\mmj2`

with default settings. From the
result, move or copy the directory `c:\mmj2\mmj2jar`

to `c:\mmj2jar`

(run `c:\mmj2\mmj2jar\copymmj2jar.bat`

to create and copy `c:\mmj2jar`

-- see below for instructions on running a "`.bat`

" file.)I assume you have Java installed. If not, I guess you'll have to read the mmj2 documentation after all.

Next, download set.mm (6MB) into the directory

`c:\metamath`

. Or, if you
want it somewhere else, change the parameter ` LoadFile,set.mm`

accordingly, using a text editor like Notepad to edit

` c:\mmj2jar\RunParms.txt`

You may also need to update the "mmj2Path" parameter in mmj2.bat (command line argument #3 after "

`mmj2.jar`

") in:` c:\mmj2jar\mmj2.bat`

Then

In Windows, select Start -> Run, type "

`cmd`

", click OK,
and a Command Prompt window will open. Type ` c:\mmj2jar\mmj2.bat`

following by Enter to start mmj2.

NOW set mmj2's ProofAsstGUI screen Edit/Set Incomplete Step Cursor menu item to "3" - Last.

A useful reference file for playing with Metamath Solitaire is the http://us2.metamath.org:8888/mmsolitaire/pmproofs.txt pmproofs.txt - Shortest known proofs list. Each of the 193 proofs begins with two lines: the theorem itself and the "Result of proof" when you enter the proof into the Metamath Solitaire applet. The "Result of proof" line is what you want to focus on: the theorem itself often requires the introduction of definitions, which is beyond the scope of this tutorial and is an exercise for advanced users.

It turns out that all of these 193 theorems also exist in set.mm. Most of them have definitions incorporated and don't match the "Result of proof". But some of them do, such as set.mm's "

`imim2`

"
for
theorem
"*2.05
Syll". So for this example, we will pick that
one, since it is already in set.mm and we won't have to type it in.From the mmj2 ProofAsstGUI screen, select File -> New Proof -> imim2.

The screen will look like this:

```
$( <MM> <PROOF_ASST>
THEOREM=imim2 LOC_AFTER=?
```

* A closed form of syllogism (see ~ syl ). Theorem *2.05 of

[WhiteheadRussell] p. 100.

qed::
|-
(
(
ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )

$)

We can see that the "

`qed`

" step matches the "Result of
proof" for theorem "*2.05 Syll", which is what we want. (For
other proofs where it doesn't, we can change the qed step so that it
does.)Look at the proof in the pmproofs.txt file:

` DD2D121; ! 7 steps`

Unlike the Metamath Solitaire applet, we are going to enter this proof from left-to-right instead of right-to-left. The letter D means ax-mp, 2 means ax-2, and 1 means ax-1.

On the mmj2 ProofAsstGUI screen, the cursor should be positioned immediately after the second colon in "

`qed::`

".
Here
are
the
exact stepsto enter the proof, following the "`DD2D121`

"
above
exactly:Type

`ax-mp`

(just the 5 characters "ax-mp" with no Enter),
ctrl-u (hold down the ctrl key and press "u"), `ax-mp`

,
ctrl-u, `ax-2`

, ctrl-u, `ax-mp`

, ctrl-u, `ax-1`

,
ctrl-u,
`ax-2`

, ctrl-u, `ax-1`

, ctrl-u.
Voila, the proof is done and will look like this:```
$( <MM> <PROOF_ASST>
THEOREM=imim2 LOC_AFTER=?
```

* A closed form of syllogism (see ~ syl ). Theorem *2.05 of

[WhiteheadRussell] p. 100.

1000::ax-1
|-
(
(
ph -> ps ) -> ( ch -> ( ph -> ps ) ) )

5000::ax-2 |-
( ( ch -> ( ph -> ps ) )

->
(
(
ch -> ph ) -> ( ch -> ps ) ) )

6000::ax-1 |-
( ( ( ch -> ( ph -> ps ) )

->
(
(
ch -> ph ) -> ( ch -> ps ) ) )

->
(
(
ph -> ps )

->
(
(
ch -> ( ph -> ps ) )

->
(
(
ch -> ph ) -> ( ch -> ps ) ) ) ) )

3000:5000,6000:ax-mp

|-
(
(
ph -> ps )

->
(
(
ch -> ( ph -> ps ) )

->
(
(
ch -> ph ) -> ( ch -> ps ) ) ) )

4000::ax-2 |-
( ( ( ph -> ps )

->
(
(
ch -> ( ph -> ps ) )

->
(
(
ch -> ph ) -> ( ch -> ps ) ) ) )

->
(
(
( ph -> ps ) -> ( ch -> ( ph -> ps ) ) )

->
(
(
ph -> ps )

->
(
(
ch -> ph ) -> ( ch -> ps ) ) ) ) )

2000:3000,4000:ax-mp

|-
(
(
( ph -> ps ) -> ( ch -> ( ph -> ps ) ) )

->
(
(
ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) )
) )

qed:1000,2000:ax-mp |- ( ( ph -> ps )
-> ( ( ch -> ph ) -> ( ch -> ps ) ) )

$= wph wps wi wch wph wps wi wi wi wph wps wi wch wph wi
wch wps wi

wi wi wph wps wi wch ax-1 wph wps wi wch wph
wps wi wi wch wph wi

wch wps wi wi wi wi wph wps wi wch wph wps wi
wi wi wph wps wi wch

wph wi wch wps wi wi wi wi wch wph wps wi wi
wch wph wi wch wps wi

wi wi wph wps wi wch wph wps wi wi wch wph wi
wch wps wi wi wi wi

wch wph wps ax-2 wch wph wps wi wi wch wph wi
wch wps wi wi wi wph

wps wi ax-1 ax-mp wph wps wi wch wph wps wi wi
wch wph wi wch wps wi

wi ax-2 ax-mp ax-mp $.

$)

[Forward Proving Narrative excised by editor]

As a final note, it is sometimes interesting to see if the proof as a whole leads to a more general theorem than the one shown by the '

`qed`

'
step.
To
do
that, just add the last `ax-mp`

in its
own new step instead of modifying the '`qed`

' step. In
this example, a more general theorem does not result, as you can verify
as an exercise.-- Norm 22 Jan 2008.