On 3 Aug 2012, at 05:49, Michael Norrish wrote:
> 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)
That isn't quite right. What the Logic Manual correctly says is that the
set-theoretic universe in which HOL types and terms take their values is closed
under certain operations and that the set of sets you mention
(V_{\omega+\omega}) is a possible universe. It doesn't say that
V_{\omega+\omega} is the universe and the axioms don't imply any upper bound on
the cardinality of types.
>
> 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.
Quite so. In particular, you don't know anything else about its cardinality. It
could be V_{\omega+\omega} itself or something much bigger. It would be
consistent (but not conservative) to use new_axiom to assert that a type
introduced with new_type was a model of HOL or of ZFC, say. This is why I said
in a reply to Ramana the other day that new_type really should be accounted for
in the Logic Manual: new_constant is equivalent to a special case of constant
specification but new_type is not equivalent to a special case of type
definition.
Regards,
Rob.
------------------------------------------------------------------------------
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
