# the choice of representing formulas and Gödel's second incompleteness theorem

In Rautenberg's book (A Concise Introduction to Mathematical Logic, Universitext, Springer 2006), Gödel's second incompleteness theorem is stated:

Theorem 3.2 (Second incompleteness theorem). PA satisfies alongside the fixed-point lemma also D1–D3. For every theory T with these properties,

(1) $\nvdash_T Con_T$ provided T is consistent,
(2) $\vdash_T Con_T \to \neg\square Con_T$

where, at the beginning of the chapter, he defines:
Let ${\bf bew_T} (y, x)$ be a formula that is assumed to represent the recursive predicate ${\it bew_T}$ in T, exactly as in 6.4. For ${\bf bwb_T} (x) = ∃y {\bf bew_T} (y, x)$ we write $\square (x)$, and $\square α$ is to mean ${\bf bwb_T} (\ulcorner α \urcorner )$.

and also:
D1: $\vdash_T \alpha \implies \space \vdash_T \square \alpha$
D2: $\vdash_T \square \alpha \wedge \square (\alpha \rightarrow \beta )\rightarrow \square \beta$
D3: $\vdash_T \square \alpha \rightarrow \square \square \alpha$

T = ZFC also satisfies these conditions (and indeed he mentions it).

from this it seems that the theorem is true for every representing formula for the theory T and for every representing formula for the predicate ${\it bew_T}$. on the other hand, there is this:

Formalize logic inside ZFC in the usual way, and for every relevand object o (term, formula, proof, etc) assign the corresponding object $\ulcorner o \urcorner$ in the usual way (so if $\phi$ is a formula in the metatheory, $\ulcorner \phi \urcorner$ is indeed a formula in the logic inside ZFC). Order formulas by their internal Gödel number (which, for formulas that come from the metatheory, it is equal to their real Gödel number...). let $t_1(x)$ be arbitrary representing formula for ZFC (e.g the most natural one, arising when formalizing first order logic inside ZFC and then formalizing the axioms of ZFC inside ZFC). let ${\bf bew_1}(y,x)$ be the formula for "y is a proof of x in ZFC" the theorem should indeed work for these. now, let ${\bf bew}(y,x,z)$ be the formula for "y is a proof of x in the theory z" and let ${\bf bwb}(x,z)$ and ${\bf Con}(z)$ be "x is provable from z" and "z is consistent" as formalized in ZFC. define:
$t_2(x) = t_1(x) \wedge {\bf Con}(\{y : t_1(y) \wedge G(y) \leq G(x)\})$. where G(x) is the Gödel number of x inside ZFC.

for every model of ZFC, the internal formulas x for which G(x) is standard are exactly those x which are $\ulcorner \phi \urcorner$ for some $\phi$ in the metatheory, and so, by the reflection theorem for ZFC, ${\bf Con}(\{y : t_1(y) \wedge G(y) \leq G(\ulcorner \phi \urcorner)\})$ for every $\phi$ in the metatheory.

therefore, since $t_1$ is representable, so is $t_2$.

on the other hand, if we let $ZFC_2 := \{x : t_2(x) \}$, clearly $\vdash_{ZFC} {\bf Con}(ZFC_2)$ but ${\bf Con}(ZFC_2)$ is exactly the same as ${\bf Con}_{ZFC}$ if we use $t_2(x)$ and the corresponding (naturally defined) ${\bf bew} (y, x)$!

it may indeed be that I messed up my argument some, but I'm quite sure it works, i.e that the "incompleteness property" depends on the choice of representing formulas for the theory in question and/or the ${ \it bew}$ predicate, and that one can chose them to yield $\vdash_{ZFC} Con_{ZFC}$.

thus, my questions: first: am I right (in the last paragraph at least)?

second: if so, why and where exactly does the proof of the second incompleteness theorem fail in these cases?

third: how exactly does these dependencies work? specifiaclly : in my argument I have used a different representation for ZFC. does the same can happen if one uses the natural representation for ZFC, but a different representation for ${ \it bew}$, or, given a representation for ZFC, all representations for ${ \it bew}$ are equal in a way?

So on the one hand, we have the usual assertion $\Con(\ZFC)$, which asserts that $\ZFC$ is consistent using a straightforward representation of the $\ZFC$ axioms, and then on the other hand, we have as with your $t_2$ the alternative assertion $\Con(\ZFC_2)$, using a representation of the $\ZFC$ that only continues to add axioms provided that the resulting theory remains consistent. So we can easily prove in a very weak theory that $\Con(\ZFC_2)$ holds, and this seems paradoxical because our two different theories seem both to be representing the same theory $\ZFC$.
Part of the resolution of the paradox is to realizing that $\ZFC$ does not prove the equivalence of the two different consistency statements, and in particular, $\ZFC$ does not prove that the two representations of $\ZFC$ represent the same theory. Although a weak theory such as $\text{PA}$ can prove $\Con(\ZFC_2)$, it cannot prove that the theory as represented in $\ZFC_2$ includes much of substance at all.