MAT 3361, INTRODUCTION TO MATHEMATICAL LOGIC, Fall 2004

Lecture Notes: Analytic Tableaux

Peter Selinger

These notes are based on Raymond M. Smullyan, “First-order logic”. Dover Publications, New York 1968.

1 Analytic Tableaux

Definition. A signed formula is an expression T X or F X, where X is an (unsigned) formula. Under a given valuation, a signed formula T X is called true if X is true, and false if X is false. Also, a signed formula F X is called true if X is false, and false if X is true.

We begin with the following observations about signed formulas:

Observation 1.1. For all propositions X, Y:

1a. T (¬ X) ⇒ F X. 1b. F (¬ X) ⇒ T X. 2a. T (X ∧ Y) ⇒ T X and T Y. 2b. F (X ∧ Y) ⇒ F X or F Y. 3a. T (X ∨ Y) ⇒ T X or T Y. 3b. F (X ∨ Y) ⇒ F X and F Y. 4a. T (X → Y) ⇒ F X or T Y. 4b. F (X → Y) ⇒ T X and F Y.

The method of analytic tableaux can be summarized as follows: To prove the validity of a proposition X, we assume F X and derive a contradiction, using the rules from Observation 1.1. In doing so, we follow a specific format which is illustrated in the following example.

Example 1.2. An analytic tableau proving the validity of X = (p ∨ (q ∧ r)) → ((p ∨ q) ∧ (p ∨ r)) is shown in Table 1. Note: the line numbers, such as (1), (2) etc, are not part of the formalism; they are only used for our discussion.

The initial premise on line (1) is of the form F (Y → Z), where Y = (p∨(q ∧r)) and Z = ((p ∨ q) ∧ (p ∨ r)). By rule 4b, we can conclude both T Y and F Z.

(1) F (p ∨ (q ∧ r)) → ((p ∨ q) ∧ (p ∨ r))
(2) T (p ∨ (q ∧ r))
(3) F ((p ∨ q) ∧ (p ∨ r))
[figure]
[figure: (4) T p; \begin{matrix}(5) F (p ∨ q) \\ (6) F p \\ (7) F q \\ × \end{matrix} \begin{matrix}(8) F (p ∨ r) \\ (9) F p \\ (10) F r \\ × \end{matrix}; \begin{matrix}(11) T (q ∧ r) \\ (12) T q \\ (13) T r \end{matrix}; \begin{matrix}(14) F (p ∨ q) \\ (15) F p \\ (16) F q \\ × \end{matrix} \begin{matrix}(17) F (p ∨ r) \\ (18) F p \\ (19) F r \\ × \end{matrix}]

Table 1: An analytic tableau for X = (p ∨ (q ∧ r)) → ((p ∨ q) ∧ (p ∨ r)).

These are called the direct consequences of line (1), and we write them in lines (2) and (3), respectively. After we have done so, we say that line (1) has been used.

Now consider the formula in line (2), which is of the form T (X ∨Y), where X = p and Y = q ∧ r. From rule 3a, we may conclude that either T X or T Y holds. Since the conclusion in this cases involves a choice between two possibilities, we say that the formula on line (2) branches. When using such a formula, the tableaux splits into two branches, one for each possibility. This has been done in lines (4) and (11).

Continuing in a similar fashion, we use up all the lines containing composite formulas. We say that a branch is closed if it contains both T X and F X, for some signed formula X. We mark closed branches with the symbol ×. A closed branch represents a contradiction. Since in this example, all branches are closed, we conclude that the original formula (p ∨ (q ∧ r)) → ((p ∨ q) ∧ (p ∨ r)) is valid.

As the example shows, note that there are essentially two types of signed formulas:

(A) signed formulas with direct consequences, which are T (¬ X), F (¬ X), T (X ∧ Y), F (X ∨ Y), and F (X → Y), and

(B) signed formulas which branch, which are F (X ∧ Y), T (X ∨ Y), and T (X → Y).

When using a formula of type (A), we simply add all of its direct consequences to each branch underneath the formula being used. When using a formula of type (B), we split each branch underneath the formula into two new branches. The rules for tableaux can be summarized schematically as follows:

\begin{matrix}\frac{T (¬ X)}{F X} & \frac{F (¬ X)}{T X} \\ \begin{matrix}T (X ∧ Y) \\ T X \\ T Y \end{matrix} & \frac{F (X ∧ Y)}{F X | F Y} \\ \frac{T (X ∨ Y)}{T X | T Y} & \begin{matrix}F (X ∨ Y) \\ F X \\ F Y \end{matrix} \\ \frac{T (X → Y)}{F X | T Y} & \begin{matrix}F (X → Y) \\ T X \\ F Y \end{matrix} \end{matrix}

Definition. A branch is said to be complete if every formula on it has been used. A tableau is said to be completed if every one of its branches is complete or closed. A tableau is said to be closed if all of its branches are closed. A tableau is said to be open if it is not closed, i.e., if it has at least one open branch.

We say that a formula X has been proved by the tableaux method if there exists a closed analytic tableau with origin F X.

Strategies. Our goal is to find a completed analytic tableau for a given formula. There are different strategies for deriving such a tableau.

Strategy 1 is to work systematically downwards: in this strategy, we never use a line until all lines above it have been used. When using this strategy, we are guaranteed to arrive at a completed tableau after a finite number of steps. However, strategy 1 is often more inefficient than the following strategy 2:

Strategy 2: give priority to lines of type (A). This means that we use up all lines of type (A) before using those of type (B). When following this strategy, we postpone the creation of new branches until absolutely necessary, thus keeping the size of the tableau smaller when compared to strategy 1.

Abbreviations. We often use the following shortcut notation when discussion signed formulas: We use the letter α to stand for any signed formula of type (A). In this case, we use α_{1} and α_{2} to denote the direct consequences (in the special case where there is only one direct consequence, we will set α_{1} = α_{2}). All possibilities for α, α_{1}, and α_{2} are summarized in the following table:

\begin{matrix}α & α_{1} & α_{2} \\ T (X ∧ Y) & T X & T Y \\ F (X ∨ Y) & F X & F Y \\ F (X → Y) & T X & F Y \\ T (¬ X) & F X & F X \\ F (¬ X) & T X & T X \end{matrix}

We also use the letter β to stand for any signed formula of type (B). In this case, we use β_{1} and β_{2} to denote the two alternative consequences. For reasons of symmetry, we further also allow β to also stand for a signed formula which is a negation, in which case we set β_{1} = β_{2}. Thus, all possibilities for β, β_{1}, β_{2} are summarized as follows:

\begin{matrix}β & β_{1} & β_{2} \\ F (X ∧ Y) & F X & F Y \\ T (X ∨ Y) & T X & T Y \\ T (X → Y) & F X & T Y \\ T (¬ X) & F X & F X \\ F (¬ X) & T X & T X \end{matrix}

With these conventions, the rules for tableaux can be written succinctly as follows:

\begin{matrix}α \\ α_{1} \\ α_{2} \end{matrix}  \frac{β}{β_{1} | β_{2}}

Definition. The conjugate of a signed formula F X is T X, and the conjugate of a signed formula T X is F X. We write φ̄ for the conjugate of a signed formula φ.

We also observe the following: the conjugate of any α is some β, and in this case, \overline{(α_{1})} = β_{1} and \overline{(α_{2})} = β_{2}. The conjugate of any β is some α, and in this case, \overline{(β_{1})} = α_{1} and \overline{(β_{2})} = α_{2}. Moreover, for any signed formula φ, we have ¯ φ̄ = φ.