Sorry, Rob, I had a dumb typo, and meant to write "there exists a b such that a !~ b (i.e. a ~ b is false)."
Konrad and Michael, as I see you're an author of the HOL Logic manual http://sourceforge.net/projects/hol/files/hol/kananaskis-7/kananaskis-7-logic.pdf/download I'll ask you a question about my miz3 code, where the first few lines are new_type("point",0);; new_type_abbrev("point_set",`:point->bool`);; new_constant("Between",`:point->point->point->bool`);; new_constant("Line",`:point_set->bool`);; new_constant("≡",`:(point->bool)->(point->bool)->bool`);; I haven't read the manual carefully, but I see that you're working in something like a model of ZFC (except there's no empty set), and that `new_type' does not occur in the manual. I see it occurs in the Description manual http://sourceforge.net/projects/hol/files/hol/kananaskis-7/kananaskis-7-description.pdf/download I hope you can appreciate my confusion, as I'm working in HOL Light, and John Harrison's documentation barely explains HOL, and he does not (I think) refer to your manuals. A few dumb questions first: Can we call your manual a HOL4 manual? Do all version of HOL (e.g. HOL Light, Proof Power & Isabelle) abide by your Logic manual? What does Kananaskis mean? My guess is that my new_type declaration of "point" says that there exists an un-named set of point, and that any variable of type point will refer to an element of this set. Is that right? Let's call this set H, for Hilbert plane. The new_constant declaration of "Line" then says there's a predicate Line defined on the power set P(H). So later on when I write let l be point_set; let A B C be point; assume Line l I mean that the variable l refers to a subset of H, the variables A, B & C refer to elements of H, and that the subset l is actually a line, meaning that Line(l) = True. Am I getting this right? Can you explain an easy way I can cite this in my forthcoming geometry paper? BTW I recently adopted a better spin of my paper. Before I was saying that I was improving Hartshorne's book Geometry: Euclid and Beyond, as a number of his proofs have gaps too wide for a high school student to leap. Sounds kinda negativistic, right? Now I say that I'm continuing Hartshorne's great work by actually formalizing Hartshorne's Theorem 10.4, that all of Euclid's propositions in book I up to Prop (I.28) are true in any Hilbert plane, except for Props (I.1) and (I.22), which require extra axioms. -- 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
