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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
