On 5/08/12 7:42 PM, Rob Arthan wrote: >> 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.
Yes, I was sloppy there.
Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
