Does Gödel's incompleteness theorem contradict itself?

Question

I have problems understanding Gödel's incompleteness theorem. I presume I have a misunderstanding of some phrase or I have to look closer at the meaning of some detail.

Gödel's second incompleteness theorem states that in a system which is free of contradictions, this absence of contradictions is neither provable nor refutable.

If we would find a contradiction, then we would have refuted the absence of contradictions. Gödel's theorem states that this is impossible. So we will never encounter a contradiction. Doesn't that mean that no contradiction exists? (If one existed, we could encounter it.) So this seems to be a proof that no contradiction exists. Thus, we proved the absence of contradictions, which contradicts the second incompleteness theorem.

This is a contradiction which I can't solve.

Answer 1

I know this is late, but your comment about "inside" and "outside" is the crux. Basically "proof" is always relative to the proof system.

Define a formal system as useful iff it has a proof verifier program. Godel effectively showed that there is a program that, given the proof verifier for any useful formal system $S$, will always output a sentence $Con(S)$ over PA, such that ( $\mathbb{N} \vDash Con(S)$ ) iff S is consistent. Note that this can only be stated and proven in a meta-system that is strong enough to effectively reason about programs and halting behaviour, which includes 'knowing' $\mathbb{N}$ as some 'structure' that satisfies PA. Godel-Rosser's theorem is that if $S$ is a consistent useful formal system that interprets arithmetic, then $S$ does not prove the interpretation of $Con(S)$. See this post about the specific case where $S$ is an extension of PA, and be careful not the make the same mistake as Robert Israel.

For more details and a bit on provability logic, see this post. The incompleteness theorem is actually far more general than most textbooks set out, because it applies to any useful formal system as I've defined above, including non-classical logics, yet-to-be-discovered logics, ... For the general case we must define what "interprets arithmetic" means, which I do in this post before proving the general incompleteness theorem using a different proof from Rosser's. And for a more precise calibration of what is "strong enough" for the meta-system, see this post.

Answer 2

I'm a bit of a novice here, but I think this may help.

(Note: I'm using Peano Arithmetic (PA) here but you can replace it with whatever theory you're talking about the Second Incompletness Theorem (G2) with respect to.)

Definitions

1. A theorem of PA is defined to be a sentence in PA's language (i.e. a string of PA's symbols satisfying certain conditions) which can be concluded from the axioms of PA by finite applications of the rules of inference of PA (those of first-order logic).
   • If S is a theorem of PA, we say PA proves S (symbolically, PA$\vdash$S). Otherwise, we say PA does not prove S (symbolically, PA$\nvdash$S). With this notation, we can state G2 as PA$\nvdash$ConPA].
2. "PA is consistent" means there is no pair of theorems of PA which are each other's negation, and "inconsistent" means not consistent.

Clarifying Key Notions

There is a statement (let us call it ConPA) in the language of PA (i.e. ConPA is a string of symbols that can actually be written out--although it takes pages), that is true in the standard model of PA iff PA is consistent (and so its negation is true iff PA is inconsistent). Crucially, by the previous sentence, I do not mean PA can prove ConPA iff PA is consistent, and I do not mean ConPA is true iff PA can prove ConPA. I mean ConPA is true iff PA is consistent. (When people talk about whether PA can prove its own consistency, all they are talking about is whether PA proves ConPA.) G2 is this: "if PA is consistent, PA does not prove ConPA i.e. PA$\nvdash$ConPA." Note that G2 is not a theorem of PA. As I've presented it here, G2 is just a general fact about the world, and is not a sentence (let alone a theorem) of any formal theory (although, as I recall, it can be sort of paraphrased and proven in some formal theories in much the same way that, in PA, ConPA paraphrases "PA is consistent" although PA doesn't prove ConPA). It is a direct consequence of the soundness of PA (the fact the axioms of PA are true and the rules of first-order logic are truth preserving) that if PA is consistent then PA$\nvdash \neg$ConPA--this is not a consequence of G2 as far as I can see.

Actually Answering the Question

If I understand the question correctly, it expresses concern that it follows from G2 that PA (or any formal theory) is consistent since if it wasn't there would be a contradiction in it and that would mean PA would prove its own inconsistency, which is just what G2 says it cannot do--a putative contradiction itself.

Various issues with that: G2 doesn't say that PA can't prove its own inconsistency; it says that if PA is consistent, it can't prove its own consistency--an inconsistent theory proves everything in its language. While it does follow from the soundness of PA (which is a fact) that if PA is consistent then PA doesn't prove its own inconsistency (and maybe this is sometimes considered part of G2), this does not show that PA does not prove its own inconsistency because we don't know for sure that PA is consistent. Now you might be concerned that under the assumption that PA is consistent, the fact (the conclusion of G2) that it cannot prove its consistency (that is, prove ConPA) would mean that PA isn't consistent and this would contradict G2. But this implication (if it doesn't prove a sentence S, then S is false) would only hold if PA were complete and it is not complete as the first incompleteness theorem shows.

Answer 3

It does not state that the absence of contradictions is not refutable. However "Gödel's second incompleteness theorem states that in a system which is free of contradictions, this absence of contradictions is not provable" is accurate.

It may be the case that ZFC for example is consistent and also that "ZFC is inconsistent" is a theorem of ZFC.