# Why is an internal proof of consistency satisfactory for some systems?

I've only a shallow understanding of the relevant theory, but I don't understand how any internal proof of consistency is in any way satisfactory (even for systems that are so weak Gödel's incompleteness theorem doesn't apply). After all, suppose you've proven consistency from the axioms, both things are possible

1. the system is inconsistent, and thus proves everything, including its own consistency
2. the system is consistent, and is one of those systems weak enough that Gödel's incompleteness theorem doesn't apply, and is capable of proving its own consistency

So upon proving the system's consistency from it's own axioms, you still can't conclude the system is consistent, for 1) could apply. Neither can you conclude it's inconsistent, for 2) could apply. You've effectively proven nothing.

However, from what I've read, people a lot more educated on this seem to disagree? I'd like to find the flaw in my reasoning.

• But we are working in a meta-theory, and in that meta-theory we generally begin by assuming something is consistent, or, you know, we can sometimes just prove it outright (e.g. theories of arithmetic pretty much required to be true in the standard model of PA). Nov 20 at 11:08
• On the technical level, your reasons seems correct, but it's a bit extreme to say that "you've effectively proven nothing". That is the case only if you were so naive as to attempt to prove consistency of a system using the system itself (who does that in the 21st century?). There may be other reasons why you would want to a self-consistency proof, e.g., to show that the system must be fairly weak. Nov 20 at 11:18
• Of course the main point of the OP is correct, and this is a fairly elementary point, which I always discuss when teaching the incompleteness theorem. Proving the consistency of a system within that system provides essentially no reason a priori to believe in the consistency of the system—it's like a con man presenting a letter of recommendation for himself, written by himself. (Now that we have the incompleteness theorem, our views about the situation are much more refined, in light of that.) Nov 20 at 13:09

The answer by user57888 is correct, but let me emphasize two things. The first is that much of the interest in this type of question predates Gödel's theorems. So if you want to understand the original motivation, you should pretend that you don't know Gödel's results. The second is that Hilbert's original hope was to prove the consistency of a strong system using a weak system. As you point out, there doesn't seem to be much if any philosophical gain if all we can prove using theory $$T$$ is that $$T$$ itself is consistent, but if $$T$$ is simple enough that you are willing to take its soundness for granted, then you do gain something if, on the basis of $$T$$, you can prove the consistency of some much stronger theory $$T'$$.

Of course, now we know that any $$T$$ that Hilbert might have been happy with can't even prove its own consistency, let alone the consistency of a stronger $$T'$$. This is why proving the consistency of $$T$$ on the basis of $$T$$ gets so much attention; it's a negative result that implies the weaker negative result ($$T$$ doesn't prove the consistency of $$T'$$) that we're really interested in.

• This seems to only push the objection back one layer, though. If a weaker theory $T$ proves the consistency of a stronger theory $T'$, then it's true that a reason to believe in the consistency of $T$ becomes a reason to believe in the consistency of $T'$; but conversely a reason to be suspicious of the consistency of $T'$ becomes a reason to be suspicious of the consistency of $T$. "One person's modus ponens..." et cetera Nov 20 at 17:03
• @SamHopkins There is no definitive way to refute extreme skepticism. A skeptic can be led to water but we cannot force the skeptic to drink. Hilbert suggested that we might trust "finitary" systems. If you are suspicious of them, then maybe it's time to give up math and take up shuffleboard. :-) Nov 20 at 17:45
• @TimothyChow Are we even sure shuffleboard can be trusted? Nov 21 at 2:53

The original context of Gödel's Theorem was slightly different. Famously, Hilbert had asked for a purely combinatorial proof of consistency for strong set theories. Notice that this seems like a very realistic programme: after all, having presented set theory, and thus essentially all known mathematics, as formal derivations, now we are only asking for a proof that a given formula is not formally derivable as the last instance of some well-described sequence of formulae. Essentially, this is a combinatorial question, like some tiling problem, and can be reasonably hoped to be solved not invoking the very notion of infinite sets.

So: you've asked what a consistency proof gives me if I don't really believe a theory in a first place. In the original question, we are asking about consistency proof for a theory we have concerns about done within a much weaker theory we fully trust.

Now, Gödel's Theorem is a much more powerful no-go result. Not only is it impossible to prove nonexistence of such proofs in finitary combinatorics (like Primitive Recursive Arithmetic), but also this is not possible if you allow any mathematical methods you accept. Of course, once you rephrase it this way, it starts to invoke this feeling of triviality you have rightly described. But how exactly do you know that this particular tiling problem cannot be solved? This clearly needs a proof which is precisely what Gödel did.

On a related note: by Matiyasevich, there exists a concrete polynomial $$p$$ such that the question whether $$p(n)$$ has integer roots is undecidable in ZFC. You could ask why we should consider it a deep fact, since that polynomial in fact says that ZFC is consistent. This is the crucial portion of what Gödel had realised: we can translate our metatheoretic notions and make meaningful statements about them within sufficiently strong theories.

• I don't think Hilbert ever spoke about "combinatorial proofs", but rather "finitistic methods". And I very much doubt axiomatic set theory was in focus. Hilbert's 2nd problem is about arithmetic, not about set theory. (This is not to say that the main points of the answer do not apply, I am just saying that history is tricky.) Nov 21 at 12:50
• @AndrejBauer It's true that Hilbert's 2nd problem was phrased as a question about arithmetic (probably meaning what we would today call second-order arithmetic), but elsewhere, Hilbert made it clear that he thought of "Cantor's paradise" as an essential part of mathematics, and he envisioned eventually proving the consistency of all of mathematics. This is perhaps clearer in his 1917 address, "Axiomatisches Denken," than in his 1905 address. I think he posed the consistency of (2nd order) arithmetic because it seemed a natural first step, not because he didn't have his eyes on set theory. Nov 21 at 15:52
• @TimothyChow: thanks for the clarification. Nov 21 at 22:33

People often reason like the OP, but I think the argument is invalid. Suppose a theory proves 2+2=4. According to the OP's reasoning, if the system is inconsistent, it proves everything, including 2+2=4. Therefore, you haven't proven anything, because maybe the system is inconsistent. But you have proven something! You have proven 2+2=4. (Taking Joel's analogy in comments after the question, you can't believe what a con man says about anything, not just a recommendation for himself.)

I thiink the OP has in the back of his mind a rather standard notion of mathematical proof - one starts with axioms one believes are true, and then by proving things, one establishes that other assertions called theorems are true, but these theorems can have no more epistemological certainty than the axioms. So proving the consistency of a theory, within a theory, does not add any epistemological certainty about its consistency, because we already know the theory is consistent - after all, the axioms are true, and truths can only validly prove truths.

But actually, you don't just know that a theory is consistent, just because its axioms are true. Think of it - maybe there are true axioms which produce an inconsistent theory. You start naively churning out theorems from the axioms and - boom - unexpectedly out comes the contradiction. Sure, there is an argument that says this can't be so - true axioms only validly prove truths, and a contradiction is not true - but that is just saying we can provide a proof. And that is what a theory is supposed to do - provide proofs.

That is, you believe in certain axioms X to be true. You want to know whether or not the theory T beginning with these axioms X is consistent. It might not be, who knows? Maybe T proves everything. You therefore set about trying to prove T's consistency, perhaps by formalizing the argument already cited. If you are able to prove it using only axioms which you believe to be true, then you can have confidence that T is consistent. Therefore, if you can prove it with the axioms X, you can have this confidence. Maybe you can prove it with other axioms in which you believe, but since you already said you thought axioms X to be true, using them and only them is kinda a nice feature.

Now someone will surely point out that, just because you have proved T is consistent, doesn't give you, in some sense, greater grounds to believe in the axioms X. And that is completely correct. But that wasn't the question. That is, proving the consistency of a system within itself can give an a priori reason to believe in the consistency of the system - it will if the axioms can be known a priori, and the rules of inference can be seen as valid a priori. What it cannot do is give an a priori reason to believe in the axioms of the system. (It may give a reason, but that reason is not a priori.)

• You write that "you don't just know that a theory is consistent, just because its axioms are true" . Even assuming a fairly weak notion of truth (namely, satisfiability in some structure), the soundness theorem guarantees that the truth (i.e. satisfiability) of a theory implies its consistency, at least assuming that the proofs in question are formalisable in some fixed deductive system for which the soundness theorem holds. Nov 21 at 12:50
• More importantly, in light of Gödel's incompleteness theorem, a formal proof of the consistency of a theory from its own axioms would constitute a (meta-mathematical) proof of its inconsistency. Nov 21 at 12:56
• @BenedictEastaugh. Exactly. That's the proof - "true axioms only validly prove truths, and a contradiction is not true" - of which I'm speaking.
– abo
Nov 21 at 13:16
• @Sam Hopkins. Some weak theories of arithmetic (not covered by Gödel) can prove their own consistency.
– abo
Nov 21 at 13:17