the intuition is just in a little diagram with 4 points and lots of edges labelled P and Q.
Thanks, Rob, and I think I understand now! You solved Los's Logic problem because you had the courage to try a bold frontal attack, while I floundered for the lack of some cool insight. This is an important point, as we're interested in how smart MESON is. Here's how I think your bold frontal attack must have gone. Let's change the symbols P & Q to ~ and <. So we know that ~ is symmetric and transitive (~symm, ~trans) < is transitive (<trans) forall x y. x ~ y or x < y (~union<) We're trying to prove (forall x y. x ~ y) or (forall x y. x < y) So we have to negate one of these two and prove the other. You got both proofs to work, I believe, so let's negate the ~ one. So we'll assume that there exists a b such that a !~ b (i.e. a !~ b is false). We must prove forall x y. x < y. So choose x y, and let's take diagrams of involving the points a, b, x & y for both ~ and <. We'll have an arrow from one point to another if there's a relation. With 4 points, there are 4^4 = 256 possible diagrams for each relation, and so 256^2 = 65536 total possibilities. We don't want to look at all 65,536! Of course we know that a !~ b by assumption b !~ a by ~symm a < b and b < a by ~union<. So in each diagram there are really only 3*3*4*4 = 144 possibilities, so we have 20,736 total possibilities. That's still way too many. I've drawn two diagrams with 4 points in each, connected by 6 lines. In the < picture I have 2 arrowheads to indicate arrows a -> b and b -> a. In the ~ picture I have 2 little x's marked in to indicate there is no arrow from a -> b or b -> a. OK, staring at the two diagrams I see nothing, so I'll look at two triangles instead, with 3 points a, b & x. I count a mere 144 = (2*2*3)^2 possibilities for the two diagrams. I don't want to check them all, though. I think it's quite possible that our bold explorer would then bifurcate on the question of a ~ x. Let's look at the two cases: a ~ x by assumption x ~ a by ~symm b !~ x and x !~ b by ~symm, ~trans, since a !~ b and b !~ a b < x and x < b by ~union< a < x and x < a by <trans, since a < b and b < a. Let's look at the other case: a !~ x by assumption x !~ a by ~symm a < x and x < a by ~union< b < x and x < b by <trans, since a < b and b < a. Whuddya know! We got the same result both ways! Thus we've proved that Lemma: forall x. a < x and x < a and b < x and x < b I think that's easier to see if you draw the 4 triangles. Now it's all downhill. Choose x and y. Then a < b and b < a by assumption x < a and a < y by Lemma x < y by <trans QED I think I showed that what MESON proved, a bold explorer could have replicated without any particular insight. Congratulations for actually doing this! -- Best, Bill ------------------------------------------------------------------------------ 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
