Gödel's second incompleteness theorem states that if $\mathsf{ZF-Inf}$ is consistent, then $\mathsf{ZF-Inf} \nvdash \mathsf{Con(ZF-Inf)}$. Moreover, if $\mathsf{(ZF-Inf)} + \neg \mathsf{Con(ZF-Inf)}$ were inconsistent, then (under the condition of $\mathsf{ZF-Inf}$ being consistent) in every model of $\mathsf{ZF-Inf}$ it is true that $\mathsf{Con(ZF-Inf)}$. Thus, $\mathsf{ZF-Inf} \vdash \mathsf{Con(ZF-Inf)}$. By contradiction, this implies that $\mathsf{(ZF-Inf)} + \neg \mathsf{Con(ZF-Inf)}$ is consistent.

How can I imagine a model of $\mathsf{(ZF-Inf)} + \neg \mathsf{Con(ZF-Inf)}$?

In my opinion it seems quite strange to have a model of $\mathsf{ZF-Inf}$ where $\mathsf{ZF-Inf}$ is not consistent. Does this mean that it is possible to prove everything in this model? This is not possible as $M \vDash\varphi$ and $M \vDash \neg \varphi$ are not possible for a model $M$.

Or, let $M$ be a model of $\mathsf{(ZF-Inf)} + \neg \mathsf{Con(ZF-Inf)}$. Then is every encoding of $\mathsf{ZF-Inf}$ in $M$ inconsistent, i.e. $PA$ and arithmetics are inconsistent in $M$. So $M$ is a model in which arithmetics is inconsistent?

Maybe this question isn't that clever or shows a lack of understanding, then please let me know.

  • 1
    $\begingroup$ The key issue here is "provability" versus "provability within a model" when the model has nonstandard natural numbers. When the question asks "Does this mean that it is possible to prove everything in this model?", what does that sentence really mean?... $\endgroup$ – Carl Mummert Jul 30 '14 at 14:03
  • $\begingroup$ "In my opinion it seems quite strange to have a model of $\mathsf {ZF−Inf}$ where $\mathsf {ZF−Inf}$ is not consistent." But the "new" theory obtained adding to $\mathsf {ZF−Inf}$ the "new" axiom $\neg \mathsf{Con(ZF-Inf)}$ is nor more $\mathsf{(ZF-Inf)}$... It is another theory (which is consistent) which proves a theorem about $\mathsf{(ZF-Inf)}$. This theorem is $\neg \mathsf{Con(ZF-Inf)}$, which is not $\neg \mathsf{Con}[\mathsf{(ZF-Inf)} + \neg \mathsf{Con(ZF-Inf)}]$. $\endgroup$ – Mauro ALLEGRANZA Jul 30 '14 at 16:38

For the sake of this answer, we'll fix some theory $T$, which could be $\mathsf{(ZF-Inf)} + \neg \mathsf{Con(ZF-Inf)}$, and "provable" in both senses always means "from the axioms of $T$". We'll also fix some (nonstandard) model $M$ of $T$.

There is a distinction between the "real" provability relation, $T \vdash \phi$, and the formalized provability relation within a model. We will write that as $\text{Pvbl}^M_T(\phi)$.

The real provability relation quantifies over real proofs: $T \vdash \phi$ holds if and only if there is a proof of $\phi$ from the axioms of $T$. The formalized provability relation in $M$ quantifies over the natural numbers of $M$ (which include nonstandard numbers). So $\text{Pvbl}^M_T(\phi)$ holds if and only if there is a natural number in $M$ which appears to code a proof of $\phi$ from the axioms of $T$.

That "coded proof" can differ from an actual proof in two ways. First, if the axioms of $T$ include any axiom schemes (as the example above does) then these axiom schemes will have "nonstandard axioms" corresponding to the nonstandard numbers of $M$. Such "nonstandard axioms" could appear in a coded proof. Second, a coded proof may have a nonstandard length. So there are two reasons why $\text{Pvbl}^M_T(\phi)$ does not imply $T \vdash \phi$.

Now, for the $T$ in question, we will indeed have that $\text{Pvbl}^M_T(\phi)$ holds for all $\phi$. This is because we have $\text{Pvbl}^M_T(0 \not = 1)$, by the axioms of $\mathsf{ZFC} - \mathsf{Inf}$, and also $\text{Pvbl}^M_T(0 = 1)$, by the axiom $\neg \mathsf{Con(ZF-Inf)}$. The overall result then follows because $T$ includes classical logic, and this is formalized into the $\text{Pvbl}$ relation.

The deeper part of the question is why $\text{Pvbl}^M_T(\phi)$ does not imply that $M$ satisfies $\phi$, written as usual $M \vDash \phi$. This question is natural because we know from the soundness theorem that $T \vdash \phi$ and $M \vDash T$ together imply $M \vDash \phi$. The trouble is that $M$ cannot define its own satisfaction relation "$M \vDash \phi$". So the usual semantic proof of the soundness theorem cannot get off the ground.

  • $\begingroup$ Great answer, thanks! Is the inability of $M$ to define "$M \vDash \phi$" a conclusion of Tarski's undefinability theorem? $\endgroup$ – namsap Jul 31 '14 at 14:56
  • $\begingroup$ It is a consequence of what is usually called the "Diagonal Lemma" in the context of the incompleteness theorems. For any formula $S(n)$ with one free variable $n$, there is a sentence $\phi$ so that $T$ proves $\phi \leftrightarrow S(\ulcorner \phi \urcorner)$. If $R(n)$ defined the set of true formulas of $M$, that is, if $R(\ulcorner \phi \urcorner)$ holds if and only if $M \vDash \phi$, then we can get a contradiction by applying the diagonal lemma to $S(n) \equiv \lnot R(n)$. This is closely related to Tarski's theorem, of course. $\endgroup$ – Carl Mummert Jul 31 '14 at 15:34

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.