See also (i) this later publication by Sebastian Grève, where he concludes that “… while Gödel indeed showed some significant understanding of Wittgenstein here, ultimately, Wittgenstein perhaps understood Gödel better than Gödel understood himself”; and (ii) this note on Rosser’s Rule C and Wittgenstein’s objections on purely philosophical considerations to Gödel’s reasoning and conclusions, where we show that, although not at all obvious (perhaps due to Gödel’s overpoweringly plausible presentation of his interpretation of his own formal reasoning over the years) what Gödel claimed to have proven is not—as suspected and held by Wittgenstein—supported by Gödel’s formal argumentation.

A: Misunderstanding Gödel’s Theorems VI and XI: Incompleteness and Undecidability

In an informal essay, “Misunderstanding Gödel’s Theorems VI and XI: Incompleteness and Undecidability“, DPhil candidate Sebastian Grève at The Queen’s College, Oxford, attempts to come to terms with what he subjectively considers:

“… has not been properly addressed as such by philosophers hitherto as of great philosophical importance in our understanding of Gödel’s Incompleteness Theorems.”

Grève’s is an unusual iconoclastic perspective:

“This essay is an open enquiry towards a better understanding of the philosophical significance of Gödel’s two most famous theorems. I proceed by a discussion of several common misunderstandings, led by the following four questions:

1) Is the Gödel sentence true?

2) Is the Gödel sentence undecidable?

3) Is the Gödel sentence a statement?

4) Is the Gödel sentence a sentence?

Asking these questions in this order means to trace back the steps of Gödel’s basic philosophical interpretation of his formal results. What I call the basic philosophical interpretation is usually just taken for granted by philosopher’s writing about Gödel’s theorems.”

In a footnote Grève acknowledges Wittgenstein’s influence by suggesting that:

“This essay can be read as something like a free-floating interpretation of the theme of Wittgenstein’s remarks on Gödel’s Incompleteness Theorems in Wittgenstein: 1978[RFM], I-(III), partly following Floyd: 1995 but especially Kienzler: 2008, and constituting a reply to inter alia Rodych: 2003”.

B: Why we may see the trees, but not the forest

We note that Grève’s four points are both overdue and well-made:

1. Is the Gödel sentence true?

Grève’s objection that standard interpretations are obscure when they hold the Gödel sentence as being intuitively true deserves consideration (see this post).

The ‘truth’ of the sentence should and does—as Wittgenstein stressed and suggested—follow objectively from the axioms and rules of inference of arithmetic.

2. Is the Gödel sentence undecidable?

Grève’s observation that the ‘undecidability’ of the Gödel sentence conceals a philosophically questionable assumption is well-founded.

The undecidability in question follows only on the assumption of ‘\omega-consistency’ made explicitly by Gödel.

This assumption is actually logically equivalent to the philosophically questionable assertion that from the provability of [\neg(\forall x)R(x)] we may conclude the existence of some numeral [n] for which [R(n)] is provable.

Since Rosser’s proof implicitly makes this assumption by means of his logically questionable Rule C, his claim of avoiding omega-consistency for arithmetic is illusory.

3. Is the Gödel sentence a statement?

Grève rightly holds that the Gödel sentence should be treated as a valid statement within the formal arithmetic S, since it is structurally defined as a well-formed formula of S.

4. Is the Gödel sentence a sentence?

Grève’s concern about whether the Gödel sentence of S is a valid arithmetical proposition under interpretation also seems to need serious philosophical consideration.

It can be argued (see the comment following the proof of Lemma 9 of this preprint) that the way the sentence is formally defined as the universal quantification of an instantiationally (but not algorithmically) defined arithmetical predicate does not yield an unequivocally defined arithmetical proposition in the usual sense under interpretation.

In this post [*] we shall not only echo Grève’s disquietitude, but argue further that Gödel’s interpretation and assessment of his own formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions is, essentially, a post-facto imposition that continues to influence standard expositions of Gödel’s reasoning misleadingly.

Feynman’s cover-up factor

Our thesis is influenced by physicist Richard P. Feynman, who started his 1965 Nobel Lecture with a penetrating observation:

We have a habit in writing articles published in scientific journals to make the work as finished as possible, to cover up all the tracks, to not worry about the blind alleys or describe how you had the wrong idea first, and so on. So there isn’t any place to publish, in a dignified manner, what you actually did in order to get to do the work.

That such `cover up’ may have unintended—and severely limiting—consequences on a discipline is suggested by Gödel’s interpretation, and assessment, of his own formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions (Go31).

Thus, in his informal preamble to the result that he intended to prove formally, Gödel wrote (cf. Go31, p.9):

The analogy of this result with Richard’s antinomy is immediately evident; there is also a close relationship with the Liar Paradox … Thus we have a proposition before us which asserts its own unprovability.

Further, interpreting the significance of his formal reasoning as having established the existence of a formally undecidable arithmetical proposition that is, however, decidable by meta-mathematical arguments, Gödel noted that:

The precise analysis of this remarkable circumstance leads to surprising results concerning consistency proofs of formal systems … (Go31, p.9)

The true reason for the incompleteness which attaches to all formal systems of mathematics lies, as will be shown in Part II of this paper, in the fact that the formation of higher and higher types can be continued into the transfinite (c.f., D. Hilbert, `Über das Unendliche’, Math. Ann. 95, p. 184), while, in every formal system, only countable many are available. Namely, one can show that the undecidable sentences which have been constructed here always become decidable through adjunction of suitable high types (e.g. of the type \omega to the system P. A similar result also holds for the axiom systems of set theory. (Go31, p.28, footnote 48a)

The explicit thesis of this foundational paper is that the above interpretation is an instance of a `cover up’—in Feynman’s sense—which appears to be a post-facto imposition that, first, continues to echo in and misleadingly [1] influence standard expositions of Gödel’s reasoning when applied to a first-order Peano Arithmetic, PA, and, second, that it obscures the larger significance of the genesis of Gödel’s reasoning.

As Gödel’s various remarks in Go31 suggest, this possibly lay in efforts made at the dawn of the twentieth century—largely as a result of Brouwer’s objections (Br08)—to define unambiguously the role that the universal and existential quantifiers played in formal mathematical reasoning.

That this issue is critical to Gödel’s reasoning in Go31, but remains unresolved in it, is obscured by his powerful presentation and interpretation.

So, to grasp the underlying mathematical significance of Gödel’s reasoning, and of what he has actually achieved, one may need to avoid focusing (as detailed in the previous posts on A foundational perspective on the semantic and logical paradoxes; in this post on undecidable Gödelian propositions, and in this preprint on undecidable Gödelian propositions):

\bullet on the analogy of the so-called `Liar paradox’;

\bullet on Gödel’s interpretation of his arithmetical proposition as asserting its own formal unprovability in his formal Peano Arithmetic P (Go31, pp.9-13);

\bullet on his interpretation of the reasons for the `incompleteness’ of P; and

\bullet on his assessment and interpretation of the formal consequences of such `incompleteness’.

We show in this paper that, when applied to PA [2], all of these obscure the deeper significance of what Gödel actually achieved in Go31.

C: Hilbert: If the \omega -Rule is true, can P be completed?

Instead, Gödel’s reasoning may need to be located specifically in the context of Hilbert’s Program (cf. Hi30, pp.485-494) in which he proposed an \omega-rule as a finitary means of extending a Peano Arithmetic—such as his formal system P in Go31—to a possible completion (i.e. to logically showing that, given any arithmetical proposition, either the proposition, or its negation, is formally provable from the axioms and rules of inference of the extended Arithmetic).

Hilbert’s \omega-Rule: If it is proved that the P-formula [F(x)] interprets as a true numerical formula for each given P-numeral [x], then the P-formula [(\forall x)F(x)] may be admitted as an initial formula (axiom) in P.

It is likely that Gödel’s 1931 paper evolved out of attempts to prove Hilbert’s \omega -rule in the limited—and more precise—sense that if a formula [F(n)] is provable in P for each given numeral [n], then the formula [(\forall x)F(x)] must be provable in P.

Now, if we meta-assume Hilbert’s \omega-rule for P, then it follows that, if P is consistent, then there is no P-formula [F(x)] for which, first, [\neg(\forall x)F(x)] is P-provable and, second, [F(n)] is P-provable for any given P-numeral [n].

Gödel defined a consistent Peano Arithmetic with the above property as additionally \omega -consistent (Go31, pp.23-24).

D: The significance of \omega-consistency

To place the significance of \omega-consistency in a current perspective, we note that the standard model of the first order Peano Arithmetic PA (cf. Me64, p.107; Sc67, p.23, p.209; BBJ03, p.104) presumes [3] that the standard interpretation M of PA (under which the PA-formula [(\exists x)R(x)], which is merely an abbreviation for [\neg(\forall x)\neg R(x)] , interprets as true if, and only if, R(n) holds for some natural number n under M) is sound (cf. BBJ03, p.174).

Clearly, if such an interpretation of the existential quantifier is sound, it immediately implies that PA is necessarily \omega-consistent [4].

Since Brouwer’s main objection was to Hilbert’s presumption that such an interpretation of the existential quantifier is sound, Gödel explicitly avoided this assumption in his seminal 1931 paper (Go31, p.9) in order to ensure that his reasoning was acceptable as “constructive” and “intuitionistically unobjectionable” (Go31, p.26).

He chose, instead, to present the formal undecidability of his arithmetical proposition—and the consequences arising from it—as explicitly conditional on the assumption of the formal property of \omega-consistency for his Peano Arithmetic P under the unqualified—and, as we show below, mistaken—belief that:

PA is \omega-consistent (Go31, p.28, footnote 48a).

E: Gödel: If the \omega -Rule is true, P cannot be completed

Now, Gödel’s significant achievement in Go31 was the discovery that, if P is consistent, then it was possible to construct a P-formula, [R(x)] [5], such that [R(n)] is P-provable for any given P-numeral [n] (Go31, p.25(2)), but [(\forall x)R(x)] is P-unprovable (Go31, p.25(1)).

However, it becomes apparent from his remarks in Go31 that Gödel considered his more significant achievement the further argument that, if P is assumed \omega -consistent, then both [(\forall x)R(x)] and [\neg (\forall x)R(x)] [6] are P-unprovable, and so P is incomplete!

This is the substance of Gödel’s Theorem VI (Go31, p.24).

Although this Theorem neither validated nor invalidated Hilbert’s \omega -rule, it did imply that assuming the rule led not to the completion of a Peano Arithmetic as desired by Hilbert, but to its essential incompletability!

F: The \omega -Rule is inconsistent with PA

Now, apparently, the possibility neither considered by Gödel in 1931, nor seriously since, is that a formal sytem of Peano Arithmetic—such as PA—may be consistent and \omega inconsistent.

If so, one would ascribe this omission to the `cover up’ factor mentioned by Feynman, since a significant consequence of Gödel’s reasoning—in the first half of his proof of his Theorem VI—is that it actually establishes PA as \omega inconsistent (as detailed in Corollary 9 of this preprint and Corollary 4 of this post).

In other words, we can logically show for Gödel’s formula [R(x)] that [\neg(\forall x) R(x)] is PA-provable, and that [R(n)] is PA-provable for any given PA-numeral [n].

Consequently, Gödel’s Theorem VI is vacuously true for PA, and it also follows that Hilbert’s \omega -Rule is inconsistent with PA!

G: Need: A paradigm shift in interpreting the quantifiers

Thus Gödel’s unqualified belief that:

PA is \omega-consistent

was misplaced, and Brouwer’s objection to Hilbert’s presumption—that the above interpretation of the existential quantifier is sound—was justified; since, if PA is consistent, then it is provably \omegainconsistent, from which it follows that the standard interpretation M of PA is not sound.

Hence we can no longer interpret `[\neg(\forall x)F(x)] is true’ maximally under the standard interpretation of PA as:

(i) The arithmetical relation F(n) is not always [7] true.

However, since the theorems of PA—when treated as Boolean functions—are Turing-computable as always true under a sound finitary interpretation \beta of PA, we can interpret `[\neg(\forall x)F(x)] is true’ minimally as:

(ii) The arithmetical relation F(n) is not Turing-computable as always true.

This interpretation allows us to conclude from Gödel’s meta-mathematical argument that we can construct a PA-formula [(\forall x)R(x)] that is unprovable in PA, but which is true under a sound interpretation of PA [8] although we may now no longer conclude from Gödel’s reasoning that there is an undecidable arithmetical PA-proposition.

Moreover, the interpretation admits an affirmative answer to Hilbert’s query: Is PA complete or completeable?

H: PA is algorithmically complete

In outline, the basis from which this conclusion follows formally is that:

(i) Gödel’s proof of the essential incompleteness of any formal system of Peano Arithmetic (Go31, Theorem VI, p.24) explicitly assumes that the arithmetic is \omega -consistent;

(ii) Rosser’s extension of Gödel’s proof of the essential incompleteness of any formal system of Peano Arithmetic (cf. Ro36, Theorem II, p.233) implicitly presumes that the Arithmetic is \omega -consistent (as detailed in this post);

(iii) PA is \omegainconsistent (as detailed in Corollary 9 of this preprint);

(iv) The classical `standard’ interpretation of PA (cf. Me64, section \S 2, pp.49-53; p107) over the structure [N]—defined as {N (the set of natural numbers); = (equality); ' (the successor function); + (the addition function); \ast (the product function); 0 (the null element)}— does not define a finitary model of PA (as detailed in the paper titled Evidence-Based Interpretations of PA presented at IACAP/AISB Turing 2012, Birmingham, UK in July 2012);

(v) We can define a sound interpretation \beta of PA—in terms of Turing-computability—which yields a finitary model of PA, but which does not admit a non-standard model for PA (as detailed in this paper);

(vi) PA is algorithmically complete in the sense that an arithmetical proposition F defines a Turing-machine TM_{F} which computes F as true under \beta if, and only if, the corresponding PA-formula [F] is PA-provable (as detailed in Section 8 of this preprint).

I: Gödel’s proof of his Theorem XI does not withstand scrutiny

Since Gödel’s proof of his Theorem XI (Go31, p.36)—in which he claims to show that the consistency of his formal system of Peano Arithmetic P can be expressed as a P-formula which is not provable in P—appeals critically to his Theorem VI, it follows that this proof cannot be applied to PA.

However, we show below that there are other, significant, reasons why Gödel’s reasoning in this proof must be treated as classically objectionable per se.

J: Why Gödel’s interpretation of the significance of his Theorem XI is classically objectionable

Now, in his Theorem XI, Gödel constructs a formula [W] [9] in P and assumes that [W] translates—under a sound interpretation of P—as an arithmetical proposition that is true if, and only if, a specified formula of P is unprovable in P.

Now, if there were such a P-formula, then, since an inconsistent system necessarily proves every well-formed formula of the system, it would follow that a proof sequence within P proves that P is consistent.

However, Gödel shows that his formula [W] is not P-provable (Go31, p.37).

He concludes that the consistency of any formal system of Peano Arithmetic is not provable within the Arithmetic. [10]

K: Defining meta-propositions of P arithmetically

Specifically, Gödel first shows how 46 meta-propositions of P can be defined by means of primitive recursive functions and relations (Go31, pp.17-22).

These include:

(\#23) A primitive recursive relation, Form(x), which is true if, and only if, x is the Gödel-number of a formula of P;

(\#45) A primitive recursive relation, xBy, which is true if, and only if, x is the Gödel-number of a proof sequence of P whose last formula has the Gödel-number y.

Gödel assures the constructive nature of the first 45 definitions by specifying (cf. Go31, p.17, footnote 34):

Everywhere in the following definitions where one of the expressions `\forall x‘, `\exists x‘, `\epsilon x (There is a unique x)’ occurs it is followed by a bound for x. This bound serves only to assure the recursive nature of the defined concept.

Gödel then defines a meta-mathematical proposition that is not recursive:

(\#46) A proposition, Bew(x), which is true if, and only if, (\exists y)yBx is true.

Thus Bew(x) is true if, and only if, x is the Gödel-number of a provable formula of P.

L: Expressing arithmetical functions and relations in P

Now, by Gödel’s Theorem VII (Go31, p.29), any recursive relation, say Q(x), can be represented in P by some, corresponding, arithmetical formula, say [R(x)], such that, for any natural number n:

If Q(n) is true, then [R(n)] is P-provable;

If Q(n) is false, then [\neg R(n)] is P-provable.

However, Gödel’s reasoning in the first half of his Theorem VI (Go31, p.25(1)) establishes that the above representation does not extend to the closure of a recursive relation, in the sense that we cannot assume:

If (\forall x)Q(x) is true (i.e, Q(n) is true for any given natural number), then [(\forall x)R(x)] is P-provable.

In other words, we cannot assume that, even though the recursive relation Q(x) is instantiationally equivalent to a sound interpretation of the P-formula [R(x)], the number-theoretic proposition (\forall x)Q(x) must, necessarily, be logically equivalent to the—correspondingly sound—interpretation of the P-formula [(\forall x)R(x)].

The reason: In recursive arithmetic, the expression `(\exists x)F(x)‘ is an abbreviation for the assertion:

(*) There is some (at least one) natural number n such that F(n) holds.

In a formal Peano Arithmetic, however, the formula `[(\exists x)F(x)]’ is simply an abbreviation for `[\neg (\forall x)\neg F(x)]’, which, under a sound finitary interpretation of the Arithmetic can have the verifiable translation:

(**) The relation \neg F(x) is not Turing-computable as always true.

Moreover, Gödel’s Theorem VI establishes that we cannot conclude (*) from (**) without risking inconsistency.

Consequently, although a primitive recursive relation may be instantiationally equivalent to a sound interpretation of a P-formula, we cannot assume that the existential closure of the relation must have the same meaning as the interpretation of the existential closure of the corresponding P-formula.

However this, precisely, is the presumption made by Gödel in the proof of Theorem XI, from which he concludes that the consistency of P can be expressed in P, but is not P-provable.

M: Ambiguity in the interpreted `meaning’ of formal mathematical expressions

The ambiguity in the `meaning’ of formal mathematical expressions containing unrestricted universal and existential closure under an interpretation was emphasised by Wittgenstein (Wi56):

Do I understand the proposition “There is . . .” when I have no possibility of finding where it exists? And in so far as what I can do with the proposition is the criterion of understanding it … it is not clear in advance whether and to what extent I understand it.

N: Expressing “P is consistent” arithmetically

Specifically, Gödel defines the notion of “P is consistent” classically as follows:

P is consistent if, and only if, Wid(P) is true

where Wid(P) is defined as:

( \exists x) (Form(x) \wedge \neg Bew(x))

This translates as:

There is a natural number n which is the Gödel-number of a formula of P, and this formula is not P-provable.

Thus, Wid(P) is true if, and only if, P is consistent.

O: Gödel: “P is consistent” is always expressible in P

However, Gödel, then, presumes that:

(i) Wid(P) can be represented by some formula [W] of P such that “[W] is true” and “Wid(P) is true” are logically equivalent (i.e., have the same meaning) under a sound interpretation of P;

(ii) if the recursive relation, Q(x, p) (1931, p24(8.1)), is represented by the P-formula [R(x, p)], then the proposition “[(\forall x)R(x, p)] is true” is logically equivalent to (i.e., has the same meaning as) “(\forall x)Q(x, p) is true” under a sound interpretation of P.

P: The loophole in Gödel’s presumption

Although, (ii), for instance, does follow if “[(\forall x)R(x, p)] is true” translates as “R(x, p) is Turing-computable as always true”, it does not if “[(\forall x)R(x, p)] is true” translates as “R(x, p) is constructively computable as true for any given natural number n, but it is not Turing-computable as true for any given natural number n“.

So, if [W], too, interprets as an arithmetical proposition that is constructively computable as true, but not Turing-computable as true, then the consistency of P may be provable instantiationally in P [11].

Hence, at best, Gödel’s reasoning can only be taken to establish that the consistency of P is not provable algorithmically in P.

Gödel’s broader conclusion only follows if P purports to prove its own consistency algorithmically.

However, Gödel’s particular argument, based on his definition of Wid(P), does not support this claim.


BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic (4th ed). Cambridge University Press, Cambridge.

Br08 L. E. J. Brouwer. 1908. The Unreliability of the Logical Principles. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North Holland / New York: American Elsevier (1975): pp. 107-111.

Go31 Kurt Gödel. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Elliott Mendelson. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York.

Hi27 David Hilbert. 1927. The Foundations of Mathematics. In The Emergence of Logical Empiricism. 1996. Garland Publishing Inc.

Hi30 David Hilbert. 1930. Die Grundlegung der elementaren Zahlenlehre. Mathematische Annalen. Vol. 104 (1930), pp. 485-494.

Me64 Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand. pp.145-146.

Ro36 J. Barkley Rosser. 1936. Extensions of some Theorems of Gödel and Church. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. Reprinted from The Journal of Symbolic Logic. Vol.1. pp.87-91.

Sc67 Joseph R. Schoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.

Tu36 Alan Turing. 1936. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid, vol 43 (1937) pp. 544-546.

Wi56 Ludwig Wittgenstein. 1956. Remarks on the Foundations of Mathematics. Edited by G. H. von Wright and R. Rhees. Translated by G. E. M. Anscombe. Basil Blackwell, Oxford.


Return to *: Edited and transcribed from this 2010 preprint. Some of its pedantic conclusions regarding the `soundness’ of the standard interpretation of PA (and consequences thereof) should, however, be treated as qualified by the broader philosophical perspective that treats the standard and algorithmic interpretations of PA as complementary—rather than contradictory—interpretations (as detailed in this post).

Return to 1: We show in this paper that, from a finitary perspective (such as that of this preprint) the proofs of both of Gödel’s celebrated theorems in Go31—his Theorem VI postulating the existence of an undecidable proposition in his formal Peano Arithmetic, P, and his Theorem XI postulating that the consistency of P can be expressed, but not proven, within P—hold vacuously for first order Peano Arithmetic, PA.

Return to 2: Although we have restricted ourselves in this paper to considering only PA, the arguments would—prima facie—apply equally to any first-order theory that contains sufficient Peano Arithmetic in Gödel’s sense (cf. Go31, p.28(2)), by which we mean that every primitive recursive relation is definable within the theory in the sense of Gödel’s Theorems V (Go31, p.22) and VII (Go31, p.29).

Return to 3: Following Hilbert.

Return to 4: Since we cannot, then, have that [\neg(\forall x)\neg R(x)] is PA-provable and that [\neg R(n)] is also PA-provable for any given numeral [n].

Return to 5: This corresponds to the P-formula of his paper that Gödel defines, and refers to, only by its Gödel-number r (cf. Go31, p.25, eqn.(12)).

Return to 6: Gödel refers to these P-formulas only by their Gödel-numbers 17Gen \hspace{+.5ex} r and Neg(17Gen \hspace{+.5ex} r) respectively (cf. Go31, p.25, eqn.13).

Return to 7: i.e., for any given natural number n.

Return to 8: Because the arithmetical relation R(x) is a Halting-type of relation (cf.Tu36, \S 8) that is constructively computable as true for any given natural number n, although it is not Turing-computable as true for any given natural number n (as detailed in this post).

Return to 9: Gödel refers to it only by its Gödel-number w (Go31, p.37).

Return to 10: Gödel’s broader conclusion—unchallenged so far but questionable—was that his reasoning could be validly “… carried over, word for word, to the axiom systems of set theory M and of classical mathematics A”.

Return to 11: That Gödel was open to such a possibility in 1931 is evidenced by his remark (Go31, p37) that “… it is conceivable that there might be finitary proofs which cannot be represented in P (or in M or A)”.

Bhupinder Singh Anand