A A’B
4. (modus ponens)
B
B[x/a]
5. (generalization), where a does not occur in B.
∀x B
Show that LH is sound and complete.
Exercise 3.3.9.
1. Let S be a set of Lsentences. Consider a proof system LH (S) consisting
of LH with additional rules of inference A , A ∈ S. Show that an LV 
sentence B is derivable in LH (S) if and only if B is a logical consequence
of S.
2. Indicate the modi¬cations needed when S is a set of LV sentences.
Notation 3.3.10. We write S B to indicate that B is derivable in LH (S).
3.4 GentzenStyle Proof Systems
Throughout this section, let L be a language. As usual, V is the set of param
eters.
Before presenting our Gentzenstyle proof system for L, we ¬rst discuss the
block tableau method, a trivial variant of the signed tableau method.
De¬nition 3.4.1. A block is a ¬nite set of signed LV sentences. A block is
said to be closed if it contains T A and F A for some LV sentence A.
Notation 3.4.2. If S is a block and X is a signed LV sentence, we write S, X
instead of S ∪ {X}, etc.
De¬nition 3.4.3. A block tableau is a rooted dyadic tree where each node car
ries a block. A block tableau is said to be closed if each of its end nodes is closed.
Given a block S, a block tableau starting with S is a block tableau generated
from S by means of block tableau rules. The block tableau rules are obtained
from the signed tableau rules (pages 11 and 23) as follows. Corresponding to
signed tableau rules of the form
. .
. . . .
. . . .
. .
X X
X X
. .
. . . .
. . . .
. .
/\ /\
 
Y Z Y1 Z1
Y Y1
Y2 Y2 Z2
45
we have block tableau rules
S, X S, X S, X S, X
  /\ /\
S, X, Y S, X, Y1 , Y2 S, X, Y S, X, Z S, X, Y1 , Y2 S, X, Z1 , Z2
respectively.
For example, we have the following block tableau rules:
S, T A & B S, F A & B
 /\
S, T A & B, T A, T B S, F A & B, F A S, F A & B, F B
S, T A ’ B S, F A ’ B
/\ 
S, T A ’ B, FA S, T A ’ B, TB S, F A ’ B, T A, F B
S, T ∀x A S, F ∀x A
 
S, T ∀x A, T A[x/a] S, F ∀x A, F A[x/a]
where a is new.
Example 3.4.4. We exhibit a closed block tableau demonstrating that ∃x A is
a logical consequence of ∀x A.
T ∀x A, F ∃x A

T ∀x A, F ∃x A, T A[x/a]

T ∀x A, F ∃x A, T A[x/a], F A[x/a]
This block tableau is of course similar to the signed tableau
T ∀x A
F ∃x A
T A[x/a]
F A[x/a]
which demonstrates the same thing.
We now de¬ne our Gentzenstyle system, LG.
De¬nition 3.4.5. A sequent is an expression of the form “ ’ ∆ where “ and
∆ are ¬nite sets of LV sentences. If S = T A1 , . . . , T An , F B1 , . . . , F Bn is a
block, let S be the sequent A1 , . . . , Am ’ B1 , . . . , Bn . This gives a onetoone
correspondence between blocks and sequents.
46
De¬nition 3.4.6 (the system LG). Our Gentzenstyle proof system LG for
the predicate calculus is as follows.
1. The objects of LG are sequents.2
2. For each closed block S, we have a rule of inference S . In other words,
for all ¬nite sets of LV sentences “ and ∆ and all LV sentences A, we
assume the sequent “, A ’ A, ∆.
3. For each nonbranching block tableau rule
S

S
S 
we have a rule of inference S1 , S , i.e., .
S
4. For each branching block tableau rule
S
/\
SS
S  S 
we have a rule of inference S , S , S , i.e., .
S
Thus LG includes the following rules of inference:
“, A ’ A, ∆
“, ¬ A ’ A, ∆ “, A ’ ¬ A, ∆
“, ¬ A ’ ∆ “ ’ ¬ A, ∆
“, A & B, A, B ’ ∆ “ ’ A & B, A, ∆ “ ’ A & B, B, ∆
“, A & B ’ ∆ “ ’ A & B, ∆
“, A ’ B ’ A, ∆ “, A ’ B, B ’ ∆ “, A ’ A ’ B, B, ∆
“, A ’ B ’ ∆ “ ’ A ’ B, ∆
“, ∀x A, A[x/a] ’ ∆ “ ’ ∀x A, A[x/a], ∆
“, ∀x A ’ ∆ “ ’ ∀x A, ∆
where a does not occur in the conclusion.
2 For this reason, LG is sometimes called a sequent calculus.
47
Exercise 3.4.7. Explicitly display the remaining inference rules of LG.
De¬nition 3.4.8. A sequent A1 , . . . , Am ’ B1 , . . . , Bn is said to be logically
valid if and only if the LV sentence
(A1 & · · · & Am ) ’ (B1 ∨ · · · ∨ Bn )
is logically valid.
Theorem 3.4.9 (soundness and completeness of LG). LG is sound and
complete. In other words, a sequent “ ’ ∆ is logically valid if and only if it is
derivable in LG. In particular, an LV sentence A is logically valid if and only
if the sequent