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?
