Saturation of infinite trees

Question

What is (are) the difference(s) between saturated and unsaturated trees in predicate logic?

We have two trees:
Tree A:
$\forall x \exists y (Fx \land Gy) \backslash ab$
$\exists y (Fa \land Gy)\checkmark b$
$(Fa \land Gb)\checkmark$
$Fa$
$Gb$
$\exists y (Fb \land Gy)\checkmark c$
$(Fb \land Gc)\checkmark$
$Fb$
$Gc$
and so on.
Tree B:
$(\forall x \exists y (Fx \land Gy) \land (Fa \land \neg Fa))\checkmark$
$\forall x \exists y (Fx \land Gy)\backslash a$
$(Fa \land \neg Fa)$
$\exists y (Fa \land Gy)\checkmark b$
$(Fa \land Gb)\checkmark$
$Fa$
$Gb$
and so on, it continues in a way similiar to the Tree A.

I understand why both of these trees are infinite. What I do not understand is why the first tree is saturated and why the second one isn't.

Answer 1

Saturated path is the path which has been simplified to the basic propositions or the negations of basic propositions and which does not contain contradicting formulas. Tree A is saturated because, altough it's infinite, if all terms could be broken down to basic proposition or the negations of basic propositions, the path would remain open. Tree B is not saturated because after breaking down (somehow escaping the loop) of wffs to basic propositions or the negations of basic propositions, the path would close because $(Fa \land \neg Fa)$ would create contradictory $Fa$ and $\neg Fa$ (the path can be closed before even entering the loop, but the point is that even if the path can go infinitely and it can be closed, therefore infinite in one case but finite in other).

Answer 2

A saturated set of sentences $S$ is one where:

1. If $\phi \land \psi \in S$ then $\phi \in S$ and $\psi \in S$

2. If $\phi \lor \psi \in S$ then $\phi \in S$ or $\psi \in S$

3. If $\phi \rightarrow \psi \in S$ then $\neg \phi \in S$ or $\psi \in S$

(similar for any other connectives)

4. If $\forall x \phi(x) \in S$ then for any constant $c$ that occurs in the set $S$: $\phi(x) \in S$

5. If $\exists x \phi(x) \in S$ then for some constant $c$: $\phi(x) \in S$

(and there is something for the $=$ as well ...)

All the statements in tree $A$ form a saturated set of sentences, but this is not the case for tree $B$, since $Fa \land \neg Fa \in B$, but we have neither $Fa \in B$ nor $\neg Fa \in B$ (assuming that indeed we never end up decomposing that one in $B$, but I suppose that is the very idea here)