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

[Pierre Hyvernat]

> 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?
>
Well, isn't it the whole point of impredicativity: that we don't really
know how to do much better than that?


This is not a definite answer to your question, but since one needs a
little bit of third order to prove SN of system F; which probably means
that you cannot hope to get a nice (say indexed by types) family of
candidates to prove SN: this would allow to prove SN in second order
arithmetic.

Am I just babbling here?
Correct me if I'm wrong...




There is something by Coquand and Altenkirch for a very restricted
subsystem of F in
"A Finitary subsystem of the polymorphic lambda-calculus", LNCS 2044.

(IIRC, this was simplified in
"Completeness theorems and lambda-calculus.", LNCS 3461.)

This is supposed to be a readable account of a more general result in
Buchholz & Schütte, "Proof theory of impredicative subsystems of
analysis". Somehow, Pi_1^1 quantification is predicative...



Some notes by R. Labib-Sami or K. Nour & S. Farkh ("Un Résultat de
Complétude pour les Types positifs du Système F") might might also be
relevant here, but I'm not sure how...

However, I've never read Labib-Sami's note, and Nour's note is in
French.

(Summary of Nour's note: there is a weak completeness result for
positive types: t in [[A]]  iff  t -->*  t' with  |- t':A.)


Pierre
-- 
Everything should be made as simple as possible, but
not simpler.
    -- Albert Einstein