On 03/08/12 07:48, Bill Richter wrote:
> 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?
A non-polymorphic type denotes a non-empty ZFC set. We can assume that this
set
is one of the "non-empty sets in the von Neumann cumulative hierarchy formed
before stage ω + ω" (Logic Manual, p10)
A polymorphic type is a effectively a function on types; when you instantiate
the type variables you are applying the function to arguments and getting back
an actual non-empty set.
When you do a new_type command, the system picks an arbitrary non-empty set and
identifies your chosen name with that set. Logically, you know nothing at all
about that type except that it is non-empty.
> 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?
Yes, the empty set, {}, that you are referring to is just a predicate (the
predicate that is everywhere false) over a type. Alternatively, it is a subset
of a non-empty set. If you read something saying that there is no empty set,
it's meaning that there is no empty type.
It is true that we can't do anything in HOL that you couldn't do in ZFC/FOL,
but
things tend to work more smoothly in HOL. In particular, there is no
distinction between predicates and 'sets', and no need for axioms restricting
what you can and can't write with a set comprehension. This is because all
such
predicates, sets and comprehensions are all done with respect to some bounding
set in the ZFC model.
HOL's handling of functions is also cleaner. In FOL, you can't quantify over a
function-symbol, so it's illegal to write
∃f. ∀n. f (n + 1) < f (n)
where f is a function symbol of the FOL. But, of course, mathematicians are
working in ZFC and sets can be held to represent functions, so you *are*
allowed to write
∃f ∈ N × N. ∀n ∈ N. f ` (n + 1) < f ` n
where the "function" f is really just a set, and the function symbols are
actually ` ("function application"), + and × (in the outer quantification).
The meta-theory of FOL tells us that we can introduce fresh function symbols in
certain circumstances, so we might be able to create formulas that use f as a
function symbol, but that f can't be the same as the f which is just a subset
of
N × N, even if it's behaviour looks pretty similar. This is pretty yucky, and
HOL hides lots of complexity.
Michael
------------------------------------------------------------------------------
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
