Some Equivalents
of Löb's Theorem⁽¹⁾

Further to the proofs (due to Kripke/Smorynski and Kreisel/Lévy) of the provable equivalence between Löb's Theorem and Gödel's Second Incompleteness Theorem, the provable equivalence of Löb's Theorem and some other sentences involving a standard and/or faithful provability predicate is established in this paper.

Since Löb's announcement of his solution to Henkin's problem [Löb (1954,1955)] there has been successful and fruitful research on provability logic tied up with modal logic. Specifically, Löb's Theorem is of far-reaching significance in the following meta-mathematical and philosophical sense.

1. Löb's Theorem plus some additional properties of the modal box r standing for provability axiomatize completely provability logic theory - cf. [Solovay (1976,1985)] for details.

2. Corresponding to this Theorem, Henkin discovered Lob's paradox underlying the sentence j with the biconditional ( j « (Pr ( é j ů) ® y)).

3. Transcending Gödel's Second Incompleteness Theorem, Löb's Theorem as the solution to Henkin's problem and to the more general problem characterizes those instances of faithfulness provable in the theory as those trivially so provable - cf. [Smorynski, C. (1991)].

As the proof of Gödel's Second Theorem is largely a formalization of the proof of Gödel's First Theorem, the Second Theorem might be said to have provided the first a cross check on proposed consistency proofs, despite Gödel's remark on the irrelevance of his Second Theorem to any sensible consistency problem. (As G.Kreisel in [Kreisel(1993)] cited: if Con(F) is in doubt, why should it be proved in F and not in an incomparable system ?) The proofs of the provable equivalence between Gödel's Second Theorem and Löb's Theorem and the significant aspect #1 above of Löb's Theorem show that Gödel's Second Theorem is of central importance for the topic of formal provability.

The present paper will be devoted to establishing the provable equivalence of Löb's Theorem and some other propositions involving Gödel's standard provability conditions with or without Faithfulness condition.

First however, we comment on notations. For the most part, our notation will be that commonly employed in mathematical logic. We write "F Ă S" to mean that S is a theorem of F. " w -Con( S)" stands for S is w -consistent.

next page

contents

Definition 1 (1) w = {0,1,2,...}

(2) Á ş_df (0 = f0) denoting logical falsehood, where f is successor function.

(3) Following Gödel's procedure, a S₁ formula Pr(x) (from "provable") can be constructed and be called a standard provability predicate iff it satisfies the following conditions (for all sentences A and B)

(Adequacy) Ă A ® Ă Pr (   é A ů)

(Conditionalization) Ă Pr( é A ® B ů) ® [Pr( é A ů) ® Pr( é B ů)]

(Formal Adequacy) Ă Pr (  é A ů) ® Pr (  é Pr (   é A ů) ů)

(4) Condition: (Faithfulness) For any sentence A, Ă Pr (  é A ů) ® Ă A.

Some authors call this condition reflection or soundness.

(5) Con ş_df ~ Pr (  é Á ů)

Unless otherwise specified, let Pr(x) be a standard provability predicate. The notation of the underlying axiomatic theory in question will be sometimes omitted when it is clear in the context.

Fact 2 ([KREISEL-LÉVY]) LT ® G2 (Löb's theorem implies Gödel's Second Theorem)

Proof G2 is the special case of LT: Ă (Pr (  é A ů ) ® A) ® Ă A, when A ş Á

Fact 3 ([KRIPKE],[SMORYNSKI]) G2 ® LT

Proof Let S be any formal system adequate for recursive number theory.

(1) S ŘĂ Y

(2) S + ~ Y : consistent

(3) S + ~ Y ŘĂ Con( S + ~ Y) ;G2

(4) S + ~ Y ŘĂ ~ Pr (  é ~ Y ® 0_ = 1_ ů )

(5) S + ~ Y ŘĂ ~ Pr (  é Y ů )

(6) S ŘĂ ( ~ Y ® ~ Pr (  é Y ů)) ;deduction theorem

(7) S ŘĂ Pr (  é Y ů) ® Y

Theorem 4 G2 + Faithfulness ® G1 (Gödel's First Incompleteness Theorem)

previous page

next page

contents

Proof (1) ( S ŘĂ Con ) " G ( S Ă G S Ă ~G ) ; G2 ~G1.

(2) S Ă Pr (  é Á ů) ; (1)

(3) S Ă Á ; Faithfulness

(4) S Ă Con ; Ă Á ® Ă A , for any A

Theorem 5 LT « "i=0,1 "j=0,1 (F_i: a formula Ă(Pr( éF_i ů) ®F_j) Ă(Pr( éF_j ů) ®F_i) ® ĂF_i)

Proof (®)

(1) Ă Pr( éF_i ů) ® F_j

(2) Ă Pr( éF_j ů) ® F_i

(3) Ă Pr( éF_i F_j ů) « Pr( éF_i ů) Pr( éF_j ů)

(4) Ă Pr( éF_i F_j ů) ® F_i F_j ; (1) ,(2) ,(3)

(5) Ă F_i F_j ; LT

(6) Ă F_i Ă F_j (for all i & j = 0,1)

(¬) Special case when for all i & j = 0,1 , F_i = F_j

Lemma 6 " G ( Ă « ~ Pr( é G ů ) ® Ă Con « G )

Proof (1) Ă Á ® G, for all G

(2) Ă (Pr ( é Á ů) ® Pr ( é G ů) ; Adequacy and Conditionalization

(3) Ă ( ~Pr ( é G ů) ® Con

(4) Ă G ® Con

(5) Ă (Pr ( é G ů) ® ~G ; Definition of G

(6) Ă (Pr ( é (Pr ( é G ů) ů) ® Pr ( é ~G ů); Adequacy and Conditionalization

(7) Ă Pr ( é G ů) ® (Pr ( é (Pr ( é G ů) ů); Formal Adequacy

(8) Ă (Pr ( é G ů)) ® Pr ( é ~G ů) ; (6), (7)

(9) Ă (Pr ( é G ů) ® ~Con ; ĂCon ® ~[Pr( é G ů) Ů Pr( é ~G ů)]

(10) Ă Con ® G

previous page

next page

contents

Remark 7 (i) Any sentence asserting its own unprovability in the theory is a consistency sentence. The Gödel sentence is of this form.

(ii) Since its existential generalization is a consistency sentence, then it at least entails a consistency sentence; and vice versa.

(iii) Any two Gödel sentences are provably equivalent, just like any two Henkin's sentences.

For all the statements below, let G be the Gödel sentence and let Pr(x) satisfy the three conditions of a standard provability predicate and Faithfulness condition. The resulting axiomatic theory in question will be denoted by S.

Theorem 8 LT ® ( w -Con( S) ® S ŘĂ (Con ® ~Pr( é ~G ů)))

Proof (1) Ă Con ® Pr ( é ~G ů) ; assumption

(2) Ă G ® ~Pr ( é ~G ů) ; Lemma 6

(3) Ă Pr( é ~G ů) ® ~G ; contrapositive

(4) Ă ~G ; LT

(5) S : w -consistent ;G1 by Theorem 4 (using Faithfulness)

Theorem 9 [ w -Con( S) ® S ŘĂ Con ® ~ Pr( é ~G ů)] ®

w -Con( S) ® S ŘĂ Pr( é (Pr( é G ů ) ů) ® Pr( é G ů)]

Proof (1) w -Con( S) ; assumption

(2) S + {Con} ŘĂ ~Pr ( é ~G ů) ;deduction th., hypothesis

(3) Pr( é (Pr( é G ů ) ů) ® Pr( é G ů)] « ~Pr( é ~G ů) Pr( é G ů)] «

« ~Pr( é ~G ů) « ~G) ;Definitions of G

(4) S+{Con} ŘĂPr( é(Pr( é G ů) ů) ® Pr( é G ů) ; (2), (3)

(5) S ŘĂPr( é (Pr( é G ů) ů) ® Pr( é G ů) ; (4)

previous page

next page

contents

Note that the hypothesis w -Con( S) of the right-hand sentence in Theorem 8 and Theorem 9 can be weakened to Con( S).

Theorem 10 w -Con( S) ® S Ă Pr( é (Pr( é G ů) ů) ® Pr( é G ů) ® G1

Proof Straightforward from the rightmost « in proof step (3) of Theorem 9

Thus we have established:

Corollary 11 The following are equivalent in S:

1. LT

2. "i=0,1 "j=0,1 (F_i: a formula Ů Ă(Pr( éF_i ů) ®F_j) Ů Ă(Pr( éF_j ů) ®F_i) ® ĂF_i)

3. w -Con( S) ® S ŘĂ Con ® ~Pr( é ~G ů)

4. w -Con( S) ® S ŘĂ Pr( é (Pr( é G ů) ů) ® Pr( é G ů)

5. G1

6. G2

Proof Theorem 5, Theorem 8 (using Faithfulness indirectly), Theorem 9, Theorem 10, and Fact 3. G2 is a consequence of G1 under our assumption stated right before Theorem 8.

Remark 12 (i) It is to note the provable equivalence between G1 and G2 in the underlying theory in question, even if G2 differs from G1 in the subtlety of what it says. For much depends on what we take to be a formal statement of the consistency of the system, e.g., requiring that Pr(x) be a standard provability predicate or not (e.g., lacking Formal Adequacy) and that the formal consistency statement Con satisfy the condition: for all sentences A, Ă Con ® ~[Pr ( é A ů) Ů
Pr ( é ~ A ů)]

(ii) If we do not assume Pr(x) to be S₁ then Corollary 11 does not hold, for e.g., for Feferman's P₁ binumeration of axioms of Peano Arithmetic the resulting Pr(x) satisfies our conditions for a standard proof predicate, the corresponding G1 is true (both G and ~G is unprovable) but G2 is false (Con is provable).

previous page

next page

contents

REFERENCES

1. Kreisel,G.(1993) About Logic and Logicians, volume II: Mathematics, A palimpsest of essays by Georg Kreisel, selected and arranged by Piergiorgio Odifreddi, Manuscript.

2. Kreisel, G. Lövy,A (1968) Reflection principles and their use for establishing the complexity of axiomatic systems, in: Z. für. math. Logik und Grundlagen der Mathematik 14 (1968) 97-142.

3. Kripke,S.(1967) A talk at UCLA Set Theory Meeting 1967

4. Löb, M.H.(1954) Solution of a problem by Leon Henkin, in: [Proc.ICM 1954] 405-406.

5. Löb, M.H.(1955) Solution of a problem of Leon Henkin, in: J.Symbolic Logic 20 (1955) 115-118.

6. Smorynski,C.(1977) The incompleteness theorems, in: Handbook of mathematical logic, Amsterdam-New York-Oxford (NHP)1977

7. Smorynski,C.(1991) The development of self-reference. Löb's theorem, manuscript.

8. Solovay,R.M.(1976) Provability interpretations of modal logic, Israel J.Math.25, 287-304.

9. Solovay,R.M.(1985) Explicit Henkin sentences, J.Symbolic Logic, 50, 91-93

NOTES

1. I would like to acknowledge DAAD grant. I also would like to thank the logicians at the University of Bonn as well as Otto Wilhelms Carls for discussions that inspired me to write this paper during the Summer 1993.

AMS Subject Classifications: 03A05, 03F50

previous page

contents