Good afternoon.
First of all, I want to thank the university authorities who are present, to thank the University of Cordoba, and to thank the Faculty of Philosophy and Humanities, for this honor which I find really moving. I consider myself an Argentinean-American, and I cannot imagine anything nicer than receiving an honorary doctorate from the oldest university in Argentina and one of the oldest in the Americas.
I'm really very moved. It's a great pleasure for me and my wife to be here in Cordoba, especially for such a nice reason, and for us to become acquainted with this city and its intellectual and scientific traditions.
So thank you very much.
Furthermore, in spite of what has just been said here by Professor Victor Rodriguez about my achievements, I don't think that I have accomplished very much. What I see constantly before me are the challenging questions that I have not been able to answer, the big holes in what we can understand. Very basic questions, such as whether it is possible to prove mathematically that Darwin's theory of evolution works or that it doesn't work --- either way it would be very interesting. Or the subject that I want to talk about today, which I will now introduce for you.
I used to work as a computer programmer; I wrote computer software and did theory as a hobby. So I'm an amateur mathematician and a professional programmer. That's how I used to earn a living.
People normally think that mathematics is a dry, serious subject where nothing dramatic ever happens. But in the past century math went through a revolution as serious as the one that took place in physics because of the theory of relativity and quantum theory. This fact is not well-known outside the math community, but it is becoming better known now.
In particular, I'm referring to a controversy over how mathematics should be done. There is a struggle for the soul of mathematics. I exaggerate a bit, but not too much. There is a struggle for the soul of mathematics between two different groups, two tendencies, two opposing viewpoints.
On one side there is the famous French mathematician Poincaré who spoke of the importance of intuition in mathematics. On the other side we have the German mathematician Hilbert who emphasized formalism and the role of the axiomatic method. The conflict is between intuition and formalism. In other words, is mathematics creative or is it mechanical? Stating it that way, I indicate my own biases.
You can see which side I am on: the romantic side. But the debate is still very much alive and I want to give you a concise history of this conflict.
About a century ago Hilbert proposed formalizing all of mathematics, dropping the use of natural language and making math into a formal axiomatic theory using an artificial language and mathematical logic. The key point is that Hilbert thought that math gives absolute certainty and that this implies that you can formalize mathematics completely in such a way that there is an algorithm, a mechanical procedure, for checking whether or not a proof is correct.
In other words, Hilbert believed that if math is objective not subjective, if it really is absolutely certain, this is equivalent to saying that there are rules of the game for carrying out proofs --- if no steps are left out and we use a completely formal language --- which provide us with a completely mechanical way to check if a proof is correct, that is, whether it obeys the rules. According to Hilbert, this is what it means to say that math gives absolute certainty, which is what most mathematicians believe, because math is a way of fleeing from the real world to a toy world where truth is black or white and proofs are absolutely convincing.
This is what Hilbert proposed about a century ago. And most people thought that it could actually be done, that one could formalize everything. Hilbert represented the orthodox, conservative position within the math community. People thought that it ought to be possible. In fact, some very pretty work was done trying to achieve what Hilbert had proposed, trying to fulfill his dream of formalizing mathematics completely and obtaining absolute certainty and total objectivity. [In particular, I'm thinking of Zermelo-Fraenkel set theory and of the von Neumann integers.]
But in 1931 and in 1936 there were two big surprises. In 1931 Kurt Gödel showed that Hilbert's project could never work, and in 1936 Alan Turing showed this completely differently and found a deeper reason why Hilbert's dream was unattainable.
These two pieces of work are greatly admired, but in my opinion the math community has a very ambiguous position about these two achievements. Gödel and Turing are heroes, but nobody wants to face the disturbing implications of their work.
What Gödel showed in 1931 is that Hilbert's dream is impossible because any formalization of mathematics --- any formal axiomatic system of the kind that Hilbert sought for all of math, to give absolute certainty, to show that the truth is black or white --- will necessarily have to be incomplete because some true results will be missing. In other words, no finite formal axiomatic theory can give us all mathematical truths, some of them will always escape us. In fact, an infinity of true math results will be missing from any formal axiomatic theory proposed to achieve Hilbert's dream. Formal axiomatic theories are always incomplete, they do not enable us to demonstrate all possible mathematical truths.
Gödel shows how to construct assertions which are true but cannot be demonstrated within a given formal axiomatic system. The way he does it is very surprising. He constructs a mathematical assertion --- in fact, an arithmetical assertion --- which states that it itself cannot be demonstrated.
If you can construct an assertion that states that it's unprovable, there are two possibilities: that it's provable and that it isn't. If it's provable and it asserts that it isn't, we're demonstrating something that's false, which is terrible. So by hypothesis we eliminate this possibility. If a formal axiomatic system enables us to prove things that are false, it doesn't interest us, it's a complete waste of time. Therefore "I'm unprovable" cannot be proved, which means that it is true.
So you either demonstrate things that are false, or there are indemonstrable truths, truths that escape us. This is the alternative that Gödel confronts us with. Assuming that the formal axiomatic system doesn't enable you to prove things that are false, there must be true mathematical assertions that cannot be proved.
Gödel incompleteness theorem was a big surprise at the time, and while not provoking panic, it did lead to some rather emotional reactions, for example, from Hermann Weyl. Weyl said that his faith in pure mathematics was badly affected, and that at first it was difficult for him to continue with his research. And Weyl was a very fine mathematician.
Now my story splits in two. On the one hand, there is more research on incompleteness, on Gödel's remarkable discovery. On the other hand, the math community begins to lose interest in these philosophical questions and continues with its everyday work.
First I'll tell you about Turing.
In 1936 Turing goes beyond Gödel and finds a much deeper reason for incompleteness. But I should emphasize that pioneering work is always the most difficult. Before Gödel nobody was courageous enough to imagine that Hilbert might be wrong. Turing found a deeper reason for incompleteness.
Turing discovered that there are many things in mathematics that can be defined but which there is no mechanical procedure, no algorithm, for calculating --- they are not computable functions. Math is full of things that can be defined but cannot be calculated. And uncomputability is a new source of incompleteness.
If we consider a mathematical question such as Turing's famous halting problem for which there is no general method for calculating the answer, we get the immediate corollary that there cannot be a formal axiomatic theory that always enables us to prove what the answer is.
Why not?
One of the most basic properties of a formal axiomatic theory is that in principle there is a mechanical procedure for systematically traversing the tree of all possible proofs and eliminating the ones that are incorrect. It would be very slow, but in principle it would enable us to find all the theorems. So if we have a theory that enables us to demonstrate in individual cases whether or not a program eventually halts, this would give us a mechanical procedure, an algorithm, that always gives the correct answer, which Turing showed in 1936 is impossible.
So Turing deduces Gödel incompleteness from a more fundamental idea, uncomputability, which is the fact that math is full of things that can be defined but cannot be calculated.
Now World War II begins and the generation that was interested in these philosophical questions disappears from the scene. The math community goes forward forgetting the crisis that was provoked by Gödel's theorem which had been such a big surprise.
My problem is that I didn't go forward. I remained obsessed with Gödel's theorem. I thought it had to be very important. I bet my professional career on the idea that it was a mistake to ignore Gödel's result.
What the math community did, since they are mathematicians and not philosophers, is to continue with their daily work, with the problems that interested them. The consensus was that yes in theory there are limits to what can be demonstrated using any particular formal axiomatic theory, but not in practice, not with the kinds of questions that interest us, not in our own particular field. This was more or less the community's reaction.
In other words, while there may be mathematical facts that are true but unprovable, these are highly artificial pathological cases. The consensus was that in practice this does not occur. At least that is what mathematicians preferred to think in order to be able to carry on with their work.
People have an amazing ability to avoid thinking about unpleasant subjects such as death. If we think about death all the time it is impossible to function. And if mathematicians think all the time about incompleteness they can't function either, since there will always be doubt about whether the matter at hand can be settled by means of a proof. Why am I wasting years of my life trying to prove something if there may not even be a proof?
Let's consider an alternative course of action. Instead of ignoring Gödel's theorem, what if we take it very seriously? I don't believe in going to extremes, but if one took Gödel's result very, very seriously, how might one proceed? Consider the Riemann hypothesis. This is an important mathematical conjecture that has a lot of significant consequences. But unfortunately in a hundred and fifty years of effort nobody has succeeded in proving the Riemann hypothesis. Mathematicians don't know what to do; the way forward is blocked. But physicists would just consider the Riemann hypothesis to be a mathematical fact that has been corroborated empirically.
In other words, I think that a possible reaction to Gödel's result is to make math a little bit more like theoretical physics. In physics axioms don't have to be self-evident. Maxwell's equations and the Schrödinger equation are not self-evident but they help us to organize, to unify a large body of experimental data.
One could do mathematics in a similar fashion, taking Gödel as justification for behaving as if math were an empirical science in which one doesn't try to demonstrate everything from self-evident principles, but instead one only seeks to organize mathematical experience like physicists organize their physics lab experience. One could proceed pragmatically and adopt unproven hypotheses as new basic principles because they are extremely fruitful and have many useful consequences even though they aren't at all self-evident. This is what I think we should do if we take Gödel's theorem seriously.
In my opinion mathematics is different from physics, but maybe not as different as most people think. My work on metamathematics using complexity and information-theoretic ideas suggests to me that perhaps we should emphasize the similarities between the world of mathematics and the world of physics instead of emphasizing the differences.
In this connection, there is a highly pertinent remark by the Russian mathematician Vladimir Arnold. In his opinion the only difference between mathematics and physics is that in mathematics the experiments are cheaper, since one can carry them out on a computer instead of having to have a laboratory full of expensive equipment! So math experiments are easier than physics experiments.
How do I try to justify this new "quasi-empirical" view of mathematics? Well, like most mathematicians, I do in fact believe in the Platonic world of math ideas in which the truth is totally black or white. But I also believe that we are denied direct access to this Platonic world and that down here at our level it may be helpful to work a bit more quasi-empirically.
It may look like my mixed, hybrid, Platonic-empiricist position is inconsistent, but I don't think that this is actually the case. Indeed, it is sometimes very fruitful to take ideas that seem to be inconsistent and show that in fact they aren't.
Okay, so where do I find arguments in favor of this quasi-empirical view of mathematics? The key question is whether the incompleteness phenomenon that was discovered by Gödel and further explored by Turing is exceptional or widespread. How pervasive is incompleteness? That's the basic question, and it is quite controversial.
My contribution to this discussion is that I've found tools for measuring the complexity or the information content of a formal axiomatic mathematical theory. And by using the concept of complexity in algorithmic information theory one can see that incompleteness is natural, not surprising. In fact, it's inevitable, it's unavoidable.
Using algorithmic information theory, one can see that the world of mathematical truths, the Platonic world of mathematical ideas, is infinitely complex. But any formal axiomatic system made by human beings necessarily has only finite complexity. Indeed, rather low complexity, since the axioms and rules of inference normally fit on a couple of pages.
So seen from this perspective, incompleteness is natural, inevitable. The world of mathematical ideas is infinitely complex, but our theories only have low, finite complexity; otherwise they wouldn't fit in a mathematician's brain nor would they be regarded as self-evident --- but I'm against the idea that in mathematics axioms have to be self-evident, because in physics self-evidence of axioms is not required.
I've used complexity and information theory to argue that since the amount of information in pure mathematics is infinite, incompleteness is only to be expected, since a formal axiomatic theory can capture at most a finite amount of this mathematical information, an infinitesimal portion in fact.
This more or less summarizes an entire lifetime of research. But you will not be surprised to learn that the mathematics community has not accepted my quasi-empirical proposal. The immune system of an intellectual community is very strong, and my ideas are rejected as foreign, as alien to the math community.
Logicians don't care much for computability, for complexity, for information and for randomness. Randomness is a nightmare for a logician, because randomness is irrational. Random events happen for no reason, they are incomprehensible from a logical point of view.
However the physics community has some interest in my work. They like the idea of using a physics-inspired approach in pure mathematics. They like the idea that math isn't that different from physics. They like the idea that a mathematics proof may be more convincing than the heuristic arguments that are accepted in physics, but that this is only a matter of degree, not an absolute black or white difference. They have always felt that mathematicians believe too much in absolute truth, and do not appreciate theoretical physics enough.
But the coin is two-sided, and the conflict between intuition and formalism has become much more acute because of the computer. Computer technology is a powerful argument against creativity and in favor of mechanization and formalization.
Just take a look at the December 2008 issue of the Notices of the American Mathematical Society which you can find for free on the web. This is a special issue devoted to formal proof. While I, a poor theoretician, have been trying to convince mathematicians to pay attention to Gödel's theorem and work slightly differently, these people --- I didn't realize what was happening until they did it --- have nearly succeeded in carrying out Hilbert's dream.
They've constructed tools for formalizing almost all of mathematics. They've done a superb piece of software engineering.
This community, which is a group of fine mathematicians and software engineers, believes that in the future all mathematical proofs should be formal proofs. In their opinion, there will soon be no reason for accepting informal proofs. We can start demanding formal proofs and re-writing all of mathematics in a formal language so that it can be checked by verification software.
There are now interactive proof checkers for verifying mathematical proofs. This is how these work: If I'm a mathematician and I have an informal proof that I want to formalize, I give it to the proof checker. It will say, "Well, there's a particular step in this proof that I don't understand yet. Can you please explain this better?" And you keep filling in the proof, providing more details, until the software says, "Now I understand everything. It's all fine. I have a complete formal proof."
You didn't have to write all the steps in the formal proof yourself; that would be a big job. You write part of it, and the software provides the rest. The final result of this joint effort is a complete formal proof that has been checked and verified by reliable software, software that you trust because it was carefully developed using the best available software engineering methodology.
And this verification technology has advanced to the point where you don't just verify toy proofs, you can verify complicated proofs of really important theorems, for example the four color theorem, which states that four colors suffice for coloring maps without having neighboring countries with the same color.
This was a rather complicated proof that not only was formalized, the mathematician who did it did not complain and even stated that going through this process enabled him to substantially improve the proof. So this formal proof business is getting really serious.
Hilbert never thought that mathematicians should be required to use detailed formal proofs in their daily work. But this community does. Furthermore, they envision an official repository for formal proofs that have been put through this verification process. Proofs will have to be accepted by this repository to be used by the mathematics community; everything that has been formalized and checked will be there, in one place.
So amazingly enough, the lines of research opened up by Hilbert's formalization proposal and by Gödel's work on the limitations of formal systems are both progressing dramatically. I think there is a wonderful intellectual tension between the work advancing formalization and the one criticizing it. Both of these lines of research are going forward splendidly in parallel!
In mathematics this circumstance is striking because one thinks that the truth is black or white. But in philosophy this situation doesn't seem so strange because philosophers understand that ideas that seem contradictory are often in fact complementary.
I won't try to predict the final outcome of this conflict; probably there will be no final outcome. In philosophy there are no final answers. Each generation does its best to resolve the fundamental questions to their own satisfaction, and then the next generation goes off in a different direction.
So I won't try to predict the future. I don't know if mathematicians will eventually think that incompleteness implies that they should do math differently, or if formalization will win.
Perhaps we don't have to choose between quasi-empiricism and formalization. Both of these approaches can contribute something to mathematics and to mathematical practice.
My late friend the mathematician Gian-Carlo Rota, whose provocative ideas I greatly enjoy, has bequeathed us a collection of his essays entitled Indiscrete Thoughts. He thinks that formal axiomatization is a cemetery.
When a theory is completely finished, then you can formalize it.
But when you are creating a new theory, you have to work with vague intuitions, with imprecise ideas, and formalization is deadly. Premature formalization stifles creativity; once a theory is formalized it becomes stiff and rigid and no new ideas can get in.
So I think that quasi-empiricism and formalism can both contribute something of value. Furthermore, both are advancing step by step.
In 1974 I proposed accepting new math axioms the way that this is done in physics, ["Information-theoretic limitations of formal systems," J. ACM 21, 1974, pp. 403--424.] and nobody took me seriously, but in the past thirty-five years this has actually happened.
It has happened in set theory, where there's a new axiom called "projective determinacy." It has happened in theoretical computer science, where you use the hypothesis that P is not equal NP, which everyone believes but nobody can prove. And it has happened in mathematical cryptography, which is based on the assumption that you can't factorize big numbers quickly.
In these fields mathematicians are behaving as if they were physicists. They've found new principles that enable them to organize the experiences of each of these communities. These are principles that are not self-evident, that have not been demonstrated, but that are accepted by consensus as new fundamental principles, at least until they are disproven or counter-examples are encountered.
Each of these mathematical communities is behaving as if they were theoretical physicists, they are doing what I call quasi-empirical mathematics. So I've been delighted to witness these developments, but not so delighted to see the striking advance of formalism in recent years.
These questions are still open, and they are very difficult ones. I've tried to argue in favor of a quasi-empirical stance, in favor of creativity and against formalism, but I myself am not completely convinced by my own arguments. More work is needed. We still do not know to what extent math is mechanical or creative.
Thank you very much!
[25 Dec 2009]