Can you find a division by zero error in the following short proof of Gödel's incompleteness theorem?

First a little background. $\text{G($a$)}$ returns the Gödel number of the formula $a$. As in Gödel's proof the primitive recursive funtion $\text{Z}(a)$ returns the Gödel number of the number $a$ of the formal system. Example: $\text{Z}(2) =\text{G}(\underline{2})=\text{G}(S(S(0)))$.

The primitive recursive function $\text{Sb($a$, $v_1$|$\text{Z}(y)$)}$ corresponds to the substitution of the formal system's number $y$ in the place of free variable $v_1$ in the formula that corresponds to number $a$. Example: $\text{Sb($\text{G}(v_1=0)$, $v_1$|$\text{Z}(2)$)}=\text{G}(v_1=0[v_1|\underline{2}])=\text{G}(\underline{2}=0)$.

The primitive recursive relation $x\text{B}y$ says that number $x$ corresponds to a sequence of formulas that proves the formula corresponding to number $y$. $\text{Provable}$ is then equivalent to $\exists x: x\text{B}y$.

And now to the actual proof. We assume that in the system $P$ primitive recursive relations are representable.

One of the following relations hold for any number $x$ corresponding to a formula with free variable $v_1$, either the formula corresponding to number $x$ with its free variable substituted by $y$ is provable or not:

$\text{Provable}(\text{Sb}(x,v_1\space|\text{Z}(y)))$ or $\neg \text{Provable}(\text{Sb}(x,v_1\space|\text{Z}(y)))$

Let formal system formula $r=\text{$\neg$Provable}(\text{Sb}(v_1,v_1\space|\text{Z}(v_1))$, where $v_1$ is the free variable. The formula is definable in $P$ since it's a primitive recursive relation with an added quantifier. Choose $x=G(r)$, $y=G(r)$. Now consider the first case:

$\text{Provable}(\text{Sb}(x,v_1\space|\text{Z}(x)))\Rightarrow P\vdash r[v_1|\underline{\text{G}(r)}] \Rightarrow P \vdash \neg \text{Provable}(\text{Sb}(\underline{x},v_1\space|\text{Z}(\underline{x})))\Rightarrow \neg \text{Provable}(\text{Sb}(x,v_1\space|\text{Z}(x)))$

The last line comes from assuming that $P$ is consistent and doesn't prove falsities. And as such, a contradiction! Therefore the second case $\neg \text{Provable}(\text{Sb}(x,v_1\space|\text{Z}(x)))$ must hold, and $r[v_1|\underline{\text{G}(r)}]$ is true but unprovable!

  • $\begingroup$ Not sure about thew technical details, but isn't this just the 'last paragraph' of any proof of Godel's First Incompleteness Theorem? That is, after all the technical set-up, don't all proofs conclude with something like: "G says that G cannot be proven. So, if G can be proven, then (since system is sound), G is true, and hence G cannot be proven. Contradiction! So, G cannot be proven .. and G is therefore true." $\endgroup$
    – Bram28
    Aug 5 '18 at 19:05
  • $\begingroup$ @Bram28 No, this version of Gödel's theorem would require Rosser's improvement or some other additional concepts and is a much longer proof. Please don't down-vote or give a reason for doing so and I will make the appropriate changes. $\endgroup$
    – Dole
    Aug 5 '18 at 19:10
  • $\begingroup$ I wasn't the downvote ... like I said, the technical details are a little beyond me, so I would certainly not feel confident to do that .. in fact, do you think I should remove my earlier comment as it it really missing the point by missing the technical details? $\endgroup$
    – Bram28
    Aug 5 '18 at 19:21
  • $\begingroup$ @Bram28 I don't mind the comment at all, it was a fair observation. Sorry, I was talking to whoever downvoted... $\endgroup$
    – Dole
    Aug 5 '18 at 19:22
  • 2
    $\begingroup$ No, you've assumed much more than mere consistency: "$P$ doesn't prove falsities" is in fact stronger than $\omega$-consistency, and much stronger than consistency. Indeed, one of the consequences of GIT is that PA + "PA is inconsistent" is consistent even though it proves clearly false statements (assuming PA is consistent of course). $\endgroup$ Aug 5 '18 at 19:37

Once all technical details are filled in,$^1$ this seems to be just the usual argument.

In particular, from your comment "in the proof consistency is assumed, not $\omega$-consistency as in Gödel's," I think what you're trying to do is optimize the hypotheses on $P$ without invoking Rosser's trick, but you haven't done so. The dangerous phrase is

The last line comes from assuming that $P$ is consistent and doesn't prove falsities.

You're not just assuming that $P$ is consistent, but also that it is sound. This is a very strong assumption, in fact strictly stronger than Godel's assumption of $\omega$-consistency.$^2$

Just in case, let me summarize the standard argument. As far as I can tell yours is ultimately the same, but let me know if I'm missing something:

  • We start by proving that every p.r. function is representable in our theory and that the relevant operations/relations are p.r. We have some flexibility here. In particular, you'll often see instead an argument that proves that every computable function is representable and then invokes Church's thesis; however, that last bit isn't truly rigorous. Personally I think that the representability of all computable functions is fundamental and worth proving even on its own.

  • We then prove the diagonal lemma. You've essentially done what Godel did here and simply proved the specific case we need - the general diagonal lemma wasn't proved until Bernays, a few years later - but in my opinion there's no reason to not prove it; it's important, it's short, and we're in the neighborhood.

  • We can now write a sentence asserting its own $P$-unprovability, which because of the soundness of $P$ must be $P$-unprovable and hence true.

$^1$Namely, the first bulletpoint in my summary.

$^2$Incidentally both of these are stronger than what you actually need to run the argument with literally no change, namely $\Sigma_1$-soundness. This is indeed strictly stronger than consistency, since (by GIT) $PA$ + "$PA$ is inconsistent" is consistent (unless PA is inconsistent) but not $\Sigma_1$-sound. And of course any amount of soundness implies consistency, since $0=1$ is false.

  • $\begingroup$ Just to be clear, this is not my proof ;). Also a quick question. By soundness you mean: $P\vdash \phi \Rightarrow P\models \phi$. This is valid for first order logic, so then so is the proof? Also what do you mean by $\sum_1$-sound or "any amount" of soundness? $\endgroup$
    – Dole
    Aug 5 '18 at 21:19
  • 2
    $\begingroup$ @Dole There are two different notions of soundness. A logic is sound if provability implies entailment (what you've written). However, there's also the separate notion of soundness of a theory. When we have a "standard model" in mind (like $\mathbb{N}$) a theory is sound (with respect to that model) if it only proves sentences true in that model. A theory is $\Sigma_1$-sound if all the $\Sigma_1$ sentences it proves are true in the intended model. $\endgroup$ Aug 5 '18 at 21:25
  • $\begingroup$ Scweber Aaaah! This is so confusing. Aren't you now assuming that the meta system is sound then, since it's assumed to tell the truth? And if it uses exact same or equivalent axioms to reason about the numbers as $P$, then should not $P$ also be assumed to be sound? What if the meta system itself is not considered sound and uses the same axioms for numbers as $P$... but then maybe it just proved a falsity? Maybe the meta-system inconsistent and proved a falsity anyway... Sorry if this seems like a totally stupid observation, but it is confusing! $\endgroup$
    – Dole
    Aug 5 '18 at 22:24
  • $\begingroup$ @Dole Let's call our meta-system $M$. Then the usual proof of GIT shows that $M$ proves "If $P$ is consistent and sound, then $P$ is incomplete." $M$ doesn't need to reason about its own soundness at all: $M$ says, "If $P$ is consistent, then if $P$ is sound $P$ can't prove that $P$ is inconsistent." Taking $P=M$ wouldn't be a problem. There's an important point here: when we prove a statement in a theory, we're just doing that - we're not proving the statement + "the theory is sound" in the theory. (cont'd) $\endgroup$ Aug 5 '18 at 22:34
  • 1
    $\begingroup$ The important point is that a theory can prove things - even about itself - without being able to prove itself sound. As a good example, take the theory PA + "PA is inconsistent." Obviously this theory doesn't think itself sound, since it doesn't even think itself consistent. But it can still prove things about itself - e.g. its own inconsistency! $\endgroup$ Aug 5 '18 at 22:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.