GÖDEL AND THE NATURE OF MATHEMATICAL TRUTH II
Great to find the "Nature of Mathematical Truth" up for discussion on Edge! We do need interdisciplinary dialogue and Edge is certainly offering a fine Forum. My comments will attempt to fill in context and add a touch of reality to the picture of the creative mathematician. Creativity being taken for granted by the profession, I prefer to avoid words that are losing their luster by indiscriminate use.
The hard working mathematician is struggling, be it with Platonic reality, the mysterious wiring of his brain or the limited power of human imagination. When at her wits end my mother used to bemoan the fate of man, doomed forever to rattle at the gates of his limitations (an seinen Grenzen zu rütteln). Incompleteness is indeed a limitation phenomenon.
Most Edge dwellers will be familiar with what Gödel's proof achieved. But among the general public there is still a maze of deplorable misconceptions. I am incapable of making any comments before laying out the land. Respect for my audience prompting me to avoid cheap short cuts, I will need a few subtle distinctions to place Gödel's achievement into perspective. But, in deference to our IT media rather than to the audience, I will avoid formulas.
We need to reach out and talk to each other. That is just what Edge is facilitating and I appreciate the opportunity to make a few clarifying comments to the current surge of Gödel lore.
Gödel's notoriety had a slow start. It took more than a decade until the incompleteness theorem gained the attention of the general mathematical community. Onto the popular stage it jumped with a bang in 1979; Douglas Hofstadter's inspired act of popularization.
Here is a true story that brings home the need for cross-disciplinary communication:
I had heard of the book Gödel, Escher, Bach from some enthusiastic students at Calgary, but not seen it, when I visited the Tatski's in summer 1979 in Berkeley. Noticing the Hofstadter book in Alfred's bookcase I asked him what he thought of it and he exclaimed: "awful, of course it's awful". When I asked whether he had read it he said "of course not". But when I asked him to let me borrow it he got annoyed; the publishers had sent it to him, it belonged to him, and I could not borrow it, of course not.
I must add that I had been working with Tarski, that we were old friends and that it is not too far fetched to call Tarski and Gödel the two pillars of modern mathematical logic. They were of the same generation and had come to America during the late thirties from Poland and from Austria respectively. But they were temperamentally totally different personalities. Tarski was an empire builder.
Anyway, I went straight to Cody's and bought the Hofstadter book, fervently hoping that I would find it wonderful and could teach Alfred a lesson about his prejudices. Well, Alfred had been right after all. When I returned to Calgary at the end of the summer I found a copy of the Hofstadter book waiting for me with a note from the Canadian Journal of Philosophy asking me to review it. I actually had fun doing that review, I was younger then and instead of getting upset I enjoyed making it into a twin enterprise of a parody and a minimal no-nonsense account of Gödel's proof.
What does get me down nowadays is to find the same kind of rash misconceptions still proliferating in the public arena. The popular writers don't consult the experts, or don't listen to them, and the experts don't encourage the public to ask and listen.
Now, let me turn to the Edge 162 of June 8, 2005 headed by a synopsis of the story Rebecca Goldstein is telling:
"Gödel mistrusted our ability to communicate. Natural language, he thought, was imprecise, and we usually don't understand each other. Gödel wanted to prove a mathematical theorem that would have all the precision of mathematics — the only language with any claims to precision — but with the sweep of philosophy. He wanted a mathematical theorem that would speak to the issues of meta-mathematics. And two extraordinary things happened. One is that he actually did produce such a theorem. The other is that it was interpreted by the jazzier parts of the intellectual culture as saying philosophically exactly the opposite of what he had been intending to say with it."
This may sound interesting, but, disregarding history and context, it is misleading a potentially receptive audience. Ms Goldstein's claim to knowledge of Gödel's personal motivations is presumptuous. Her conjecture is, in fact, incorrect as a glance at Gödel's introduction to his famous paper, quoted below, shows. It is hard to talk about mathematical truth without having battled with it and understanding where we are at now with this conundrum.
The distrust of natural language is age old, so is the flight into music, poetry and the abstractions of mathematics, to mention only a few escape hatches. Already Leibniz proposed a characteristica universalis. Russell and Whitehead aimed at an all-encompassing formal Foundation in their Principia Mathematica and various versions of symbolic Logic were being investigated at the time of Hilbert's Foundations of Geometry (1899) and his incendiary proclamation, at the international congress of mathematicians in Paris (1900), of a list of tasks for the 20th century; among them a formal proof of the consistency of the axioms of arithmetic under the rules of classical logic. A formal consistency proof is not to appeal to the truth of axioms nor to the truth preserving properties of the deductive mechanism; it is expected to be based solely on the combinatorial structure of the system under investigation. Hilbert was demanding a finitary proof, a proof that could be encoded in arithmetic.
Hilbert's dogmatic optimism concerning the powers of formalism is often exaggerated; his own fault, he had a tendency to polemic rhetoric. For balance of perspective consider a quote from his address on infinity of 1925:
"Now to be sure, my proof theory cannot specify a general method for solving every mathematical problem; such a method does not exist. But the demonstration that the assumption of the solvability of every mathematical problem is consistent falls entirely within the scope of our theory." 
Approaching Hilbert with today's demand for rigor and lucidity can be most frustrating. In how many a seminar session did I discuss his infinity paper with my most astute students and it still is not clear to me whether by the solvability of every mathematical problem Hilbert meant the law of the excluded middle or syntactic completeness. I will come back to this distinction in the section on Intuitionism.
A brief glance at the three annotated collections of original papers on the foundational issues of that time by Jean van Heijenoort , by Martin Davis  and by Benaceraff and Putnam  will put the current Edge discussion into context for the interested reader. They contain translations of Gödel's first publication in 1931 of his incompleteness theorem: "On formally undecidable propositions of the Principia Mathematica and related systems." :
Königsberg, September 7, 1930
The story of the first announcement of the incompleteness theorem is told by Feferman et al. in the commentary to Gödel's completeness paper  in the first volume of Gödel's collected works ; as fascinating as any current news story of a scientific breakthrough. The occasion was the second conference on Epistemology of the exact sciences organized by the Society for Empirical Philosophy in Königsberg, held on 5-7 September 1930. On the 6th Gödel presented the results of his PhD thesis, that is, his proof of the equivalence between the formal concept of derivability and the semantic notion of consequence for first order languages. On Sunday the 7th the conference concluded with a discussion of foundational problems aroused by the key addresses of Carnap on Logicism, Heyting on Intuitionistic Foundations and von Neumann on the axiomatic method.
Towards the end of that discussion Gödel apparently made his "seemingly casual but dramatically timed announcement" (Dawson) of the discovery of formally undecidable propositions. At first the audience was baffled and Gödel is described as somewhat tentative, but then he really got off the ground and now the editors of Vol 1 themselves are baffled, trying to explain Gödel's surge of boldness psychologically. My hunch is that he had more of a sense of humor and a knack for one-upmanship that he is ever credited for, his legendary aloofness notwithstanding.
First Gödel observed that:
"No formal system can, with certitude, be claimed capable of representing all contentual trains of thought."
After that statement the editors of volume 1 insert three asterisks, to mark a pause of presumably baffled silence broken only by von Neumann's vigorous assent, pointing out that:
"It remains unsettled whether all intuitionistically acceptable means of proof are formally representable."
To which Gödel responded — after the editors' three asterisks — by announcing that:
"One may, in fact, exhibit sentences, which, although intensionally correct (true), are not provable in the formal system of Mathematics."
"The adjunction of the negation of such a sentence to the axioms of the system yields a consistent extension of formalized classical mathematics in which an actually false proposition [ein inhaltlich falscher Satz] is derivable."
What a dramatic event that must have been — perfect for a stage presentation by a skilled playwright competent in mathematical logic.
A few comments must suffice here, for more see  and . First of all the translation of the qualification "inhaltlich" as opposed to formal by "contentual" is literal but awkward. Some translators use the term "material" instead. We all know what is meant, but I am still looking for a more appropriate and gracious word. "Inhalt" stands for content, but is meant here in the sense of cognitive content or meaning rather than stuff, of intension as opposed to extension. Bluntly put, the term refers here to facts of platonic reality. But there is no need to go that far.
With his famous sure touch von Neumann narrowed down the term "inhaltlich" to the more specific qualification "intuitionistisch". It is significant that he, not only an exceptionally sharp mind but also an intuitionist in his philosophical views, at least at that time, was the only one to understand immediately what Gödel was talking about.
It is most significant that even at that early stage von Neumann opened up the possibility of intuitionist reasoning transcending classical formalism, a point taken up by Gödel in 1933 , but quite unheard of at the time when everybody considered intuitionist logic a severe restriction of classical reasoning.
Turning my attention to the editors for a moment, let me quote Dawson catching his breath after his three asterisks and commenting on Gödel's feelings (none of the editors are old enough to have been there in 1931):
"Then, abruptly, as though emboldened and spurred by von Neumann's leader, Gödel shifts from subjunctive to indicative."
Is it not most natural that, after having opened the scenario by casting doubt on expectations of completeness, Gödel would spend a few asterisks worth of deliberation on how best to articulate his findings? That settled, it was plain sailing. Von Neumann sure was a welcome second, but a leader? I should think that Gödel was emboldened by what he had to say next.
To put the impact of Gödel's announcement into proper perspective I must backtrack a bit.
Soundness, consistency and three forms of completeness
In the 1930 paper, his PhD thesis, Gödel proved the completeness of first order predicate logic: every logically valid sentence of the pertinent formal language is derivable in this calculus.
A symbolic sentence is called logically valid if and only if it becomes true under every interpretation of the language, the concept of an interpretation and truth under an interpretation being precisely defined within the realm of set theory. Whether based on naive or formal set theory, the proof is not constructive; it does not provide a method for deciding whether or not a sentence is valid. In other words, although, if a sentence is valid a proof for it can eventually be found by systematically running through all possible derivations in the calculus, there is no obvious method for finding counterexamples to sentences that are non-theorems. In fact, honing down Gödel's incompleteness proof to a finitely axiomatizable fragment of arithmetic eventually led to the conclusion that there cannot possibly be such an algorithm, at least not for any but the most anemic first order language. Thus, every reasonably expressive predicate calculus is what we call undecidable.
The completeness proof for predicate logic ensured that there was nothing missing in the accepted predicate calculus, at least within the frame of classical logic, or so it seemed. It established the equivalence between derivability in the predicate calculus and logical validity, i.e., truth by virtue of logical structure alone. This first kind of completeness marks a link between truth and form. Just like Aristotle's syllogisms, only more so.
The next step was to investigate completeness and consistency of theories obtained when extending the formalism by suitable axioms intended to describe fully and correctly certain familiar mathematical structures, in particular the Universe of Sets and the Arithmetic of Natural Numbers, the non-negative integers. Two types of problems must be distinguished here: the syntactic and the semantic. The syntax treats a formal theory T as an abstract object, a conglomerate of strings of symbols (well formed formulas and sentences, wff's and wfs' for short) that have a certain structure and can be transformed into each other according to certain definite rules. The axioms are the starting wff's, the theorems are the end results of finite chains of wff's put together according to the rules. These chains are the proofs. The syntax of a system is independent of its intended meaning.
A formal system is called syntactically consistent if never both a wfs and its negation have proofs, and syntactically complete if, for every wfs, either it or its negation is provable. These are philosophically untroubled notions, but methodologically of key importance; settling these problems can be technically most demanding tasks. There are plenty of theories, such as group theory, that are not meant to be complete in that sense, because they describe a whole tribe of structures. For them decidability is the big syntactic question: does there exist an algorithm for deciding, given a well-formed sentence, whether or not it is a theorem?
The semantic notions are the ones that link a formal system to the philosophical problem of the nature of mathematical truth. A formalism is sound or semantically consistent, if only true wfs', i.e., wfs that make true claims, have proofs and semantically complete if all true wfs' are theorems. Unfortunately the unqualified term "complete" is often used for both its versions.
In the ideal situation the syntactic and the semantic concepts coincide. There are a few nontrivial such phenomena, e.g., Tarski's completion  of Hilbert's formalization  of Geometry.
But, before these questions could be tackled the notion of a formal system had to be characterized precisely, a task for which Gödel numbering or an equivalent streamlining of syntax is indispensable. It is not a deep idea but an extremely useful tool. The KK (Königlich Kaiserliche) administration of the Austro Hungarian Empire knew as well as the FBI and any efficiently run business that for easy handling it is most convenient to assign ID numbers to the objects of your attention. In a formal system symbols, strings of symbols, words, wff's, wfs' as well as finite chains of these, proofs among them, must all be Gödel-numbered effectively; there must exist a definite program for going back and forth between the language and the Gödel numbers.
Talking about a mathematical environment in terms of numbers, just like a government keeping files on its citizenship in a numerical net, the question arises what can be said that way and what is bound to fall between the meshes of the net. Particularly valuable fish to catch are of course the proofs. And that is where Gödel's second insight struck: a reasonable but precise definition of the concept of a calculation is needed, be it to "calculate", given a number, whether or not it is the Gödel number of a proof or, given a nicely axiomatized formal system, to grind out one after the other the Gödel numbers of its theorems.
When asked why they were taking Baby Logic or Linear Algebra instead of something more exciting for their electives my freshmen used say "because in Math's you cannot go wrong if you plug in the correct numbers and turn the crank according to instructions." Alas, by the end of the course some felt cheated, others claimed to have seen the light.
A foolproof formal system is exactly the pipe dream of those freshmen. But setting it up is a challenge, checking whether or not it lives up to expectations a chore and, once all that is settled one way or the other, the system itself becomes an object of study and starts growing all sorts of new tentacles and barnacles. It is not an end in itself. It is hardly ever used for proving theorems, because that would be too tedious, time consuming and unenlightening.
It is the leaps of intuition that shed light on a problem and point the way to a proof that explains a theorem and points beyond it. But the formalization of a discipline may serve as basis for applications and technology. Of course I am thinking now of computers. They can work so fast that they do not need any intuition. But they cannot judge what is a good proof or a significant theorem. In spite of all their garish displays they only know black and white, correct or false; at least so far. Speed, size and quantity of work, diligence, make up for their lack of imagination, common sense and judgment. They cannot leap over into infinity and build castles in the air!
What distinguishes a proof from any other tool of persuasion is its decidability. A proof may be messy, dreary, tedious, or look like a joke, but there must be an unequivocal criterion for its validity, even if accessible to but a few specialists. For an arithmetized formal system this means that there must be a procedure for deciding, given the Gödel-number of a sequence of formal sentences, whether or not it is that of a proof in the system. We want the decision function, which takes on the value 0 when fed the number of a proof and the value 1 when fed a number that is not the Gödel-number of a proof, to be computable.
Thus is raised the problem of characterizing the concept of a computable function. Encountering one it is easy to recognize it as such. When faced with instructions for putting together some gadget, if they are all there, you'll eventually get the job done, but until then you will not know whether you have complete instructions, and all along you'll be wondering: "if something's missing, how will I know for sure it's not just me?"
We all know how to follow instructions, but if we want to prove something about calculable functions we need a definition that also tells us what is not a calculable function. We know that there are uncountably many more non-calculable functions than calculable ones, because, no matter how complicated, a computable function must be presented by a parcel of instructions for its calculation in some language or other intelligible to us finite creatures, and of such manuals there can only be countably many. That argument does not give a clue to finding a non-calculable function but is evidence for their abundance.
At this point it should be clear that what Gödel needed for the "arithmetization" of a formal language was a precise definition of the intuitive concept of calculability for numerical functions. And that is what he invented recursive functions for, one of his major achievements, a bold stroke for which he would indeed deserve to be declared a hero of our times. The time was ripe for this step; there were alternative definitions by Emil Post, Alan Turing, Alonzo Church and others. These definitions were eventually all proven equivalent; sure confirmation that the definitions were on the right track — and, incidentally, bound for today's computer culture.
Within the familiar idiom of computers we now have a precise notion of a Formal System. Couched in a symbolic language it is Gödel-numbered effectively. Shunting back and forth between a language and its Gödel numbers is something that a computer can do with more ease and less tripping than we humans with our limited attention span. A batch of Gödel numbered items is called effective if its Gödel numbers can be enumerated by a recursive function or, in other words, listed by a computer program. The basis for a theory consists of an effective list of axioms, expressed in the symbolic language, as well as an effective list of rules. A sequence of formal sentences consisting of axioms and wff's hanging together according to these rules is called a proof and its last entry is the theorem proved by it.
An example of a first order language is what can be said in Elementary Arithmetic about the set of non-negative integers including the constant 0 under the operations of the successor that transforms n into n+1, addition and multiplication and the natural ordering; a structure so concrete that it practically invites Platonism. We know what those numbers are and how to reach each one of them, in principle if not in practice. It's different with sets, at least to me.
While claims like "unless the difference between two numbers is odd, their product equals the difference between two squares," which happens to be true, or "every even integer is the sum of two primes," still a conjecture, can be expressed, the simple fact that every non empty set of natural numbers contains a smallest one transcends first order expressive power. In an elementary (i.e., first order) language you can talk about individuals, about all and about some of them, but not about sets and families of sets of objects, which can be done in higher order. True elementary arithmetic consists of all true well-formed sentences of this restricted language. The axiomatic method builds a formal theory by selecting certain obviously true sentences as axioms and applying to them the deductive apparatus of first predicate calculus to derive ever more intricate theorems; a calculus proved complete in the first sense by Gödel in 1930. Thus the axiomatic method, intended to provide systematic approximations to truth, can only be trusted if the axioms are true and the rules of inference preserve truth.
Once the definition of a formal system is articulated, its meta-theory is developed within recursive arithmetic, the concept of proof is proved decidable by a recursive function and theoremhood is shown to be effective, all this demanding plenty of nitpicking labor. The rare case of syntactic completeness leads directly to decidability. A syntactically completely and consistently formalizable theory has an effective proof procedure as well as an effective disproof procedure and its decision function is easily pieced together from these two.
Alas most of the mathematically meaningful axiomatic systems are doomed to remain approximations. For, Gödel showed how to construct, in any formal system that encompasses a minimal fragment of elementary arithmetic, a sentence, which is true if and only if it cannot be proved, and therefore is true but not provable, unless the system is unsound. His method has been expanded and applied to many systems, but it does not work in the first order theory of the field of the real numbers. This remarkable result by Tarski  shows how closely the limitations of a formal system are connected with their expressive power. More can be said and less proved in Arithmetic than in the Real-Number-Field. The integers are not definable among the reals! Interesting, when you consider how much more concrete, graspable, manageable and real(!) than the reals the integers appear to us.
With all this talk about truth, we are not getting any closer to what truth is and how we come to recognize it. Well, if we could say precisely what it is, we would be proving Gödel a liar — and Tarski as well .
Consistency is not enough
By now the big foundational debates of the twenties have not so much been resolved as swept under by highly technical developments. Hilbert's paper on the infinite  vividly illuminates the scene that Gödel found when he entered that quagmire.
Hilbert was primarily concerned with consistency. The most unassailable way of reasoning is finitist. Over finite domains of discourse the predicate calculus boils down to the classical propositional calculus, which is indeed a cut and dried affair, alternatives being surveyable.
Its extension to infinite domains leads to some dubious practices of the classical predicate calculus such as the acceptance of the absurdity of a universal claim as evidence for the existence of an object. To bring this remark down to earth: if you claim that there are honest people and I ask you why and you reply "they can't all be crooks" I am entitled to ask you to show me an honest person. Hilbert was fully aware of the risks lurking in the make-believe world created by jumping from our finitary experience to conclusions about the Infinite. He was hoping that this jump would amount to no more than a convenient gimmick.
But his mathematical conscience demanded a consistency proof. What kind of a consistency proof? That is where Hilbert tripped up. Wanted was a proof that the system using, what Hilbert called "ideal elements" — reasoning about infinite sets the way we are used to reason about finite ones — was not going to lead beyond the realm of what is justified by finitary reasoning, in other words, that the make believe world of predicate logic was a mere conservative extension of finitism. Alas, he wishfully thought that all he needed was a proof of simple consistency as defined above. That is why the demand for a finitist proof of the consistency of any of the current formal systems was his major concern.
Exactly at that point Gödel unhinged Hilbert's dreams, but not his basic plan of proof theory; elaborating his Königsberger revelation Gödel pointed out that
"it is entirely possible to conceive of a theory, both consistent and complete, in which a sentence claiming the existence of an object with a certain property is a theorem, while each object of the domain of discourse provably fails to have that property."
Here we are confronting the subtleties of intuitionist reasoning. There is an important distinction between "all" and "each". It is conceivable that each proof fails to prove a certain sentence G while it is absurd to assume that all proofs fail to prove G.
An undesirable situation; conclusive evidence that a mere proof of consistency could not be sufficient evidence for the soundness of a system, even if all its axioms were true. The weak link is in the logic. Here is a loosely technical elaboration:
For a fixed system S Gödel constructed a sentence G such thatG is true if and only if G is not provable in S.Therefore, if G is true it is not S-provable and neither is its negation, unless S is unsound.If however, G is false then it is provable in S and S, proving a false proposition, is unsound.It follows that S is either unsound or incomplete or both.
For each proof P it is true that P is not a proof of G, and also provable that P is not a proof of G, because being a proof is decidable. Thus
It is true and provable that each P fails to prove G but not provable that all P's fail to prove G, because of the way G is constructed.
"There exists a P that proves G" is a theorem of a complete, consistent extension S' of S, while for each particular P, "P is not a proof of G" is also a theorem of S'.
S' though complete and consistent is what we call omega-incomplete, because every numerical instance of the phrase "x is not a proof of G" is provable in S', but the general statement "no x is a proof of G" is not. It is also omega-inconsistent because, "there exists an x that proves G " is a theorem of S' while every numerical instance of "x fails to prove G" is also a theorem.
This Gedankenexperiment highlights essential shortcomings of the formalism. There is no way of making sure that "all" means "all natural numbers" and "some" means "some natural number". Just think how easy that would be if we were dealing with a finite set, say all numbers smaller than a million.
The trouble comes in via the back door of classical reasoning. No matter how true the mathematical axioms may be, jumping to conclusions from analogy, not heeding Hilbert's own warning that what is OK for finite sets, may not be so for infinite ones, leads the unwary formalist astray, formal consistency notwithstanding.
Guided by the wisdom of his intuitionist approach Gödel was on the right track.
Remarks on Intuitionism
Intuitionism is, to my mind, the most realistic and fruitful approach to mathematical philosophy and methodology. It analyzes mathematical reasoning rather than proclaiming laws for its practice and then setting up a bureaucracy of mechanized thought processes. Trying to explain it would lead me too far afield. Many attempts have been made to pin it down in terms familiar from mathematical experience. Constructivism, the most popular approach, coming from logic and methodology, is often, though incorrectly, identified with Intuitionism. An important aspect of intuitionism is its dynamic nature, hence the danger inherent in attempts to embalm it in a system. Some intuitionists objected to Heyting's formalization of its first order logic, although his axiom system is a valuable tool for comparing intuitionist with classical reasoning. During the late sixties Bill Lawvere 's category theoretic approach to the Foundations led to the amazing discovery of Topos Theory as the natural habitat for Intuitionist Logic, (for details and more references see chapter III of ). Since then much interesting work has been done in this direction.
I have not been keeping track of recent developments, but my general hunch, based on experience, is that once technical interpretations start cropping up the philosophical roots of a way of thinking get overgrown by interesting technical developments and recede into twilight. Small wonder, because truly philosophical ideas are indeed uncomfortably elusive. It may well be true that the job of philosophy is to ask questions, not to answer them. Be that as it may, I'll just give an idea how an intuitionist's understanding of the elementary logical operations transforms the classical rules governing their use:
The classical law of the excluded middle practically strangles imagination, freedom and intuition. "Either A or Else!" What do you do when confronted with a menu that says "either fish and chips or else"? The law of non-contradiction, however, makes good sense: never both A and not A. In classical logic the two are connected by boldly identifying the negation of a conjunction A&B with the disjunction: (not A or not B), which gets us to the law (notA or notnotA) , from which it is only a small step to (notA or A). Well that small step is another one of the pitfalls lurking in the shadows of classical logic. If you accept the law of the excluded middle the rule of double negation, which concludes A from notnotA, follows immediately: from notnotA and the make believe law (A or notA) follows A, since by the law of non-contradiction (notA & nonotA) is impossible.
In a nutshell: intuitionist reasoning is a refinement of classical thinking. Identifying notnotA with A only when there is good reason to do so is much closer to everyday reasoning than the practice of the classical law of double negation. With a bit of care most of the popular but devious proofs of positive claims by reductio ad absurdum can be replaced by direct arguments. You can teach calculus without recourse to the parlor trick of producing, for every epsilon, a delta with property P out of a proof of the absurdity of the assumption that every delta fails to have that property; just take the trouble to construct, for every epsilon, a delta with property P. That's what doing mathematics constructively means. It is a good clean habit to argue constructively:
claim (A or B) only if you have a method for deciding which one of them is the case; if you want to insist on the existence of an object with a certain property, be sure you have a method for producing such an object when called for.
The subtleties of intuitionist distinctions make the use of language much more flexible, colorful and expressive than classical reasoning. Allow me my favorite illustration of the power of double negation. Coming from Europe I am still taken aback when my thanks for some gesture or other prompt the response "no problem". Back home I'd get a friendly "gaern gscheh" which would amount to "my pleasure", while I cannot help interpreting "no problem" by what a New Yorker cartoon said on a doormat some time ago: it is apparently a wintry Sunday afternoon, a middle aged couple dressed in furs and mufflers, armed with a bottle, has just rung the doorbell of an apartment when they both catch sight of the doormat which says, in appropriately ornate lettering, "Not Unwelcome", they are staring at it, at each other--what are they to do now ?
In the classical predicate calculus only conjunction, negation and the universal quantifier are needed. Disjunction, implication and the existential quantifier are definable making free use of double negation. (A or B), (if A then B) and (there exists an object with property P) are classically equivalent to (not(notA¬B)), not(A¬B) and (notallobjects have property notP) respectively. This indeed shows that there is something very artifical about the classical predicate calculus. Indeed some meaning is lost. Double negating the classical predicate calculus you arrive at a weak but valid fragment of intuitionist logic. And so, classical logic is seen to be a fragment of intuitionist logic and obtains a legitimate, if virtual, existence, in the shadow world of double negations, a compelling picture.
But more than that: in a gem of a paper , concise and lucid, Gödel extends this interpretation to Arithmetic and thus provides classical first order Atihmetic with the seal of consistency, tacitly accepting the fact that intuitionist reasoning is in no need of justification.
In response to Ms Goldstein's story presented at the beginning of this essay in an excerpt from the Edge interview let me quote from Gödel's introduction to his 1931 paper.
"It is well known that the development of mathematics in the direction of greater precision has led to the formalization of extensive mathematical domains, in the sense that proofs can be carried out according to a few mechanical rules..... It is reasonable therefore to make the conjecture that these axioms and rules of inference are also sufficient to decide all mathematical questions, which can be formally expressed in the given systems. In what follows it will be shown that this is not the case."
A simple announcement of what the general expectation was and what Gödel had found; a straightforward introduction to a research report in the face of which it is grotesque to picture Gödel rolling up his sleeves and saying to his pal Plato "Ok, now that the PhD is under the hat let's show them something to make them jump out of their smug positivist skins." Several people were actually working on the completeness problem at that time.
I do not see how the incompleteness theorem bears on the question of Platonism. Personally I am a selective Platonist, Gödel probably was a pretty radical one, but he was not blind to other approaches to the Foundations as his contributions and comments to Intuitionism show. He may have been guided in his choice of work by his philosophical beliefs, but the results stand on their own. Platonism and Intuitionism are not incompatible, they can be considered as complementary manifestations of mathematical realism, the static and the dynamic, its ontological and its epistemological aspect.
The incompleteness theorem uncovered a limitation phenomenon of the tool of formalization. Mechanization or computerization cannot do all the jobs of the working, thinking and visualizing mathematician. Who would expect a Swiss army knife to be capable of tuning a piano? Gödel's incompleteness theorem has not overthrown Hilbert's program but it has caused a shift in it: the call for a Diophantine Decision Procedure turned into the Diophantine Decision Problem, proved unsolvable in 1970, after long hard technical work by Julia Robinson, Martin Davis and Yuri Matijasevic — to mention only the most far-reaching result of that nature.
As Hilbert himself stressed in the passage cited above in the introduction, there was never any question of setting up a formal system to encompass all of mathematics, at least not by working mathematicians. As we have seen by now, already the choice of language imposes limitations.
Once language, axioms and rules are fixed, a formalism is pinned down and there is no tampering with the concept of proof. That seems pretty straightforward. But the question is: what are we talking about in that language, where do the axioms come from, what justifies the rules of inference? We are limited creatures, finite beings with a finite amount of temporal and spatial reach allotted to us. The mind is an unfathomable tool; it projects and imagines. It can conceive of unending processes, it can remember extinct events and it can create the weirdest gadgets. Does it create mathematical objects, rules and axioms out of the blue? Not likely. And surely not by deliberate consensus, just think of the debates, controversies and battles we would be facing if anybody could arbitrarily choose how to see the world — and try to impose this view on her fellow beings. I believe that we are basically wired to perceive and handle the world according to the blueprint of mathematics. With slight variations; careful people won't accept the law of the excluded middle all across the board, common sense will demand constructive existence proofs, others will balk at every use of the axiom of choice, a few deny the Uncountable and some will insist on Finitism. But the squirrels scurrying along my telephone line may well be operating according to a totally different notion of the world although we perceive them as navigating according to the laws of our geometry.
I personally do not think that mathematical objects have an existence of their own independent of the human mind. Such a strong Platonic hypothesis does not seem required to explain the inevitability of mathematical concepts and practice. I would not even talk about objects, at least not to start with. They start out as ideas of tools born of a need to cope with the world, just like the idea of a hammer, the wheel, the bed; constructs that take on reality by use and handling. They grow and adjust to our needs. With familiarity and use they pick up reality like moss — and a patina of beauty. They are indeed alive.
The finality of a fully formalized theory is that of halfway houses, of temporary stops. Chevalley has likened the Bourbaki volumes  to mausolea where beautiful theories are embalmed, while mathematics is going on, developing. No more do we conduct our research inside a formalism than the Egyptians had their orgies in the pyramids. A fully developed formal system becomes an object of study rather than a tool for reasoning. For that it would be much too cumbersome. We cannot do without the agility of well-developed mathematical intuition.
Consider the example of the complete theory of real closed fields. Soon after that was embalmed the idea of non-standard models emerged. It very clearly brought home the limitations of the language of first order theories and opened up a new understanding of 17th Century puzzles. Formalisms are not ends in themselves; they serve as archives or become objects of mathematical investigation, or both.
Might not Mathematics be a grid developed by the human species to find its way in the struggle for survival? It is cumulative in the sense that, once understood, a theorem or a structure remains true — true to itself. But it is not static, it is growing, its horizons are forever expanding, new concepts are shedding light on old riddles. And it is genuinely a joint venture of humanity, although accessible to but a few in its entire scope, and it sure is hard work.
It is remarkable that we can talk to each other, that we do agree about the facts of mathematics and amazing how much use we make of its basics, so much that we could not imagine getting along in daily life without it. And then some are able to reach its remotest areas, which, for all we know in a few more generations will be accessible to all. Others spend a lifetime beating their head against the wall of one piddling problem. There are indeed such cases; casualties of the mathematical endeavor, some really good brains, their stories are not told — not so far. Paul Finsler, one of my teachers, springs to mind in close connection to the topic of our discussion (cf.  p 265-267). There are particularly vicious problems such as the four-color conjecture, mercifully laid to rest by now.
Gödel's renowned paranoia may well have been a symptom of a deep depression caused by the frustration of not quite seeing his way through, wherever a hunch was driving him. It may have been an axiom transcending Gödel-Fränkel-von Neumann set theory to settle the continuum hypothesis lurking within grasp only to keep escaping precise articulation, or it may have been some elusive insight that he forever kept expecting just from his next session with Leibniz. Think of all those telltale scribbled records of his Leibniz studies in the Nachlass (the many boxes of notes left in the Gödel Archives at Princeton's Firestone library). Futile and compulsive, one might say. You don't have to be a hypochondriac or prone to paranoia to be unable to feed yourself when in the grips of one of those attacks by what the group theorist Noboru Ito in Chicago used to call a "Great Problem, very annoying, very annoying".
Familiarity breeds reality. There is no Königsweg—no regal path for avoiding strife. When a stranger asks a native on the street how to get to the Vienna Philharmonic the answer is "practice, practice, practice". There are no short cuts to those platonic realms of Mathematics, neither to the gut experience of mathematical intuition nor to the vision of its beauty.
I doubt that pure philosophical discourse can get us anywhere. Maybe phenomenological narrative backed by psychological and anthropological investigations can shed some light on the nature of Mathematical Truth. (Piaget has made a start with children.)
As to Beauty in mathematics and the sciences, here speaks Sophocles' eyewitness in Antigone:
"..... Why should I make it soft for you with tales to prove myself a liar. Truth is Right."
A true Realist, a true Platonist will not stoop to choose between Beauty and Truth, he will have the tenacity to stick it through until Truth is caught shining in her own Beauty. Sure there are messy proofs, we have to bushwhack trough a wilderness of ad hoc arguments, tours de force, combinatorial jungles, false starts and the temptations of definitions ever so slightly off target. Eventually, maybe not in our own lifetime, a good proof, a clear and beautiful proof, will be honed out. That, I think, is the belief of the true Platonist. What Gödel and Einstein were doing when walking together over the Institute's grounds may have been just that; bush whacking, comparing mental notes and encouraging each other not to give up while getting all scratched and discouraged. Yet finding solace in speaking to each other in their mother tongue about their deepest concerns, and the state of the cosmos, the world, the weather and their households too.
Gödel probably never found a home in Amerika. Adele gave him shelter as best she, or anyone could. He did have disciples; Georg Kreisel, John Myhill, Gaisi Takeuti, Stanley Tennenbaum, Hao Wang and other visitors to the Institute. But, although one grumbles about the drudgery, there is something wholesome in teaching American undergraduates. It makes for a link with ordinary life and it helps to adjust to a foreign culture. Gödel had a very austere life; partly due to his nature, partly due to his calling and partly due to the way the world was and still is.
By far the most illuminating survey of Gödel's work including its methodological and philosophical implications is Kreisel's memoir for the Royal Society .
What kind of a person was Gödel?
Long before anybody but a logician and a few philosophers had heard the name Gödel people used to ask me whether I had known Einstein. Now they ask me about Gödel. The answer to the specific question is simple and short. Of course I knew who Gödel was, heard stories about him and wondered about him, a bit about that later. But I really met him only once. That was Georg Kreisel's doing. Kreisel was, and probably still is, a very complex person, a brilliant logician, a deep thinker and difficult to get along with. His understanding of human nature was, and probably still is, remarkable.
During the years 1955-57 of his fellowship at the Institute for Advanced Study Kreisel, originally from Graz, was very close to Gödel. They remained vibrantly in touch for many years, by daily handwritten letters, in German of course, occasional visits and by, most vivid in my memory, interminable long distance phone discussions of ideas, results, pitfalls and technical gossip. Kreisel maintained the same intense style of work and philosophical ruminations with Hao Wang. Although Hao was in close contact with Gödel he never became "family" at the Gödel's like Kreisel did. Their common Austrian background and language must have added significantly to the bond based on philosophical and mathematical kinship.
During my postdoc year at the Institute and then while teaching at Goucher College in Baltimore I was working with Kurt Reidemeister, a fellow at the IAS for the two academic years 1948-1950. The Gödel's and the Reidemeister's had known each other in Europe, maybe in Königsberg, though during the forties Reidemeister was a professor at Marburg. Later he was called to Göttingen, a distinction at his ripe old age. As a topologist and group theorist his bond with Gödel was more cultural than professional. Like Kreisel at the Gödel's I became part of the family at the Reidemeister's and remained so to the end of their days.
As Hao Wang and many others observed, somewhat puzzled, Gödel appeared to be more relaxed and in better health during 1948-50. I am sure this was largely due to the comfortable expansion of his environment by the presence of old time friends, including the wives. Even at that time, mostly from stories that Pinze Reidemeister told, I had a distinct impression that Kurt Gödel never assimilated to American life, much less so than his wife Adele.
Pinze was a delightfully spontaneous person. Since Gödel did not like visiting outside his home and the Reidemeister's did not drive, Adele would pick them up for many a social evening at the Gödel's and eventually drive them home to the institute's housing project. Pinze used to tell what fun it was to be driven by Adele after dinner, while Kurtele stayed home. They were all relaxed, telling jokes driving along the dark deserted Princeton back roads. Invariably Adele would heave a deep sigh and declare what a relief it was to be driving such good friends without having to worry about a genius in her car. Pinze enjoyed telling that story at Princeton cocktail parties, preferably within earshot of her Kurt — no one would ever think of calling him Kurtele.
By the time Kreisel appeared at the institute at Gödel's invitation I had given up mathematics and was raising a family, not that I considered the two tasks incompatible, but it so happened. It was Kreisel who encouraged me to pick up my mathematics again. As a student in Zürich I had been intrigued by foundational problems, but, unable to find a teacher — Finsler being in bad health and Bernays unfortunately not known to me at the University — I settled on group theory and got quite engrossed in that, still am, though no longer agile and active. Anyway it was natural for me to get into logic under Kreisel's demanding tutelage, and then, to my delight, I found my way to Intuitionism — just what I had been looking for all along! So much so that when I started teaching again I made quite a fuss doing my calculus courses constructively; making a point of presenting my epsilon-delta's as explicit functions, calculable ones of course.
Probably sometime in spring 1957 Kreisel took me, Esther and George to the Gödel's for tea, a pleasant occasion, a thoughtful gesture on Kreisel's part towards both Mrs. Gödel and me.
It was a gracious occasion; old world geniality with George and Esti, aged four and six, in the center of attention, irresistibly cute of course. Eventually Gödel himself came down from his study to join us for half an hour. He was very pleasant and natural, extending his friendly feelings for Kreisel to my children and me. I do not recall what we talked about, I am sure it was mostly small talk, except for a few sharp and witty asides from Adele about Princeton society. At that time I felt a vague kinship with her, both of us balancing, a bit precariously, at the edge of the society we were living in, albeit for totally different reasons. I did appreciate their friendly gesture. Two years later I was on my own starting out on a career teaching and doing mathematics.
The whole Gödel lore is beset by psychological myth making. I would like to make a plea not to forget what a conscientious person Gödel was. That goes a long way to explain his reticence, his hesitation to publish or pronounce or do anything that was not honed down to perfect precision and lucidity, and stripped of all superfluous bulk. Kreisel used to have some great quotes of Gödel-comments to news reports, both full of common-sense and — baffling. The familiar story of Gödel pointing out a flaw in the US constitution to the judge on the occasion of his citizenship interview comes to mind. Less known is how diligently, to the point of pedantry, he scrutinized every proposal, every piece of work or mere argument submitted to him.
An illustration of Gödel's professional conscientiousness is the case of W. For years, in the 70's I think, a Mr. W. made the circuit of Mathematics meetings claiming to have discovered an inconsistency, first in accepted set theory and finally in all of mathematics. Gödel apparently studied all this gentleman's voluminous and laborious manuscripts, and eventually, to the relief of us all but not to our surprise, found Mr. W.'s claims unfounded. Unfortunately I do not remember the details, but I am sure there are records.
Gödel was a very private person. Just looking at him you could see the gentleman of the old world, discretely well groomed, shoes polished as a matter of course, tie in its proper place. Maybe he wore sneakers and jeans while working in his garden, if he ever did work in his garden. But I am sure there exists no public photograph of Gödel in sneakers and jeans drinking a coke out of a bottle. There does, however, exist just such a photo of Tarski in the recent biography .
Deeply pondering the question of the nature of mathematical truth and struggling to understand the messages from his own mathematical intuition, haunted by the questions he set himself, Gödel needed total focus to pursue them. I believe that deep concentration on a mathematical problem induces a state of meditation, transcendental meditation in a literal sense.
There are times when ill health can serve as a subterfuge to secure the necessary isolation from the bustle of one's human environment, not a deliberate strategy of course. It was said of Tarski that whenever he, such a robust and gregarious character, was complaining of being unwell he was about to reach a break-through in his work. Mufflers and over coats, hats and spats are a way of keeping the environment at bay; more symbolic than appropriate in fine weather, but psychologically effective, even if not motivated by hypochondria or paranoia. I had several uncles of the same impeccable appearance and demeanor; very gracious, not at all intimidating; yet it would never occur to me to ask them a personal question, or even to assume they might have secrets that the family would enjoy gossiping about.
Just think how lucky we are that Gödel lived long enough to give us so much real stuff to ponder. Time to close this discourse with a pause of respect to Kurt Gödel, a deep thinker and a gracious gentleman.
Takeuti in his memoirs  recalls:
"The last occasion on which I spoke with Gödel was a long distance call from London. While I was in England at a conference, Tennenbaum called and, failing to reach me left a message saying 'Please give a call to Gödel at any cost!' The person who answered the telephone was not the Gödel I had known. Instead, there was a Gödel whose only wish was that death come as soon as possible without causing any trouble to others."
Let us not cause him too much trouble in his well-deserved peace.
References, in order of occurrence:
 David Hilbert, "Ueber das Unendliche," Math Ann. 95 (1926), for translation cf. .
 Jean van Heijenoort, From Frege to Gödel, A source book in mathematical logic, 1879-1931. Harvard University Press, 1971.
 Martin Davis, The Undecidable, basic papers on undecidable propositions, unsolvable problems and computable functions. Raven Press, 1965 (Dover paperback 2004).__ P. Benaceraff and H. Putnam (eds.), Philosophy of Mathematics, selected readings. Cambridge University Press, 1985, first printing Prentice 1964.
 Kurt Gödel, "Die Vollständigkeit der Axiome des logischen Funktionenkalküls," Monatshefte für Mathematik und Physik, 37, 349-360, 1930.
 ............., "Über formal unentscheidbare Sätze der Principia Matematica," ibid, 38, 173-198, 1931.
 ............., Collected works, volume I: publications 1929-1936. Oxford University Press 1986, edited by S. Feferman, J. Dawson. S. Kleene, C.Moore, R. Soloway and J. van Heijenoort..
 ............., "Über intuitionistische Arithmetik und Zahlentheorie," Ergebnisse eines mathematischen Kolloquiums, Heft 4 (1933), Vienna. (translation in )
 Verena Huber-Dyson, Gödel's Theorems; a workbook on Formalization. Teubner-Texte zur Mathematik vol 122, Teubner Verlagsgesellschaft, Stuttgart-Leipzig ,1991.
 Alfred Tarski, A decision method for elementary algebra and geometry, Rand Corporation, 1948.
 ............., Der Wahrheitsbegrif in den deduktiven Disciplinen. (The concept of truth_in the deductive sciences) Aqkad. Wiss. Wien, Mathem. Naturwiss. Anzeiger 69, 1932
 David Hilbert, Grundlagen der Geometrie, Gauss Weber Festschrift, Teubner Verlag, 1899
 Georg Kreisel, "Kurt Gödel, 28 April 1906-14 January 1978," Biographical memoirs of the Fellows of the Royal Society 26, 1980.
 Anita and Solomon Feferman, Alfred Tarski; a life in Logic, Cambridge U. P. 2004.
 Gaisi Takeuti, Memoirs of a Proof Theorist — Gödel and Other Logicians, in Japanese, English translation by Mariko Yasugi (Kyoto Sangyo University, Japan) & Nicholas Passell (University of Wisconsin, Eau Claire, USA) , World Scientific Publishing 2003.