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

Question

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?

score 7 · Accepted Answer · edited Apr 13 '17 at 12:58

$\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, 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, and also Marc Alcobé García's question Feferman's extensional and intensional applications of the method of arithmetization, 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.

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

1 Answers1

Linked