## Abstract

Attitudes towards formalization and proof have gone through large swings during the last 150 years. We sketch the development from Frege's first formalization, to the debates over intuitionism and other schools, through Hilbert's program and the decisive blow of the Gödel Incompleteness Theorem. A critical role is played by the Skolem–Lowenheim Theorem, which showed that no first-order axiom system can characterize a unique infinite model. Skolem himself regarded this as a body blow to the belief that mathematics can be reliably founded only on formal axiomatic systems. In a remarkably prescient paper, he even sketches the possibility of interesting new models for set theory itself, something later realized by the method of forcing. This is in contrast to Hilbert's belief that mathematics could resolve all its questions. We discuss the role of new axioms for set theory, questions in set theory itself, and their relevance for number theory. We then look in detail at what the methods of the predicate calculus, i.e. mathematical reasoning, really entail. The conclusion is that there is no reasonable basis for Hilbert's assumption. The vast majority of questions even in elementary number theory, of reasonable complexity, are beyond the reach of any such reasoning. Of course this cannot be proved and we present only plausibility arguments. The great success of mathematics comes from considering ‘natural problems’, those which are related to previous work and offer a good chance of being solved. The great glories of human reasoning, beginning with the Greek discovery of geometry, are in no way diminished by this pessimistic view. We end by wishing good health to present-day mathematics and the mathematics of many centuries to come.

## 1. Introduction

I should like to thank the organizers of the conference for inviting me to express my ideas on the nature of mathematical proof. What I have to say may be somewhat anachronistic, in that I shall review a debate that raged almost a century ago, but which has been quiescent lately. Nevertheless, in light of what has occurred, I believe that one can come to some reasonable conclusions about the current state of mathematical proof. Most of the references to the older literature are to be found in the excellent collection ‘From Frege to Gödel’, edited by Jean van Heijenoort (1971).

The title of my talk alludes to both the work of Thoralf Skolem, and, perhaps even more, to the conclusions he came to at a rather early stage of the development of mathematical logic. The work is, of course, the famous Lowenheim–Skolem Theorem, for which Skolem gave a simplified proof, and which is undoubtedly the most basic result about general axiomatic systems. It can be given various formulations, but the form which Skolem himself attributes to Lowenheim is that ‘every first order expression is either contradictory or satisfiable in a denumerably infinite domain’ (Skolem 1970). As Skolem showed, there is a natural extension to the case of countably many such expressions. ‘Contradictory’ here is defined by reference to the rules of the predicate calculus, i.e. normal mathematical reasoning. The startling conclusion that Skolem drew is the famous Skolem Paradox, that any of the usual axiom systems for set theory will have countable models, unless they are contradictory. Since I will not assume that my audience are all trained logicians, I point out that though the set of reals from the countable model is countable seen from outside, there is no function ‘living in the model’ which puts it in one-to-one correspondence with the set of integers of the model. This fact and other considerations led Skolem to this viewpoint:

I believed that it was so clear that axiomatization in terms of sets was not a satisfactory ultimate foundation of mathematics, that mathematicians would, for the most part, not be very much concerned by it.

The view that I shall present differs somewhat from this, and is in a sense more radical, namely that it is unreasonable to expect that any reasoning of the type we call rigorous mathematics can hope to resolve all but the tiniest fraction of possible mathematical questions.

The theorem of Lowenheim–Skolem was the first truly important discovery about formal systems in general, and it remains probably the most basic. It is not a negative result at all, but plays an important role in many situations. For example, in Gödel's proof of the consistency of the Continuum Hypothesis, the fact that the hypothesis holds in the universe of constructible sets is essentially an application of the theorem. In Skolem's presentation of the basic theorem, it reads like a plausible, natural theorem in mathematics, unencumbered by the jargon prevalent both in many papers of the time, and, above all, in the contemporary philosophical debates concerning the foundations of mathematics. As the reader can verify by referring to van Heijenoort's reference book, all of Skolem's writings on logic and set theory have a clarity and simplicity which is striking. Even now it is truly rewarding to read these papers and reflect on them.

Now, no discussion of proof can fail to refer to the Incompleteness Theorem of Gödel. The result states that no reasonable system of mathematics can prove its own consistency, where the latter is stated as a theorem about proofs in its own formal system, and hence can be construed as a result in combinatorics or number theory. The Incompleteness Theorem is a theorem of mathematics, and not a philosophical statement. Thus, in this sense, it is unassailable, but, in another sense, since it refers to such a specific question, it is not really relevant to the question which I am addressing in this talk, namely the extent to which problems in mathematics can reasonably be expected to be settled by mathematical reasoning. It is, of course, the first, and perhaps the only, proved statement supporting the basic pessimism of Skolem's viewpoint.

Let me begin by recalling some facts concerning the development of the axiomatic method, which I am sure are familiar to all of you. With the publication of Frege's epic work ‘Begriffschrift’ in 1879, the notion of a formal system was given a definitive form. Important related work was done by Boole, and Pierce, and later Peano presented a similar approach, but with Frege's work, for the first time in the history of human thought, the notion of logical deduction was given a completely precise formulation. Frege's work not only included a description of the language (which we might nowadays call the ‘machine language’), but also a description of the rules for manipulating this language, which is nowadays known as predicate calculus. Now the Greeks had introduced the axiomatic method, and Leibnitz had speculated about a universal deductive mechanism. Thus, as with many great discoveries, the precise formulation, of what is meant by a formal system, grew gradually in the collective unconscious, and so perhaps did not appear to many people at the time as a breakthrough. Certainly no radically new ideas were introduced, nor any particularly difficult problems overcome. But this was a major landmark. For the first time one could speak precisely about proofs and axiomatic systems. The work was largely duplicated by others, e.g. Russell and Whitehead, who gave their own formulations and notations, and even Hilbert made several attempts to reformulate the basic notion of a formal system. The variety of such attempts relates to the problem of clearly distinguishing between the axioms which are assumed as the starting point of a theory and the methods of deduction which are to be used. The Gödel Completeness Theorem, which many people regard as implicit in Skolem's work, explicitly shows that there is no ambiguity in the rules of deduction. This is in marked contrast to the Incompleteness Theorem, which shows that no reasonable axiom system can be complete.

Alongside these developments, there raged a lively debate, continuing almost to the onset of World War 2, about the ultimate validity of mathematics. This debate saw the emergence of formalism, logicism and intuitionism as competitors for the correct foundation of mathematics. I will briefly discuss these competing philosophies, noting at the outset that each seems to focus on proofs rather than models. In this respect Skolem's ideas were in sharp contrast to those of most of his contemporaries. I believe that today the situation is rather the reverse, due in part to my own work, showing how many models of set theory can be constructed using the notion of forcing (Cohen 1966). Indeed, Skolem even foresaw, in his 1922 paper, the construction of new models of set theory, for there he states:

‘It would in any case be of much greater interest if one could prove that a new subset of Z could be adjoined without giving rise to contradictions; but this would probably be very difficult.’ As I said, his interest in models was perhaps ahead of his time, so let me discuss now some of the common viewpoints on foundations.

First, I would mention the belief of Hilbert that the beautiful structure of mathematics, erected in the course of centuries, was in some sense sacrosanct, not to be challenged. Indeed, he felt that mathematical knowledge was our birthright, and that in principle human reasoning could decide all mathematical questions. He felt it necessary to defend, at all costs, mathematics from the attacks of such as Kronecker and Brouwer. In his 1904 article he summarizes the viewpoints of Kronecker, Helmholtz, Christoffel, Frege, Dedekind and Cantor, finding deficiencies in their viewpoints, and offering his own treatment as an alternative. I am not very impressed by his efforts in this paper, but greatly admire the tenacity with which he defends the inviolability of mathematical reasoning. Perhaps he himself realized the difficulties of giving any completely satisfactory foundation, and so retreated, if I may use the expression, to a more modest position, that at least if we regard mathematics as a formal game played with symbols we should be able to show that the game is consistent, This became known as the Hilbert Program, and though many attempts were made not too much was accomplished, the reasons for which became clear when Gödel proved his Incompleteness Theorem. The Program survived in some form, under the name of Proof Theory, and we shall later refer to Gentzen's outstanding result in that discipline. Hilbert's goal was informally outlined, since what was meant by a consistency proof was not entirely explicit. In his basic belief that beyond any doubt mathematics was referring to an existing reality, and that it must be made secure from all philosophical attacks, he undoubtedly enjoyed the support of the vast majority of mathematicians.

Second, there arose a school that questioned methods of proof involving what may be called non-constructive reasoning. Foremost proponents were Brouwer and Weyl, both very distinguished mathematicians. The objections strike at the use of the classical predicate calculus, rejecting for example the use of Excluded Middle and related non-constructive proofs of existence. The school of Intuitionism probably never obtained much support among working mathematicians, but it has repeatedly resurfaced in various forms, for example in the work of Errett Bishop on constructive analysis. In some forms, the school may even reject the use of formal systems entirely, on the grounds that they are irrelevant for mathematical reasoning.

A recurring concern has been whether set theory, which speaks of infinite sets, refers to an existing reality, and if so how does one ‘know’ which axioms to accept. It is here that the greatest disparity of opinion exists (and the greatest possibility of using different consistent axiom systems).

## 2. Questions concerning the predicate calculus

The formulation, by Frege and others, of mathematics as a formal system, must certainly be regarded as a milestone in the history of human thought. In a way it is a most curious achievement, in that it merely codified what was generally known. However, as a completed structure, reducing mathematical thought to what we today would call a machine language, and thereby eliminating any vagueness, it was a historic step. Perhaps Frege and the early workers did not completely separate the formalization of logical thinking and the rules of logical deduction. Today we clearly do so, and these rules are known as the predicate calculus. Concerning the predicate calculus itself, there is no controversy, though the intuitionists and others would restrict its use. The work of Lowenheim and Skolem, and the Completeness Theorem of Gödel, indeed show that one has an invariant, natural notion. Let me state these results now.

First, I review the formulation of the language. One has symbols for relations (of various arities) between objects. We have the logical connectives, the quantifiers, and some helpful symbols such as parentheses, commas and subscripts, and finally the symbols for individual variables and constants. The rules for manipulation of the connectives are sometimes called the Boolean or propositional calculus. Much more powerful, in the sense that they contain the crux of mathematical reasoning, are the quantifiers. These are the existential quantifier (‘there exists’) and the universal quantifier (‘for all’). The rules of propositional calculus are elementary and well known. The key step in mathematical thinking is that if a statement asserts that there exists an *x* such that a certain property *A*(*x*) holds then we invent a name for such an object, and call it a constant, and can then form sentences with it.

Conversely, if a universal statement asserts that *A*(*x*) holds for all *x* then we can deduce *A*(*c*) for all constants. For example, if we have a constant positive real number a, and we know square roots exist for general positive reals, then we invent the symbol b for a square root of *A*.

Viewed this way, the rules become extremely transparent, if one takes care to avoid clash of constants and the like. The fundamental discovery of Lowenheim–Skolem, which is undoubtedly the greatest discovery in pure logic, is that the invention (or introduction) of ‘constants’ as in predicate calculus, is equivalent to the construction of a ‘model’ for which the statements hold. More precisely, if the use of predicate calculus does not lead to a contradiction on the basis of a set *S* of sentences, then repeated use of the rules will result in a model for the system *S*. Moreover, the method ensures that we get a countable model if *S* is countable. And thus we get to the Skolem ‘Paradox’ that if a first-order system of axioms is consistent then it has a countable model, because all current systems of set theory have countably many primitives.

As an aside, I remark that the work received amazingly little attention. Indeed Skolem remarks that he communicated these results to mathematicians in Gottingen, and was surprised that, despite this revealed ‘deficiency’ in the axiomatic method, there still existed, in his opinion, an unwarranted faith that the axiomatic method can capture the notion of mathematical truth. This is the pessimism to which I refer in the title. Later I shall refer to an even deeper pessimism, which has found little expression in the literature.

Skolem wrote in a beautiful, intuitive style, totally precise, yet more in the spirit of the rest of mathematics, unlike the fantastically pedantic style of Russell and Whitehead. Thus, Hilbert even posed as a problem the very result that Skolem had proved, and even Gödel, in his thesis where he proved what is known as the Completeness Theorem, does not seem to have appreciated what Skolem had done, although in a footnote he does acknowledge that ‘an analogous procedure was used by Skolem’. A possible explanation lies in the fact that Skolem emphasized models, and was amazingly prescient in some of his remarks concerning independence proofs in set theory. A discussion of the priority question can be found in the notes to Gödel's Collected Works (Gödel 1986). Gödel was undoubtedly sincere in his belief that his proof was in some sense new, and in view of his monumental contributions I in no way wish to find fault with his account. What is interesting is how the more philosophical orientation of logicians of the time, even the great Hilbert, distorted their view of the field and its results. When Gödel showed, in his Incompleteness Theorem, that the Hilbert Program was doomed, Hilbert (as far as I can find out from the records) did not even invite him to present his results in Gottingen. Gödel did not have a permanent position, and it was only due to the perspicacity of American mathematicians, who understood the significance of his work, that he was eventually appointed to the Institute for Advanced Study at Princeton.

So what are the disputes involving the rules of logic, given that the Completeness Theorem seems to say that they account for all correct reasoning in first-order logic? I will not attempt to categorize the various schools in this dispute, nor their philosophical principles. But I think that one can safely say that the differences involve the notion of constructivity, and the restriction to existence proofs based on constructive reasoning. Many people devoted their efforts to developing various parts of mathematics in a constructive manner. I think that for many the crucial issue is already present in the most basic part of mathematics, number theory. Since classical set theory is non-constructive almost by definition, in that it speaks of infinite sets, one hardly expects constructive ideas to be successful here. (Of course Gödel, in his epoch-making proof of the consistency of the Continuum Hypothesis and the Axiom of Choice, does use a notion of ‘constructibility’, but this is in an extended sense involving reference to ordinals, and thus is entirely natural within set theory.)

In number theory, most results are constructively obtained, even if it may require some work to see this. Let me give what I believe to be the first example of a truly non-constructive proof in number theory, so that the reader, if not a logician, will be exposed to some of the subtleties involved. This is the famous theorem of Skolem's compatriot, Thue, extended by Siegel, and in a sense definitively completed by Roth. It says that an algebraic number can have only finitely many ‘good’ approximations by rational numbers. There is no need to specify the meaning of ‘good’ here, the basic idea being that the error in the approximation should be less than a certain function of the denominator of the approximating rational. The theorem has as a consequence that certain polynomial equations in two variables have only finitely many integral solutions.

Now, all the classical proofs are totally ‘elementary’ (though ingenious), and are constructive except in the very last lines of the proof. Thue showed that there could not be two approximations *p*/*q* and *p*′/*q*′, where both *q* and *q*′ are greater than a number *c* (constructively given), and *q*′ greater than a constructively given power of *q*. Now he draws the conclusion that there can be only finitely many good approximations, since if *p*/*q* is given there is a bound for all other approximations *p*′/*q*′. This is a perfectly correct deduction, but if one does not know one solution one is in no position to bound the others. This is a most difficult problem, and, though Baker's work has yielded constructive estimates in some cases, one seems far from constructive bounds in general. Since the time of Thue, other examples have been found, though perhaps no more than a dozen. Of course one has no proof that constructive bounds do not exist. Even if one is uncertain about the exact limits of the notion, one can, and does, ask whether there are general recursive bounds, or better primitive recursive ones.

Since I do not share the intuitionist ideology, or any of its variants, I will not raise the objections that they would raise, but clearly every mathematician must feel a certain unease about the above proof. It is simply desirable to have a more constructive proof.

There are people who are more extreme, and who claim that any inductive proof (such as the above) based on predicates with too many quantifier changes (so that no instance is immediately verifiable) should not be allowed. The most extreme view, held by at least one mathematician at a respectable university, is that eventually a contradiction will be found even in elementary number theory.

Let me say briefly why I cannot accept such limitations on the use of the predicate calculus. The reason lies in the very procedures of the predicate calculus, because in a sense every statement is proved by contradiction. The form of the proof may vary, but, in essence, the Completeness Theorem says that if a set of statements does not lead to a contradiction it is satisfiable. So, to show that something is valid, i.e. that it is necessarily satisfied, one must show that the assumption of its negation leads to a contradiction.

Since I shall refer to this procedure again later, let me emphasize in slightly more detail what the rules are. Using elementary rules one can bring every statement into prenex form. Something of prenex form will be of one of the forms ‘for all *x*, *A*(*x*)’ or ‘there exists *x* such that *A*(*x*)’, where *A* itself may have other quantifiers, and constants which have been introduced before. In the case of ‘for all *x*, *A*(*x*)’ one can add to the list from which one is trying to deduce a contradiction all ‘*A*(*c*)’. In the case of ‘there exists *x* such that *A*(*x*)’ one adds correspondingly ‘*A*(*c*)’ for a new constant. If there is a contradiction derivable from our original assumption, then it will be revealed after finitely many applications of these rules of procedure, and at that point the contradiction will be obtainable by propositional calculus, as all the prenex quantifiers will have been stripped off. More specifically, as Skolem points out explicitly, we look at all the original undefined relations, and substitutions got by using the constants introduced at the various stages, and we will eventually be unable to assign consistently truth-values to the quantifier-free formulas produced by our procedure. Conversely, and this is only slightly harder to see, if we can always find truth assignments that work, we are in effect constructing a model of the original set of sentences. There are technical details involving revisiting requirements over and over, but these are not difficult. I refer the reader to Skolem's original paper for an intuitive explanation.

Now it is clear to me that if a contradiction is obtained the original statement must be ‘false’. Of course the intuitionist might argue that this is not good enough, that one wants more than a proof of contradiction from classical logic. I can only reply that in the usual, everyday mathematics, as practiced by the vast majority of mathematicians, all proofs proceed by contradiction. This may be surprising at first sight, but thinking about the above sketch of the Completeness Theorem will show that this is exactly what is done in all proofs. In my final comment, where I shall present a ‘pessimistic’ view, it is important that one understands the method allowed by the predicate calculus.

## 3. Consistency questions

During the period of the great debate, between 1910 and 1920, there emerged the Formalist School associated with Hilbert. My impression is that Hilbert shared the viewpoint of ‘naive’ mathematicians, that is, that existing mathematics, with its notion of proof, corresponded to a real world. And yet, in a sense formalism asserts the opposite. Hilbert wished to secure mathematics from the attacks of intuitionists and others, and therefore proposed as a minimal program to prove that formalized mathematics was consistent. No doubt this appeared at the time to be a reasonable goal, and one could even have hoped that the consistency proof might be done within elementary combinatorial mathematics (from this point of view mathematics could be construed as a combinatorial game). An accompanying idea was more daring, namely that such a combinatorial analysis might even result in a decision procedure, i.e. a method of deciding whether a given statement could be proved or not, or, even more ambitiously, for deciding the truth value of the statement in question.

This hope was of course shattered by the Gödel Incompleteness Theorem, which asserts that no reasonably complex system can prove its own consistency, unless it is inconsistent, in which case everything is provable and the system is useless. My main thesis here, which I shall discuss at the end of my lecture, is that the premise of the Hilbert program is more profoundly untrue. I claim that mathematics can prove only an incredibly small proportion of all true statements. But for now I discuss some technical issues in Proof Theory.

The proof of Incompleteness can be formulated in different, essentially equivalent, ways. In particular, it is closely related to the notion of recursive or computable function, and motivated the large subject of recursive function theory, so that one cannot regard Gödel's result as purely negative.

A technical subject, Proof Theory, arose, with one of its goals to understand the fine detail of unprovability of consistency. For a given theory, one seeks a combinatorial principle which is natural and allows one to prove consistency. The first, and still most striking, results are those of Gentzen (1969), who analysed the consistency strength of elementary number theory (first-order Peano arithmetic). Since elementary number theory would seem to be need in any kind of combinatorial analysis, it may seem silly to use number theory to prove number theory is consistent. However, Gentzen's elegant work is not circular, and can be formulated so as to yield precise information about proofs in elementary number theory. Let me sketch the idea of his proof, in my own version which I intend to publish some day.

Let us consider (in number theory) a proof *P* of a contradiction. In our discussion of the rules of deduction, we said that there are various possibilities, all equivalent. Now we must make matters precise. It is most natural to regard the proof as a division of cases. This means that, in various stages of the proof, we consider a division into *A* and not *A*, and regard the proof as a tree, such that starting from the top of the tree, quoting the axioms of number theory, and allowing for the division into branches, we arrive at a situation where, allowing for invention and substitution of constants as described, we have a contradiction in every branch, among the statements involving constants alone. We also allow Boolean manipulations in the usual way. Thus a proof of a contradiction becomes a tree, with a contradiction in every branch. Now, the branch structure is important, because of the structure of the axioms of number theory. The key axiom is the Axiom of Induction. Really this is a countable set of axioms, with one instance for each property *A*(*n*) involving only one free variable *n*. Such an instance states that one of three possibilities holds:

either

*A*(0) is false

or

for some *n*, *A*(*n*) is true and *A*(*n*+1) is false

or

*A*(*n*) is true for all *n*.

Clearly this branching is an essential feature of induction.

The idea behind Gentzen's proof is to go from *P* to another proof *P*′ of contradiction, with a simpler tree structure.

How to simplify the proof? Well, in any induction branching as above, the easiest branch to investigate is the third, since it says that something is true for all *n* and does not assert the existence of any particular constant. Briefly, we go down the tree and wait till we encounter a particular integer, say 5, where *A*(5) occurs. But then induction up to 5 is obvious and can be replaced by five cases of the induction hypothesis. This has to be done carefully. However, one sees that in at least one branch no constants are created, except particular numerals such as 5 or 7. In this way the use of the induction axiom can be eliminated in at least one case.

Now, assuming that this reduction from *P* to *P*′ is defined, the question is whether the new proof of a contradiction is simpler. The set of all finite trees can be ordered in a simple manner, namely, starting from the first node of a tree, we compare two trees by comparing the branches of the trees, assuming by induction that tree whose depth is one less have already been ordered. We use the usual lexicographic ordering. Now, if we define things correctly, we can show that indeed the order of the tree goes down each time we eliminate a single use of induction. This ordering is a well-ordering, and it corresponds to the ordinal *ϵ*_{0}, which can also be defined as the limit of *ω*_{n} as *n* goes to *ω*, where *ω*_{1} is *ω*, and *ω*_{n+1} is . From Gödel's Theorem it follows that either we cannot formulate this kind of induction in the system, or we can, but we cannot prove it. The latter is the case, and in this way we reach a plausible combinatorial principle just out of reach of elementary number theory, and one from which one can prove the consistency of elementary number theory in an elementary way. Proof Theory has gone on to seek analogous principles for more complex systems, e.g. fragments of set theory.

## 4. Set theory, the ultimate frontier

At about the same time as Frege was developing the first universal formal system, Cantor was developing the foundations of mathematics as based on set theory. More precisely, it can be said that Cantor realized that set theory was a legitimate area of study, perhaps not realizing that it was the basis of all mathematics. In any event, Frege made an attempt to axiomatize a universal ‘set theory’, and made a mistake by allowing the existence of the set of all sets, thereby getting a contradiction. One normally attributes to Zermelo the first axiomatization of set theory, in more or less the form that we consider today. However, the system was still vaguely defined, and again it was Skolem who pointed out the deficiencies (Fraenkel did so too, in a less precise way). This gives the system now known as Zermelo–Fraenkel set theory.

The development of set theory has been largely separate from that of the rest of mathematics, except perhaps for considerations around the Axiom of Choice. Nevertheless, mathematicians have as a rule regarded the problems of set theory as legitimate mathematical questions. The Continuum Hypothesis, despite the independence results, remains an object of speculation for set theorists.

It is in set theory that we encounter the greatest diversity of foundational opinions. This is because even the most devoted advocates of the various new axioms would not argue that these axioms are justified by any basic ‘intuition’ about sets. Let me give some examples of the scope of such axioms.

One may vary the rank of sets allowed. Conventional mathematics rarely needs to consider more than four or five iterations of the power set axiom applied to the set of integers. More iterations diminish our sense of the reality of the objects involved.

One can attempt to vary the properties allowed in the comprehension axiom, while dodging the Frege problem.

Axioms of infinity assert the existence of large cardinals whose existence cannot be proved in the Zermelo–Fraenkel system. The earliest example is that of inaccessible cardinals, and more recently one has considered much larger cardinals whose existence has remarkable consequences even for real analysis. These kinds of axioms can be extended indefinitely, it seems, and, despite the interest of their consequences, the reality of the cardinals involved becomes more and more dubious. The same can be said for more exotic axioms, of determinacy type, despite the remarkable connections now known between their consistency strength and that of large cardinals.

So we come now to one of the most basic questions. Does set theory, once we get beyond the integers, refer to an existing reality, or must it be regarded, as formalists would regard it, as an interesting formal game? In this sense, we are going beyond the scope of the conference, which concerns proof. Rather we are questioning the very sense of some things which are proved. I think that for most mathematicians set theory is attractive, but lacking the basic impact of arithmetic. There is almost a continuum of beliefs about the extended world of set theory.

A typical argument for the objective reality of set theory is that it is obtained by extrapolation from our intuitions of finite objects, and people see no reason why this has less validity. Moreover, set theory has been studied for a long time with no hint of a contradiction. It is suggested that this cannot be an accident, and thus set theory reflects an existing reality. In particular, the Continuum Hypothesis and related statements are true or false, and our task is to resolve them.

A counter-argument is that the extrapolation has no basis in reality. We cannot search through all possible sets of reals to decide the continuum hypothesis. We have no reason at all to believe that these sets exist. It is simply an empirical fact that no contradiction has been found.

Clearly both points of view have their strengths and weaknesses. Through the years I have sided more firmly with the formalist position. This view is tempered with a sense of reverence for all mathematics which has used set theory as a basis, and in no way do I attack the work which has been done in set theory. However, when axiom systems involving large cardinals or determinacy are used, I feel a loss of reality, even though the research is ingenious and coherent. In particular, a strong defect of the first view, for me, is the idea that if mathematics refers to a reality then human thought should resolve all mathematical questions. This leads me to my final section, on the ultimate pessimism.

## 5. The ultimate pessimism deriving from Skolem's views

Skolem, in his papers, was so struck by the existence of non-isomorphic models of all but the most trivial axiom systems that he was led to doubt the relevance of any mathematical axiom system to the philosophical questions concerning foundations of mathematics. For example, he pointed out the existence of countable models of set theory. He seems to have been the first clearly to emphasize models rather than methods of proof. Whether or not he believed in an absolute model of set theory, which was beyond all attempts to describe it by axioms, is not clear to me. But certainly he was aware of the limitations on what could be proved. In a remarkable passage, he even discusses how new models of set theory might be constructed by adding sets having special properties, although he says he has no idea how this might be done. This was exactly the starting point of my own work on independence questions, although I was totally unaware that Skolem had considered the same possibility. It always seemed to me that it was futile to adopt the proof-theoretic approach and analyse the structure of proofs. Even if the formalist position is adopted, in actual thinking about mathematics one can have no intuition unless one assumes that models exist and that the structures are real.

So, let me say that I will ascribe to Skolem a view, not explicitly stated by him, that there is a reality to mathematics, but axioms cannot describe it. Indeed one goes further and says that there is no reason to think that any axiom system can adequately describe it.

Where did the confidence, expressed so vividly by Hilbert, that all questions must be resolved, come from? One view that has struck me, ever since my earliest encounters with mathematics, originates with the Greeks, and Euclid in particular. Here for the first time we see the power of the human intellect being brought to bear not only on mathematics, but also on physics and astronomy. What a fantastic thrill it must have been to live through this era and enjoy the escape from superstition and primitive beliefs, and the sudden bright light dawning of the triumph of reason alone! We have all felt this thrill, encountering, at an early age, Euclid and the wonderful beauty and completeness of his geometric system. Just a hundred years ago even the Pythagoras Theorem was regarded as a marvel of deductive reasoning, and books were published containing many proofs.

But let us recall Skolem's theorem. How does one actually proceed in a proof? After a finite stage one invents symbols for the objects that are known to exist under a certain assumption *A*. Also one makes finitely many substitutions of the constants into universal statements, and repeats this in some dovetailing procedure. Then one sees if there is a propositional contradiction in what is now known about those finitely many constants. For example, suppose one wish to disprove (and thereby prove the negation of) some statement about primes. If one is working in number theory, one will be able to divide into cases, according to the principle of induction outlined above. But, in essence, all one can do is run a check on finitely many integers derived from the hypothesis. With luck, we reach a contradiction, and thereby prove something. But suppose one asks an unnatural statement about primes, such as the twin primes question. Perhaps on the basis of statistical considerations, we expect the primes to satisfy this law. But the primes seem rather random, and in order to prove that the statistical hypothesis is true we have to find some logical law that implies it. Is not it very likely that, simply as a random set of numbers, the primes do satisfy the hypothesis, but there is no logical law that implies this? Looked at from the point of view of the Skolem construction, it would seem that we can run checks, but they may be hopelessly weak in determining the truth.

Now, one can ask, how does the introduction of higher axioms of infinity (perhaps having analytic implications) affect whether the statement can be proved. Indeed, doesn't the Gödel Incompleteness Theorem show exactly that the consistency of a given system, which is a combinatorial, or number-theoretic, statement, gets resolved by passing to a higher infinity? Will not the use of more and more complicated set-theoretic axioms resolve more and more arithmetic statements?

My response is twofold. One, the above is a rather idealistic hope. The only statements of arithmetic, resolved by higher set theory, which are known today, are basically consistency statements or close relatives. In a sense the higher systems almost assume the principles we want proved. There is no intuition as to why the consideration of the higher infinite should bring us closer to solving questions about primes. Secondly, how far can we go by extending set-theoretic axioms? As said before, one rapidly gets removed from intuition, and we have no idea at the outset how to relate the axioms to primes.

Therefore, my conclusion is the following. I believe that the vast majority of statements about the integers are totally and permanently beyond proof in any reasonable system. Here I am using proof in the sense that mathematicians use that word. Can statistical evidence be regarded as proof? I would like to have an open mind, and say ‘Why not?’. If the first ten billion zeros of the zeta function lie on the line whose real part is 1/2, what conclusion shall we draw? I feel incompetent even to speculate on how future generations will regard numerical evidence of this kind.

In this pessimistic spirit, I may conclude by asking if we are witnessing the end of the era of pure proof, begun so gloriously by the Greeks. I hope that mathematics lives for a very long time, and that we do not reach that dead end for many generations to come.

## Footnotes

One contribution of 13 to a Discussion Meeting Issue ‘The nature of mathematical proof ’.

- © 2005 The Royal Society