HomePage RecentChanges

mmj2ProofDerivationMethods

Regrettably, the new mmj2 Step Selector Search feature is not a magical cure for every proof derivation attempt.

I find the proof of pm2.61 difficult, and mmj2 is not very helpful! In desperation I pulled out the old fashioned method of Fitch's Subordinated Derivations to see just how hard it would be to work out pm2.61 by hand. Once I abandoned pen and paper and turned to my text editor I was able to crank this out pretty fast (below). I think I did it correctly, but I don't see how to turn it into a Metamath proof! I've used the Fitch method before and been able to translate into Metamath, but this one is stumping me.

pm2.61 |- ( ( ph -> ps ) -> ( ( -. ph -> ps ) -> ps ) )

     1  |   | ph -> ps                                  * hyp int
     2  |   --
     3  |   |   | -. ph -> ps                           * hyp int
     4  |   |   --
     5  |   |   |   | -. ps                             * hyp int
     6  |   |   |   --   
     7  |   |   |   |   | -. ph                         * hyp int
     8  |   |   |   |   --
     9  |   |   |   |   | -. ph -> ps                   * 3 reit
    10  |   |   |   |   | ps                            * 7,9 mp
    11  |   |   |   |   | -. ps                         * 5 reit
    12  |   |   |   | -. -. ph                          * 7->11 neg int
    13  |   |   |   | ph                                * 13 neg elim
    14  |   |   |   | ph -> ps                          * 1 reit
    15  |   |   |   | ps                                * 13,14 mp
    16  |   |   | -. -. ps                              * 5->15 neg int
    17  |   |   | ps                                    * 16 neg elim
    18  |   | ( -. ph -> ps ) -> ps                     * 3,17 imp int
    19  | ( ph -> ps ) -> ( ( -. ph -> ps ) -> ps )     * 1,18 imp int
             

Any ideas?


Each hypothesis in this proof can be instantiated to form a stand-alone theorem, such as ( ph → ph ) for the first hypothesis, which means that in principle the propositional calculus version of the weak deduction theorem dedt / elimh can be used. See the Deduction Theorem page. In practice this would lead to a long proof (as the con3th example shows, compared to the manually-created proof con3).

Alternately, the algorithm for the standard deduction theorem, e.g. as described in Margaris, could be applied. That would lead to an even longer proof, possibly even several thousand steps in this case, since the proof length grows exponentially as hypotheses are popped. See the paragraph I wrote starting with "I worked this out" on WhyAreMetamathProofsSoShort for an illustration of the exponential behavior.

Another approach is to forget about trying to translate the deduction but instead write down the truth table for the tautology, then apply the algorithm of the completeness theorem (also described in Margaris). I actually did this a long time ago for the proof of theorem meredith, using a program I wrote to implement the algorithm, after being completely stumped on how to even begin to approach such a nonintuitive and cryptic theorem. Over time I found shorter and shorter versions of various pieces of it, until it evolved into the proof that's there now.

Also, there are proofs generated by resolution-based provers. While the resolution algorithm is clever and finds predicate calculus proofs that other automated methods cannot, they are in essence proofs by contradiction, which I often find to be less intuitive than direct proofs.

Anyway, those are possible general approaches to the problem that are guaranteed to work (since propositional calculus is decidable). As for specific clever ideas for translating this particular deduction efficiently, I'll defer that to someone who is clever. :) – norm


I find your approaches deeply interesting. The fact that Hilbert-style proofs and the "natural" approach embodied in Fitch's Subordinated Derivations are so profoundly different and yet reasonable, is fascinating to me. I wonder if there is a way to write a Proof Assistant based on Fitch which can interface back to the mmj2 Proof Assistant and create a proof (and maybe if the algorithm encounters problems then that would signify the need to add theorems/ inferences to set.mm.)

You may want to check out Lifschitz's On Calculational Proofs (PS file). The idea is that with appropriate inference rules, Hilbert-style proofs are not necessarily inefficient compared natural deduction proofs. This is what set.mm essentially does. There is also some related discussion in metamathCalculationalProofs and WhyAreMetamathProofsSoShort. I do think with the right inference rules a reasonable natural deduction "translator" could be made. By "reasonable" I mean generates proofs that are not in general astronomically sized. Such proofs could then be used as a starting point to shorten by hand.

Anyway…the Step Selector Search proved its worth this morning!

OK, once I looked at this differently, as an inference --

    h1 |- ( ph -> ps )
    h2 |- ( -. ph -> ps )
    qed |- ps
    

And after another look at the set.mm proof of pm2.61, I added a dummy proof step to the Proof Worksheet:

    10:? |- ( ( ph -> ps ) -> ( ( -. ph -> ps ) -> &W1 ) )
    

and pressed Ctrl-8 to initiate the Step Selector Search. The Step Selector Dialog showed me that using pm2.37 instead of the existing set.mm proof's pm2.36 would eliminate an extra two Derivation Steps! So here is the new shortened proof of pm2.61:

    $( <MM> <PROOF_ASST> THEOREM=pm2.61  LOC_AFTER=?
    1::pm2.37          |- ( ( ph -> ps ) ->
                            ( ( -. ph -> ps ) -> ( -. ps -> ps ) ) )
    2::pm2.18          |- ( ( -. ps -> ps ) -> ps )
    qed:1,2:syl6       |- ( ( ph -> ps ) ->
                            ( ( -. ph -> ps ) -> ps ) )
    $)

shorter proof of ja

I set the 'qed' step Hyp to "1,?", like this:

    qed:1,?        |- ( ( ph -> ps ) -> ch )
    

and pressed Ctrl-8 to initiate the Step Selector Search. It showed that pm2.61d1 would yield the 'qed' step with additional hypothesis:

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

This hypothesis is easily derived from hypothesis 2, so I double-clicked pm2.61d1 on the Step Selector Dialog screen to accept the Ref and unify. The proof easily followed:

    $( <MM> <PROOF_ASST> THEOREM=ja  LOC_AFTER=?
    h1::ja.1           |- ( -. ph -> ch )
    h2::ja.2           |- ( ps -> ch )
    3:2:imim2i         |- ( ( ph -> ps ) -> ( ph -> ch ) )
    qed:3,1:pm2.61d1    
                       |- ( ( ph -> ps ) -> ch )
    $=  wph wps wi wph wch wps wch wph ja.2 imim2i ja.1 pm2.61d1 $. 
    $)
    

syld shorter proof

This one is just obvious…

Requires moving mpd ahead of syld.

    $( <MM> <PROOF_ASST> THEOREM=syld  LOC_AFTER=?
    
    * Syllogism deduction.  (The proof was shortened by Mel L. O'Cat,
      7-Aug-2004.)
    
    h1::syld.1         |- ( ph -> ( ps -> ch ) )
    h2::syld.2         |- ( ph -> ( ch -> th ) )
    3:2:imim2d         |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )
    qed:1,3:mpd        |- ( ph -> ( ps -> th ) )
    
    $=  wph wps wch wi wps wth wi syld.1 wph wch wth wps syld.2 imim2d 
        mpd $. 
    $)
    

hbimd -- A challenge

existing proof of hbimd – This proof is masterful and clever. I find it difficult to accept that there is no "better" and shorter proof. If that is true, then given hbimd's location within the first 5% of set.mm, then the difficulty level increases exponentially – and if that is true then the world has greatly underestimated the value of the content of Metamath and set.mm (to say nothing of ql.mm).

Shorter and/or "better" (more direct and elegant) proof of hbimd, anyone?

--ocat 1-Mar-2008

Here is the "skeleton" of the might hbimd:

    $( <MM> <PROOF_ASST> THEOREM=hbimd  LOC_AFTER=?
    
    * Deduction form of bound-variable hypothesis builder ~ hbim .
    
    h1::hbimd.1        |- ( ph -> A. x ph )
    h2::hbimd.2        |- ( ph -> ( ps -> A. x ps ) )
    h3::hbimd.3        |- ( ph -> ( ch -> A. x ch ) )
    
    qed:?              |- ( ph -> ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
    $)
    

And deep thought hath availeth me naught. So… what about without the "ph", which is a bit of a red herring in this mystery story? Can we do this? Or why not? If so, does it help?

There is such a critter already in set.mm, called "hbim". Curiously, it uses hbimd in its own proof. Here is a shorter proof of hbim which steals hbimd's trick with ja for its own use – and which does not use hbimd, thus enabling the shift down in set.mm of hbimd to where it is actually needed.

    $( <MM> <PROOF_ASST> THEOREM=hbim  LOC_AFTER=?
     
    * If ` x ` is not free in ` ph ` and ` ps ` , it is not free in
      ` ( ph -> ps ) ` .
     
    h1::hb.1           |- ( ph -> A. x ph )
    h2::hb.2           |- ( ps -> A. x ps )
    3:1:hbne           |- ( -. ph -> A. x -. ph )
    4::pm2.21          |- ( -. ph -> ( ph -> ps ) )
    5:3,4:19.21ai      |- ( -. ph -> A. x ( ph -> ps ) )
    6::ax-1            |- ( ps -> ( ph -> ps ) )
    7:2,6:19.21ai      |- ( ps -> A. x ( ph -> ps ) )
    qed:5,7:ja         |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
     
    $=  wph wps wph wps wi vx wal wph wn wph wps wi vx wph vx hb.1 hbne 
        wph wps pm2.21 19.21ai wps wph wps wi vx hb.2 wps wph ax-1 19.21ai 
        ja $. 
    $)
     

Even shorter proof of 19.20

Requires moving 19.20i and friend 19.20ii ahead of 19.20 (they don't depend on 19.20.)

NOTE: I used RunParm?.txt command "LoadEndpointStmtLabel?,wsbc" to dramatically reduce startup time because I am working on the theorems before wsbc (about 1.1 sec on iMac).

    $( <MM> <PROOF_ASST> THEOREM=19.20  LOC_AFTER=?
     
    1::id              |- ( ( ph -> ps ) -> ( ph -> ps ) )
    2:1:a4sd           |- ( ( ph -> ps ) -> ( A. x ph -> ps ) )
    3:2:19.20i         |- ( A. x ( ph -> ps ) -> A. x ( A. x ph -> ps ) )
    4::ax-5            |- ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) )
    qed:3,4:syl        |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
     
    * OLD $=  wph wps wi vx wal wph vx wal wps wi vx wal wph vx wal wps vx wal 
        wi wph wps wi wph vx wal wps wi vx wph wps wi vx wal wph wps wph vx
        wal wph wps wi vx ax-4 wph vx ax-4 syl5 a5i wph wps vx ax-5 syl 
        $. 
    $=  wph wps wi vx wal wph vx wal wps wi vx wal wph vx wal wps vx wal 
        wi wph wps wi wph vx wal wps wi vx wph wps wi wph wps vx wph wps wi
        id a4sd 19.20i wph wps vx ax-5 syl $. 
    $)
     

19.2 in most general form

I came across this, which I am calling 19.2y, after independently reinventing 19.8a :-)

We could really just change 19.2 as everything, including the proof is the same except that we use y for x in one spot.

I think this is a more interesting form of 19.2 because it helps to illustrate the mysteries of metavariables.

    $( <MM> <PROOF_ASST> THEOREM=19.2y  LOC_AFTER=?
     
    * Theorem 19.2 of [Margaris] p. 89., in most general form
     
    1::19.8a           |- ( ph -> E. y ph )
    qed:1:a4s          |- ( A. x ph -> E. y ph )
     
    $=  wph wph vy wex vx wph vy 19.8a a4s $. 
    $)
     

More of Mel L. O'Cat's Pioneering Proof-Shortening Techniques :-)

re: ( 1 + 1 ) = 2

Proof-shortening is not only a fun hobby, it is a worthwhile pasttime for students of Metamath. Shortening existing proofs in say, set.mm, requires the student to review and re-think existing theorems. The goal forces this, and the hair-pulling frustration is also a powerful motivator (IMO suffering is a precondition of progress.) Also, optimizing set.mm is interesting in its own right because shorter proofs tend to represent "clarity of thought"; though often they just seem tricky, the shorter proof derivation techniques are idiomatic artifacts of the user's system and are potentially reuseable.

1) When re-proving, say, theorem "xyz", it may be helpful to prove a clone of the theorem – "xyzTEMP", plus renames of any hypotheses. Leave the LOC_AFTER field blank on the mmj2 Proof Assistant GUI to instruct mmj2 to treat the clone as an addition at the end of set.mm, and thus allows for theorems occurring after "xyz" to be used in unification. Because set.mm is arranged linearly but is actually a two-dimensional tree of derivations, in some cases a useful theorem can be moved toward the beginning and used in re-proving an existing theorem.

2) One annoyance in the mmj2 Proof Assistant GUI is that Unification Search, which inserts unifying assertion label in proof steps, is not performed for steps which contain Work Variables (or "?" in the Hyp). The reason is that Unification Searches involving Work Variables and missing hypotheses can return many answers, and furthermore, the answers interact with other proof steps. Unification Searching with Work Variables amounts to solving a 3-D system of equations, in the most general case. In specific instances the user knows that there is only one correct answer but the program is not gifted with the intelligence to know that.

To get around this "problem" use the Step Selector Search (Ctrl-8 or double-click proof step) to display the Step Selector Results dialog page and then select the appropriate assertion. This will probably be faster and easier than manually updating the proof step formula to eliminate the Work Variables.