71

associated with T are primitive recursive. Introduce the provability predicate

PvblT by de¬nition:

PvblT (x) ” ∃y Prf T (x, y) .

Note that, for all L-sentences B, PvblT (#(B)) is true if and only if T B.

Lemma 6.5.2 (derivability condition 1). For any L-sentence A, if T A

then

PRA PvblT (#(A)) .

Proof. Suppose T A. Let p be a proof of A in T . Then we have Prf T (#(A), #(p)).

Since Prf T (x, y) is a primitive recursive predicate, it follows by Theorem 6.1.2

that PRA Prf T (#(A), #(p)). Hence PRA PvblT (#(A)), q.e.d.

Lemma 6.5.3 (derivability condition 2). For any L-sentence A, we have

PvblT (#(A)) ’ PvblPRA (#(PvblT (#(A)))) .

PRA

Proof. This is just Lemma 6.5.2 formalized in PRA. The details of the formal-

ization are in Section 6.7.

Lemma 6.5.4 (derivability condition 3). For any L-sentences A and B, we

have

PvblT (#(A ’ B)) ’ (PvblT (#(A)) ’ PvblT (#(B))) .

PRA

Proof. This is a straightforward consequence of the fact that our rules of infer-

ence include modus ponens.

6.6 The Incompleteness Theorems

In this section, let T be a theory which is primitive recursively axiomatizable

and includes PRA. For example, T could be PRA itself, or it could be an

appropriate de¬nitional extension of Z1 or Z2 or ZFC. As in Section 6.5, let

PvblT be a provability predicate for T .

Lemma 6.6.1. Let A(x) be a PRA-formula with one free variable x. Then we

can ¬nd a PRA-sentence B such that PRA B ” A(#(B)).

Proof. This is the Self-Reference Lemma 6.4.1 specialized to PRA.

Lemma 6.6.2. We can ¬nd a PRA-sentence S such that

S ” ¬ PvblT (#(S)) .

(—) PRA

Note that S is self-referential and says “I am not provable in T .”

Proof. This is an instance of Lemma 6.6.1 with A(x) ≡ ¬ PvblT (x).

72

Lemma 6.6.3. Let S be as in Lemma 6.6.2. If T is consistent, then T S.

Proof. Suppose for a contradiction that T S. By Lemma 6.5.2 we have

PRA PvblT (#(S)). Hence by (—) it follows that PRA ¬ S. Since T includes

PRA, we have T ¬ S. Thus T is inconsistent.

Theorem 6.6.4 (the First Incompleteness Theorem). If T is consistent,

then we can ¬nd a sentence S in the language of ¬rst order arithmetic such

that S is true yet S is not a theorem of T .

Proof. Let S be a PRA-sentence as in Lemma 6.6.2. By Lemma 6.6.3, T S.

It follows by (—) that S is true. As in Section 6.2, let S be the translation of S

into the language of ¬rst order arithmetic. Thus S is also true. By the results

of Section 6.2, PRA S ” S . Hence T S ” S . Hence T S .

Assume now that the primitive recursive predicate AxT has been chosen

∀x (AxPRA (x) ’ AxT (x)). It follows that PRA

in such a way that PRA

∀x (PvblPRA (x) ’ PvblT (x)). In particular we have:

Lemma 6.6.5. For all PRA-sentences A, we have

PvblPRA (#(A)) ’ PvblT (#(A)) .

PRA

De¬nition 6.6.6. ConT is de¬ned to be the sentence ¬ PvblT (#(F)). Here F

is the identically false sentence. Note that ConT is a PRA-sentence which asserts

the consistency of T .

Theorem 6.6.7 (the Second Incompleteness Theorem). If T is consistent,

then T ConT .

Proof. Let S be as in Lemma 6.6.2. By Theorem 6.6.4 we have T S. Therefore,

to show T ConT , it su¬ces to show T ConT ’ S. Since T includes PRA, it

su¬ces to show PRA ConT ’ S. By (—) it su¬ces to show

ConT ’ ¬ PvblT (#(S)) .

(——) PRA

But this is just Lemma 6.6.3 formalized in PRA.

Details: We need to prove (——). Reasoning in PRA, suppose PvblT (#(S)).

By Lemma 6.5.3 we have PvblPRA (#(PvblT (#(S)))). Moreover, from (—) and

Lemma 6.5.2 we have PvblPRA (#(S ” ¬ PvblT (#(S)))). Hence by Lemmas

6.5.2 and 6.5.4 we have PvblPRA (#(¬ S)). By Lemma 6.6.5 it follows that

PvblT (#(¬ S)). Hence by Lemmas 6.5.2 and 6.5.4 it follows that PvblT (#(F)),

i.e., ¬ ConT . This completes the proof.

S ” ConT .

Exercise 6.6.8. Show that PRA

6.7 Proof of Lemma 6.5.3

FIXME Write this section!

73

Bibliography

[1] Neil D. Jones and Alan L. Selman. Turing machines and the spectra of

¬rst-order formulas. Journal of Symbolic Logic, 39:139“150, 1974.

[2] Raymond M. Smullyan. First-Order Logic. Dover Publications, Inc., 1995.

XII + 158 pages.

[3] Alfred Tarski. Introduction to Logic and to the Methodology of Deductive

Sciences. Oxford University Press, New York, 4th edition, 1994. XXII +

229 pages.

74

Index

arity, 19, 57, 62 free variable, 20

assignment, 5

Gentzen-style proof system, 47

atomically closed, 33

G¨del number, 67

o

atomic formula, 3, 19, 58, 63

graph, 17

binary, 3 group, 61

block tableau, 45

Hilbert-style proof system, 38

modi¬ed, 48

Hintikka™s Lemma, 14, 30

bound variable, 20

identity, 64

Church™s Theorem, 40

identity axioms, 53, 61, 64

clause, 9

identity predicate, 53

closed, 13, 30

immediate extension, 10, 26

atomically, 33

immediate predecessor, 15

co¬nite, 55

immediate successor, 15

Compactness Theorem, 54

interpolation, 49, 51

companion, 39, 40

interpretable, 66

completeness, 39