Concerning the canonical example for Gödel's first incompleteness theorem:

G cannot be proved within the theory T

If G were provable under the axioms and rules of inference of T, then T would have a theorem, G, which effectively contradicts itself, and thus the theory T would be inconsistent. This means that if the theory T is consistent then G cannot be proved within it, and so the theory T is incomplete.

The problem I have with this example, is that in my impression, it cannot be expressed in first-order Peano arithmetic. The predicate isProvable() somehow expects true and false to be defined, while Tarski's undefinability theorem insists that they cannot be defined in first-order arithmetic. Consequently, first-order arithmetic cannot be expected to have the capacity to express predicate functions.

Therefore, I think that isProvable() can only be a function in the meta-axiomatization making statements ABOUT first-order arithmetic. I do not see how it could be a function WITHIN first-order arithmetic.

In that sense, the example statement does not look like an example for the incompleteness of first-order arithmetic but like an example for the incompleteness of the meta-axiomatization used to describe it.

By the way, does anybody have better examples for Peano's incompleteness?

  • 2
    $\begingroup$ You wrote a fairly reasonable question. But before doing that, have you tried searching the site for the myriad of threads about "true but not provable" statements, or the many explanations of the incompleteness theorems? $\endgroup$
    – Asaf Karagila
    Commented Nov 3, 2015 at 5:05
  • $\begingroup$ @AsafKaragila: You are clearly not interested in my question. But before doing that, have you tried searching the site for the myriad of threads in which you could be interested instead? $\endgroup$
    – erik
    Commented Nov 3, 2015 at 6:23
  • 1
    $\begingroup$ You clearly know me very well. I would have enjoyed writing an answer to your question, but you spent no time searching for prior threads, and Noah gave a very good answer. If you are taking this tone with me because you think I downvoted, you're wrong. I haven't voted on your question. $\endgroup$
    – Asaf Karagila
    Commented Nov 3, 2015 at 6:26
  • $\begingroup$ Concerning Noah's answer, this is what puzzles me: "figuring out how to internally express the provability predicate is the bulk of Godel's argument". I was pretty much convinced that Peano arithmetic could not express this. I wonder how Gödel managed to express a predicate function, knowing that he is not allowed to define 'true' or 'false'. Concerning "on formally undecidable propositions", I tried to read it five years ago. I am back to square one on that issue ... I've got a copy opened up in another browser tab ... None of us will escape his fate! $\endgroup$
    – erik
    Commented Nov 3, 2015 at 7:08
  • 2
    $\begingroup$ Try to read it again. There are several very good books on the topic. Smullyan's and Peter Smith's to name a few. But math is hard, and often mind boggling. If it were easy, you wouldn't have asked this question here. $\endgroup$
    – Asaf Karagila
    Commented Nov 3, 2015 at 7:21

1 Answer 1


When you write "I do not see how it could be a function WITHIN first-order arithmetic," it is certainly surprising, but this is in fact the case: figuring out how to internally express the provability predicate is the bulk of Godel's argument. If you actually read the proof, you will see how it is done.

Briefly, the point is that if $\varphi$ is provable from $T$, then there is a certificate for this fact: a (natural number which codes a) proof! A proof is a finite string of sentences satisfying some simple properties, corresponding to the axioms of $T$ and the inference rules of first-order logic. Via Godel coding, it turns out that all relevant statements about proofs can be expressed as first-order arithmetic statements about the codes of proofs.

(Note that this is not true for truth! A certificate for $\varphi$ being true in a structure is a family of Skolem functions, which are second-order objects. There are additional complications as well, but this is the big difference I want to highlight.)

EDIT: A few steps towards understanding the provability predicate:

CLAIM: Peano arithmetic proves "Every finite sequence of 0s and 1s, which has exactly as many 0s as 1s, has even length."

Note that this is silly - the language of arithmetic does not let us talk directly about sequences! Still, we can make sense of this statement via (a silly example of) Godel numbering: to the finite binary sequence $\alpha=a_1a_2a_3. . . a_n$, where $a_i\in\{0, 1\}$, we associate the number $Code(\alpha)=2^{a_1+1}3^{a_2+1}5^{a_3+1} . . . p_n^{a_n+1}$. (Here "$p_i$" denotes the $i$th prime number.) Now, we have:

  • There is a formula $\varphi(x)$ in the language of arithmetic such that for every numeral $k$, we have $PA\vdash \varphi(k)$ iff $k=Code(\alpha)$ for some finite binary string $\alpha$ with exactly as many 0s as 1s. (If exponentiation isn't in the language of arithmetic, then this is actually pretty difficult! For that reason we often use the conservative extension $PA_{exp}$ instead of $PA$; it's not really any different, but it makes some technical steps easier.)

  • There is a formula $\psi(x, y)$ in the language of arithmetic such that for every pair of numerals $k, l$, we have $PA\vdash \psi(k, l)$ iff $k=Code(\alpha)$ for some binary string $\alpha$ of length $l$.

  • Finally, $PA$ proves the sentence $\forall x, y(\varphi(x)\implies \exists z(\psi(x, y)\iff y=2z))$, that is, "Every finite binary string has even length." (This of course depends on the exact choices of $\varphi$ and $\psi$, so the previous two steps really should be made more explicit.)

Note that the above paragraphs take place outside of $PA$, but the formulas $\varphi$ and $\psi$ are formulas of $PA$. There's a deep philosophical issue here: is $PA$ really talking about finite binary strings, or just "simulating" them somehow? (This is closely related to the "Chinese Room" thought experiment of Searle, and many others.) While this is interesting, we're just going to sidestep it: in proving Godel's theorem, we fix a coding scheme, and prove that all the relevant facts - when interpreted by this scheme - are in $PA$. In particular, we get:

  • A formula $Prov(x, y)$ in the language of arithmetic.

  • A proof - in the "metatheory" - that, for any pair of numerals $m, n$, we have $PA\vdash Prov(m, n)$ iff $m$ is the code of a sentence $\sigma$ and $n$ is the code of a proof of $\sigma$ from $PA$.

So there is a metatheory here, but its role is interpreting the predicate "$Prov$," not in formulating it. (And, by the way, we can ask what sort of metatheory we need, and the answer is, in a precise sense, "not very much" . . . but that's going a bit too far for now.)

As far as "better examples" go, there are many sentences not obviously of the form "$Con(T)$" now known to be independent of the theory $ACA_0$, which is a conservative extension of $PA$ to a larger language (so there are more things that are expressible - this just makes the examples better). Some examples include:

  • The Paris-Harrington theorem.

  • The linear order $\epsilon_0=\omega^{\omega^{\omega^{...}}}$ is in fact well-ordered. (Due to Gerhard Gentzen, who showed that "$\epsilon_0$ is well-founded" implies $Con(PA)$ over a very weak base theory.)

  • Every two-player perfect information game, which is guaranteed to end after finitely many moves, is determined.

  • And many more.

If you are interested in this sort of thing, you should check out Reverse Mathematics.

  • $\begingroup$ The example involving the determinacy of finite games came as a surprise to me, I would have thought that could be proved in $WKL_{0}$. Is there are reference for that? $\endgroup$
    – Rupert
    Commented Nov 3, 2015 at 16:08
  • $\begingroup$ @Rupert If there is a bound on how long the game will take, then in fact it is provable in $RCA_0$; and if the game is played on a finite set, then it is equivalent to $WKL_0$ (this was proved by Nemoto). But if the game is played on $\omega$, and we merely know that every play is finite, then this is equivalent to $ATR_0$. This was proved by Steel; see Simpson's book "Subsystems of Second-Order Arithmetic" for more details. $\endgroup$ Commented Nov 3, 2015 at 21:37
  • $\begingroup$ "Figuring out how to internally express the provability predicate is the bulk of Godel's argument." I have looked it up. In "On formally undecidable propositions", section 2.4, Gödel combines Peano's axioms with the proposition axioms and the function application axioms. Of course, when doing that, his entire basis becomes Turing complete. From there on, he can certainly implement the provability predicate, because he is expressing his theorem in a fully-fledged programming language. He would never be able to do that just with Peano's axioms. $\endgroup$
    – erik
    Commented Nov 5, 2015 at 1:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .