There are many proofs based on a "tertium non datur"-approach (e.g. prove that there exist two irrational numbers a and b such that a^b is rational).
But according to Gödel's First Incompleteness Theorem, where he provides a constructive example of a contingent proposition, which is neither deductively (syntactically) true nor false, we know that there can be a tertium.
My question: Are all proofs that are based on that principle useless since now we know that a tertium can exist?
You are confused.
The best way out of your confusion is to maintain a very careful distinction between strings of formal symbols and their mathematical meanings. Godel's theorem is, on its most primitive level, a theorem about which strings of formal symbols can be obtained from other strings by certain formal manipulations. These formal manipulations are called proofs, and the strings which are obtainable in this way are called theorems. For clarity, I'll call them formal proofs and formal theorems.
In particular, let G be a string such that G is not a formal theorem and neither is NOT(G). It is still true that G OR NOT(G) is a formal theorem. Moreover, if G IMPLIES H and NOT(G) IMPLIES H are both formal theorems, then H will be a formal theorem; because there are rules of formal manipulation that allow you to take the first two strings and produce the third. I believe that Douglass Hofstader discusses this in a fair bit of detail when he goes over Godel's theorem.
The above is mathematics. Next, some philosophy. I don't find it helpful to say that G is neither true nor false. It find it more helpful to say that our systems of formal symbols and formal manipulation rules can describe more than one system. For example, Euclid's first four axioms can describe both Euclidean and non-Euclidean geometries. This doesn't mean that Euclid's fifth postulate has some bizarre third state between truth and falsehood. It means that there are many different universes (the technical term is models) described by the first four axioms, and the fifth postulate is true in some and false in others.
However, in any particular one of those universes, either the fifth postulate is true or it is false. Thus, if we prove some theorem on the hypothesis that the fifth postulate holds, and also that the fifth postulate does not hold, then we have shown that this theorem holds in every one of those universes.
There are fields of mathematical logic, called constructivist, where the law of the excluded middle does not hold. As far as I understand, that issue is not related to Godel's theorem.
I accidentally ran into this old question and thought to give an example whose (humble!) intention is to permanently deconfuse anyone who knows just a little bit of undergraduate mathematics.
Consider group theory. In a typical introductory course, you will learn the simple axioms and immediately encounter sentences like
$$\forall y \forall x \forall z( (xy=e) \wedge (zy=e ) \Rightarrow x=z);$$
or slightly more complicated ones like
$$(\forall x(x^2=e ))\Rightarrow (\forall x\forall y(xy=yx)).$$
You also learn how to deduce them rather easily from the axioms of the theory.
How about the sentence
$$S:\ \ \ \ \ \ \ \forall x \forall y( xy=yx)$$
?
Can it be deduced from the axioms? Obviously not, but it requires at least a bit of thoughtfulness to prove that it can't. You see, we can just write down a structure like $S_3$ that satisfies the axioms of group theory, a model of group theory, and produce two elements in it for which the sentence is not true. Obviously we couldn't produce such a model if the sentence was a logical consequence of the axioms.
How then about $\neg S$? Can it be deduced from the axioms? Again obviously not. Consider the integers $Z$.
So we see that group theory is incomplete: We've written down a sentence $S$ such that neither $S$ nor $\neg S$ can be deduced from the axioms.
But here is an important point: If the context of the discussion was the group $Z$, is the sentence $S$ true? Yes, of course, and I can prove it for you. (Using more than the axioms of group theory, of course.)
For a complete theory, every true assertion $S$ (in the language of the theory) about a given model $G$ can be deduced from the axioms. This is because $S$ or $\neg S$ can be deduced, but if $\neg S$ could be deduced, then it would have to be true in any model of the theory, in particular, $G$. So $S$ would be false in $G$. But $S$ is true. Therefore, it must be the one that can be deduced. The upshot is that whenever you have a theory (like group theory) with a model that admits a true sentence that can't be deduced from the axioms, then the theory is incomplete. The point of boring you with this discussion is to illustrate that an incomplete theory is a very mundane object.
In case this suggests (as it should) that a complete theory, on the other hand, is bound to be very exotic, you might like this simple list of a few complete theories. For example, the theory of algebraically closed fields of characteristic zero is complete. This implies, in particular, a logical incarnation of the 'Lefschetz principle': A field-theoretic sentence true in $C $ is true in every algebraically closed field of characteristic zero. In fact, as noted above, a sentence true in any given model, since it can be deduced from the axioms, is true in any other model. I found this fact quite mind-boggling when I first encountered it. A good exercise is to see why a sentence like 'every element of $\bar{Q}$ is algebraic' doesn't cause a problem. (You need to get a bit more precise to do this, especially about the language of the theory.)
There is a complete theory of the natural numbers, by the way. Add to your favorite axioms of arithmetic all the sentences that are true in the natural numbers. This is a perfectly respectable complete theory, sometimes referred to as the theory of natural numbers. Goedel's first incompleteness theorem can be interpreted as saying this theory doesn't admit a recursively enumerable set of axioms. (Which should be at least intuitively plausible if you consider difficult unresolved problems like, say, Goldbach's conjecture.)
Added:
In my opinion, it's not such a good idea to emphasize the 'string of formal symbols and rules' point of view when explaining the incompleteness theorem. It's true that to prove the theorem, you need to set up such background formalities. But the statement itself can plausibly be interpreted as something about everyday reasoning in mathematics. We are usually interested in some structure, a rather specific one like $Z/2$, a somewhat more general one like 2-groups, or more general yet like all groups. The question concerns which properties (or axioms satisfied by the structure, if you prefer) we use to prove certain assertions. The everyday nature of this question was the reason for bringing up the commutativity of $Z$, which I can certainly prove in the course of a normal discussion on the chalkboard, but anyone can see requires more than group theory.
This question also comes up rather frequently as one of great interest to practicing mathematicians. An advanced example that I can remember off the top of my head is 'Can one prove the Kodaira vanishing theorem using only algebraic geometry?,' which was resolved first by Faltings (although there is room for interpretation of the phrase 'only algebraic geometry').
In some sense, the rationale for the abstract formalism surrounding the incompleteness theorem is also pretty commonsensical. To prove that something can be done, you just need to do it. For example, I think it is uncontroversial that the proof of the Kodaira vanishing theorem by Deligne and Illusie uses 'only algebraic geometry.' And then, there are the famous elementary proofs of the prime number theorem. To prove that something can't be done, on the other hand, often requires more careful foundations.
Added again:
After some conversations, I decided to put in a few final words of clarification. I hope I didn't slight anyone with the joke about 'permanent deconfusion.' I don't claim to have any serious understanding of philosophical ramifications, for example. However, I tried to articulate what seems to me a sensible view of the matter for practicing mathematicians. Starting from the one given, you can yourself quickly make up examples illustrating the (uninteresting) incompleteness of a large majority of the theories we usually work with, rings, fields, topological spaces, etc. After that process, and thinking through just the few implications of completeness already mentioned, if someone came up to you and claimed that Peano Arithmetic was complete, I suspect your eyes would pop out.
Someone once told me that a good way to sound sophisticated as an amateur logician is to proclaim that the completeness theorem* is much more important than the incompleteness theorem. That's perhaps too sweeping a statement, but it seems to be the one that's useful for usual mathematics. For people interested in pursuing this line of thought, I recommend the nice lectures delivered by Angus Macintyre at the Arizona Winter School in 2003:
http://math.arizona.edu/~swc/aws/03/03Notes.html
One intriguing observation there I sometimes think about is how number-theoretic completions (reals and $p$-adics) correlate to logically complete theories.
*The completeness theorem essentially says that a sentence is a logical consequence of the axioms if and only if it's true in all models of the axioms. The idea for the non-trivial direction is to show how to construct, given any sentence that can't be deduced, a model for the axioms in which it is false.
You're missing the distinction between truth and proof. Godel's Theorem says there are statements which are neither provable nor disprovable (from a given set of axioms). Those statements are still either true or false in a given universe. Godel just says your axioms aren't good enough to tell which one.
If you believe in classical logic, such proofs are still fine. Godel incompleteness just states that in first order logic, any system capable of expressing arithmetic must contain an undecidable formula P. You can still prove (P or ~P) - that's an axiom actually. In every model of the axioms either one or the other is true. So a classical mathematician (who is a platonist), says Godel's incompleteness theorem just shows that FOL is insufficient for expressing everything about the "real" mathematical universe, but that doesn't mean that the law of the excluded middle (LEM) fails. If you have a philosophical problem with this, you have some constructivist leanings. I have strong formalist tendencies, and would say that LEM is cool if you think its cool, and not if you don't like it. We should be free to change our foundations to suit our whims!
In classical logic, for any proposition $A$, either $A$, or $\lnot A$.
What Godel showed was that under certain conditions (which hold for the formal system most of us use) there are propositions $A$ such that neither $A$ nor $\lnot A$ are provable.
Note the difference between these statements. In one case it's about the assertions $A$ and $\lnot A$. In the other case it's about the provability of the assertions $A$ and $\lnot A$. The former is about whatever $A$ is about. The latter is about whether or not you can produce a string of symbols by following certain rules.
For example, if you assert "for all real $a>1, a^2>1$" you're saying something about real numbers. But if you assert "for all real $a>1, a^2>1$ is provable", you're saying something about how you can produce the string of symbols "for all real $a>1, a^2>1$" by following a bunch of rules. These two things are entirely different kinds of assertion.
In particular, if you know $A \lor \lnot A$, you can conclude that either $A$ is true, or that $\lnot A$ is true. But if you know that $A \lor \lnot A$ is provable, you can't deduce (in a classical context) that either $A$ is provable or that $\lnot A$ is provable.
As long as you make clear the distinction between asserting $A$ and asserting that $A$ is provable, you're fine.
There are reputable mathematicians who assert that "tertium non datur" arguments are at best incomplete and at worst meaningless. I recommend "A Constructivist Manifesto", Chapter 1 of Errett Bishop's "Foundations of Constructive analysis".
The idea is not to assert some "bizzare state" between truth and falsity, but rather to take seriously the possibility that there may be simple and natural propositions that (a) Are independent of ZFC and (b) Will not or can not ever yield to any compelling new intuition or axiom. The idea that in some magical timeless world such assertions are forever true or false in themselves is at least questionable, and Godel was the first to expose this difficulty.
I think that many of the responses here are overlooking the key part of your question, "Are all proofs that are based on that principle useless?". The question of whether LEM is not merely formally consistent but actually useful, i.e., pertaining to reality, is a deep question that has been debated for at least a century (since Brouwer). One partial answer to your question is that no, not all such proofs are useless, because often they involve LEM on propositions which are indeed decidable. In constructive mathematics, $\varphi \vee \neg \varphi$ is precisely what it means for a proposition $\varphi$ to be decidable, and making use of this fact in a proof amounts to calling a decision procedure.
