Is there any particular formulation of $Con(T)$ that makes $Con(T)$ derivable from $T$?

Question

In the proof of Gödel's second incompleteness theorem in my textbook, it is required that we choose the formula $Drv$ to be one that satisfies certain additional properties, rather than any formula that represents the set ${\tt Drv}$. Such properties are used in the proof of "$Con(T)$ is not derivable from $T$". This makes me wonder, if we choose a $Drv$ that does not satisfy these properties, could it be true that $Con(T)$ is derivable from $T$?

Answer 1

You certainly have to place some additional assumption on the derivability predicate beyond its defining the actual derivability relation in the standard model of arithmetic in order to avoid very silly behaviors (of which side-stepping the second incompleteness theorem is one).

For example, consider what happens if we shift from the usual derivability relation $\mathrm{Drv}$ to the following alternative: $$\mbox{$\mathrm{Silly}(x,y)$ = "$\forall z\neg \mathrm{Drv}(\underline{\#\perp}, z)$ and $\mathrm{Drv}(x,y)$."}$$ Intuitively, $\mathrm{Silly}(x,y)$ says "$y$ is a proof of $x$ and $T$ is consistent (in the usual $\mathrm{Drv}$-based sense)." Trivially we have $$T\vdash\neg\exists y \mathrm{Silly}(\underline{\#\perp},y),$$ so the second incompleteness theorem fails for $\mathrm{Silly}$. However, since $T$ is consistent the formulas $\mathrm{Silly}$ and $\mathrm{Drv}$ define the same relation in $\mathbb{N}$.

---

OK, there's a natural objection here. The relation $\mathrm{Silly}$ defined above defines, but doesn't represent in the theory $T$, the derivability relation. This is because - per Godel! - $T$ isn't powerful enough to prove that the crucial first clause of $\mathrm{Silly}$'s definition holds.

However, we can get around this. Simply look at $$\mbox{$\mathrm{VerySilly}(x,y)=$ "$\forall z\le y\neg \mathrm{Drv}(\underline{\#\perp},z)$ and $\mathrm{Drv}(x,y)$."}$$ This successfully represents the derivability relation (since we've bounded the universal quantifier), but we still get trivial $T$-provability of the corresponding consistency analogue.