Bill, On 29 Jul 2012, at 07:28, Bill Richter wrote:
> https://dl.dropbox.com/u/34693999/nonobv.pdf > > Rob, I like your 2nd proof (although I think your 4 cases are about P and not > P, instead of P and Q), My argument does work exactly as stated, but I agree that it is simpler to avoid having overlapping cases by doing the case analysis as you suggest. Thanks for the improvement, which I have adopted in the write-up. > and it got me thinking, and I now have some understanding of Los's Logic > problem. The problem with Los's result is it makes no sense: P is symmetric > and transitive, Q is transitive, P or Q is true, show either all P or all Q. > Our reaction is What is going on??? That's why it's so impressive you solved > it. But I made some progress understanding it: > > The result is almost about entirely about P, with Q almost being ~P. So > let's prove the case special case Q = ~P first. That turns out to have a > comprehensible proof! Then we just have to fiddle with the proof a bit to > handle the general case. Below is my miz3 proof of Los's Logic result, to a > large extent a modification of your 2nd proof. I am not quite sure exactly what you were trying to achieve here. I would have hoped that miz3 would be able to express my 2nd proof as it stands. Not knowing miz3, I have done the next best things with the tools I do know and done a ProofPower transcription of my 2nd proof with your improvement in a "quasi-declarative" style. See: https://dl.dropbox.com/u/34693999/los-non-obv-proof.pdf I am guessing that you didn't really want to express my 2nd proof as is, but were after a comprehensible proof expressed in miz3. I think one needs to have a comprehensible proof in mind to achieve that and I don't quite see one following your approach. My proof 1 at least has a comprehensible proof strategy, and that may be the best you can hope for. Did you not find proof 1 comprehensible? Regards, Rob. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
