Fdtxjr

Having trouble wrapping my head around how to prove this. My first question about this is what it means for the tree method to determine that $T$ $models$ $A$. I'm taking it to mean that if we apply the tree method with every sentence in $T$ and $-A$ as inputs, then after the tree is finished, there are no open paths? Is this the correct way to unpack the original assumption?

From there, i'm confused as to where to go. Using the definition I wasn't sure about, my first thought was to try a proof by contradiction and show that there couldn't possibly be an open path if the truth tree method determines $T$ $models$ $A$, but i'm not sure how to show this. Any help/insight would be greatly appreciated. Thanks in advance!

We have to exploit the fact that in case of a tableau (or : truth tree) for the set $S$ of formulas, a complete open branch defines a truth-assignment that satisfies the initials set $S$.

This fact corresponds to the obvious fact that a closed path is unsatisfiable, because we close a path finding a pair of contradictory formulas.

What we have to prove is the soundness of the proof procedure, i.e. that:

if $T cup lnot A $ closes without open paths, then $T vDash A$.

The proof is by induction, starting from the soundness of the rules.

This means to consider each rule and prove that if the assumption of the rule is true, also at least one of the following path is true.

Consider e.g. rule :

$dfrac A to Blnot A $;

clearly, if $A to B$ is true, either $B$ is true or $A$ is false (i.e. $lnot A$ is true).

Similarly for $dfrac lnot (A land B)lnot A $.

The same for the rules regarding quantifiers, like e.g. $dfrac lnot forall x Alnot A[x/a] text with a text new$: if it is not true that $A$ holds of every object, this implies that there is an object, call it $a$, of which $A$ does not hold.

Having verified the base case, we have to consider a tree $mathcal T$ and a truth-assignment $v_0$ to the sentential variables occurring in the tree.

We say that a path of $mathcal T$ is true under $v_0$ if every formula occurring in the path is true under $v_0$.

Finally, we shall say that the tree $mathcal T$ is true under $v_0$ iff at least one path is true under $v_0$.

Consider now a tree $mathcal T_1$ and let $mathcal T_2$ the immediate extension of $mathcal T_1$ obtained with the application of one of the rules.

The soundness of the rules proved above amounts to proving that any immediate extension $mathcal T_2$ of a tree $mathcal T_1$ which is true under a given truth-assignment $v_0$ is again true under $v_0$.

From this it follows by mathematical induction that for any tree $mathcal T$, if the origin is true under $v_0$, then $mathcal T$ must be true under $v_0$.

Last step : a closed tree $mathcal T$ cannot be true under any interpretation, hence the origin of a closed tree must be unsatisfiable.

Conclusion : if the tree for $T cup lnot A $ closes (i.e. it is complete with no open paths) then the set of formulas $T cup lnot A $ is unsatisfiable, and this in turn means that :

$T vDash A$.