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