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.
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.)
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 ) ) $)
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 $. $)
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 $. $)
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 $. $)
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 $. $)
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 $. $)
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.