Paradoxes as Analogues
to Gödel's Second
Incompleteness Theorem⁽¹⁾

As Löb's paradox was uncovered by L.Henkin as an analogue to Löb's theorem, paradoxes as analogues to Gödel's Second Incompleteness Theorem are derived in this paper from an inconsistent set of sentences arising from Gödel's Second Incompleteness Theorem.

As the proof of Gödel's Second Theorem (G2) is largely a formalization of the proof of Gödel's First Theorem (G1), G2 might be said to have provided G1 a cross check on proposed consistency proofs, despite Gödel's remark on the irrelevance of G2 to any sensible consistency problem - "if Con(F) is in doubt, why should it proved in F and not in an incomparable system?" [KREISEL].

Since Löb's announcement of his solution to Henkin's problem ([LÖB54], [LÖB55]) there has been successful and fruitful research on provability logic tied up with modal logic. Löb's theorem (LT) is of far-reaching significance in the metamathematical and philosophical sense. In particular, LT plus some additional properties of the modal box r standing for provability axiomatize completely provability logic theory. Thus, the proofs of the provable equivalence between G2 and LT show that G2 is of central importance for the topic of formal provability.

Corresponding to LT, Henkin discovered Löb's paradox underlying the sentence j such that the biconditional ( j « Pr ( é j ů) ® y). As Löb's paradox can be viewed as an analogue to LT, what can be the paradox(es) as analogue(s) to G2? (i.e., any paradox to which G2 bears the relation that LT bears to Löb's paradox). In view of the provable equivalence between LT and G2, must the answer be just Löb's paradox? The present paper will be devoted to answering these questions.

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.

" ~ Con( S)" stands for S is not consistent.

next page

contents

We start with

Definition 1

(1) é ů is the Gödel numbering that carries formulas to formal numerals.

(2) Á ş ( 0 = f 0) 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) Con ş ~ Pr (  é Á ů)

For all the statements below, Pr(x) is assumed to be a standard provability predicate.

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

In the following, S is assumed to be a consistent formal system extending Peano arithmetic.

previous page

next page

contents

Lemma 4 The following set of sentences are inconsistent.

I. S Ă Con

II. (Adequacy)

III. (Conditionalization)

IV. (Formal Adequacy)

V. $ F [ S Ă F « (Pr (  é F ů) ® Á)]

Proof By G2

Remark 5 Replacing Pr(x) in previous Lemma with another provability predicate B(x) (interpreted as general derivability) and renumbering each sentence in Lemma 4 with the symbol " ' ", we obtain another inconsistent set of sentences I', II', III', IV', V'.

Theorem 6 " F [ S Ă ( F « ~ B( F)) ® S Ă B(B( F)) Ů B( ~B( F))]

Proof

(1) F « ~ B( F) « (B( F) ® Á ) ; V' (i.e., Gödel's diagonal method for constructing F)

(2) B( F « (B( F) ® Á)) ; II', (1)

(3) B( F) ® B(B( F) ® Á) ; III', (2)

(4) B( F) ® B(B( F)) ; IV'

(5) B(B( F) ® Á) ® (B(B( F)) ® B( Á)) ; III'

(6) B( F) ® B( Á) ; M.P., (3), (5), (4)

(7) B ( ~ B ( Á) ® ~ B( F)) ; contrapositive of (6), II'

(8) B( ~B( F)) ; M.P., I', III', (7)

(9) B( F) ; (1), II', III', (8), M.P.

(10) B(B( F)) ; M.P., (4), (9)

Furthermore we obtain:

Theorem 7 There exists a paradox underlying F such that F « (B( F) ® Á ).

Proof Replacing B(x) in the biconditional F « (B( F) ® Á) with Tarski's truth predicate Tr(x) and invoking Convention T, we have F « ( F ® Á). If F is true, F is false. If F is false, F is true.

previous page

next page

contents

Note 8 Convention T, also called Tarski paradigm, says that for any sentence F of a formal language, the biconditional ( Tr (  é F ů) « F ) is true. We may phrase this generally: the account must yield everything of the form ( S is true iff p ) where for p we substitute a sentence and for S a name of that sentence.

Remark 9 (i) By replacing standard provability predicate with general derivability, a paradox as an analogue to G2 has been found in Theorem 6, and this should shed new light on somewhat different phenomena of G2 as the paradigm in different logic system.

(ii) The paradox in Theorem 6 differs from the Liar paradox viewed as an analogue to G1, just like 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 ů)].

References

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

[KREISEL-LÉVY] 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.

[KRIPKE] Kripke, S. (1967) A talk at UCLA Set Theory Meeting 1967

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

[LÖB55] Löb, M.H. (1955) Solution of a problem of Leon Henkin, in: Journal of Symbolic Logic 20 (1955), 115-118.

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

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 their hospitality.

AMS Subject Classifications: 03A05

previous page

contents