Thanks, Ramana and Rob! As Rob says, I don't use new_axiom to define by type "point", but I do use new_axiom to define Hilbert's geometry axioms, so I took no offense. I would definitely prefer to use neither new_type nor new_axiom. I'm using what John set me up with, but I think he thought of it as more of a way to get started, rather than the best way to formalize Euclid's book 1. BTW I don't think either of you answered my question
> 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? I would prefer to say that a Hilbert plane is a set H with two relations, Between and ===, with a predicate Line defined on subsets of H, so that H satisfies the axioms I1--3, B1--4 and C1--6. That's how I wrote my Tarski geometry Mizar code. I wasn't quite happy with that, and folks certainly believe that Hilbert's axioms are consistent. But I would like to know how to avoid new_type nor new_axiom. It's possible that miz3 could not handle the extra set theory load, as John suggested, and he said he'd improve the miz3 set theory capacity when he returned. Neither of you addressed > John Harrison's documentation barely explains HOL, and he does > not (I think) refer to your manuals. Do you agree with me? What is to be made of this? I mean, if one uses new_type in HOL Light, what theorems is HOL Light supposed to be formalizing? I don't know where John writes anything stronger about types than on p 13 of his tutorial: A key feature of HOL is that every term has a well-defined type. Roughly speaking, the type indicates what kind of mathematical object the term represents (a number, a set, a function, etc.) -- 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
