.
/\
¬ ∀x B B[x/a]
noting that the lefthand path is closed.
41
Similarly, if Ri is the tableau rule
.
.
.
¬ ∀x B
.
(——) .
.

¬ B[x/a]
where a is a new parameter, let Ci be the companion B[x/a] ’ (∀x B), and
replace the application of (——) by
.
.
.
B[x/a] ’ (∀x B)
.
.
.
¬ ∀x B
.
.
.
/\
¬ B[x/a] ∀x B
noting that the righthand path is closed.
Example 3.2.8. As an example illustrating Theorem 3.2.7, let A be the sen
tence (∃x (P x ∨ Qx)) ’ ((∃x P x) ∨ (∃x Qx)). Let „ be the closed tableau
¬A
∃x(P x ∨ Qx)
¬ ((∃x P x) ∨ (∃x Qx))
¬ ∃x P x
¬ ∃x Qx
P a ∨ Qa
¬Pa
¬ Qa
/\
Pa Qa
which shows that A is logically valid. Examining the applications of quanti¬er
rules in „ , we obtain the companion sequence C1 , C2 , C3 for A, where C1 is
(∃x (P x ∨ Qx)) ’ (P a ∨ Qa), C2 is P a ’ ∃x P x, C3 is Qa ’ ∃x Qx. Clearly
(C1 & C2 & C3 ) ’ A is a quasitautology.
3.3 A HilbertStyle Proof System
Let L be a language. Recall that V is the set of parameters.
42
De¬nition 3.3.1 (the system LH ). Our Hilbertstyle proof system LH for
the predicate calculus is as follows:
1. The objects are LV sentences.
2. For each quasitautology A, A is a rule of inference.
3. (∀x B) ’ B[x/a] and B[x/a] ’ (∃x B) are rules of inference.
4. A, A ’ B, B is a rule of inference.
5. A ’ B[x/a], A ’ (∀x B) and B[x/a] ’ A, (∃x B) ’ A are rules of in
ference, provided the parameter a does not occur in A or in B.
Schematically, LH consists of:
1. A, where A is any quasitautology
2. (a) (∀x B) ’ B[x/a] (universal instantiation)
(b) B[x/a] ’ (∃x B) (existential instantiation)
A A’B
(modus ponens)
3.
B
A ’ B[x/a]
4. (a) (universal generalization)
A ’ (∀x B)
B[x/a] ’ A
(b) (existential generalization),
(∃x B) ’ A
where a does not occur in A, B.
Lemma 3.3.2 (soundness of LH ). LH is sound. In other words, for all L
V sentences A, if A is derivable, then A is logically valid.
Proof. The proof is straightforward by induction on the length of a derivation.
The induction step is similar to the proof of Lemma 3.2.4.
Example 3.3.3. In LH we have the following derivation:
1. (∀x A) ’ A[x/a] (universal instantiation)
2. A[x/a] ’ (∃x A) (existential instantiation)
3. ((∀x A) ’ A[x/a]) ’ ((A[x/a] ’ (∃x A)) ’ ((∀x A) ’ (∃x A)))
(This is a quasitautology, obtained from the tautology
(p ’ q) ’ ((q ’ r) ’ (p ’ r)).)
4. (A[x/a] ’ (∃x A)) ’ ((∀x A) ’ (∃x A)) (1, 3, modus ponens)
5. (∀x A) ’ (∃x A) (2, 4, modus ponens)
Thus, by Lemma 3.3.2, (∀x A) ’ (∃x A) is logically valid.
43
Example 3.3.4. In LH we have the following derivation:
1. B[x/a] ’ (∃x B) (existential instantiation)
2. (B[x/a] ’ (∃x B)) ’ ((A & B)[x/a] ’ (∃x B)) (quasitautology)
3. (A & B)[x/a] ’ (∃x B) (1, 2, modus ponens)
4. (∃x (A & B)) ’ (∃x B) (3, existential generalization)
Thus, by Lemma 3.3.2, (∃x (A & B)) ’ (∃x B) is logically valid.
We now turn to the proof that LH is complete.
Lemma 3.3.5. LH is closed under quasitautological consequence. In other
words, if A1 , . . . , Ak are derivable, and if B is a quasitautological consequence
of A1 , . . . , Ak , then B is derivable.
Proof. We are assuming that B is a quasitautological consequence of A1 , . . . , Ak .
Thus A1 ’ (A2 ’ · · · ’ (Ak ’ B)) is a quasitautology, hence derivable. We are
also assuming that A1 , . . . , Ak are derivable. Thus we obtain B by k applications
of modus ponens.
Lemma 3.3.6. If C is a companion of A, and if C ’ A is derivable in LH , then
A is derivable in LH .
Proof. First, suppose C is of the form 3.2.3(1), namely (∀x B) ’ B[x/a]. By
universal instantiation, C is derivable. In addition, we are assuming that C ’ A
is derivable. Hence, by modus ponens, A is derivable.
Next, suppose C is of the form 3.2.3(2), namely B[x/a] ’ (∀x B), where
a does not occur in A, B. We are assuming that C ’ A is derivable, i.e.,
(B[x/a] ’ (∀x B)) ’ A is derivable. It follows by Lemma 3.3.5 that both (i)
(¬ A) ’ B[x/a] and (ii) (¬ A) ’ (¬ ∀x B) are derivable. Applying universal gen
eralization to (i), we see that (¬ A) ’ (∀x B) is derivable. From this plus (ii),
it follows by Lemma 3.3.5 that A is derivable.
The other cases, where C is of the form 3.2.3(3) or 3.2.3(4), are handled
similarly.
Theorem 3.3.7 (completeness of LH ). LH is sound and complete. In other
words, for all LV sentences A, A is derivable if and only if A is logically valid.
Proof. The “only if” part is Lemma 3.3.2. For the “if” part, assume that
A is logically valid. By Theorem 3.2.7, there exists a companion sequence
C1 , . . . , Cn for A such that (C1 & · · · & Cn ) ’ A is a quasitautology. Hence
Cn ’ (Cn’1 ’ · · · ’ (C1 ’ A)) is a quasitautology, hence derivable. From this
and n applications of Lemma 3.3.6, we obtain derivability of A.
Exercise 3.3.8. Consider the following proof system LH , which is a “stripped
down” version of LH . The objects of LH are LV sentences containing only ∀,
’ , ¬ (i.e., not containing ∃, ” , & , ∨ ). The rules of LH are:
44
1. quasitautologies
2. (∀x B) ’ B[x/a]