FOM: Franzen vs HA; polymorphic type theory

[Stephen G Simpson]

Franzen vs HA:

Torkel Franzen said that "intuitionistically we have to distinguish"
among

   forall x exists y P(x,y)

   not not forall x exists y P(x,y)

   forall x not not exists y P(x,y)

where P(x,y) is primitive recursive.  But Neil Tennant pointed out
that if any one of these sentences is provable in HA (= Heyting
arithmetic), then all of them are.  So it would appear that all of
these sentences have the same intuitionistic status.  Is there
anything left of Franzen's claim?  If there is, I think Franzen needs
to explain it.

Polymorphic type theory:

Till Mossakowski called our attention to Pitts' work (LNCS 283, pages
12-39) in which an appropriately chosen topos provides a semantics for
polymorphic type theory.  That's a good point!  At the very least,
it's an interesting connection between topos theory and polymorphic
type theory.  I don't remember the details of Pitts' paper; I may have
read it years ago.  Does Pitts actually refer to toposes or use any
results of topos theory?  His title refers instead to "constructive
set theory", so once again it appears that topos theory is slavishly
imitating set theory.  In any case, I'm familiar with the PER model of
polymorphic type theory; I think this is essentially the same thing as
what Hyland calls the effective topos.  In this model, the types are
partial equivalence relations, i.e. PERs, on N, and the functions from
one type to another are given by equivalence-preserving partial
recursive functions.  A very nice model!  You could explain this model
to anybody who is familiar with the rudiments of recursive function
theory.

But now let's ask, what does polymorphic type theory have to do with
f.o.m.?  Is polymorphic type theory viable as a foundational setup for
mathematics?  Is polymorphic type theory "practically complete"?  What
about undergraduate real analysis (calculus, etc) in polymorphic type
theory?  What is the underlying picture of polymorphic types?  From
the viewpoint of sets and mappings, the PER model seems rather
strange; for example, the product type Pi_x.T(x) is just the
intersection of the PERs T(X) where X is an arbitrary PER.  Again,
what is the underlying picture?  Can this picture support the
development of real analysis and other standard mathematical topics?

-- Steve