Thanks, Ramana! I don't quite understand. In each theorem I should make an extra hypothesis which will look something like assume Hilbert_plane H (Between) (===) Line {HP}; And I'll add the label HP to each "by" list in which I refer to one of my earlier theorems? In your earlier post, I think you said you preferred shallow embeddings. Do you call this a shallow embedding?
Back to my earlier question, my miz3 code begins new_type("point",0);; new_type_abbrev("point_set",`:point->bool`);; new_constant("Line",`:point_set->bool`);; I still don't know what the HOL, or HOL4 meaning of this is, but I have a new conjecture: My new_type command defines a set called "point", And later when I write let A B C be point; that means that the variables A, B & C refer to elements of the set "point" Does that sound right? In particular, a type is the name of a set? I'm having trouble with the term HOL. If someone asked me to describe what HOL Light was doing, I'd say that we were working in a model of ZFC with some extra features. E.g. it's quite difficult in ZFC to construct the real line R (see Halmos's book Naive Set Theory), but HOL Light hands us a nice copy of R with all its properties. So if one did not have a model of ZFC, one would be doing FOL, just manipulating the f.o. ZFC axioms, but it's a lot nice to actually have a model of ZFC, i.e. a collection of sets. I don't mean that we have all the sets that a model of ZFC would contain. There's a set UNIV, the universe we work in, and a ZFC model would not contain that. All this is great, but I don't know why we're using the term HOL to describe it. I understand that HOL means 2nd order logic, 3rd order logic etc, but that just means you can quantify over more and more complicated sets, and I guess we get all those sets in a model of ZFC. I'm also confused about the HOL Logic manual saying we don't get the empty set. I use the empty set all the time, it's called EMPTY or [ {}, defined in sets.ml. Maybe there's a technicality which going like this. In sets.ml, sets are "constructed" as boolean functions. So (assuming that "point" is actually a set, as I conjectured above) we can define the empty subset of point as the function {}: point -> bool which takes every element of point to False. So is that it, we can get the empty set by confusing sets with boolean functions? -- 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