Trouble viewing the formulas? You need a MathML compatible browser.

# Truth-Trees

Truth Trees, or refutation trees, are most often used as a method of testing the validity of arguments. The truth tree method tests the validity of an argument by assuming the argument is not valid. If one is testing a valid argument, this assumption will lead to contradiction. If one is not lead to contradiction, then that means that it is possible for the premises to be true and the conclusion false. The truth tree method can also be used to test for other properties of sentences (like whether they are logically equivalent).

## The Rules

The rules for truth-trees are derived from the truth tables for the connectives. We will divide the truth tree rules into three categories: Branching, Non Branching, and Quantifier rules. Only the first two are needed for testing arguments in propositional logic. The addition of the third category is required to test the validity of arguments in predicate logic.

## Some definitions

• A branch is closed if it contains an occurrence of an atomic sentence together with its negation.
• A tree is closed if every branch is closed.
• A tree is complete if every sentence is either checked off or starred or is atomic or is the negation of an atomic sentence.

### Strategies

To use the truth tree method to determine the validity of an argument, follow these strategies:

1. Write the premises of the argument at the top.
2. Write the negated conclusion underneath the premises.
3. Start unpacking formulae that do not branch, if applicable. Write down the unpacked formulae on every open branch and check off the formula you've unpacked.
4. Check to see if any open branches have an atomic sentence and its negation. If so, close that branch. If not, apply more rules.
5. If you have star-rules, apply those rules next.
6. Repeat step 4.
7. If you have formulas that require branching, do the following: Split every open branch the formula occurs on. Write the unpacked formula on every branch on which it occurs.
8. Repeat step 4.
9. Stop when the tree is complete.

## Examples

The following case demonstrates what it means to unpack a sentence on every branch on which it occurs:
Note we don't instantiate $\forall x\phantom{\rule{0}{0ex}}P\phantom{\rule{0}{0ex}}x$ with the constant $d$, since it occurs on a different branch.

### Arguments of Propositional Logic

Here is an argument: $¬\left(A\wedge B\right);\left(B↔A\right)⊢\left(A\to B\right)$

In this first truth tree, we see that we first apply the rule for negated implication (since it is non-branching), and then we applied the rule for negated conjunction...

 First we applied the rule for negated implication (since it's a non-brancher), then we applied the rule for negated conjunction.

Our tree is not complete, since there is a sentence $\left(B↔A\right)$ that has not been unpacked. Once we apply the rule for the biconditional, we get:

The tree is complete (since all sentences are either checked or are atomics or the negation of an atomic). The tree is closed, so the argument is valid.

Now, we can consider the following argument:

$¬\left(A↔B\right);A⊢\left(B\wedge A\right)$

The truth tree for this argument is:

 Since there is an open branch and,so, the tree is not closed, the argument is invalid.

### Arguments of Predicate Logic

Consider the argument, $\exists x\phantom{\rule{0}{0ex}}F\phantom{\rule{0}{0ex}}x$, $\forall x\forall y\left(F\phantom{\rule{0}{0ex}}y\to ¬R\phantom{\rule{0}{0ex}}x\phantom{\rule{0}{0ex}}y\right)$ $⊢\exists x\forall y¬R\phantom{\rule{0}{0ex}}y\phantom{\rule{0}{0ex}}x$. The following set of truth trees are designed to chart the application of some of the rules above:

The last truth tree in this set is complete. Since the tree is closed, we can see that the original argument is valid.