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?



the choice of representing formulas and Gödel's second incompleteness theorem
$\newcommand\Con{\text{Con}}\newcommand\ZFC{\text{ZFC}}$


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$. 


This way of thinking goes back to [S. Feferman, Arithmetization of metamathematics, Fundamenta Mathematicae, 1960](https://eudml.org/doc/213578), who discussed intensional and extensional consistency statements, and it was discussed previously here on MO on Sergei Tropanets question [Clarification of Gödel's second incompleteness theorem](https://mathoverflow.net/questions/28025/clarification-of-godels-second-incompleteness-theorem), and also Marc Alcobé García's question [Feferman's extensional and intensional applications of the method of arithmetization](https://mathoverflow.net/questions/64777/fefermans-extensional-and-intensional-applications-of-the-method-of-arithmetiza), which you may find helpful.


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. 


