There are consistent first-order theories that prove their own inconsistency. For example, construct one like this:

Assuming there is a consistent and sufficiently expressive first-order theory at all, call it $T'$. The incompleteness theorem gives us that $\mathrm{Con}(T')$ (the consistency of $T'$) is not provable in $T'$. Hence $T=T'+\neg\mathrm{Con}(T')$ is consistent. Since $T$ proves that we can derive a contradiction from $T'$ alone, it also proves that we can derive it from $T$ (because $T'\subset T$). So $T$ is consistent but proves $\neg\mathrm{Con}(T)$.

How to think about such a strange theory? Obviously the theory $T$ is lying about itself. But what does this lying mean mathematically? Are the formulas and deductive rules interpreted in the language of $T$ different from the one in my meta theory? Can I trust $T$'s ability to express logic, deduction and arithmetic at all?

Note that a theory $T$ as above is just an example to demonstrate that such strange theories might exist. It might be hard to argue about the usefulness of a theory with such a complicated and highly dubious axiom as $\neg\mathrm{Con}(T')$. But not all such self-falsifying theories must be so obvious and artificial. For example, it could be that ZFC can prove $\neg\mathrm{Con(ZFC)}$ while still being consistent. But how can we trust in a theory that fails to mirror our logic even when we try to implement it carefully? How can we be sure that all other theorems on logic derived in ZFC are trustworthy despite ZFC proves at least one wrong statement (wrong in the sense that our meta logic gives us a different result than the internal proof logic of ZFC)?

  • 3
    $\begingroup$ If ZFC proves $\lnot Con(ZFC)$ then ZFC is inconsistent, since we have completeness in first order logic. What the above means is that there exists a model of ZFC such that the model satisfies $\lnot Con(ZFC)$. The idea is that in that model there might exist non-standard numbers. These "numbers" code a "proof" of the inconsistency. $\endgroup$
    – Apostolos
    Commented May 19, 2017 at 14:47
  • 4
    $\begingroup$ Completeness "says" that what you prove is true. This means that if ZFC could prove the inconsistency of ZFC then the inconsistency of ZFC is true. Therefore if ZFC proved its own inconsistency it would be inconsistent. What Godel's second incompleteness implies is that there exists models of ZFC where the formula "ZFC is inconsistent" holds, which is much weaker than saying that that ZFC proves $\lnot Con(ZFC)$ which would imply that in all models of ZFC the formula holds. $\endgroup$
    – Apostolos
    Commented May 19, 2017 at 15:24
  • 1
    $\begingroup$ Completeness is proven in some metatheory, which is probably some fragment of ZFC. What I'm saying is that in your question you say: "For example, it could be that ZFC can prove ¬Con(ZFC) while still being consistent." This is simply impossible. If ZFC proves its inconsistency then it is inconsistent. $\endgroup$
    – Apostolos
    Commented May 19, 2017 at 15:58
  • 2
    $\begingroup$ I am mistaken, I meant to write soundness. Soundness says that what you prove is true, while completeness is the converse. Still, the point remains. A proof of the inconsistency of ZFC implies the inconsistency of ZFC, by soundness, assuming that the coding is done in a correct way. $\endgroup$
    – Apostolos
    Commented May 19, 2017 at 16:03
  • 12
    $\begingroup$ @Apostolos Your first comment is false, at least without additional assumptions. It's perfectly possible that ZFC could prove $\neg Con(ZFC)$ without being inconsistent. To rule this out we need some extra assumption on ZFC, such as $\omega$-consistency. $\endgroup$ Commented May 19, 2017 at 17:17

2 Answers 2


When we think about theories like ZFC or PA, we often view them foundationally: in particular, we often suppose that they are true. Truth is very strong. Although it's difficult to say exactly what it means for ZFC to be "true" (on the face of it we have to commit to the actual existence of a universe of sets!), some consequences of being true are easy to figure out: true things are consistent, and - since their consistency is true - don't prove that they are inconsistent.

However, this makes things like PA + $\neg$Con(PA) seem mysterious. So how are we to understand these?

The key is to remember that - assuming we work in some appropriate meta-theory - a theory is to be thought of as its class of models. A theory is consistent iff it has a model. So when we say PA + $\neg$Con(PA) is consistent, what we mean is that there are ordered semirings (= models of PA without induction) with some very strong properties.

One of these strong properties is the induction scheme, which can be rephrased model-theoretically as saying that these ordered semirings have no definable proper cuts.

It's very useful down the road to get a good feel for nonstandard models of PA as structures in their own right as oppposed to "incorrect" interpretations of the theory; Kaye's book is a very good source here.

The other is that they satisfy $\neg$Con(PA). This one seems mysterious since we think of $\neg$Con(PA) as asserting a fact on the meta-level. However, remember that the whole point of Goedel's incompleteness theorem in this context is that we can write down a sentence in the language of arithmetic which we externally prove is true iff PA is inconsistent. Post-Goedel, the MRDP theorem showed that we may take this sentence to be of the form "$\mathcal{E}$ has a solution" where $\mathcal{E}$ is a specific Diophantine equation. So $\neg$Con(PA) just means that a certain algebraic behavior occurs.

So models of PA+$\neg$Con(PA) are just ordered semirings with some interesting properties - they have no proper definable cuts, and they have solutions to some Diophantine equations which don't have solutions in $\mathbb{N}$. This demystifies them a lot!

So now let's return to the meaning of the arithmetic sentence we call "$\neg$Con(PA)." In the metatheory, we have some object we call "$\mathbb{N}$" and we prove:

If $T$ is a recursively axiomatizable theory, then $T$ is consistent iff $\mathbb{N}\models$ "$\mathcal{E}_T$ has no solutions."

(Here $\mathcal{E}_T$ is the analogue of $\mathcal{E}$ for $T$; remember that by the MRDP theorem, we're expressing "$\neg$Con(T)" as "$\mathcal{E}_T$ has no solutions" for simplicity.) Note that this claim is specific to $\mathbb{N}$: other ordered semirings, even nice ones!, need not work in place of $\mathbb{N}$. In particular, there will be lots of ordered semirings which our metatheory proves satisfy PA, but for which the claim analogous to the one above fails.

It's worth thinking of an analogous situation in non-foundationally-flavored mathematics. Take a topological space $T$, and let $\pi_1(T)$ and $H_1(T)$ be the fundamental group and the first homology group (with coefficients in $\mathbb{Z}$, say) respectively. Don't pay attention too much to what these are, the point is just that they're both groups coding the behavior of $T$ which are closely related in many ways. I'm thinking of $\pi_1(T)$ as the analogue of $\mathbb{N}$ and $H_1(T)$ as the analogue of a nonstandard model satisfying $\neg$Con(PA), respectively.

Now, the statement "$\pi_1(T)$ is abelian" (here, my analogue of $\neg$Con(PA)) tells us a lot about $T$ (take my word for us). But the statement "$H_1(T)$ is abelian" does not tell us the same things (actually it tells us nothing: $H_1(T)$ is always abelian :P).

We have a group $G$, and some other group $H$ similar to $G$ in lots of ways, and a property $p$; and if $G$ has $p$, we learn something, but if $H$ has $p$ we don't learn that thing. This is exactly what's going on here. It's not the property by itself that carries any meaning, it's the statement that the property holds of a specific object that carries meaning useful to us. We often conflate these two, since there's a clear notion of "truth" for arithmetic sentences, but thinking about it in these terms should demystify theories like PA+$\neg$Con(PA) a bit.

  • $\begingroup$ Also a very interesting point of view. Thank you for this answer! $\endgroup$
    – M. Winter
    Commented May 22, 2017 at 8:25

If I understand correctly you problem the key to solve it is to think carefully to the concept of encoding.

For simplicity allow me to consider the case where $T'$ is PA (Peano Arithmetic).

The internalization of the syntactic properties of PA in itself uses an encoding which is roughly a mapping that associates to formulas and proofs constant terms (their encodings) and to meta-theoretical properties ("$x$ is a proof of $y$ in PA", "$x$ is provable in PA", etc) formulas in the language of $T$ in such a way the following holds:

if $RS$ is a syntactic (meta-theoretic) property and $O_1,\dots,O_n$ are syntactic objects (formulas or proofs) then $RS(O_1,\dots,O_n)$ holds if and only if $PA \vdash Enc(RS)(Enc(O_1),\dots,Enc(O_n))$, where $Enc$ is the mapping that associates to syntactic objects their encodings in $PA$'s language.

The important thing to keep in mind is that this encoding-condition is required to hold only for encodings.

Now let consider a theory $T=PA+\neg Enc(Con(PA))$ in the language of arithmetic.

Clearly $T \vdash \neg Enc(Con(PA))$ but what does this mean? By soundness and completeness this is equivalent to say that in every arithmetic structure $M$ which is a model of $T$ it must hold $M \models \neg Enc(Con(PA))$. We have that $$Enc(Con(PA))\equiv \neg \exists x\ Enc(\text{*is a proof*})(x,Enc(\bot))$$ hence $$\neg Enc(Con(PA)) \equiv \exists x\ Enc(\text{* is a proof *})(x,Enc(\bot))$$ so in each model $M$ of $T$ there is an element $m \in M$ such that $$M \models Enc(\text{* is a proof *})(m,Enc(\bot))$$ the problem is that this $m$ is not an encoding, it is not even required to be the interpretation of a constant term, hence there is no way that we could decode this term to a proof (in PA) of $\bot$.

The point is that the formula $Enc(\text{* is proof of*})$ define a relation for each arithmetic structure but it has its intended meaning only when applied to encodings: meaning that $Enc(\text{*is a proof of*})(m,n)$ expresses that $m$ is the encoding of a proof of the formula encoded by $n$ only when $m$ and $n$ are encoding.

The argument shown here should be easy to adapt to other kind of theories such as the ones you described.

I hope this helps.

  • $\begingroup$ Very interesting! Is the following conclusion correct? If we assume that PA is consistent and our encoding (of proofs) is sound and surjective on the standard numbers, then we could be sure that $\neg\mathrm{Con(PA)}$ can not be provable. This is because then at least the standard model can have no element $x$ which is not an encoding of a proof. And because of soundness no $x$ can encode a proof of inconsistency. $\endgroup$
    – M. Winter
    Commented May 21, 2017 at 15:41
  • 1
    $\begingroup$ @M.Winter I would say that you are actually proving that $PA$ cannot prove $Enc(\neg Con(PA))$, which is even stronger than saying that $\neg Con(PA)$ cannot be proven (that would follow just by the requirement that $Con(PA)$ holds). $\endgroup$ Commented May 21, 2017 at 20:20
  • $\begingroup$ Yes of course ;) That's what I want to say. $\endgroup$
    – M. Winter
    Commented May 21, 2017 at 21:39

You must log in to answer this question.

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