Is no proof based on “tertium non datur” sufficient any more after Gödel?

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?

-
I think it's a bit unfair to downvote this question. Logic can have many confusing aspects, and most people I know take some time to appreciate its subtleties. – aorq Oct 29 2009 at 15:42
I agree. This is a common error, and it is one that I think is not so naive that it is not of interest to mathematicians to know how to correct it. – David Speyer Oct 29 2009 at 16:06
This is somewhat addressed in some answers below, but this point is important enough that it warrants stressing here: questioning the validity of using the law of excluded middle is a legitimate (albeit minority) position, and it has a distinguished history. It just does not have much to do with Gödel's First Incompleteness Theorem, and indeed, pre-dates it by at least a couple of decades. – Thierry Zell Aug 13 2010 at 13:14

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.

-
This is a side comment, not a criticism of your answer: I find it quite helpful to think of a statement containing variables as neither true nor false. For example, for a real variable x, "(x+1)^3 > 0" is neither true nor false, but "(x+1)^2 > 0" is true. I have written about this in several places and talked to people about it. I get two reactions: One, like yours, is that that is a bizarre way to think. The other is "well of course -- that's the normal way to describe such assertions". Perhaps there is a Deep Divide among mathematicians... – SixWingedSeraph Oct 29 2009 at 15:20
My perspective is that both your examples are not full sentences. A full sentence should not have bound variables, so it should say: "For all x in R, (x+1)^3 > 0." or "For the x defined in Section 2, (x+1)^3>0.". Of course, we often drop the preceding phrase, but only because it is clear from context. But I've run into a lot of people who think the way you do, and I don't want to claim that I am more right in any absolute sense. I think one of the reasons that I have a hard time understanding the notation of predicate calculus was that it was invented by people who take your perspective. – David Speyer Oct 29 2009 at 15:48
Of course, when I wrote "bound", I meant "unbound". – David Speyer Oct 29 2009 at 15:51
For what it's worth, many standard presentations of predicate calculus call the things SixWingedSeraph is talking about "well-formed formulas" (or "wffs"), and then reserves the term "sentence" for wffs with no free (unbound) variables. Then the terms "true" and "false" are applied only to sentences, and not to wffs in general. There are some proof systems that allow non-sentence wffs in intermediate steps in proofs, while others only allow sentences as steps in proofs. – Kenny Easwaran Nov 6 2009 at 6:42
-1: The argument in the question is sketchy, but it is not confused. Your "answer" comes down to assertions involving "I don't find it useful" and existence of "different universes": I find it hard to see why anyone attracted by the argument in the question would find this response cogent. – Charles Stewart Jan 15 2010 at 12:37

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.

$$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.)

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.

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.

-
I'm afraid you're far too sophisticated for me. But I'll leave it to a professional to write down the absolutely correct version of group theory and its language in a way that my assertions make good sense. – Minhyong Kim Apr 14 2010 at 22:01
Isn't it pretty clear that "xy=yx" refers to multiplying group elements together? – Peter Samuelson Apr 14 2010 at 22:25
So these comments make sense, I'll explain the comments I deleted: I made a comment regarding some set-theoretic nonsense because I misread the post and didn't see that Minhyong was assuming the axioms of group theory instead of set theory. – Harry Gindi Apr 15 2010 at 18:23
Just found and not yet read, <a href="rsta.royalsocietypublishing.org/content/363/1835/…; title="abstract">here</a> an article on Skolem's thoughts on the meaning of that incompleteness. BTW, I found that incompleteness theorem (after I had learned it's precise formulation) not very surprising, but would have been shocked about a completeness theorem, as the later would show that elementary number theory were "trivial" and just like some chess game. – Thomas Riepe Apr 21 2010 at 14:13

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.

-
 Your fourth paragraph is slightly confusing. If you say "for all real $a>1$, $a^2>1$ is provable", you should really say "provable from a given collection of axioms". – Stefan Geschke Aug 30 2010 at 12:02

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.

-
Of course, G&ouml;del himself seems to have been a Platonist --- he thought that his result showed the poverty of formalism, and motivated the necessity of a direct cognitive link to the Platonic realm, for discovering mathematical truth! – Niel de Beaudrap Apr 15 2010 at 8:07
@Niel: Yes, and Cohn, it seems, was a passionate formalist..... Which goes to show how questionable it is to draw philosophical conclusions from mathematical results. – SJR Apr 15 2010 at 10:09
I don't think it is accurate to say that "Godel was the first to expose this difficulty". Brouwer was on record a constructivist some 20+ years before Godel's incompleteness theorem was published. It's the crisis in the foundations itself that sent mathematicians scrambling for fixes, one of which being the restricted use of excluded middle. – Thierry Zell Aug 13 2010 at 13:06

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.

-
 Even LEM on propositions that will never or can never be decided is not useless -- An LEM proof of a proposition indicates that attempts to prove the negation of the proposition are futile. A wise old logician once told me that the attempt to make proofs constructive is not so much a logical imperative as it is a crucial method of discovery. For example, the project of making constructive the fact that the rationals are dense in the reals gives rise to the discipline of diophantine approximation. – SJR Apr 17 2010 at 11:17