In Rautenberg's book (A Concise Introduction to Mathematical Logic, Universitext, Springer 2006), Godel'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 godel number (which, for formulas that come from the metatheory, it is equal to their real godel 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 godel 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?