Does Gödel's incompleteness theorem imply that proofs by contradiction don't work?
I think what you're saying is this:
- Godel's incompleteness shows that there are statements $P$ such that neither $P$ nor $\neg P$ are provable from certain sets of axioms.
- Therefore, just knowing that $\neg P$ is not provable is not enough to conclude that $P$ is provable with such a set of axioms.
However, a proof by contradiction does not show that $\neg P$ is not provable: it shows that $\neg P$ is false. This is stronger. What makes proof by contradiction work is the law of the excluded middle or something equivalent to it, and when you work in a setting where the law of the excluded middle is valid (such as ordinary first-order logic), a proof by contradiction is no different from an ordinary proof.
People seem to generally get very hung up on the distinction between truth and provability. I'm not an expert in logic, but my understanding is as follows.
For any first-order theory (set of axioms) $T$ there is a notion of a model of $T$, which consists of a collection of sets, functions, and relations satisfying the axioms. For example, the models of the first-order theory of groups are groups. $T$ is consistent if it has a model. A statement $P$ is true if it is true for all models, and false if it is false for all models; in other words, truth is semantic. A statement $P$ is provable if it can be deduced from the axioms of $T$; in other words, provability is syntactic.
Godel's completeness theorem asserts that truth and provability are equivalent: a statement is true in all models if and only if it is provable.
Godel's incompleteness theorem, on the other hand, asserts that if $T$ satisfies certain conditions, there exist statements which are true in some models (in particular in "the one true model" that we care about, which in the case of arithmetic is the ordinary positive integers), but not in others. By the completeness theorem, this is equivalent to saying that neither $P$ nor $\neg P$ can be provable.
But this is not some weird, out-there property for $T$ to have. For example, obviously there are statements which are true for some groups but not for others, e.g. "$G$ is abelian." You can't prove this statement from the group axioms because there exist non-abelian groups, but you also can't prove its negation because there exist abelian groups. What the incompleteness theorem says is that even more sophisticated theories $T$ behave in this respect like the theory of groups: there are lots of models, and some of them behave differently from others. For example, there are models of Peano arithmetic which behave very differently from the usual natural numbers: they might have a number $n$ which satisfies $1 < n, 1 + 1 < n, 1 + 1 + 1 < n, ...$.
No, of course not. Proofs by contradiction "work" because of the Law of the Excluded Middle: if not-S is false, then S must be true. Godel says that (in a formal system with certain properties) there exist statements S such that neither S nor not-S can be proved. But that's not the same as saying neither S nor not-S is true.
No. And perhaps one should stop there.
Many theories are incomplete, because we want them to be. Look for example at the elementary theory of groups. It is easy to write down a sentence that says that the group has at least $47$ elements. This sentence is neither provable (after all, there are groups with $46$ or fewer elements), nor is its negation provable.
But when we seek axiomatizations for something like elementary number theory, we would like to choose the axioms so that any sentence is either provable or refutable. Unfortunately, it turns out that if we want our collection of axioms to be recursive, and we want all the axioms to be true in the non-negative integers, we can't do that. Too bad, but isn't it beautiful that we can prove we can't do that?
Proofs by contradiction work everywhere, both for theories that are incomplete by design (like the elementary theory of groups) and theories like elementary number theory, where we might wish to have a complete recursive axiomatization.
After all, proof by contradiction uses only basic reasoning. Suppose we want to show that if $p$ is true, then $q$ must be true. We examine possible consequences of $q$ being false. If we show that one of these consequences is that $p$ must be false, then we know that if $p$ is true, then $q$ is true. The rules of formal logic are designed to make that sort of reasoning available at the formal level.
The Incompleteness Theorem is mathematically fascinating. But the Theorem has also given rise to a great deal of informal speculation, often based on misreadings of the Theorem.