Saturation of infinite trees 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.

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 \
eg Fa)$ would create contradictory $Fa$ and $\
eg 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).