Monday 2/10

Monday 2/10

Truth Tropic Language III: Validity by Analytic Tableaux

Readings

Notes

Synopsis

Recall how we defined validity using the Method of Truth Tables:

A PC argument is valid iff on no row of a standard truth table are all the premises true and the conclusion false.

Since each row of a standard truth table is a possible combination of truth values and all the rows of a standard truth table are all the possibilities, the definition above adequately captures the general definition of validity.

An argument is valid iff it is impossible for the conclusion to be false when all the premises are true.

That is, if we do discover on a row on a standard truth table all true premises and a false conclusion, then we know it is possible (since each row represents a possibility) for the conclusion to be false when all the premises are true, and thus the argument is invalid. What's nice about Truth Tables is they give us a mechanical, systematic way to define and test for validity.

What's not so nice about Truth Tables is how quickly the grow in size as the number of distinct sentence letters contained in an argument grow. A modest 7 sentence letters gives us 27 = 2x2x2x2x2x2x2 = 128 rows!

The method of Analytic Tableaux provides an elegant alternative.

To be sure, our definition of validity is a little more complicated when it comes to Analytic Tableaux, involving as it does the concept of a Semantic Tree (also called a Truth Tree.) It takes us three steps, thusly,

First, we say that a PC argument is valid iff a Semantic Tree which i) asserts all the premises while ii) denying the conclusion dies.

Second, we note that a Semantic Tree dies iff every branch of the Tree dies.

Third, and finally, we specify that a branch of a Semantic Tree dies iff it both asserts and denies the same PC-WFF--that is, iff a contradiction can be found on it, no matter how far back up the trunk we must track.

That is, if on any branch (and extending perhaps all the way back up the trunk, but never hopping over to a another branch!) we find a formula and its negation, we have shown that the branch dies. Think of it as having been poisoned by contradiction.

Lastly, it bears pointing out that when we assert a PC-WFF on a Semantic Tree, we simply write it, but when we deny it, we write (or assert) its negation. This should make sense: To deny a proposition is simply to assert its negation.

All of this boils down to both a second definition of validity on the Propositional Calculus and a second method for determing when we have valid arguments.

The Method of Analytic Tableaux

Suppose we have a PC argument and we wonder whether it is valid--whether, that is to say, the premises entail the conclusion. They do if, and only if, it is impossible for them to all be true and the conclusion false at the same time. Put another way, it is impossible to assert each of the premises on a tree while denying the conclusion--which, as we've seen, is just to assert its negation--without killing the tree. So we list the premises on the trunk along with the negation of the conclusion and see if all the resulting branches die upon determing what each of these assertions amounts to according to the following rules:

Rules of Analytic Tableaux

To implement the strategy of Analytic Tableaux, we need to understand what it comes to when we assert a given PC-WFF. Assertions, it turns out, can resolve either conjointly, which gives us our non-branching rules, or disjointly, which gives us our branching rules. Suppose A and B are any PC-WFF's. Then,

Non-Branching Rules

Since '∼A' is true iff 'A' is false, '∼∼A' asserts 'A' on the same branch.

Since 'A ∧ B' is true iff both 'A' is true and 'B' is true, 'A ∧ B' asserts both 'A' and 'B' on the same branch.

Since '∼(A ∨ B)' is true iff 'A ∨ B' is false, and 'A ∨ B' is false iff both 'A' is false and 'B' is false, '∼(A ∨ B)' asserts both '∼A' and '∼B' on the same branch.

Since '∼(A → B) is true iff 'A → B' is false, and 'A → B' is false iff both 'A' is true and 'B' is false, '∼(A → B)' asserts both 'A' and '∼B'.

Branching Rules

Since 'A ∨ B' is true iff either 'A' is true, or 'B' is true, or both 'A' and 'B' are true, 'A ∨ B' splits between asserting 'A' on a branch and 'B' on another branch.

Since '∼(A ∧ B)' is true iff 'A ∧ B' is false, and 'A ∧ B' is false iff either 'A' is false or 'B' is false, '∼(A ∧ B)' splits between asserting '∼A' on a branch and '∼B' on another branch.

Since 'A → B' is true iff either 'A' is false or 'B' is true, 'A → B' splits between asserting '∼A' on a branch and 'B' on another branch.

Since 'A ↔ B' is true iff either both 'A' is true and 'B' is true or both 'A' is false and 'B' is false, 'A ↔ B' splits between asserting both 'A' and 'B' together on one branch and '∼A' and '∼B' together on another branch.

Since '∼(A ↔ B)' is true iff 'A ↔ B' is false, and 'A ↔ B' is false iff either both 'A' is true and 'B' is false or both 'A' is false and 'B' is true, '∼(A ↔ B)' splits between asserting both 'A' and '∼B' together on one branch and '∼A' and 'B' together on another branch.

In general we want to apply non-branching rules before branching rules to keep our trees tall and skinny. Remember also that assertions propagate (repeat themselves) across branches beneath them (our trees grow upside down!) Our goal on every branch is the same: We keep resolving assertions until we get to a PC-WFF and its negation on a branch, no matter how far back up the branch we have to trace to reach either the PC-WFF or its negation. The branch then 'dies', which we indicate by putting an 'x' under the dead branch.

The handout The Rules of PC Analytic Tableaux (pdf) summarizes these rules, but organizes them by connective instead of branching/non-branching to make it easier (maybe) to look up relevant rules.

To revisit, once all the branches have been shown to die, we have shown that the tree dies--that is, that it is impossible to assert all of the premises while denying the conclusion. If we assert the premises, we must, in the strongest sense possible, also assert the conclusion.

Neat, eh?

Next time we will apply these methods (truth tables and analytic tableaux) to natural language arguments in preparation for our first examination on Monday.