On 14 Aug 2012, at 00:30, Cris Perdue wrote:
>
>
> On Mon, Aug 13, 2012 at 6:05 PM, Bill Richter <rich...@math.northwestern.edu>
> wrote:
>
> I prefer not to say that a type is a set, because the set of all
> things having a type is expressible as \x. T (or {x | T}.
>
> Cris, I'm tempted to go with Michael, who sorta disagreed with you above.
> Let me try to resolve the semi-disagreement. My guess is that if you can
> really write {x | T}, then that means that we're doing all our type theory in
> a "universe" which in ZFC would actually be called a set. The model of ZFC
> isn't going to be a set, by Russell's paradox, and that's a way in which HOL
> is weaker than ZFC, a weakness that doesn't bother me at all.\
>
In HOL, if you just parse {x | T}, the bound variable x will be given the most
general type, namely some type variable, so in a sense {x | T} does denote the
set of a all things in the universe (since !x. x IN {x | T} is true). But it is
probably easier to think of { x | T } as something with an implicit parameter
(the type variable) that represents an unknown type, and can be specialised to
any type of our choice.
> Well, yes. I have frequently been omitting explicit type annotations on
> variables (and constants). So if "i" is the notation for a type of
> "individuals" then you can write {x:i | T} for the set of all individuals.
> And if "i->i" is the notation for functions from individuals to individuals
> then {x:i->i | T} denotes the set of all functions from individuals to
> individuals. In the usual varieties of type theory the annotation for a type
> must be finite in size, and this limits the universe of discourse. As I
> understand it this does result in a weaker system than ZFC.
>
There are two aspects to that: an unsubtle one and a subtle one (that I only
know of by hearsay and that I don't claim to understand).
The unsubtle aspect is that the axiom of replacement in ZFC makes it much much
stronger than HOL by imposing a much bigger lower bound on the rank of the
universe (which essentially means that you cannot define biggish ordinals or
cardinals in a uniform way and can't define really big ordinals or cardinals at
all). Really you should be comparing HOL with Zermelo set theory with choice
(ZC). ZC and HOL feel very comparable - both have models with a universe of
rank omega+omega. Using choice, you can construct cardinals like the
cardinality of the continuum in an ad hoc way, but you can't fit it in nicely
into an endless sequence of cardinals as you can in ZFC.
The subtle aspect, if my memory is correct, means that the untyped nature of ZC
makes it stronger than HOL in rather subtle ways whose mathematical impact I am
not qualified to assess (and is probably completely negligible for mainstream
pure mathematics). My recollection was that this follows from work of A.R.D.
Mathias on Slim Models of Zermelo Set Theory (a paper on this can be downloaded
from https://www.dpmms.cam.ac.uk/~ardm/). If anyone can give a better statement
of the position on this, I would be grateful.
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
