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

Question

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.

Answer 1

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.