4
$\begingroup$

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.

$\endgroup$
2
  • 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$ Commented Jul 30, 2014 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$ Commented Jul 30, 2014 at 16:38

1 Answer 1

5
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Great answer, thanks! Is the inability of $M$ to define "$M \vDash \phi$" a conclusion of Tarski's undefinability theorem? $\endgroup$
    – namsap
    Commented Jul 31, 2014 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$ Commented Jul 31, 2014 at 15:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .