On 22 Jul 2012, at 10:39, Bill Richter wrote: > https://dl.dropbox.com/u/34693999/nonobv.pdf > > Congratulations, Rob,
Thank you! > I had no idea how to prove Los's non-obvious theorem until I read your > solution. I'm not quite satisfied with your exposition, though, and here's > a miz3 version of your proof not using your extension P', reflexivity, domain > P or range P I was using these things because it is typical of how things look in standard textbook mathematics. > (isn't dom = ran anyway?). Yes, but as I had set myself a rigid limit of 1 page, I didn't have room for that particular digression (while I did want to give the right general formula for the field of the relation). > The key is my `a_works', which I learned from your proof. > I relaxed my page limit to 2 pages, and added two more proofs to https://dl.dropbox.com/u/34693999/nonobv.pdf. The new proofs are the simple direct and "fairly mindless" one that I referred to in my previous post and one involving a bit of baby model theory to explain why the mindless approach is guaranteed to work, because from the form of the problem one can see that if the theorem were false, there would be a counter-example with at most 4 elements. Your neat proof with a_works implicitly exploits a bit more of the details to reduce to a 3-element counter-example. (When it works, I am actually quite a fan of the device of using counter-example generators like Mace as theorem-provers as it gives a very nice separation of concerns: the human worries about the reduction of infinite problems to finite ones and the machine then worries about the finite problems). 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
