Explanation of the definition of Saturated Sets in Lambda Calculus I have a question on the definition of Saturated Sets, as particular subset of the set of strongly normalizing terms in lambda calculus.
Here is the definition: a set $S$ of strongly normalizing $\lambda$-terms is
said saturated if:
1) For all $x : var$ and for all sequences $a_{1} \dots a_{n}$ of strongly
   normalizing terms we have $x\, a_{1} \dots a_{n} \in S$.
2) For all strongly normalizing term strongly normalizing $a$ we have that $c[x:=a] \, a_{1} \dots a_{n} \in
   S$ implies $(\lambda x . c)\, a \, a_{1} \dots a_{n} \in S$.
Now, I'd like to know why this definition is the way it is. I understand that
originally the definition came from Girard, in a paper on "Candidats De
Reductibilité". Can anyone give me a general insight of the reason of this particular definition?
 A: Aha! I can give some answer to this one: saturated sets are a tool, designed specifically to allow the proof of strong normalization of System F.
First notice that the strongly normalizing terms are a particular instance of saturated sets. However they are not the only one! In particular, there is another important example, the neutral terms, i.e. the terms that reduce to a term of the form
$$ x\ a_1\ldots a_n$$
Note that this set does not contain any $\lambda$-abstractions, for example.
The crucial use of this concept is the proof that every well type term in say, the STLC is normalizing: in particular, simple induction over the typing rules does not work, as in the application case
$$ \frac{\Gamma \vdash t: A\rightarrow B\quad \Gamma\vdash u:A}{\Gamma\vdash t\ u:B}$$
you cannot conclude that $t\ u$ is SN even though $t$ and $u$ are.
The trick is to associate to each type $A$ a set $[\![ A ]\!]\subseteq \mathrm{SN}$ of computable terms of that type, and show that well-typed terms of type $A$ are in fact in $[\![A]\!]$. The fundamental trick here is to define
$$ [\![A\rightarrow B]\!] = \{t\in\mathrm{SN}\mid \forall u\in[\![A]\!],\ t\ u\in[\![B]\!]\}$$
But the proof still doesn't go through! The problem is now on the $\lambda$ case!
$$ \frac{\Gamma, x:A\vdash t:B}{\Gamma\vdash\lambda x.t: A\rightarrow B} $$
the proof doesn't go through because the induction hypothesis only says $t\in[\![B]\!]$ which doesn't help much to show that $\lambda x.t\in [\![A\rightarrow B]\!]$ (which requires a quantification over all $u\in[\![A]\!]$).
Ugh. The solution now is to carry around a suspended substitution, in which you prove $t[\vec{x}:=\vec{u}]\in [\![A]\!]$ instead of just $t\in [\![A]\!]$. So what does that give us in the $\lambda$ case:

$(\lambda x.t)[\vec{x}:=\vec{u}]\in [\![A\rightarrow B]\!]$, provided for all $u\in [\![A]\!]$, $(\lambda x.t)[\vec{x}:=\vec{u}]\ u\in [\![B]\!]$

Ah, but this is looking a lot like condition 2) for Saturated Sets! Very conveniently, your induction hypothesis gives
$$ t[x,\vec{x}:=u,\vec{u}]\in [\![B]\!]$$
Squinting a little (applications instead of suspended substitutions), if $[\![B]\!]$ is a saturated set the conclusion follows directly.
What about condition 1)? Well we have shown that a certain substitution applied to our term is SN. If we are to show that that $t$ itself is SN, it would be nice to apply the previous theorem ($t[\vec{x}:=\vec{u}]$ is SN for all computable $\vec{u}$) with the substitution $t[\vec{x}:=\vec{x}]=t$. This is exactly what condition 1) allows you to do, by showing that every variable is computable.
Alright, we see that (modulo a bit of squinting), being saturated is exactly the property required of $[\![A]\!]$ to make the proof go through. But why consider saturated sets on their own instead of just proving that each individual type $[\![A]\!]$ is saturated?
The answer there is that this does not work for system F. In system F the rule for universal quantification is
$$ \frac{\Gamma \vdash t:A}{\Gamma\vdash t:\forall X.A}$$
provided $X$ is free in $\Gamma$. So how do you define $[\![\forall X.A]\!]$? Girard's brilliant idea is that one may take the intersection
$$ \bigcap_S [\![A]\!]_{X:=S}$$
where $[\![X]\!]_{X:=S}=S$. This uses an implicit quantification over all subset of the set of (SN) terms! But $S$ can't be any arbitrary set of terms: it has to make the proof go through! So you must restrict $S$ to being a saturated set of terms. This is exactly what allows the above proof to generalize to system F.

Now after all these explanations, it sounds a lot like the definition of saturated sets is "just because it makes the proof go through". Unfortunately, that is somewhat the case. It would be really nice to have a higher-level understanding of the reducibility proofs that explain why these properties and not others are what is needed in the definition of saturated sets.
One attempt to do this that I know of is Jean Gallier's On Girard's "Candidats de Reducibilite", which describes a variant of saturated sets using the language of sheaves! Unfortunately, I don't know of a satisfying tie-in to the main corpus of work on models of typed $\lambda$-calculi, so this work is a bit of a lone wolf, so to speak.
