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.