I don't see why the original version of Gödel's first incompleteness theorem (before Rosser's improvement, I mean) had to include the assumption of $\omega$-consistency in order to show that $F \nvdash \neg G_F $ -- as opposed to the other direction, $F \nvdash G_F $, where consistency suffices anyway, by my understanding.

Could someone point out the flaw in the following (sketchy) argument?

(1) The provability relation for a formal system F is weakly representable in F, i.e. a predicate $PRV_F$ exists s.t. $F \vdash A \Leftrightarrow F \vdash PRV_F(A)$

(2) We define sentence $G_F$ s.t. $F \vdash G_F \leftrightarrow \neg PRV_F(/G_{F}/)$

(3) To show: If F is consistent, then $F \nvdash \neg G_F$ (second part of Incompleteness I)

Assume $F \vdash \neg G_F$.

Then by (2), $F \vdash \neg \neg PRV_F(G_F)$, so $F \vdash PRV_F(G_F)$.

Then by (1), $F \vdash G_F$, so F is inconsistent (and $\omega$-inconsistent as a result as well) from assumption that $F \vdash \neg G_F$.

  • $\begingroup$ I've just tried to recall the outline of the Gödel's first incompleteness theorem and realised that i do not know how to do it without assuming $\omega$-completeness. I do not see what can stop the theory from being consistent but appear inconsistent from its own point of view. If i suppose that $F \vdash \neg G_F$, i can at most deduce that the theory thinks that everything in it is provable. Then what? So, i am eager to see that "Rosser's improvement." $\endgroup$
    – Alexey
    Jan 11, 2019 at 16:03

2 Answers 2


The issue is already present in step 1. Consistency is not a strong enough assumption on the theory to guarantee that the provability relation is representable.

For example, if $T$ is taken to be $\text{PA} + \lnot\text{Con}(PA)$, which is not $\omega$-consistent, then we have $T \vdash \text{Pvbl}_T(\phi)$ for all $\phi$, but $T$ is consistent, so for many $\phi$ we also have $T \not \vdash \phi$. Thus we do not have the whole scheme $T \vdash \phi \Leftrightarrow T \vdash \text{Pvbl}_T(\phi)$, as claimed by (1).

The source of confusion may be that you seem to be quantifying over predicates when you write "a predicate $PRV_F$ exists s.t. $F \vdash A \Leftrightarrow F \vdash PRV_F(A)$". In fact we construct a specific predicate $\text{Pvbl}$ in order to derive scheme (1) from the question.

In order to show that $T \vdash A$ implies $T \vdash \text{Pvbl}(A)$, which is part of showing that $\text{Pvbl}$ does represent the provability relation, we rely on $\text{Pvbl}$ being the actual provability predicate, so that we can transform any derivation of $A$ into a derivation of $\text{Pvbl}(A)$.

Similarly, in showing that $T \vdash \text{Pvbl}(A)$ implies $T \vdash A$, we use the $\omega$-consistency of $T$ to know that, if $T \vdash \text{Pvbl}(A)$ then there is actually a natural number $n$ that codes a derivation of $A$ from $T$.

You may be thinking of general results that show that certain theories are able to represent every computable set, or weakly represent every r.e. set. It is true that the representability of the provability relation follows from these general results. But the proofs of these general results also assume that the theory is $\omega$-consistent, or at least $1$-consistent, not just that the theory is consistent.

  • $\begingroup$ Thank you very much for this clarification. So with assumption of consistency alone, but without assumption of $\omega$-consistency, it is possible that $T \vdash \text{Pvbl}(A)$ but that $T \nvdash (A)$ because there is no natural number coding a derivation of A from the axioms of T, so intuitively speaking, no "actual" proof exists. Is my paraphrasing correct so far? (1/2) $\endgroup$ Jun 1, 2015 at 20:57
  • $\begingroup$ If so, what is changed by assuming that, instead of PA, we consider a second-order theory that allows us to exclude elements that are not natural numbers? Would the correspondence between $T \vdash (A)$ and $T \vdash \text{Pvbl}(A)$ hold automatically then? I am probably mixing up things now, but it's kind of late here... (2/2) $\endgroup$ Jun 1, 2015 at 20:57
  • $\begingroup$ Yes, the issue is that there may not be an "actual" derivation of a formula $\phi$ even if a non-$\omega$-consistent theory proves $\text{Pvbl}(\phi)$. Regarding second-order logic, it makes no difference when you talk about provability - the only differences in first and second order logic are in the semantics, so syntactic theorems like the incompleteness theorem apply to both logics equally. In particular, even a second order theory $T$ that logically entails $G_T$ may not be able to prove $G_T$. $\endgroup$ Jun 1, 2015 at 21:19
  • $\begingroup$ I understand that Gödel's result applies to second order theories (of arithmetic) as well, but I don't see how the particular mistake I made in (1) above applies verbatim in that case. A second-order axiomatization of arithmetics excludes non-standard models that first-order PA cannot exclude, so it seems that, for formulas with one free variable over the natural numbers, $T \vdash \text{Pvbl}(A)$ does ensure $T \vdash A$ then, or am I mistaken about this? $\endgroup$ Jun 1, 2015 at 22:14
  • $\begingroup$ I suppose another way to look at it is this: in theories using second-order logic, where the only possible model is the standard natural numbers (which is what we get from invoking second order semantics), if a theory is consistent then it is automatically $\omega$-consistent (because it has the natural numbers as a model) and so the claim you made does hold, just as it would for any $\omega$-consistent theory with first-order logic. So, by eliminating nonstandard models, second-order semantics turn "consistent" into "$\omega$-consistent". $\endgroup$ Jun 1, 2015 at 22:55

Since I had some issues with this topic, too, I would like to share my thoughts on it.

Notice, that I use $\color{red}{red}$ whenever the so denoted things are meant to be syntactic ones. This was (and remains) to me always the key to get things clear: in which "world" are these objects I'm thinking about?

1. There are two different predicates involved:

First, one construct the proof-predicate $Pr_F(x,y)$ in the recursive world, which states that $x$ codes a proof (in $F$ with the Hilbert Calculus) for the formula which is coded by $y$. This is strongly representable in $F$, hence, there is a formula $\color{red}{Pr_F}$ such that:

$$\begin{align}Pr_F(x,y) &\Leftrightarrow F\vdash \color{red}{Pr_F(\overline{x},\overline{y})}\\\neg Pr_F(x,y)&\Leftrightarrow F \vdash\color{red}{\neg Pr_F(\overline x,\overline y)}\end{align}$$

Now, what we are interested in is more: we want to say that some formula is provable, i.e. that there is a proof. So, second, we define the provable-predicate in the first-order language world:

$$\color{red}{P_F(y)\leftrightarrow\exists x . Pr_F(x,y)}$$

Now, what you've stated in (1) holds for $Pr_F$, but it makes no sense to state such a property for $\color{red}{P_F}$, since this is just a formula, but not a primitive recursive predicate. Even more: if we would like to define it as a primitive recursive predicate (at first, then get it via representability into the syntactic world), we couldn't, since there is an unbound quantifier involved!

2. These predicates aren't equivalent in $F$

What we have now is the following:

$$\begin{align} F \vdash \color{red}\phi &\Longleftrightarrow \text{exists closed term $\color{red}{t}$, such that }F\vdash\color{red}{Pr_F(t,\ulcorner\phi\urcorner)}\\&\Longrightarrow F\vdash\color{red}{P_F(\ulcorner\phi\urcorner)}\end{align}$$

but the other direction does not need to hold. You can see it clearly here, what we would need is a closed term $\color{red}t$.

Consider the following note: The quantifiers range over the hole universe, but not every element in the universe must be expressible within the given language. (If you find some time, there are pretty simple examples you could construct. The most obvious is of course the language with one constant symbol, etc.)

Now, $\omega$-consistency to the rescue gets us the $\color{red}t$.

3. A historical note

Although Gödel's original proof assumed $\omega$-consistency it had its effect already on the community. So it shouldn't be overrated, it's more a small taint.

  • $\begingroup$ I really want to stress how useful it was for me, to see your method of visually distinguishing the 'syntactic' side from the 'mathematical argument' side. I will mark your answer as 'accepted' since it was the one that was the most "on my level", not because I'd want to claim that it is objectively better than Carl's excellent answer. Hopefully that's acceptable stackexchange etiquette... as per meta discussion here $\endgroup$ Jun 2, 2015 at 13:49
  • $\begingroup$ One follow-up question, if you allow: You say that it makes no sense to think of my version of 'provable' as as a prim. rec. predicate because it contains an unbounded quantifier. So, does it make sense to speak about a prim. rec. predicate as follows: "$Prv_F(x)$ iff there exists a natural number coding a proof of x given the axioms of F"? This can be "translated" into the syntactic world, correct? And if I would have thought of the prim. rec. predicate that way, I probably would have noticed my initial mistake on my own. $\endgroup$ Jun 2, 2015 at 14:30
  • $\begingroup$ Thanks for your vote, accept and comment. : ). I wasn't mean to devalue any other answer. At least $Prv_F(x)$ is a predicate, but again you use an unbound quantifier in its definition: "iff there exists... " which takes it out of the primitive recursive class and hence is not strongly representable per se. $\endgroup$
    – aphorisme
    Jun 2, 2015 at 14:41
  • $\begingroup$ I suppose I misunderstood the point about it containing an unbounded quantifier. This is not solved by knowing that the variable is ranging over the natural numbers, but that I need to make use of an unbounded search operator, which places it in the class of partial recursive functions, hence: not strongly representable. Correct this time? $\endgroup$ Jun 2, 2015 at 15:23
  • $\begingroup$ Yes. Well, the need of an unbounded search operator explains why provability can't be primitive recursive! And strongly representable is about primitive recursive. : ) $\endgroup$
    – aphorisme
    Jun 2, 2015 at 21:47

You must log in to answer this question.

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