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!
Best Answer
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
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.