indicating that X1 , . . . , Xk , Y ∈ R. This is to be understood as “from the
premises X1 , . . . , Xk we may immediately infer the conclusion Y ”. For k = 0
we may write
Y
or simply Y , indicating that Y ∈ R. This is to be understood as “we may
infer Y from no premises”, or “we may assume Y ”.
De¬nition 3.1.3. Let L be a language. Recall that V is the set of parameters.
A Hilbertstyle proof system for L is a proof system with the following properties:
1. The objects are sentences with parameters. In other words,
X = {A : A is an LV sentence} .
2. For each rule of inference
A1 · · · Ak
B
38
(i.e., A1 , . . . , Ak , B ∈ R), we have that B is a logical consequence of
A1 , . . . , Ak . This property is known as soundness. It implies that every
LV sentence which is derivable is logically valid.
3. For all LV sentences A, B, we have a rule of inference A, A ’ B, B ∈ R,
i.e.,
A A’B
.
B
In other words, from A and A ’ B we immediately infer B. This collection
of inference rules is known as modus ponens.
4. An LV sentence A is logically valid if and only if A is derivable. This
property is known as completeness.
Remark 3.1.4. In Section 3.3 we shall explicitly exhibit a particular Hilbert
style proof system, LH . The soundness of LH will be obvious. In order to verify
the completeness of LH , we shall ¬rst prove a result known as the Companion
Theorem, which is also of interest in its own right.
3.2 The Companion Theorem
In this section we shall comment on the notion of logical validity for sentences of
the predicate calculus. We shall analyze logical validity into two components: a
propositional component (quasitautologies), and a quanti¬cational component
(companions).
De¬nition 3.2.1 (quasitautologies).
1. A tautology is a propositional formula which is logically valid.
2. A quasitautology is an LV sentence of the form F [p1 /A1 , . . . , pk /Ak ],
where F is a tautology, p1 , . . . , pk are the atoms occurring in F , and
A1 , . . . , Ak are LV sentences.
For example, p ’ (q ’ p) is a tautology. This implies that, for all LV sentences
A and B, A ’ (B ’ A) is a quasitautology.
Remarks 3.2.2.
1. Obviously, every quasitautology is logically valid.
2. There is a decision procedure1 for quasitautologies. One such decision
procedure is based on truth tables. Another is based on propositional
tableaux.
1 Inother words, there is a Turing algorithm which, given an LV sentence A as input, will
eventually halt with output 1 if A is a quasitautology, 0 if A is not a quasitautology.
39
3. It can be shown that there is no decision procedure for logical validity.
(This result is known as Church™s Theorem.) Therefore, in relation to the
problem of characterizing logical validity, we regard the quasitautologies
as trivial.
Let A be an LV sentence.
De¬nition 3.2.3 (companions). A companion of A is any LV sentence of
one of the forms
(∀x B) ’ B[x/a]
(1)
B[x/a] ’ (∀x B)
(2)
(∃x B) ’ B[x/a]
(3)
B[x/a] ’ (∃x B)
(4)
where, in (2) and (3), the parameter a may not occur in A or in B.
Lemma 3.2.4. Let C be a companion of A.
1. A is satis¬able if and only if C & A is satis¬able.
2. A is logically valid if and only if C ’ A is logically valid.
Proof. Let C be a companion of A.
For part 1, assume that A is satis¬able. In accordance with De¬nition 2.3.7,
let M, φ be an LV structure satisfying A. If C is of the form 3.2.3(1) or
3.2.3(4), then C is logically valid, hence M, φ satis¬es C & A. Next, consider
the case when C is of the form 3.2.3(2). If M, φ satis¬es ∀x B, then M, f
satis¬es C. Otherwise we have vM (∀x B φ ) = F, so let c ∈ UM be such that
vM (B φ [x/c]) = F. De¬ne φ : V ’ UM by putting φ (a) = c, φ (b) = φ(b)
for b = a. Since a does not occur in A, we have that M, φ satis¬es A. Also,
since a does not occur in B, we have B[x/a]φ = B φ [x/c] = B φ [x/c], hence
vM (B[x/a]φ ) = vM (B φ [x/c]) = F, i.e., M, φ satis¬es ¬ B[x/a]. Thus M, φ
satis¬es C & A. The case when C is of the form 3.2.3(3) is handled similarly.
For part 2 note that, since C is a companion of A, C is a companion of ¬ A.
Thus we have that A is logically valid if and only if ¬ A is not satis¬able, if
and only if C & ¬ A is not satis¬able (by part 1), if and only if ¬ (C & ¬ A) is
logically valid, i.e., C ’ A is logically valid.
De¬nition 3.2.5 (companion sequences). A companion sequence of A is a
¬nite sequence C1 , . . . , Cn such that, for each i < n, Ci+1 is a companion of
(C1 & · · · & Ci ) ’ A.
Lemma 3.2.6. If C1 , . . . , Cn is a companion sequence of A, then A is logically
valid if and only if (C1 & · · · & Cn ) ’ A is logically valid.
Proof. Note that (C1 & · · · & Cn ) ’ A is quasitautologically equivalent to
Cn ’ (Cn’1 ’ · · · ’ (C1 ’ A)).
40
Our lemma follows by n applications of part 2 of Lemma 3.2.4.
Theorem 3.2.7 (the Companion Theorem). A is logically valid if and only
if there exists a companion sequence C1 , . . . , Cn of A such that
(C1 & · · · & Cn ) ’ A
is a quasitautology.
Proof. The “if” part is immediate from Lemma 3.2.6. For the “only if” part,
assume that A is logically valid. By Theorem 2.5.5 let „ be a ¬nite closed
unsigned tableau starting with ¬ A. Thus we have a ¬nite sequence of tableaux
„0 , „1 , . . . , „n where „0 = ¬ A, „n = „ , and each „i+1 is obtained by applying
a tableau rule Ri to „i . If Ri is a quanti¬er rule, let Ci be an appropriate
companion. Thus C1 , . . . , Cn is a companion sequence for A, and we can easily
transform „ into a closed tableau „ starting with
¬A
C1
.
.
.
Cn
in which only propositional tableau rules are applied. Thus (C1 & · · · & Cn ) ’ A
is a quasitautology. This proves our theorem.
For instance, if Ri is the tableau rule
.
.
.
∀x B
.
(—) .
.

B[x/a] ,
where a is an arbitrary parameter, let Ci be the companion (∀x B) ’ B[x/a],
and replace the application of (—) by
.
.
.
(∀x B) ’ B[x/a]
.
.
.
∀x B
.