HomePage RecentChanges

mmj2FeedbackV20061101

Back to: mmj2

Questions/Comments About mmj2?

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

Feel free to use this page for other items, I will check in every day or so?

NOTE: It is not necessary to be a member or to register, log-on, or otherwise prepare for making a comment. Simply enable "cookies" on your browser, click on "Edit this page", and type in your comment/question/note. Then "save". It is desired that you identify yourself in some way, and perhaps even add your name to the "guest" list. Make up a pseudonym if you are inclined and use that, if your are security conscious. --ocat

Bug, Grammatical Loop Not Detected

mmj2 not detecting loop in example below – unless the last two axioms were reversed! Will be fixed in Oct-1-2005 update. Offending code was in mmj.verify.TypeConversionRule?#deriveAdditionalRules()

  $( E-GR-0041 Syntax Axiom, label = ";
               " is a Type Conversion Rule that creates a 
               " Type Conversion loop from Type = ";
               ", to Type = "; $)
  $c c41a c41b c41c $.
  $v v41a v41b v41c $.
  vH41a $f c41a v41a $.
  vH41b $f c41b v41b $.
  vH41c $f c41c v41c $.
  conv41c $a c41b v41c $.
  conv41b $a c41a v41b $.
  conv41a $a c41c v41a $.

--ocat


How would you describe the potential of mmj2 for mapping Metamath code to H-code, once a spec for the latter exists? --jcorneli


mmj2 reads ".mm" formatted files and loads them into objects, such as "Axiom", "Theorem" and so on. Regurgitating these objects would not be hard. A big question is what would be the semantic mapping. You will notice that set.mm contains a "$t" section with typesetting information for html and latex, so converting that one .mm file to hcode might be as easy as running a metamath.exe command and then feeding the text output files into the HDM parser, which presumably has enough smarts to deal with arbitrary, foreign data. At this time mmj2 does not make use of, or store the $t information for a .mm file.

Previously I suggested defining a lower level than hcode, such as Ghilbert format which HDM would be expected to be able to parse to and from. Were that approach taken, the task of converting an arbitrary .mm file to a .gh file would be the objective.

A deeper issue is that Metamath and Ghilbert are self-defining and are self-contained. A "mathelogical" system in Metamath/Ghilbert has its own language, symbols, definitions and can exist in its own universe. This means that there can be many systems and they need not be consistent with each other – there may be no common point of reference, symbols, logicks and concepts may be disjoint. So the real problem, if you want to be a perfectionist is the same as converting between two different Semantic Web Ontologies. That task requires human understanding.

There is an unresolved technical problem also involving the use of the $d, Disjoint Variable Restriction command in Metamath/Ghilbert instead of "free" and "bound" variables. As far as I know, the conversion from $d's to free/bound is understood by fewer people than understand quantum physics. I'm not sure which field of study is simpler, either. Better check with Sensei Megill on that one!

In the end, mmj2 is all just batch Java code so any monkey ought to be able to chunk out the conversion program! Get the hcode specs and ontology written and we'll slam set.mm in there one way or another! Har. --ocat

I guess I was thinking about the potential of mmj2 being part of the foundation of the HDM parser itself, which mythological construct finds itself in a similar position vis a vis "symbols, logicks, and concepts" to the one you describe above. By restricting at least to "Metamath code" instead of "mathematical language in general", perhaps we can sort out some of the ontological & linguistic difficulties attendant upon the Parsing Problem. At least, the idea sounds nice. I'm also noting that on the mmj2 page you seem to be expressing interest in working on this sort of problem, yes? It would be interesting to know how Raph did the translations from MM to GH; if it was with code, presumably it would be nice to have this code bundled with GH. --jcorneli

Yes, I wrote code to do this, but it's unpolished and needs a fair amount of manual fixup to be useful. The Python code is mm_xlat.py. It was written over a year ago, and thus will no doubt need some work to handle the changes to the set.mm grammar since then. Hope you find it useful or interesting anyway. --raph

Thank you, Raph!

JCorneli: I see that mm_xlat.py is designed to work only with set.mm. That's big though! Maybe that's all you need! And Python can be invoked from Lisp? --ocat

P.S. I received information today about another grammatical parser for Metamath files. I am fascinated by the huge interest in Metamath as a language and a means of expressing "mathelogic". One day villages all over the world will have statues of Norman Megill, Planetary Benefactor. Of that I am sure :) In the meantime, it would be excellent if everyone could work together to develop a GUI system suitable for use by beginners, even high school students, that wish to learn logic. I think Raph has chosen well with Python and his initial draft of Ghilbert, so I plan to follow that lead (noting that Ghilbert needs a way to store the notations for terms so that the UI can display formulas similar to the way they are shown in Metamath – or otherwise – since sexp's are intractable beyond a few levels… And I think the language should accomodate term notations, along with Metamath's $t specifications. Somehow. It would be ok to fork Ghilbert, I guess, but better if the whole planet could unite and make this happen. Never before has Earth been so in need of Logic – and Vulcans.) --ocat 19-Oct-2005

Here's a script to compile mmj2 to a jar under linux:

  #! /bin/sh
  #
  # A script to compile mmj2 under linux with jdk1.5.
  # Run from the mmj2 top directory.
  # Should produce "mmj2.jar".
  #
  echo "Manifest-Version: 1.0" >MANIFEST.MF
  echo "Main-Class: mmj.util.BatchMMJ2" >>MANIFEST.MF
  cd src && javac `find -name *.java` -d ../classes && cd ../classes && \
  jar cfm ../mmj2.jar ../MANIFEST.MF \
  `find -name "*.class" | sed -e "s/^\.\///"

mmj2 processes uncompressed set.mm (Sample001.txt) in 11 sec on my P4 2GHz, 256M machine. You said it was 33 sec on Celeron 1.8GHz, 256M. Hmm… I was unable to use that SystemOutputFile? for some reason, so I redirected output through a pipe. Probably this has something to do with performance. I didn't try it, but I suggest something like

  new PrintWriter(new BufferedWriter(new FileWriter(filename)))

instead of vanilla new PrintWriter?(filename). --alih

Good catch! I was just in mmj.util.Boss today creating a Writer for exported ProofAsst? proofs – and I see that section of code. Will use buffered, for sure. I am doubting that affected Sample001 very much though because that has a "MaxStatementPrintCount?,50" RunParm?. [Unless someone really needs the output in a file, is best to just not use the "SystemOutputFile?" and "SystemErrorFile?" RunParms? – especially the error file, which is nice to see in realtime on the console.]

And thanks for the Linux compile info. If you can also provide a script for running BatchMMJ?2, etc. that will be very helpful, I think.

--ocat 16-Jan-2006

Glad it worked.

Hm, the output of Sample001 is about 140K despite MaxStatementsProofCount? of 50.

Well, running a jar is very simple:

  java -jar mmj2.jar <parameters>

and it's a standard way of running java programs, so I don't think any scripts are necessary here. Also note that under linux there is no C:\, so absolute pathnames won't work. Probably it's a good idea to accept mm file name from the command-line arguments. --alih

Hmmm, interesting. Thanks for the tutorial! I wonder how java knows which program inside mmj2.jar to run first?

Re: arguments… The RunParm? file is passed via command-line, and its options will handle relative pathnames, so the facilities should be operable. When I threw the BatchMMJ?2 thing together just before posting mmj2 to PlanetMath, I decided to make the options like a language, with commands, so that it would be open-ended. The number of RunParm? commands is growing even more now with the Proof Assistant. At the expense of some work I could have made BatchMMJ?2 conform to Unix arguments, but I decided no based on the theory that once a user gets something working, the RunParms? will be stable (after all, inventing a proof can take anywhere from 5 minutes to 5 hours). And, mmj2 is the throwaway model, the one you build to learn so that you can throw it away and do the next one properly.

One touch I did add is that there can be multiple "load,mmfilename" RunParms?. In fact, the RunParm? file is almost like a script except there is no looping and no condition checking beyond "this is messed up, I quit".

After I finish testing Proof Assistant and post it here let's have a serious re-look at the many flaws in mmj2, architecturally and otherwise. That will be very fun!

--ocat

Jars are simply zip files with one special file, the manifest. Inside the "classes" directory, create another directory META-INF, and create a file MANIFEST.MF in it with the following text:

  Manifest-Version: 1.0
  Main-Class: mmj.util.BatchMMJ2

That's how java knows what to run. Then zip the contents of the "classes" directory and rename the zip to jar. That should do the trick, java -jar <file.jar> should work.

I wonder why mmj2 is so big? Are there auto-generated parts? --alih

Thanks for the explantion. Very interesting and helpful!

I am editing my answer as to "Why so big?"

I don't have a short answer to that question :)

mmj2 represents the journey, which I began in near total ignorance of what would be required. I wanted three things: 1) a parser to detect unbalanced parentheses, which the Metamath proof assistant reports as a unification failure; 2) a proof assistant that does not require proofs to be entered in reverse or memorization of statement labels; and 3) a complete understanding of what a Metamath proof proves – is it really real, in other words.

Now that I am this close to having the Proof Assistant I have wanted for more than a year, I plan to use my new mmj2 tools to do proofs and resume my self-education. I would hope that the code could be tightened up enough to distribute along with informational material for self-study in propositional logic, and perhaps the predicate calculus, etc., though I don't know enough about those to write anything – yet. I do want to contribute something before I turn in my lunchpail and sci-fi collection :)

The new mmj2 Proof Assistant is going to be very excellent. Not only will it alleviate much memorization of arbitrary statement labels, but it allows proofs to be entered front-to-back or back-to-front, as desired. And students will be able to use it with Metamath and mmj2's other facilities to create their own .mm languages, for educational purposes. Fun stuff.

Once the Proof Assistant is ready and posted to the web, the lessons learned might be used profitably. Now I know enough about the problem space to actually design a system properly, one with an integral, unified structure, top to bottom. And there is much more that can be done (and should be done?) Whether or not future efforts should be focused on F.O.M. or the native Metamath format is another question. The two primary contenders are Ghilbert and Bourbaki, though that is based on preliminary information and represents my own impressions.

Way back I mentioned to Norm that I believed Metamath to be the perfect project for students of computer sciences. If you look at the Metamath.pdf book and investigate set.mm and ql.mm, perhaps working out the first 100 proofs by hand, you'll see an entire universe of ideas. What Norm has created is amazing, and it is right there for people to take.

--ocat 18-Jan-2006

I see :) Waiting to take a look at your Proof Assistant!

You seem determined that Metamath can be used for educational purposes. I am sceptical here. Metamath is ultimately minimalistic but it's by no means simple. To understand Metamath style of doing metatheorems, one has to understand clearly the semantics of underlying theorems. And the underlying theorems have more structure (bound/free variables) than meta-statements. So Metamath is harder to learn then predicate calculus. And if a person tries to prove something, many additional complications arise like the lack of deduction.

For learning propositional calculus, Metamath is better suited, but it is unable to understand the semantics, for example, to present a counterexample if the user tries to prove a wrong theorem. So again some specialized program might be better here. --alih

Here is an idea about how the axiom system and database can be transformed to address some of this concern. I don't think I'd be doing this myself, but it would not be a difficult project. Mainly I bring it up to describe what can be done in principle.

The fact that free and bound variables needn't always be distinct seems to confuse some people, because they don't grasp the "set metavariable" concept but tend to view the set variables as the actual variables of the theory (which are always distinct by definition).

We can emulate the "actual variable" viewpoint by having $d's associated with all variables in the axioms. In other words, we would revise ("weaken" in a metalogical sense) the axiom system so that all axioms have $d requirements on all set variables. To do this, we would repeat each axiom for each possible substutution instance of set variables, then place all the set variables occurring in that instance into a $d statement. For example, ax-9 would become 2 separate axioms:

  ax-9a    -. A. x -. x = y  where $d x y
  ax-9b    -. A. x -. x = x

This would add about 2 dozen axioms to ax-1 through ax-16. Some would be redundant and provable from the others, and possibly they could be reformalized into a cleaner overall set of axioms.

Similarly, all theorems would be proved with all possible substitution cases, with $d's on all the variables of each case. In principle this could be automated. It would result in larger database of course. I don't think it would be too much larger, perhaps a factor of 2 or 3 in the predicate calculus part and then very little change after that (since most later theorems have $d's on their set variables). A lot of the extra theorems, perhaps most of them, would never be used and could be discarded.

In addition to "simplifying" the metalogic, this would also make the database easier to translate to other proof languages, which most likely wouldn't have set metavariables.

On another issue… The lack of the deduction theorem is a disadvantage, but it is interesting to compare the approach used in calculation proofs (see metamathCalculationalProofs on this wiki), which I think set.mm often tends to use subconsciously. From On Calculation Proofs (.ps): "What we learn from Dijkstra and Scholten is that the importance of assumptions in formal proofs is overrated: with the right choice of inference rule, proving predicate formulas is easy even without introducing assumptions (and without the use of auxiliary derivable objects such as sequents)."

Another opinion, in Structured Calculational Proof (.pdf): "Natural deduction, on the other hand, is well suited to the structured decomposition of proofs. However, natural deduction proofs are seldom as easy to read as calculational ones."

I don't mean to diminish the utility of the deduction theorem for creating proofs. I use it all the time informally when sketching proofs for set.mm, then translating them (usually in my head) to Hilbert-style proofs.

--norm 19-Jan-2006

Forcing $d seems to be a nice trick, but what about definitions? I hope they won't get expanded into multiple variants…

Translation of Metamath into other proof systems sounds cool. Once Ghilbert is up (or probably mmj2 can deliver something Ghilbert-like?), there would be much fun around.

I'm currently planning a NBG-unfriendly version of ufomath, so a question naturally arises: can something be done to get rid of classes? Suppose that we can introduce any iota-definable functions on sets, we can unify free set variables with terms, and we can use separation set builders { x | x e. m /\ ph }. Some NBG theorems like Russell's paradox can't be translated anyway; but how big part of Metamath will be lost in such a way?

--alih

The only definitions that would be affected would be df-sb and df-clab, each of which would be broken into two. All the other definitions have $d's on their set variables, so no splitting would be needed.

Another point: should we require $d's between free variables, in particular on ax-8, ax-13, and ax-14? I would argue that we should if we truly want to emulate the "actual variable" viewpoint, even though textbook systems usually don't do that. Textbooks are sometimes sloppy (or more politely, "hybrid") in this sense: set variables that are bound are always required to be distinct whereas those that are free are not. I think this may cause some confusion among students, since the books may not always obviously distinguish the actual variables vs. metavariables ranging over them. (Carefully written works such as those by Tarski are meticulous about maintaining the distinction.)

In any case I think it would be very interesting to see what the axiom system - when carefully reformalized for elegance and to eliminate redundancies - could look like with the all-$d approach. We might be surprised by its elegance. It would be the exact opposite of the current approach: currently we state as much as it is theoretically possible to state without introducing any $d's, even achieving a complete system in a certain sense, then finally we strengthen the system with the minimal axioms ax-16 and ax-17 needed to add the $ d-ness.  With the alternate approach of all  $d's, it might be interesting to see what minimal additional axioms would be needed to recover the non-$d-ness of the original system. (My guess is that among the axioms needed to recover non-$d-ness we would find ax-10 and the theorem form of dvelim or an equivalent.) This sounds exciting! If only I could clone myself, so much to do… Maybe someone else will catch the bug - which, for non-native-English speakers, means "become inspired to the point of irrational obsession" - and play with this fun puzzle. Mainstream logicians and mathematicians might find such a reformalization more palatable than the existing ax-4 to ax-17, even if the rest of set.mm is untouched (with ax-4 to ax-17 proved as theorems).

As for NBG vs. ZFC, I made some comments on the metamathMathQuestions page under the heading "ZF vs. NBG set theory in set.mm" that may or may not be relevant. In particular, people sometimes confuse the individual variables ranging over classes in NBG (which can be quantified) with the class-term metavariables used in NBG (which, like in ZFC, cannot be quantified), since the word "class" is used for both. But they are different things. Quine's Set Theory and Its Logic is probably the best book to read on this. As for Russell's paradox, I'm not sure what you mean - the theorem ru is exactly the same in ZFC and NBG whether x is a individual set variable (ZFC) or individual class variable (NBG). More generally, when A is a class-term metavariable, A e. V is false in both NBG and ZFC when A is a proper class. One difference is that E. x x = V is true in NBG (x is an individual class variable) and false in ZFC (x is an individual set variable).

--norm 21-Jan-2006

Comment for Alih:

You were right about mmj2 being faster than advertised. I discovered that the BatchMMJ?2 program batch file – distributed – was being executed with the "-xProf" java parm. Ooops. I like the xProf parm, but it appears to consume 67% of run time! The set.mm load process, including proof verification and grammatical parsing looks to be around 10 seconds in mmj2. Thanks for pointing out the discrepancy!

--ocat 29-Jan-2006

There are I think some typos in alih's script, and possibly some discrepancies between his "find" program (presumably GNU find) and mine (BSD find). But I've just tested this with both GNU find and BSD find and it works fine in both cases. So, I propose this as version 2.0 of the build script above.

 #! /bin/sh
 #
 # A script to compile mmj2 under GNU/Linux / Mac OS X / BSD with jdk1.5.
 # Run from the mmj2 top directory.
 # Should produce "mmj2.jar".
 # You can then run "java -jar mmj2.jar"
 #
 echo "Manifest-Version: 1.0" >MANIFEST.MF
 echo "Main-Class: mmj.util.BatchMMJ2" >>MANIFEST.MF
 cd src && javac `find . -name "*.java"` -d ../classes && cd ../classes && \
 jar cfm ../mmj2.jar ../MANIFEST.MF \
 `find . -name "*.class"` | sed -e "s/^\.\///"

However! This hasn't completely solved my problems.

I'm getting compilation errors like

 ./mmj/verify/Grammar.java:200: cannot resolve symbol
 symbol  : class PriorityQueue 
 location: class mmj.verify.Grammar
     private   PriorityQueue derivedRuleQueue;
               ^and subsequent run-time error
 Exception in thread "main" java.lang.NoClassDefFoundError: mmj/util/BatchMMJ2

I assume this means I don't actually have the appropriate Java stuff installed. Its curious, because Apple asserts that OS X "comes complete with a fully configured and ready-to-use Java Development Kit" (http://developer.apple.com/java/). Well… maybe something is lacking. I'll try updating Java, since I see they are offering me a Java update.

Apparently Apple does their own Java distro, because Sun doesn't seem to serve the OS X platform directly (no Mac instructions at http://java.sun.com/j2se/1.5.0/download.jsp).

--jcorneli

Well, thanks for this info! PriorityQueue? was new in the Java SDK 1.5. Let us know if you can make mmj2 happen on the Mac! --ocat

Apparently it should "just work" on 10.4.*, but won't work at all on 10.3.* or before, see e.g. http://forums.macrumors.com/archive/index.php/t-107091.html -- I think this is called "planned obsolescence" and its a good reason to not use proprietary software (especially operating systems, but also programming platforms :(). --jcorneli

Thanks for the corrections! By the way, I think the next version should use an existing (but currently not existing) manifest instead of creating it.

To Norm:

The idea sounds fun now. I hope I had more time…

You're right about Russell's paradox. I meant the following. Consider any wff with class builders; now let's introduce a new set variable m and write {x | ph /\ x e. m} instead of plain {x | ph}. We'll obtain a class-free formula which can be interpreted in terms of sets only. The problem is, the new formula might be false. Sometimes it can be fixed by hand, but I'm afraid that automated translation is not possible here. --alih


Nat.mm in mmj2

Hi ocat. I've been trying to load nat.mm in mmj2 but I don't succeed. Could you give me an adapted nat.mm (and a RunNat?.mm as well).

frl 11-Feb-2006


Hi frl! Here are the goods :)

NatMmInMmj2

RunParmsForNatMmInMmj2

p.s. FYI, to run the Proof Assistant, there must be no loading errors, such as invalid tokens, and the Grammar must be able to syntactically parse every statement. Errors in these areas kick out Java "exceptions" which the BatchMMJ?2 module allows to "manifest" as fatal errors. So when you run the code and the system out/err stream terminates with a Java exception, there will normally be a mmj2 error message embedded. And there will probably be other errors earlier in the print stream. If one runs the .bat file and outputs to the screen in the "Command Window" and the amount of output exceeds the Command Window's buffer then you might not see all of the output (in Windows(tm), right?) So one option is to rerun the .bat file and pipe the output, like this

    runpagui.bat > temp.txt
    

p.p..s. in future, if incomprehensible problems, post error message text and i can have a look…

ocat


oh yeah! My first mmj2 proof.

 $( <MM> <PROOF_ASST> THEOREM=try  LOC_AFTER=?
 
 h1::try.1          # G |- ps
 2:1:ax-we         # [ G , ph ] |- ps
 qed:2:ax-ii        # G |- ( ph -> ps )
 
 $=  cong wph wps cong wps wph try.1 ax-we ax-ii $. 
 $)

Why are the # not in an only row ?

frl 11-Feb-2006


Congratulations!

But I do not comprehend what is the question you ask. Are you asking why does not the screen appear as this:

 $( <MM> <PROOF_ASST> THEOREM=try  LOC_AFTER=?
   
 h1::try.1          # G |- ps
 2:1:ax-we          # [ G , ph ] |- ps
 qed:2:ax-ii        # G |- ( ph -> ps )
     
 $=  cong wph wps cong wps wph try.1 ax-we ax-ii $. 
 $)
    

Or are you asking why "#" does not appear in the "$=" row?

If former, hard to say. The program respects the columns that are input, except when the label generated by Unification requires more room than is available before the start of the formula. I need screenshots before and after Unification to see what you did/are doing.

If latter, the "$=" contains the Metamath RPN proof and can be copied into a .mm file. So the "#" is implied by the type code of ax-ii, which is the final label in the proof (the root of the proof tree.)

--ocat 11-Feb-2006


I've tried again and now the # are correctly put. So I don't know what happened. If you had to characterize the philosophy of your own prover in a few words what would you say ?

frl 11-Feb-2006


Oh, good.

The philosophy of the Proof Assistant GUI? He is an Existentialist :)

My philosophy with respect to the Proof Assistant is that memorizing theorem labels and then entering the proof steps in reverse order is very hard, so it is better to let humans do formulas and make programs search databases for labels and technicalities such as hypothesis sequences.

This is closer to the way people do math. Lots of derived equations scribbled on a blackboard while arms are waved explaining the steps.

The Unification algorithm is a problem in searching for formulas with a certain shape. Very interesting problem that requires the existence of a parse tree for each formula. So, back when I started, my decision to do parsing before proof assistant was a lucky choice!

Note: the "prover" is the same as Norm's (and Raph's) prover, with optimizations for batch processing in Java using fixed arrays of massive size.

P.S. I am gratified that you were able to prove a theorem. I hope for your success in your investigations and that the mmj2 Proof Assistant may be an aid. I think you have helped me understand more about it. TWO more releases will be necessary in order for it to be a "popular" program.

P.P.S. I will probably move this later discussion to the GUI feedback page, fyi. --ocat


Here is a new natural deduction proof.

 $( <MM> <PROOF_ASST> THEOREM=eqcoms  LOC_AFTER=?
 h1::eqcoms.1       # [ G , A == B ] |- ph
 h2::eqcoms.2       # bound x A
 h3::eqcoms.3       # bound x B
 4:2,3:eqcom            # [ G , B == A ] |- ( A == B <-> B == A )
 5::ax-hyp              # [ G , B == A ] |- B == A
 6:4,5:rembi2         # [ G , B == A ] |- A == B
 7:1:ax-ii              # G |- ( A == B -> ph )
 8:7:ax-we            # [ G , B == A ] |- ( A == B -> ph )
 qed:6,8:ax-ie      # [ G , B == A ] |- ph 
 $=  cong cB cA wceq conr cA cB wceq wph cong cB cA wceq conr cA cB wceq cB cA 
     wceq cong cB cA wceq conr sx cA cB eqcoms.2 eqcoms.3 eqcom cong cB cA wceq 
     ax-hyp rembi2 cong cA cB wceq wph wi cB cA wceq cong cA cB wceq wph eqcoms.1 
     ax-ii ax-we ax-ie $. 
 $)

#1 When designing the proof, I had to renumber the steps several times. It can be boring.

It is not necessary that proof steps have sequential, ascending step numbers. I.E. 3…1…983…4…qed is ok. --ocat

#2 It is perfectly impossible to prove `dummylink' in mmj2.

see comments below

#3 In this proof hypotheses about dummy variables are necessary. But I had read that you, Raph Levien and Norman Megill had thought about the possibility of removing hypotheses concerning dummy variables.

I assume you are talking about $d's for dummy variables. Nothing was officially decided by those discussions. At this point they are required to be made explicit by the official Metamath spec, and that is the safest assumption to make. They are optional in Marnix's Hmm, but not in Metamath, mmj2, and mmverify.py. --norm
Not only. In your system, there is only one proviso: the d statements. The fact is that, in my opinion, having hypotheses concerning dummy variables is just like having a function with local variables declared as parameters. In a certain way it seems not appropriate. --frl
My (weak) argument for keeping them is that if they are implicit, it is "one more thing" for a new user to learn, so that it may be complicating the language conceptually. But I am leaning in that direction, and at some point in the future I may change the spec to make them optional. Of course, all the programs would have to be changed accordingly. Since they would be optional, existing databases would not be affected. So no matter what happens, if you put them in your database, even though it might be a nuisance, you will be safe. They are easier to put in if you use a script to identify them, as described under "Metamath tips and techniques: creating $d statements" on the metamathMathQuestions page. --norm
It is true that the beautifully economical metamath framework will be less economical. And perhaps the economical point of view is the most important feature in metamath. --frl

frl 12-Feb-2006


frl, good catch on "dummylink"! With dummylink as the first assertion in a .mm file, the Proof Assistant GUI will not complete unification for the qed step. I tried the experiment myself, with dummylink located prior to ax-1. Does not work! This is interesting because the metamath.exe proof verification engine accepts the 1 label RPN proof "dummylink.1".

However, by moving dummylink to the spot immediately after ax-mp I was able to produce this proof:

    $( <MM> <PROOF_ASST> THEOREM=dummylink  LOC_AFTER=?
        
    h1::dummylink.1    |- ph 
    h2::dummylink.2    |- ps 
    3::ax-1            |- ( ph -> ( ph -> ph ) )
    4:1,3:ax-mp        |- ( ph -> ph )
    qed:1,4:ax-mp      |- ph 
        
    $=  wph wph dummylink.1 wph wph wph wi dummylink.1 wph wph ax-1 ax-mp ax-mp $.
    
    $)
    

Convoluted, but justified by the axioms in the set.mm file!

Oh Jesus! I meant the normal sort of proof a middle-aged man without problem with the police can hope :)
I love the French police :)
Really ? You know them ?
My humor is untranslatable, even into American, I think :) What I know of the French police is that they are far away :)

Metalogically, when we look at dummylink, we see that dummylink.1, "|- ph", justifies the conclusion, "|- ph". This reasoning is obvious: if a thing is true then it is true! In my favorite book on logic, "Symbolic Logic – An Introduction" by Richmond H. Thomason, natural deduction techniques are covered at length: Reiteration, Implication Introduction, Implication Elimination, etc. And Reiteration ("reit") is precisely what Thomason would use to justify the 'qed' step of dummylink. But if dummylink precedes all axioms in the input Metamath file, then is it surprising that the poor Proof Assistant GUI finds no justification for dummylink's qed step?

Metalogically (if I use the term correctly here), I say that the Proof Assistant GUI is on solid territory in refusing to prove dummylink when it is located prior to every axiom in a .mm file.

But I can't really understand why technically speaking mmj2 refuses to make this proof because conceptually speaking this sort of proof is correct in all the inference systems I have seen described up to now.
Technically speaking the reason is that the PA GUI explicitly checks to see that each Ref is an assertion (axiom or theorem), and when it is searching for unifying assertions the list it checks contains only assertions. Technically speaking, it could build in Reiteration as a valid deduction. Or we could just add ax-0 and make it explicit, in which case the PA GUI would find ax-0 as the unifying Ref for the dummylink qed step. I also note that Reiteration is Axiom "I" of Sequent Calculus ( http://en.wikipedia.org/wiki/Sequent_calculus ) --ocat
Oh! A vey important axiom indeed. In nat.mm it is called ax-hyp. It is the only axiom of a natural deduction system (if we only consider propositional + predicate calculus). A natural deduction system has many inferences and only one axiom.

--

In fact, there are other Metamath proofs that the Proof Assistant cannot replicate. For example, miu.mm has statements that do not parse without syntax axiom "wxy $ a wff x y  $.", and yet the Metamath.exe proof verifier has no problem. In this case the Proof Assistant will not even get started because a precondition for running the PA GUI is that every statement is parseable.

P.S. The fact that a theorem can be proven using the Metamath Proof Verification Engine and zero axioms is a clue :) What I deduce from this clue is that the Axiom of Reiteration is built in! We might as well call it ax-0 and say that Metamath is not 100% logic agnostic.

--ocat

"dummylink" is not a theorem in the strict formal sense. In a Hilbert-style system - for which Metamath was designed - a "theorem" is defined as the final step in a sequence of steps, each of which is an axiom instance or the result of an inference rule (ax-mp, ax-gen) applied to earlier steps. Anything else is a metalogical device, or shortcut, to help us prove things more efficiently. One such shortcut is the ability to reference earlier theorems, not just axioms. Another shortcut is the ability to prove statements that have hypotheses, that strictly speaking we should call "deductions" or "inferences" rather than "theorems". Both of these shortcuts are conservative extensions of the logic of any Hilbert style system, no matter how weak: they are eliminable and have no effect on what actual theorems are provable, except that the proofs would be much longer. In particular, if we have no axioms - which is the weakest possible logical system - then we cannot prove any theorems (in the strict formal sense). In this sense, Metamath is indeed 100% logically agnostic.
.
Perhaps dummylink could be considered to be analogous to say arithmetic done with preprocessor directives in C - no actual code is generated from that arithmetic, just as no actual math content exists in dummylink. We could go further with this analogy. A derived inference can be considered to contain math content in the same way that a preprocessor definition (to which a C code snippet is assigned) can be considered to contain real code. The derived inference isn't true math content in the formal sense until it is used as part of an actual theorem's proof. Similarly, the preprocessor code snippet is not by itself real code - it has no effect, and may as well not exist, until it is referenced in the actual code. Informally, of course, we treat both as if they are the real thing.
.
For sequent calculus, it isn't correct to say that axiom "I" (Reiteration) is equivalent to dummylink. Do not confuse Metamath hypotheses with the hypothesis list of a Gentzen sequent. The latter accompanies the conclusion in the same sequent symbol string, separated by "|-". If you look at the sequent inference rules on the Wikipedia page, the Metamath hypotheses correspond to the the starting sequents on top of the solid line in the various rules. One very obvious difference between a starting sequent and a sequent hypothesis, for example, is that you can eliminate the latter with the standard deduction theorem (Rule → R) but not the former. That page doesn't define "theorem", but the definition of a formal proof doesn't include starting sequents like the inference rules do. --norm 13-Feb-2006
From what you are saying, it appears that the mmj2 Proof Assistant GUI is being rather strict and dogmatic – a purist :) I do not see a significant reason to change it, but will need to do CYA documentation. I found some information to study that directly relates to what you are saying about "Hilbert style" systems (and more). It is a draft of an article written by authors Herre and Schroeder-Heister that (later) appeared in the Routledge Encyclopedia of Philosophy): Formal Languages And Systems. --ocat 13-Feb-2006

Removing useless #

Hi ocat. I'd like to remove the # in the `bound' statements. For instance eqcoms quoted above would look like this afterwards.

 $( <MM> <PROOF_ASST> THEOREM=eqcoms  LOC_AFTER=?
 h1::eqcoms.1       # [ G , A == B ] |- ph
 h2::eqcoms.2       bound x A
 h3::eqcoms.3       bound x B
 4:2,3:eqcom            # [ G , B == A ] |- ( A == B <-> B == A )
 5::ax-hyp              # [ G , B == A ] |- B == A
 6:4,5:rembi2         # [ G , B == A ] |- A == B
 7:1:ax-ii              # G |- ( A == B -> ph )
 8:7:ax-we            # [ G , B == A ] |- ( A == B -> ph )
 qed:6,8:ax-ie      # [ G , B == A ] |- ph 
 $=  cong cB cA wceq conr cA cB wceq wph cong cB cA wceq conr cA cB wceq cB cA 
     wceq cong cB cA wceq conr sx cA cB eqcoms.2 eqcoms.3 eqcom cong cB cA wceq 
     ax-hyp rembi2 cong cA cB wceq wph wi cB cA wceq cong cA cB wceq wph eqcoms.1 
     ax-ii ax-we ax-ie $. 
 $)

Would it change anything concerning the axioms you added to nat.mm. frl 18-Feb-2206

Hi frl, you can experiment and see what error messages result :) There are issues.

1) Metamath requires each $ a,  $e, $ f and  $p statement to begin with a constant. The constant is semantically = the Type Code of the statement, which in set.mm is either "set", "class", "wff" or :|-";

2) the statements in logic – logical axioms and theorems -- begin with "|-" in set.mm and must be derived from other "|-" hypotheses, axioms and theorems. So essentially what your change is doing is either a) downgrading the "bound" statements to the level of "set", "class" or "wff", which makes them ineligible for use as logical hypotheses in proofs; or b) kicking them outside the proof derivation process to go live with $d statements, which serve as additional constraints on generated proofs – but since the Metamath Proof Engine does not have any knowledge of "bound" the way it does "$d", there is no support for this alternative.

mmj2 follows Metamath in these regards but imposes additional constraints on input:

1) every $ a,  $e and $p statement must be parseable using the input Syntax Axioms ($a statements with initial constant != the designated Provable Logic Statement Type (which is "|-" in set.mm))

and 2) There can be only one designated Provable Logic Statment Type ("|-"), along with a single designated Logic Statement(formula) Type ("wff"). #2 provides the grammatical parser a Start Type, which is "|-", so that it knows that a $ a,  $e or $p statement with Type Code "|-" must have a formula that parses to a tree whose root node has Type Code = "wff".

The alternative to all of this is using Norm's "distinctors", or using $d's, or perhaps even cloning Metamath's code and adding support in Proof Verification for the bound/free constraints (but I have no idea how feasible/logical/useful) that would be and how it relates to Norm's initial decisions not to support bound/free.)

#1 According to me using the $d proviso with natural deduction is masochistic because you very often meet a $ d x G  $. which means that no wff in your context can have a x (which rarely occurs). #2 Except this masochistic effect, I think we can describe a natural deduction system with a $d proviso. However we will have to add most of the axioms of set.mm to make it work. And the system of axioms will be therefore far from a `norma' natural deduction system. #3 I think these two points lead to the conclusion we must add `bound x ph' provisos. The consequence is that the system is not as beautifully concise as in set.mm. The properties about binding are not infered but are added as a system of axioms. In a certain way it's pityfull because set.mm learns me a lot about the real nature of binding (namely that they are wff like the others even if in textbook description they seem black magic needed textual notes to be managed.) But there is always the possibility to refer to set.mm to understand what they are exactly.
Should binding be embedded in the heart of metamath ? I think not. I think it's more interesting to see that binding is just a logical property like the others. And in fact it's rarely very difficult to prove that a variable is bound in a wff. --frl
I seem to recall "free" and "bound" being syntactic and being built-up recursively according to a set of rules, like wffs. Perhaps some insight will magically appear in your brain. --ocat
Well in fact that's exactly the way "bound" is managed in nat.mm, recursively and much like the wff nature of a formula is checked. – frl
frl, I like you. You are dogged about this and determined! I guess what needs to happen is a full-on analysis of what is needed and why, and how that relates to Metamath's Proof Engine. We need a keen, focused-like-a-laser review starting from first principles that rips apart terminology and all the fancy words. So disregard everything but the Truth, Necessity and Satisfaction and get to the bottom of this. Shovel away the merde, and take it down to the bare metal. Use any means necessary. Then report back here :) --ocat

--ocat 18-Feb-2006


Compressed proofs

Have you ever had a customer require you to program something that you consider so ugly and so wrong that it grates you the wrong way and makes you want to scream, especially after they've rejected your carefully and logically explained correct way of doing it? For example, they may want to bastardize a standard communications protocol or file format with some ill-conceived extension, making it incompatible with everything else, when the existing standard is perfectly suited to the task if used in the right way. But you must acquiesce since they are the customer, and the customer is always right. In the meantime, the stress of forcing yourself against your will to program something that is so distasteful and just plain wrong, if not immoral, has probably reduced your life expectancy by several years.

I know, O'Cat, how much you abhor compressed proofs. The purity and simplicity of standard RPN proofs is such that if you beamed the uncompressed set.mm into outer space, probably an alien race could not only figure it out but could use it as a Rosetta stone, via the comments, to decipher other math works and eventually bootstrap their way up to the whole of the English language itself, as they successively apply their knowledge to works that are more and more informal. Whereas if they intercepted a compressed set.mm, this knowledge might be locked away from them for millenia if not forever.

Here is my problem. When I work with set.mm, I typically will use a text editor to scan around the area of interest to see where it might be best to place a new theorem, and also to see what related things exist.

Now, propositional calculus proofs are relatively short, and it doesn't make a whole lot of difference for text editing purposes whether they are compressed or uncompressed. But as you know, I spend a lot of time in some of the more bleeding edge areas of set.mm, where proofs are often very long. For example: projlem7 has a 30-line compressed proof, but a 660-line uncompressed proof. That means you have to scroll through pages and pages of stuff to get to the next theorem, and if you scroll too fast you might miss it. OK, you could search for the next $p instead of scrolling, but the point is that everything just becomes more clumsy and inefficient. This is the very reason I added the compressed proof alternative.

The compressed proof format is not some obscure cryptographic compression method, but is very simple and closely tied to the RPN proof. So closely, in fact, that the Metamath program verifies proofs directly from the compressed proof for higher speed, without bothering to translate it. On my computer, 'verify proof *' takes 3.5s for the compressed set.mm and 15.9s for the uncompressed.

In marnix's 440-line Hmm proof verifier, the compressed proof code (located in HmmImpl.hs) is 80 lines long. The compressed proof format is precisely documented in Appendix B of the Metamath book, from which Marnix wrote his verifier. He provided me with this helpful outline of his nice algorithm, which I have now incorporated into the Metamath program also:

  A..T stand for 1..20 in base 20, and U..Y stand for 1..5 in base 5. (So
  not 0..19 and 0..4.)  This is when counting A=1, etc., as in the book;
  which seems most natural for this encoding.  Then decoding can be done
  as follows:
   * n := 0
   * for each character c:
      * if c in ['U'..'Y']: n := n * 5 + (c - 'U' + 1)
      * if c in ['A'..'T']: n := n * 20 + (c - 'A' + 1)
  For encoding we'd get (starting with n, counting from 1):
   * start with the empty string
   * prepend (n-1) mod 20 + 1 as character using 1->'A' .. 20->'T'
   * n := (n-1) div 20
   * while n > 0:
      * prepend (n-1) mod 5 + 1 as character using 1->'U' .. 5->'Y'
      * n := (n-1) div 5

An objection to the compressed proof format has been, why have yet another compression algorithm when gzip, etc. are already available? Well, if you use gzip to compress a compressed-proof set.mm, the resulting file is 25% smaller (4.6MB → 1.5MB) than using gzip to compress an uncompressed-proof set.mm (14.2MB → 2MB).

So, I would like to put in an official request to add compressed proofs to the to-do list for mmj2. Encoding them is not too important, but decoding them (the easier part) would make life a little more pleasant, not having to recreate expset.mm all the time and so on. I'm not asking for any particular delivery schedule, but just that you open your mind to the possibility. :) Thanks! --norm 12-Mar-06

I would be honored to attempt to perform that task for you. I am also planning to attempt undo/redo, which you mentioned previously. --ocat 12-Mar-2006

Perhaps a bug in mmj2

In step 61 ( E. n e. om ( A \ U_ y e. u y ) is identified with E. n e. om ( A \ U_ y e. u x ) ~~ n in step 51. It shoudln't ?

mmj2 bug

Hi, did you apply the patch for the earlier bug reported by you???

mmj2PATCH20060725 ???

I am now – after a recompile with the patch – getting the following (correct) error message with "sylibd" on step 61:

    E-PA-0410 Theorem fctop Step 61: Unification failure in derivation    
    proof step.sylibd. The step's formula and/or its hypotheses could not
    be reconciled with the referenced Assertion. A list of unifying 
    assertion alternates (if any) will be presented in a subsequent
    message.
    

It appears that with the patch the code is working – now -- the way it should, and is finding the x vs. y unification error.

--ocat

Not yet (I had read it dealt with blank input formula and I had concluded it was a minor fix: I was wrong) but I will. Thank you. frl