In Logic, a truth tree, also called an semantic tableau, (/tæˈbloʊ, ˈtæbloʊ/; plural: tableaux), an analytic tableau, is a method of testing for various properties of a set of premises or an argument.
Compare to a truth table, a truth tree can often to be faster to work with. An argument with basic premises need rows in a truth table, so it quickly gets unpractical. Also, it is possible to extend truth tree to predicate logic while truth table is limited to propositional logic.
The primary purpose of a truth tree is to determine whether a given set of propositions is satisfiable. However, with some adjustments, it can also be used to test other properties, such as validity.
Tree Rules in Proposition Logic
We can reduce a proposition to its more basic form by using one of the tree rules. All the tree rule for propositional logic can be derived from the truth table. Note that or are not reducible.
Uses of Trees
Satisfiability
Satisfiability is the most straightforward application of a truth tree.
Validity
If an argument is validity, it means that “all premises are true and the conclusion is false” is unsatisfiable. Thus, to test the validity with a tree, we write out all the premises and negate the conclusion at the top of the tree, and apply rules and close branches as appropriate until the tree is finished.
Example
Is the following argument valid?
Solution
We can see that all path in the tree are closed, so the argument is valid.
Example
Is the following argument valid?
Solution
We can see that some paths are open, so the argument is invalid.
For example, when , we have true premises but false conclusion
Tautologies
To ask whether a proposition is a tautology is to ask whether it is true in every scenario. In other word, its negation is not satisfiable.
Equivalence
The formula is equivalent to iff is tautology. In other word, iff is not satisfiable.
Are and equivalent?+
All paths close, so and are equivalent
In Predicate Logic
In predicate logic, we use trees similarly to how we do in propositional logic — for testing satisfiable. In predicate logic, a tree tell us whether there is a model that satisfies the formulas at the top of the tree exists. We read off such as model from an open path. If no such models exist, then all paths of the tree will be closed.
Tree Rules
The existing rules from the propositional logic stay the same, but we need add some new rules for quantifiers in predicate logics:
the notation means to substitute all variable in as
The tree rules for negated quantifiers are simple: switch the existential quantifier to a universal one and vice versa, while also putting the negation inward. For unnegated quantifiers, we need to introduce variables.
Existential Quantifier
For existential quantifiers, we introduce a name which is new to the path. We then strip the quantifier, and substitute all the free occurrence of the variable with .
Universal Quantifier
For universal quantifiers, can be any name and does not have to be new to the path. Note that when we applying this rule, we write a backslash instead of a check mark, since this rule can be repeatedly applied with different variable names
We can technically apply the rule above an infinite number of times,
but we can stop when a path is saturated.
We define “saturated” as
For every formula on whose main operator is a universal quantifier
The universal quantifier rule has been applied at least once.
The rule has been applied to it once for every name in the path.
For every other formula, the relevant rule has been applied.
Example: the following tree is finished
Example: the following tree is not finished
because we can still apply to the universal quantifier .
Once we do that, the tree is finished
Example: the following tree is not finished
We need to apply the universal rule at least once:
Heuristics for Applying Tree Rules
When applying tree rules, it is desirable to follow the following order:
propositional logic rules - and among those rules, nonbranching rules first
negated quantifiers rules
unnegated existential quantifier rules
unnegated universal quantifier rule
This heuristics usually result in a shorter tree proof.
Infinite Tree
When we apply trees to formulas containing quantifiers, it is possible for us to get infinite trees. In this case, we need to identify patterns in the tree paths in order to draw conclusion.
For example, suppose we want to know whether is satisfiable. We may start to write it into a tree like this:
However, since we introduced a new variable , we need to apply it to the universal quantifier again:
Note that in this process, we introduced another variable, , which means we also need to apply that. We are stuck in an infinite loop of introducing new variables and then applying them to the universal quantifier.
In this case, we can say that the tree path is saturated since from the pattern, we don’t see the possibility that the tree path getting closed. And thus this formula is satisfiable. We can also read off a model from the tree pattern:
Tree Rules for Identity
When we extend predicate logic to include the identity predicate, we need to add tree rules to accommodate it.
First, we close any paths that contains a formula of the form (or equivalently ).
Second, given an arbitrary formula containing the name , and an identity statement (or ), we can derive by substituting for .
Note that
we do not apply the rule for formulas that are ticked off
After applying this rule, we do not tick off the original formula, as the substitution can be applied repeatedly
A path is considered saturated when no further application of the substitution rule can generate new formulas not already present in the path.