5
$\begingroup$

I tried to prove the exercise problem in Kunen (Chapter IV, problem 36.)

Problem. Show that there is a formula $\chi(x)$, such that

  1. $\chi$ represents ZF; i.e.,$$\phi\in \mathsf{ZF}\to \mathsf{ZF}\vdash\chi(\ulcorner\phi\urcorner)\quad\text{and}\quad \phi\notin \mathsf{ZF}\to \mathsf{ZF}\vdash \lnot\chi(\ulcorner\phi\urcorner)$$

  2. If $\ulcorner\mathsf{ZF}\urcorner$ is added via the definition $\ulcorner\mathsf{ZF}\urcorner=\{x:\chi(x)\}$, then $\mathsf{ZF}\vdash \mathsf{CON(\ulcorner ZF\urcorner)}$.

(where $\mathsf{CON}(\ulcorner T\urcorner)$ is consistency argument of $T$ which is formalized within formal theory $\mathsf{ZF}$.)

But I am not even understand the problem. Why the second incompleteness does not applied in that case? In page 144-145 in Kunen, he writes

(...) We now have for each such $S$, a sentence $\mathsf{CON}(\ulcorner S\urcorner)$ in the language of set theory asserting that $S$ is consistent. (...) The Gödel Incompleteness Theorem shows that if $S$ is consistent and extends $\mathsf{ZF}$, then $S\nvdash\mathsf{CON}(\ulcorner S\urcorner)$. (Caution: this presupports that we used a "reasonable" $\chi_S$ to represent $S$.)

(Add: $\chi_S$ represents $S$; it was explained the front of above comment.)

I also don't understand that comment. I would be thankful for any reasonable explanation.

$\endgroup$
  • 1
    $\begingroup$ I can't explain why the second incompleteness theorem doesn't apply, but the following is (I think) a $\chi$ satisfying the two conditions: $\chi(x)$ iff $x\in ZF$ and $Con(\{y\in ZF: y \leq x\})$. $\endgroup$ – GME Dec 1 '14 at 11:51
  • 2
    $\begingroup$ GME's proposed representation works. This weird example is due, I believe, to Feferman. The reason that the second incompleteness theorem doesn't apply is that it assumes that the representation of the theory is effective (i.e. computable) and the proposed one isn't. $\endgroup$ – Miha Habič Dec 1 '14 at 12:07
  • $\begingroup$ @Miha, GME: Thanks for your comment. It is really helpful for me. $\endgroup$ – Hanul Jeon Dec 2 '14 at 10:58
  • $\begingroup$ This is an awesome problem. (+1 for Kunen). $\endgroup$ – hot_queen Dec 16 '14 at 19:17
3
$\begingroup$

Thanks to GME and Habič's comments, I understand and can prove that problem. This answer is just filling in the details of their comments.

Let define $$\chi(n)\leftrightarrow n\in \mathsf{ZF}\land \mathsf{CON}\{m\in\mathsf{ZF}:m\le n\}.$$

We regard $\mathsf{ZF}$ as the recursive set of Gödel numberings of the axioms of ZF. If $\phi\in \mathsf{ZF}$, then $\mathsf{ZF}\vdash (\ulcorner\phi\urcorner\in \mathsf{ZF})$. Also, if $\psi_1$, $\psi_2$, $\cdots$, $\psi_k$ are axioms of ZF whose Gödel number is less than the Gödel number of $\phi$ then by reflection, the consistency of $\{\psi_1,\cdots,\psi_k,\phi\}$ is provable from ZF; that is, $\mathsf{ZF}\vdash \mathsf{CON}\{m\in\mathsf{ZF}:m\le \ulcorner\phi\urcorner\}$. Therefore $\mathsf{ZF}\vdash\chi (\ulcorner\phi\urcorner)$. If $\phi\notin \mathsf{ZF}$ then $\mathsf{ZF}\vdash (\ulcorner\phi\urcorner\notin \mathsf{ZF})$ so $\mathsf{ZF}\vdash\lnot\chi(\ulcorner\phi\urcorner)$

We will prove that, if $\ulcorner\mathsf{ZF}\urcorner$ is added via the definition $$\ulcorner\mathsf{ZF}\urcorner=\{n:\chi(n)\}$$ then $\mathsf{ZF}\vdash \mathsf{CON(\ulcorner ZF\urcorner)}$. We will use the reduction to absurdity within the formal theory $\mathsf{ZF}$.

If $\lnot\mathsf{CON(\ulcorner ZF\urcorner)}$ holds, then there is a proof $\pi$ from some assumptions $a_1,a_2,\cdots,a_n\in \ulcorner \mathsf{ZF}\urcorner$ to contradiction. But we already know that $\mathsf{CON}\{a_1,a_2,\cdots a_n\}$ holds. So we cannot derive a contradiction from $a_1$, $\cdots$, $a_n$. From this, we get $\mathsf{ZF+}\lnot\mathsf{CON(\ulcorner ZF\urcorner)}$ derives contradiction so $\mathsf{ZF}\vdash \mathsf{CON(\ulcorner ZF\urcorner)}$.

It does not contradict with second imcompleteness theorem since $\chi$ is at least $\Pi_1^0$, so is not recursive.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.