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.

Maybe it is that for the first tree it is the case that every non-checked statement is either a literal or a universal that is instantiated for every constant appearing in its branch, while for the second this is not the case (because you have $Fa \land \neg Fa$ that never gets checked)? — Bram28, Jan 02 '18 at 19:46
Not clear... Tree B must close due to $(Fa \land \lnot Fa)$ applying the $\land$-rule. — Mauro ALLEGRANZA, Jan 02 '18 at 19:47
I think that the relevant clause (regarding $\land$) for a saturated tree is : if $(X \land Y)$ is in $S$ then $X, Y$ are both in $S$. — Mauro ALLEGRANZA, Jan 02 '18 at 19:49
The idea is: if you want to use the procedure in a "mechanical way", you have to apply all the possible rules to each formula in the tree. If not, you can go on forever (like in B) skipping the crucial consition that is needed to close it. — Mauro ALLEGRANZA, Jan 02 '18 at 19:51
@MauroALLEGRANZA Have you ever seen this 'saturated' term before? I've never come across it before ... — Bram28, Jan 02 '18 at 19:56
@Bram28 - Raymond Smullyan, First Order Logic : (one of) the father of Tableaux. — Mauro ALLEGRANZA, Jan 02 '18 at 19:59

Hanlon · Accepted Answer · 2018-01-03T11:03:40.010

0

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).

edited Jan 03 '18 at 11:03

answered Jan 02 '18 at 20:15

Hanlon

1,749

I don't think that's quite it ... If in tree $B$ instead of $Fa \land \neg Fa$ we would have had $Fa \land Ha$, then the tree would still be unsaturated, even though it would now be impossible to close: even if we did decompose this statement to its parts, it would still not close. So, the open vs close is not quite the right way to think about saturatedness, but rather whether everything is decomposed/instantiated or not. – Bram28 Jan 02 '18 at 20:24
I corrected the answer. I forgot to add and which does not contain contradicting formulas in the definition of saturated path. – Hanlon Jan 03 '18 at 10:00

score 0 · Answer 2 · answered Jan 02 '18 at 20:20

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

If $\phi \land \psi \in S$ then $\phi \in S$ and $\psi \in S$
If $\phi \lor \psi \in S$ then $\phi \in S$ or $\psi \in S$
If $\phi \rightarrow \psi \in S$ then $\neg \phi \in S$ or $\psi \in S$

(similar for any other connectives)

If $\forall x \phi(x) \in S$ then for any constant $c$ that occurs in the set $S$: $\phi(x) \in S$
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)

Saturation of infinite trees

2 Answers2