John, I wasn't clear in my last message, but I think you said to use HOL sets instead of types, so planes and lines both have type point->bool? If I'm misunderstanding you, please correct me.
I agree that it seems much simpler, and thinking of lines and planes as sets of points certainly corresponds to my intuition. Though I wonder if this is just because of the ubiquity of the set concept in modern mathematics. Would, say, an 18th-century mathematician have taken the same view? I would have thought you knew more about this than I, but Cantor's set theory was a over 100 years later, and he met with fierce resistance: http://en.wikipedia.org/wiki/Georg_Cantor. But your 1700s mathematicians (Cauchy, who discovered Cauchy sequences?) weren't writing axiomatic geometry proofs. Everyone was doing Euclid's picture proofs until Pasch & Hilbert. Wiki says ``Hilbert adopted and warmly defended Georg Cantor's set theory.'' Perhaps because using sets might be felt to make things less clear from a foundational perspective, since on the face of it you are also using some set-theoretic properties in addition to the explicit axioms. Now, in fact, I think it is clear that such uses are in some sense inessential and eliminable. My point was that having a corpus of totally explicit formal proofs might be a good starting-point for making that belief more rigorous. Are you saying that my set-theory powered Hilbert proofs will show that the set-they is ` inessential and eliminable', or that you want to see non-set-theory axiomatic geometry proofs? I could write up non-set-theory versions of my Hilbert proofs, although it wouldn't ``debug'' my paper very well, and my Tarski proofs have no set theory. -- 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
