# Can a formal system's consistency be an axiom of that system?

Godel's Incompleteness Theorem tells us that no formal system (with elementary arithmetic) can prove it's own consistency. Now, I've never heard of "limits" on what can and cannot be an axiom of a formal system, so I considered the following:

Let's say we have a formal system $\text{S}$. What if we define another formal system with an added axiom:

$\text{S}\ + \text{S is consistent}$

Does this raise any contradiction? It's hard for me to wrap my head around (I've never studied mathematical logic or axioms), but the way I see it, the axioms of a formal system can never raise any contradictions unless they contradict each other, and the consistency of a system does not contradict the system itself.

In fact, if we call this system $\text{S'}$, we can define another system $\text{S''}$:

$\text{S'}\ + \text{S' is consistent}$

And we can repeat this infinitely, creating a system that can prove it's own consistency. Is there a problem with this?

I find it incredibly difficult to wrap my head around this, so hopefully someone here can shed some light on the issue - is this a valid system? If so, what are the consequences of our consistency axiom?

Yes, you can do this - and in fact you can construct a hierarchy of such systems! This hierarchy can even be continued into the transfinite. See this question for more details.

However, note that $S+Con(S)$ does not necessarily prove its own consistency! The issue is that a contradiction could arise when we add $Con(S)$ to $S$, even if $S$ itself were consistent; see e.g this question. So there's no violation of Goedel's theorem here.

Interestingly, it turns out that the iteration process here is much more complicated than it may first appear. These complexities are very briefly touched on in this question, and are seriously delved into in the book "Inexhaustibility".

Now, you might ask (and you did, in your edit!): do we ever "catch our tail" and wind up with a consistent system which proves its own consistency? Or, in particular: why doesn't $S_\omega=S+Con(S)+Con(S+Con(S))+...$ prove its own consistency in general? In particular, it proves the consistency of each of its finite fragments, so doesn't that mean it proves its own consistency?

This is a bit of a subtle point. While $S_\omega$ proves "$Con(F)$" for each finite fragment $F\subseteq S_\omega$, $S_\omega$ does not prove "$Con(F)$ for each finite fragment $F\subseteq S_\omega$." This may seem weird, but this is a standard phenomenon, and here's a tamer example of it: by checking by hand, PA proves "$p$ is not a proof of a contradiction" for each PA-proof $p$; but PA clearly doesn't prove "for each PA-proof $p$, $p$ is not a proof of a contradiction," since this statement is exactly the consistency of PA! That is, in general, $$\forall n\in\mathbb{N}, T\vdash\varphi(n)\quad\not\rightarrow \quad T\vdash \forall x\in\mathbb{N}\varphi(x).$$ (Here I'm abusing notation a bit and conflating a natural number with the numeral representing it.) Basically, this is a consequence of proofs being only finitely long, and our needing to paste infinitely many $T$-proofs together to get a $T$-proof of $\forall x\in\mathbb{N}\varphi(x)$; and this can be made precise via the compactness theorem.

There's another trick we might try, by the way, one which better matches your title question. Start with a reasonable theory $T$ (like PA). Using the diagonal lemma, we can construct a sentence $\varphi$ such that $\varphi$ says "$T+\varphi$ is consistent". Let $S=T+\varphi$; then $S$ proves its own consistency, and seems to be built from $T$ by adding a "safe" axiom!

By Goedel's theorem, however, we know that (as long as $S$ is sufficiently powerful) this $S$ will be inconsistent. Even though this construction doesn't necessarily look much worse than the iterated consistency hierarchies described above, it turns out to be insidious, and figuring out how to construct a proof of a contradiction in it is a useful exercise towards understanding Goedel's theorem.

Meanwhile, if $S$ is not too powerful (or rather, if $S$ is really really weak), then it is possible for $S$ to prove its own consistency. Willard's paper is unfortunately behind a paywall, but the first two pages can be read, and the second page gives the "shape" of the axiom systems he investigates; in particular, you can see that they do in fact contain axioms asserting explicitly their own consistency. You may be interested in this other question, which explores some further subtleties around adding consistency statements to a theory.

• Huh! Just as you posted your answer I edited my question with a proposed construction of such a hierarchy - weird! Thanks for your answer, it really helps. I'm going to take a minute and try to wrap my head around it before asking any questions. – TreFox May 30 '17 at 16:14
• Ok, I think I understand. But why could a contradiction arise from adding $Con(S)$ to $S$, if $S$ is consistent? – TreFox May 30 '17 at 16:15
• Noah, I thought the question (at least, the first question, certainly the title) was whether, via coding, we can have $S$ such that $S\vdash{\rm Con}(S)$. Naturally, there would be restrictions on $S$ so we do not violate incompleteness but $S$ is still sufficiently expressible so some formal version of ${\rm Con}(S)$ makes sense. (There are such self-verifying systems.) – Andrés E. Caicedo May 30 '17 at 16:19
• @TreFox See my first linked question. Briefly, if $T$ is consistent (and reasonable), then by Goedel $T$ doesn't prove it's own consistency. But that means the theory $S=T+\neg Con(T)$ is consistent! And this $S$ proves its own inconsistency. – Noah Schweber May 30 '17 at 16:19
• @AndrésE.Caicedo Hm, I disagree. I think the body makes it clear that they are talking about iterating consistency principles. For instance, looking at the first question we have "Let's say we have a formal system $S$. What if we define another formal system with an added axiom: $S$ + $S$ is consistent" - that is, the new system is not $S$ itself, so we're not incorporating the consistency of a theory into the theory itself, but rather building a new one. – Noah Schweber May 30 '17 at 16:21