FOM: the PER model; unlimited comprehension; excessive generality

[Stephen G Simpson]

Till Mossakowski writes:
 > if you want to interpret polymorphic lambda calculus in a standard
 > way, i.e. products are interpreted as products, and function spaces
 > are interpreted as full function spaces, then you have to consider
 > the PER model to be a topos.

Harvey pointed out to me that the logical aspects of the PER model are
closely related to realizability as developed a long time ago in
papers by Kleene, Kreisel, and Harvey himself.  I don't think this
work was influenced by topos theory in any way.

 > topos theory could serve as a foundation of mathematics with an
 > unlimited comprehension principle for sets.

*How* could topos theory serve in that way?  In fact, are there *any*
interesting toposes that satisfy an unlimited comprehension principle?
Maybe I don't understand what you mean by "an unlimited comprehension
principle".

 > I merely cited polymorphism as an application of unlimited
 > comprehension, not as a foundation in itself.

Could you please state the unlimited comprehension principle that
holds in the PER model or that you think is compatible with
polymorphic type theory?

 > I think there is a chance to identify suitable axioms that, when
 > added to the topos axioms, give you an unlimited comprehension
 > principle. (I am not sure how far this has been worked out.)

Aren't the set theorists already way out ahead of the topos theorists
on this?  I'm thinking of alternative set theories with comprehension
schemes that go beyond what is available in ZFC.  I'm not an expert on
this stuff, but see for instance Randall Holmes' web site on NF at
http://math.idbsu.edu/~holmes/holmes/nf.html, and Harvey's work on set
theory with universes and predication theory at
http://www.math.ohio-state.edu/foundations/AxiomSetThy.ps and
http://www.math.ohio-state.edu/foundations/IntSetThyMathPred.ps.  Can
topos people do better?

 > Then topos theory would be the least common denominator of
 > 
 > 	set theory with limited comprehension, and excluded middle
 > and
 > 	set theory with unlimited comprehension, without excluded middle

Here it is again: the argument that topos theory is wonderful because
it is so very very general and has so many many different
interpretations that differ so very very wildly from each other.  Why
do topos people find this charming?  My colleagues in the Penn State
Math Department tend to regard excessive generality as a strategic
error.

-- Steve