premises of both and put them into a single list above the Fitch

bar. Then we follow the Fitch bar with the steps from the proof of

R, followed by the steps from the proof of S. The citations in these

steps need to be renumbered, but other than that, the result is a

legitimate proof in FT . At the end of this proof, we add a single step

containing R § S which we justify by § Intro. The merged proof

looks like this:

Section 17.2

474 / Advanced Topics in Propositional Logic

P1

.

.

.

Pn

Q1

.

.

.

Qk

.

.

.

R

.

.

.

S

R§S

We now turn to (2). One half of this, the direction from right to

left, is very easy, using the rule of ∨ Intro, so let™s prove the other

direction. Thus, we want to show that if T T (R ∨ S) then T T R or

T T S. (This is not true in general, but it is for formally consistent,

formally complete sets.)

Assume that T T (R ∨ S), but, toward a proof by contradiction,

that T T R and T T S. Since T is formally complete, it follows

that T T ¬R and T T ¬S. This means that we have two formal

proofs p1 and p2 from premises in T , p1 having ¬R as a conclusion,

p2 having ¬S as a conclusion. As we have seen, we can merge these

two proofs into one long proof p that has both of these as conclusions.

Then, by § Intro, we can prove ¬R § ¬S. But then using the proof of

the version of DeMorgan from Exercise 25, we can extend this proof

to get a proof of ¬(R ∨ S). Thus T T ¬(R ∨ S). But by assumption

we also have T T (R ∨ S). By merging the proofs of ¬(R ∨ S) and

R ∨ S we can get a proof of ⊥ by adding a single step, justi¬ed by ⊥

Intro. But this means that T is formally inconsistent, contradicting

our assumption that it is formally consistent.

One direction of part (3) follows immediately from the de¬nition of

formal completeness, while the left to right half follows easily from

the de¬nition of formal consistency.

Parts (4) and (5) are similar to part (2) and are left as an exercise.

With this lemma in hand, we can now ¬ll in the ¬rst step in our outline.

Chapter 17

Completeness for propositional logic / 475

Proposition 4. Every formally consistent, formally complete set of sentences

is tt-satis¬able.

Proof: Let T be the formally consistent, formally complete set of

sentences. De¬ne an assignment h on the atomic formulas of the

language as follows. If T T A then let h(A) = true; otherwise let

h(A) = false. Then the function ˆ is de¬ned on all the propositional

h

formulas of our language. We claim that:

for all w¬s S, ˆ

h(S) = true if and only if T S.

T

The proof of this is a good example of the importance of proofs by

induction on w¬s. The claim is true for all atomic w¬s from the way

ˆ

that h is de¬ned, and the fact that h and h agree on atomic w¬s.

We now show that if the claim holds of w¬s R and S, then it holds

of (R § S), (R ∨ S), ¬R, (R ’ S) and (R ” S). These all follow easily

from Lemma 3. Consider the case of disjunction, for example. We

ˆ

need to verify that h(R ∨ S) = true if and only if T T (R ∨ S). To

prove the “only if” half, assume that ˆ ∨ S) = true. Then, by the

h(R

de¬nition of ˆ either h(R) = true or ˆ

ˆ

h, h(S) = true or both. Then,

by the induction hypothesis, either T T R or T T S or both. But

then by the lemma, T T (R ∨ S), which is what we wanted to prove.

The other direction is proved in a similar manner.

From the fact that we have just established, it follows that the as-

signment h makes every sentence provable from T true. Since every

sentence in T is certainly provable from T , by Reit if you like, it fol-

lows that h makes every sentence in T true. Hence T is tt-satis¬able,

which is what we wanted to prove.

Extending to formally complete sets of sentences

The next step in our proof of completeness is to ¬gure out a way to get from

formally consistent sets of w¬s to sets of w¬s that are both formally consistent

and formally complete. The next lemma shows us that this is not as hard as

it may seem at ¬rst.

Lemma 5. A set of sentences T is formally complete if and only if for every

atomic sentence A, T T A or T T ¬A.

Proof: The direction from left to right is just a consequence of the

de¬nition of formal completeness. The direction from right to left

Section 17.2

476 / Advanced Topics in Propositional Logic

is another example of a proof by induction on w¬s. Assume that

T T A or T T ¬A for every atomic sentence A. We use induction

to show that for any sentence S, T T S or T T ¬S. The basis of

the induction is given by our assumption. Let™s prove the disjunction

case. That is, assume S is of the form P ∨ Q. By our inductive hy-

pothesis, we know that T settles each of P and Q. If T proves either

one of these, then we know that T T P ∨ Q by ∨ Intro. So suppose

that T T ¬P and T T ¬Q. By merging these proofs and adding a

step, we get a proof of ¬P § ¬Q. We can continue this proof to get

a proof of ¬(P ∨ Q), showing that T T ¬S, as desired. The other

inductive steps are similar.

We can now carry out the second step in our outline of the proof of the

Completeness Theorem.

Proposition 6. Every formally consistent set of sentences T can be ex-

panded to a formally consistent, formally complete set of sentences.

Proof: Let us form a list A1 , A2 , A3 , . . . , of all the atomic sentences

of our language, say in alphabetical order. Then go through these

sentences one at a time. Whenever you encounter a sentence Ai such

that neither Ai nor ¬Ai is provable from the set, add Ai to the set.

Notice that doing so can™t make the set formally inconsistent. If you

could prove ⊥ from the new set, then you could prove ¬Ai from the

previous set, by Lemma 2. But if that were the case, you wouldn™t

have thrown Ai into the set.

The end result of this process is a set of sentences which, by the

preceding lemma, is formally complete. It is also formally consistent;

after all, any proof of ⊥ is a ¬nite object, and so could use at most

a ¬nite number of premises. But then it would a proof of ⊥ at some

stage of this process, when all those premises had been thrown in.

Putting things together

Just for the record, let™s put all this together into a proof of the Completeness

Theorem for FT .

Proof: Suppose T T S. Then by Lemma 2, T ∪ {¬S} is formally

consistent. This set can be expanded to a formally consistent, for-

mally complete set, which by our ¬rst proposition is tt-satis¬able.

Suppose h is a truth value assignment that satis¬es this set. Clearly,

Chapter 17

Completeness for propositional logic / 477

h makes all the members of T true, but S false, showing that S is

not a tautological consequence of T .

There is an interesting and logically important consequence of the Com-

pleteness Theorem, known as the Compactness Theorem. We state it as fol-

lows:

Theorem (Compactness Theorem for Propositional Logic) Let T be any set Compactness Theorem

of sentences of propositional logic. If every ¬nite subset of T is tt-satis¬able,

then T itself is tt-satis¬able.

Proof: We prove the contrapositive of the claim. Assume that T is

not tt-satis¬able. Then by the Completeness Theorem, the set T is

not formally consistent. But this means that T T ⊥. But a proof of

⊥ from T can use only ¬nitely many premises from T . Let P1 , . . . , Pn

be these premises. By the Soundness Theorem, P1 , . . . , Pn are not

tt-satis¬able. Consequently, there is a ¬nite subset of T that is not

tt-satis¬able.

Remember

1. The Completeness Theorem is proven by showing that every formally

consistent set T of sentences is tt-satis¬able. This is done in two steps.

2. The ¬rst step is to show the result for sets T which are also formally

complete.

3. The second step is to show how to extend any formally consistent set

to one that is both formally consistent and formally complete.

Exercises

17.4 Consider the following set T :

‚

{(A § B) ’ ¬A, C ∨ A, ¬A ’ A, B}

The Fitch ¬les Exercise 17.4A and Exercise 17.4B contain proofs showing that T T ¬A and

T T ¬¬A. Take these two proofs and merge them into a third proof showing that T T ⊥.

Submit the merged proof as Proof 17.4.

Section 17.2

478 / Advanced Topics in Propositional Logic

For the following three exercises, suppose our language contains only two predicates, Cube and Small,

two individual constants, a and b, and the sentences that can be formed from these by means of the

truth-functional connectives.

17.5 Let T be the following set of sentences:

{¬(Cube(a) ∨ Small(a)), Cube(b) ’ Cube(a), Small(a) ∨ Small(b)}

Show that this set is formally consistent and formally complete. To prove the former, you

will have to appeal to the Soundness Theorem. To prove the latter, you will want to refer to

Lemma 5.

17.6 Let T again be the following set of sentences:

{¬(Cube(a) ∨ Small(a)), Cube(b) ’ Cube(a), Small(a) ∨ Small(b)}

By Proposition 4, there is a truth assignment h making all these sentences true. What values

does h assign to each of the atomic sentences of the language?

17.7 This time let T be the following set of sentences (note the di¬erence in the ¬rst sentence):

‚|

{¬(Cube(a) § Small(a)), Cube(b) ’ Cube(a), Small(a) ∨ Small(b)}

This set is not formally complete. Use the procedure described in the proof of Proposition 6 to

extend this to a formally consistent, formally complete set. (Use alphabetical ordering of atomic

sentences.) What is the resulting set? What is the truth value assignment h that satis¬es this

set? Submit a world making the sentences in your formally complete set true.

17.8 Suppose our language has an in¬nite number of atomic sentences A1 , A2 , A3 , . . .. Let T be the

following set of sentences:

{A1 ’ A2 , A2 ’ A3, A3 ’ A4 , . . .}

There are in¬nitely many distinct truth value assignments satisfying this set. Give a general

description of these assignments. Which of these assignments would be generated from the

procedure we used in our proof of the Completeness Theorem?

Each of the following four exercises contains an argument. Classify each argument as being (A) provable

in FT , (B) provable in F but not in FT , or (C) not provable in F . In justifying your answer, make

explicit any appeal you make to the Soundness and Completeness Theorems for FT and for F. (Of