. .
. .
. .
TA’B FA’B
. .
. .
. .
/\ 
FA TB TA
FB
. .
. .
. .
TA”B FA”B
. .
. .
. .
/\ \
/
TA FA TA FA
TB FB FB TB
. .
. .
. .
T¬A F¬A
. .
. .
. .
 
FA TA
Table 1.1: Signed tableau rules for propositional connectives.
11
. .
. .
. .
¬ (A & B)
A&B
. .
. .
. .
 \
/
¬A ¬B
A
B
. .
. .
. .
A∨B ¬ (A ∨ B)
. .
. .
. .
\ 
/
¬A
A B
¬B
. .
. .
. .
A’B ¬ (A ’ B)
. .
. .
. .
/\ 
¬A B A
¬B
. .
. .
. .
A”B ¬ (A ” B)
. .
. .
. .
\ \
/ /
¬A A ¬A
A
¬B ¬B
B B
.
.
.
¬¬A
.
.
.

A
Table 1.2: Unsigned tableau rules for propositional connectives.
12
by repeatedly applying tableau rules.
De¬nition 1.4.5. A path of a tableau is said to be closed if it contains a
conjugate pair of signed or unsigned formulas, i.e., a pair such as TA, FA in
the signed case, or A, ¬ A in the unsigned case. A path of a tableau is said to
be open if it is not closed. A tableau is said to be closed if each of its paths is
closed.
The tableau method:
1. To test a formula A for validity, form a signed tableau starting with FA, or
equivalently an unsigned tableau starting with ¬ A. If the tableau closes
o¬, then A is logically valid.
2. To test whether B is a logical consequence of A1 , . . . , Ak , form a signed
tableau starting with TA1 , . . . , TAk , FB, or equivalently an unsigned
tableau starting with A1 , . . . , Ak , ¬ B. If the tableau closes o¬, then B is
indeed a logical consequence of A1 , . . . , Ak .
3. To test A1 , . . . , Ak for satis¬ability, form a signed tableau starting with
TA1 , . . . , TAk , or equivalently an unsigned tableau starting with A1 , . . . , Ak .
If the tableau closes o¬, then A1 , . . . , Ak is not satis¬able. If the tableau
does not close o¬, then A1 , . . . , Ak is satis¬able, and from any open path
we can read o¬ an assignment satisfying A1 , . . . , Ak .
The correctness of these tests will be proved in Section 1.5. See Corollaries
1.5.9, 1.5.10, 1.5.11.
Example 1.4.6. Using the signed tableau method to test (p & q) ’ (q & p) for
logical validity, we have
F (p & q) ’ (q & p)
Tp&q
Fq&p
Tp
Tq
/\
Fq Fp
Since (every path of) the tableau is closed, (p & q) ’ (q & p) is logically valid.
1.5 The Completeness Theorem
Let X1 , . . . , Xk be a ¬nite set of signed formulas, or a ¬nite set of unsigned
formulas.
Lemma 1.5.1 (the Soundness Theorem). If „ is a ¬nite closed tableau start