[TYPES] SN for System F with countable universe of types?

[Andreas Abel]

When proving strong normalization for System F a la Girard, one uses a
complete lattice SAT of saturated sets (reducibility candidates, resp.).
  SAT is uncountable.  However, there are only countably many type
expressions.  Thinking naively, it should be possible to only use a
countable part of SAT to interpret type expressions.

Is this possible?  Are there any results on this question?

Reminder:  The interpretation [[A]]rho in SAT of type A in environment
rho is defined by induction on A as follows:

   [[X]]rho = rho(X)
   [[A -> B]]rho = [[A]]rho => [[B]]rho   (function space on SAT)
   [[forall X A]]rho = intersect_{S in SAT} [[A]](rho,X=S)

The intersection is over an uncountable set.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/