Consider the theory with the following axioms:

  • The axioms of ZFC
  • The "axiom of consistency": "This theory, including this axiom and all of the theory's other axioms, is consistent." Phrased differently (and equivalently):

    • This theory does not prove $\text{False}$
    • This theory states its own consistency as an axiom.

Can one have such a theory, one that includes its own consistency as an axiom? Can this theory be consistent?

  • 3
    $\begingroup$ I seem to recall reading that Hilbert tried to get away with this sort of thing, but it's clear it can't work in general. If there's a contradiction in ZFC, there will still be a contradiction when you add "ZFC is consistent" to it. $\endgroup$ – Cheerful Parsnip Jul 4 '16 at 4:33
  • $\begingroup$ A lot of things studied in Axiomatic Set Theory is the metamathematics. If you ever read Kunen and learn about basic model theory, you find that a lot of the deeper stuff is about showing how Con(ZFC) |-- Con(ZFC + CH) and things of the sort. What I just wrote there means that assuming ZFC is consistent, then so is ZFC with the continuum hypothesis (CH) as an additional axiom. You can also (through a much harder process called forcing) show how The consistence of ZFC implies the consistency of ZFC plus the negation of the continuum hypothesis as an additional axiom. $\endgroup$ – gorzardfu Jul 4 '16 at 5:10
  • $\begingroup$ The crux of this Question is making sense of how "this axiom" refers to itself. There will be many Godel-like encodings of meta-properties of a set theory, such as Con(ZFC), so we cannot rely on an informal mention of such a property in formalizing axioms. $\endgroup$ – hardmath Jul 4 '16 at 18:28
  • 3
    $\begingroup$ I'm not entirely sure what's unclear in this question. Yes, this "axiom of consistency" is unclear, but it is the crux of the issue here. This is the confusion... $\endgroup$ – Asaf Karagila Jul 17 '16 at 10:10
  • $\begingroup$ Is there anything wrong with my answer? $\endgroup$ – Asaf Karagila Aug 4 '16 at 4:57

What is this "axiom of consistency"?

Is it the statement $\operatorname{Con}(T)$? Because $T+\operatorname{Con}(T)$ is not the same as $T$. Or do you mean that $T=T+\operatorname{Con}(T)$? Which is just to say that $T$ proves its own consistency.

And if $T$ proves its own consistency, then it must violate one of the conditions of Gödel's theorem:

  1. So either $T$ is not recursively enumerable,
  2. or it is not consistent,
  3. or it is not strong enough to interpret arithmetic.

If by adding one axiom to $\sf ZFC$ you managed to violate any of these, it has to be the second condition. So either $\sf ZFC$ was inconsistent in the first place, or that $\sf ZFC$ proves the negation of your new axiom, and you've added a new contradiction to the system.

  • $\begingroup$ Adding the axiom $Con(T)$ to $T$ is obviously not the same as adding to $T$ the axiom that we can prove $Con(T)$ inside $T$, so what did you mean ? And it seems for saying $T+Cont(T)$ is not consistent or not able to formalize the arithmetic, we need to prove $Cont(T+Con(T))$ inside $T+Con(T)$ $\endgroup$ – reuns Jul 18 '16 at 1:24
  • $\begingroup$ Con (T) is not the same as con ([T]) ,where [T] is an encoding of T . In some systems, such as T=ZF or T=ZFC, there is no sentence Con (T) as any attempt to state it would require an infinitely long sentence. $\endgroup$ – DanielWainfleet Jul 18 '16 at 2:32
  • 1
    $\begingroup$ @user254665: No, Con(T) is a statement about the natural numbers, after coding T via Goedel coding and internalizing the first-order logic. Since ZF and ZFC are recursively enumerable, Con(ZF) is a simple first-order statement in the language of arithmetic, which can be interpreted in ZF using the finite ordinals and ordinal arithmetic. So it is most certainly not an infinitely long sentence. $\endgroup$ – Asaf Karagila Jul 18 '16 at 4:19
  • 1
    $\begingroup$ @user1952009: The OP said that the axiom of consistency for T is "T with this axiom is consistent". So this is not the situation that we add to T the axiom Con(T). $\endgroup$ – Asaf Karagila Jul 18 '16 at 4:20

Let me address a point which is implicit in the question but hasn't been squarely addressed by the other answers. Your description of the "axiom of consistency" is not precise: it is not at all obvious how to encode this axiom in the language of set theory. In particular, there is no direct way to encode the self-reference involved in saying "this axiom".

Here is one way you might try to make it precise. Let us say that a sentence $\varphi$ in the language of set theory can encode your "axiom of consistency" if $$ZFC\vdash \varphi\Leftrightarrow\text{"ZFC$+\varphi$ is consistent"}.$$ Now unfortunately, this criterion is rather weak. For instance, if $\varphi$ is any sentence that ZFC proves to be false, then it satisfies this criterion, with both sides of the implication simply being false.

Nevertheless, there still is a reasonably "natural" candidate for such a $\varphi$: you can construct a sentence $\varphi$ that can naturally be interpreted as saying that ZFC$+\varphi$ is consistent, by essentially the same trick as is used in Gödel's incompleteness theorem. More generally, such self-referential statements can be constructed by the diagonal lemma.

So there is a reasonable candidate for the theory you are proposing. Unfortunately, this theory is inconsistent by Gödel, as discussed in Asaf's answer. In fact, Asaf's answer shows that the sentences $\varphi$ satisfying the criterion above are exactly the sentences which ZFC disproves!


Yes, one can have a theory that includes its own consistency as an axiom.

That theory is always (by Gödel's Second Incompleteness Theorem) inconsistent.

  • 1
    $\begingroup$ That's not true (see Asaf's answer). $\endgroup$ – Stefan Mesken Jul 4 '16 at 10:59
  • 2
    $\begingroup$ @Stefan The theory described in the question is meant to be recursive. $\endgroup$ – Andrés E. Caicedo Jul 4 '16 at 13:19

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.