I have created a clone of Metamath's peano.mm

http://us2.metamath.org:8888/ocat/mmj2/peanoInfix.zip

That zip file contains

peanoInfix.mm

PLUS

mmj2PeanoInfix?.bat

PLUS

RunParmsPeanoInfix?.txt

for running mmj2 and the mmj2 Proof Assistant with the infix version of peano.mm.

I added a "dummy" theorem to the .mm file so that mmj2 has at least one theorem to start with (standard proof = ax-1 ax-mp ax-mp).

The RunParms? required mods to the WorkVar? prefixes, as you will see.

To use the zip file, unpack it and copy the 3 individual files (not the "peanoInfix" directory) to the c:\mmj2jar subdirectory. (If you're using Linux or OS X I don't need to tell you how to configure your systems :-)

P.S. Note on validity of the transformation to the new grammar (aside from any inadvertent typos I may have inserted). The original peano.mm contains an unambiguous polish prefix notation grammar. The peanoInfix.mm file contains an unambiguous infix+prefix (combo) notation grammar – essentially just adding parentheses to binary operations and moving the operation symbol between the operands. The new grammar does not invalidate the existing axioms and theorems, which Solovay painstakingly proves using metalogical arguments and considerations involving length of formulas, which require polish prefix notation…because assuming that the infix+prefix grammar is unambiguous, the resulting parse trees can be converted (and vice-versa) to polish prefix or reverse polish notation. So nothing we do using a different syntax, if the syntax is unambigously convertible to the original polish prefix notation, invalidates the axioms or theorems; we're just writing the formulas out in a more human-readable form.

--ocat 4-May-2008

—

New version of mmj2 uploaded: 1-Mar-2008!

http://us2.metamath.org:8888/ocat/mmj2/mmj2.zip

Refer to mmj2\CHGLOG.TXT in the mmj2.zip downwload for a description of the changes. (A last minute change was made to trigger the Step Selector Search via double-clicking on a Derivation proof step – or just position the cursor on the step and use Ctrl-8.)

Hope you enjoy it!

--ocat 17-Feb-2008

— mmj2 is an open source software package for use with metamath (.mm) databases. It is written in Java and provides both batch (command line) and GUI capabilities. Its most notable feature is the mmj2 Proof Assistant GUI, which provides support for Metamath proof development and is perhaps easier to use than the metamath.exe proof assistant (note: power users benefit from using both proof assistants simultaneously, and employ the Metamath eimm.exe utility to transfers proofs between the two proof assistants.)

For documentation, tutorial, etc., plus the full source code and .jar (java executables), download:

http://us2.metamath.org:8888/ocat/mmj2/mmj2.zip

and

http://us2.metamath.org:8888/ocat/mmj2/mmj2.md5

See also (new!): mmj2ProofAssistantQuickTips

Inspirational Quote

     "We have put ourselves to work for the sake
     of an idea, seeking by magnificent exertions
     to arrive at the incredible." ~ José Ortega y Gasset 
     -- http://www.des.emory.edu/mfp/impossibleG.html

Feedback

MMJ2 Laboratories, Inc. is interested in hearing from you about your happy or unhappy experiences with mmj2.

Please use the dedicated page for mmj2 Feedback/Questions: mmj2Feedback

Here is a dedicated page for feedback about the mmj2 Proof Assistant GUI: mmj2ProofAssistantFeedback

NOTE: To update the wiki your "username" must be "whitelisted". Send an email to the wikilord if you are not already a user – and, if you don't care to do that, I authorize you to post as "ocat" for the purposes of mmj2 feedback and problem reports, etc. (Just put some initials on your edits so I know who is doing what…)

ALSO, you may get the "Cannot acquire main lock" error message when attempting to post to the wiki. In this case, hit the Back button on your browser, open a new window and go to RecentChanges then click on Administration, then Unlock Wiki. Wait, and then return to your original post and click on "submit" again.

--ocat 2007-10-15

Index of mmj2* pages

(This is wiki everything regardless of any "enduring merit". The mmj2 "doc" directory in the mmj2.zip download contains the most valuable information – whereas these pages contain tenative drafts and discussions, among other things, such as errors and possibly even misinformation, depending…)

MaximallyCompressedMetamathDatabases

MetamathForProgrammers

mmj2-01-Oct-2007ReleaseEnhancements

mmj2ASCIITypesetting

mmj2BetaRelease01Sep2007Feedback

mmj2Feedback

mmj2FeedbackV20061101

mmj2FeedbackV20070716

mmj2Feedback20080113

mmj2GrammaticalInductiveSets

mmj2InverseProvingProjectIdea

mmj2MoreDummyVarSpecs