Construction of a model of $ZFC+\neg Con(ZFC)$

Question

By Gödel's second incompleteness theorem, the following assertion is true in ZFC: $$ Con(ZFC)\rightarrow Con(ZFC+\neg Con(ZFC)) $$ Considering the completeness theorem, this assertion is equivalent to that one can always construct a model of $ZFC+\neg Con(ZFC)$ from a given model of $ZFC$. Is there any concrete construction of the new model, just like the constructible universe and forcing method?

Answer 1

As has been discussed in the comments, there is no inner model or forcing-like construction that will give you a model, since the collection of natural numbers needs to grow.

You'll have to tell me if this is 'natural' enough, but by modifying the construction mentioned by Joel David Hamkins here, we can get the following:

Proposition. There is a formula $\varphi(x)$ in the language of set theory such that for any $V \models \mathsf{ZFC}$, there is a unique $a \in V$ satisfying $\varphi(x)$ and this $a$ is always (externally) a model of $\mathsf{ZFC}+ \neg\mathrm{Con}(\mathsf{ZFC})$.

Proof: As Noah Schweber mentioned in the comments, by standard (computable) procedure, for any theory $T$, we can find an expansion $H_{T} \supseteq T$ which is term complete, i.e., for every formula $\varphi(x,\bar{y})$ and tuple of closed terms $\bar{t}$, there is a closed term $s$ such that $H_{T}\vdash \exists x \varphi(x,\bar{t}) \to \varphi(s,\bar{t})$. The two most common ways to do this are adding Henkin constants and Skolemizing the theory. This implies that for any completion $T'$ of $H_T$, the term structure of $T'$ is a model of $T'\supseteq T$, where the term structure is the structure whose universe is the collection of all closed terms in the language of $T'$ with the interpretations of the atomic relations dictated by $T'$.

Another thing to note is that the construction of the language of $H_T$ can be done in such a way that if the language of $T$ is countable with a given enumeration, then the language of $H_T$ is countable with a given enumeration which is uniformly computable from the enumeration of the language of $T$. Also note that this language really only depends on the language of $T$, not on $T$ itself.

$\mathsf{ZFC}$ proves that for any theory $T$, $\mathrm{Con}(T) \to \mathrm{Con}(H_T)$. (This is also provable in significantly weaker theories for the standard definitions of $H_T$.)

Let $\{\psi_i\}_{i<\omega}$ be a fixed computable enumeration of the axioms of $\mathsf{ZFC}+\neg\mathrm{Con}(\mathsf{ZFC})$, and let $T_i$ be $\{\psi_j\}_{i<j} + \neg \mathrm{Con}(\mathsf{ZFC})$ for each $i\leq \omega$ (so in particular, $T_\omega = \mathsf{ZFC} + \neg \mathrm{Con}(\mathsf{ZFC})$). Through a combination of the reflection theorem and Gödel's incompleteness, you can show that for each $i<\omega$, $\mathsf{ZFC}\vdash \mathrm{Con}(T_i)$. (Crucially though, we don't have that $\mathsf{ZFC} \vdash (\forall i<\omega)\mathrm{Con}(T_i)$ unless $\mathsf{ZFC}$ is inconsistent.) So by the above comment, we also have that for each $i<\omega$, $\mathsf{ZFC} \vdash \mathrm{Con}(H_{T_i})$. Note that the choice of enumeration here matters, and we will get different models with different choices of enumeration.

Let $\mathcal{L}$ be the common language of the $H_{T_i}$'s. By the above discussion we may assume that $\mathcal{L}$ has a fixed computable enumeration. By a standard argument, this implies that we have a computable enumeration of the collection of $\mathcal{L}$-sentences. Let $\{\chi_{i}\}_{i<\omega}$ be such an enumeration.

$\mathsf{ZFC}$ proves that every consistent $\mathcal{L}$-theory $S$ has a unique 'leftmost' completion. What I mean by this is that we may regard complete $\mathcal{L}$-theories $S'$ as elements of $2^{\omega}$ by considering $\{i : S' \vdash \chi_i\}$. The leftmost completion is the one which is smallest in the lexicographical ordering on $2^\omega$. Such a completion exists by a typical compactness argument.

Okay so now pass to our model $V$ of $\mathsf{ZFC}$. $\mathsf{ZFC}$ implies that there is a maximal $k\leq \omega^V$ such that $V\models \mathrm{Con}(T_k)$. So in particular, if this $k$ is not $\omega^V$, then $V\models \neg \mathrm{Con}(T_{k+1})$. By the reflection theorem, $V \models \mathrm{Con}(T_i)$ for every externally finite $i$, so if $k<\omega^V$, then it must be a non-standard integer. Since $V$ thinks that $T_k$ is consistent, it also thinks that $H_{T_k}$ is consistent, and so it thinks that the leftmost completion $S$ of $H_{T_k}$ is consistent. $S$ has a term model $M$ which satisfies $S$ since $H_{T_k}$ is term complete.

So we can let $\varphi(x)$ be a formula that is satisfied if and only if $x$ is the term model of the leftmost completion of $H_{T_k}$ where $k\leq \omega$ is the largest for which $T_k$ is consistent. Although there are arbitrary choices in the construction of this formula, it does not have any parameters.

So to see that $M$ is externally a model of $\mathsf{ZFC}+\neg \mathrm{Con}(\mathsf{ZFC})$, note that we either have that $V \models k = \omega^V$ or that $k$ is a non-standard integer. In both cases, for every $i<\omega$, $V \models (M\models \psi_i)$, so since satisfaction of formulas is absolute, we have that $M$ models all of $\mathsf{ZFC}+\neg\mathrm{Con}(\mathsf{ZFC})$. $\square$

---

It is possible to make this construction slightly more 'canonical.' For example, if we start with $\mathsf{ZFC}+ V=L + \neg \mathrm{Con}(\mathsf{ZFC})$, then there are natural definable Skolem functions, so we don't have to make any arbitrary choices to introduce them.

We still ultimately need to pick a completion of the Henkinized/Skolemized theory. We were able to do this in a definable way, but ultimately our completion depends heavily on the enumeration of the language. I doubt there is an 'enumeration invariant' way to choose a definable completion of a theory like $\mathsf{ZFC}$ or $\mathsf{PA}$, but maybe someone will show up and point out that there actually is one.