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.
Best Answer
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.