Introduction

Ever since the time of the Greeks, mathematics has involved proof; and it is even doubted by some whether proof, in the precise and rigorous sense which the Greeks gave to this word, is to be found outside mathematics. We may fairly say that this has not changed, because what constituted a proof for Euclid is still a proof for us; and in times when the concept has been in danger of oblivion, and consequently mathematics itself has been threatened, it is to the Greeks that men have turned again for models of proof. But this venerable bequest has been enlarged during the past hundred years by important acquisitions.

By analysis of the mechanism of proofs in suitably chosen mathematical texts, it has been possible to discern the structure underlying both vocabulary and syntax. This analysis has led to the conclusion that a sufficiently explicit mathematical text could be expressed in a conventional language containing only a small number of fixed “words”, assembled according to a syntax consisting of a small number of unbreakable rules : such a text is said to be formalized. The description of a game of chess, in the usual notation, and a table of logarithms, are examples of formalized texts. The formulae of ordinary algebraic calculation would be another example, if the rules governing the use of brackets were to be completely codified and strictly adhered to; in practice, some of these rules are never made explicit, and certain derogations of them are allowed.

The verification of a formalized text is a more or less mechanical process, the only possible causes of error being the length or intricacy of the text : this is why a mathematician will normally accept with confidence the result of an algebraic calculation performed by another, provided he knows that the calculation is not unduly long and has been done with care. On the other hand, in an unformalized text, one is exposed to the dangers of faulty reasoning arising from, for example, incorrect use of intuition or argument by analogy. In practice, the mathematician who wishes to satisfy himself of the perfect correctness or “rigour” of a proof or a theory hardly ever has recourse to one or another of the complete formalizations available nowadays, nor even usually to the incomplete and partial formalizations provided by algebraic and other calculi. In general he is content to bring the exposition to a point where his experience and mathematical flair tell him that translation into formal language would be no more than an exercise of patience (though doubtless a very tedious one). If, as happens again and again, doubts arise as to the correctness of the text under consideration, they concern ultimately the possibility of translating it unambiguously into such a formalized language: either because the same word has been used in different senses according to the context, or because the rules of syntax have been violated by the unconscious use of modes of argument which they do not specifically authorize, or again because a material error has been committed. Apart from this last possibility, the process of rectification, sooner or later, invariably consists in the construction of texts which come closer and closer to a formalized text until, in the general opinion of mathematicians, it would be superfluous to go any further in this direction. In other words, the correctness of a mathematical text is verified by comparing it, more or less explicitly, with the rules of a formalized language.

The axiomatic method is, strictly speaking, nothing but this art of drawing up texts whose formalization is straightforward in principle. As such it is not a new invention; but its systematic use as an instrument of discovery is one of the original features of contemporary mathematics. As far as reading or writing a formalized text is concerned, it matters little whether this or that meaning is attached to the words, or signs in the text, or indeed whether any meaning at all is attached to them; the only important point is the correct observance of the rules of syntax. Thus, as everyone knows, the same algebraic calculation can be used to solve problems about pounds weight or pounds sterling, about parabolas or motion under gravity. The same advantage attaches to every text written according to the axiomatic method, and for the same reasons: once the theorems of general topology have been established, they may be applied at will to ordinary space, Hilbert space, and many others. This faculty of being able to give different meanings to the words or prime concepts of a theory is indeed an important source of enrichment of the mathematician’s intuition, which is not necessarily spatial or sensory, as is sometimes believed, but is far more a certain feeling for the behaviour of mathematical objects, aided often by images from very varied sources, but founded above all on everyday experience. Thus one is often led to study with profit those parts of a theory which traditionally have been neglected in this theory but studied systematically in a general axiomatic context, of which the given theory is a special case (for example, properties which have their historical origin in another specialization of the general theory). Moreover — and this is what concerns us most particularly in this series of volumes — the axiomatic method allows us, when we are concerned with complex mathematical objects, to separate their properties and regroup them around a small number of concepts : that is to say, using a word which will receive a precise definition later, to classify them according to the structures to which they belong. (Of course, the same structure can arise in connection with various different mathematical objects.) For example, some of the properties of the sphere are topological, others are algebraic, others again can be considered as belonging to differential geometry or the theory of Lie groups. Although this principle may occasionally become somewhat artificial when applied to closely interwoven structures, it is the basis of the division into Books of the subject-matter of this series.

¶ Just as the art of speaking a language correctly precedes the invention of grammar, so the axiomatic method had been practised long before the invention of formalized languages; but its conscious practice can rest only on the knowledge of the general principles governing such languages and their relationship with current mathematical texts. In this Book our first object is to describe such a language, together with an exposition of general principles which could be applied to many other similar languages; however, one of these languages will always be sufficient for our purposes. For whereas in the past it was thought that every branch of mathematics depended on its own particular intuitions which provided its concepts and prime truths, nowadays it is known to be possible, logically speaking, to derive practically the whole of known mathematics from a single source, the Theory of Sets. Thus it is sufficient for our purposes to describe the principles of a single formalized language, to indicate how the Theory of Sets could be written in this language, and then to show how the various branches of mathematics, to the extent that we are concerned with them in this series, fit into this framework. By so doing we do not claim to legislate for all time. It may happen at some future date that mathematicians will agree to use modes of reasoning which cannot be formalized in the language described here : it would then be necessary, if not to change the language completely, at least to enlarge its rules of syntax. But that is for the future to decide.

It goes without saying that the description of the formalized language is made in ordinary language, just as the rules of chess are. We do not propose to enter into a discussion of the psychological and metaphysical problems which underlie the use of ordinary language in such circumstances (for example, the possibility of recognizing that a letter of the alphabet is “the same” in two different places on the page, etc.). Moreover, it is scarcely possible to undertake such a description without making use of numeration. It is objected by some that the use of numbers in such a context is suspect, even tantamount to petitio principii. It is clear, however, that in fact we are using numbers merely as marks (and that we could for that matter replace them by other signs, such as colours or letters), and that we are not making use of any mathematical reasoning when we number the signs which occur in an explicitly written formula. We shall not enter into the question of teaching the principles of a formalized language to beings whose intellectual development has not reached the stage of being able to read, write, and count.

If formalized mathematics were as simple as the game of chess, then once our chosen formalized language had been described there would remain only the task of writing out our proofs in this language, just as the author of a chess manual writes down in his notation the games he proposes to teach, accompanied by commentaries as necessary. But the matter is far from being as simple as that, and no great experience is necessary to perceive that such a project is absolutely unrealizable : the tiniest proof at the beginning of the Theory of Sets would already require several hundreds of signs for its complete formalization. Hence, from Book I of this series onwards, it is imperative to condense the formalized text by the introduction of a fairly large number of new words (called abbreviating symbols) and additional rules of syntax (called deductive criteria). By doing this we obtain languages which are much more manageable than the formalized language in its strict sense. Any mathematician will agree that these condensed languages can be considered as merely shorthand transcriptions of the original formalized language. But we no longer have the certainty that the passage from one of these languages to another can be made in a purely mechanical fashion : for to achieve this certainty it would be necessary to complicate the rules of syntax which govern the use of the new rules to such a point that their usefulness became illusory; just as in algebraic calculation and in almost all forms of notation commonly used by mathematicians, a workable instrument is preferable to one which is theoretically more perfect but in practice far more cumbersome.

As the reader will see, the introduction of this condensed language is accompanied by “arguments” of a particular type, which belong to what is called metamathematics. This discipline ignores entirely any meaning which may originally have been attributed to the words or phrases of formalized mathematical texts, and considers these texts as particularly simple objects, namely as assemblies of previously given objects in which only the assigned order is of importance. Moreover, just as for example a chemistry textbook announces in advance the result of an experiment performed under given conditions, so metamathematical “arguments” usually assert that when a succession of operations has been performed on a text of a given type, then the final text will be of another given type. In the simplest cases, the assertions are indeed the purest truisms (comparable, for example, to the following : “if a bag of counters contains black counters and white counters, and if we replace all the black counters by white ones, then there will be only white counters in the bag”). But very soon we meet examples where the argument takes a typically mathematical turn, in which the use of arbitrary integers and mathematical induction predominates. Although we have countered the objection made earlier against the use of numeration in the description of a formalized language, it is no longer possible at this point to deny the danger of begging the question, because right from the beginning it seems that we are making use of all the resources of arithmetic, of which (among other things) we propose later to lay down the foundations. To this objection the reply is sometimes made that arguments of this type merely describe operations which can be actually carried out and verified, and for this reason carry conviction of another order from that which can be accorded to mathematics proper. But it seems simpler to say that we could avoid all these metamathematical arguments if the formalized text were explicitly written out : instead of using the “deductive criteria”, we should recommence each time the sequences of operations which the purpose of the criteria is to abbreviate by predicting their result. But formalized mathematics cannot in practice be written down in full, and therefore we must have confidence in what might be called the common sense of the mathematician : a confidence analogous to that accorded by a calculator or an engineer to a formula or a numerical table without any awareness of the existence of Peano's axioms, and which ultimately is based on the knowledge that it has never been contradicted by facts.

We shall therefore very quickly abandon formalized mathematics, but not before we have carefully traced the path which leads back to it. The first “abuses of language” thus introduced will allow us to write the rest of this series (and in particular the Summary of Results of Book I) in the same way as all mathematical texts are written in practice, that is to say partly in ordinary language and partly in formulae which constitute partial, particular, and incomplete formalizations, the best-known examples of which are the formulae of algebraic calculation. Sometimes we shall use ordinary language more loosely, by voluntary abuses of language, by the pure and simple omission of passages which the reader can safely be assumed to be able to restore easily for himself, and by indications which cannot be translated into formalized language and which are designed to help the reader to reconstruct the complete text. Other passages, equally untranslatable into formalized language, are introduced in order to clarify the ideas involved, if necessary by appealing to the reader’s intuition; this use of the resources of rhetoric is perfectly legitimate, provided only that the possibility of formalizing the text remains unaltered. The first examples of this will appear in Chapter III of this Book, which describes the theory of integers and cardinal numbers.

Thus, written in accordance with the axiomatic method and keeping always in view, as it were on the horizon, the possibility of a complete formalization, our series lays claim to perfect rigour : a claim which is not in the least contradicted by the preceding considerations, nor by the need to correct errors which slip into the text from time to time.

¶ We take the same realistic attitude towards the question of consistency (or non-contradiction). This question has been one of the main preoccupations of modern logicians, and is partly responsible for the creation of formalized languages (cf. Historical Note). A mathematical theory is said to be contradictory if a theorem and its negation have both been proved in the theory; from the usual rules of reasoning, which are the basis of the rules of syntax in formalized languages, it follows then that every theorem is both true and false in the theory, and the theory is consequently of no interest. If therefore we are involuntarily led to a contradiction, we cannot allow it to remain without rendering futile the theory in which it occurs.

Can we be certain that this will never happen? Without entering into a discussion — which is outside our competence — of the very notion of certainty, we may observe that metamathematics can set itself the task of examining the problems of consistency by its own methods. To say that a theory is contradictory means in effect that it contains a correct formalized proof which leads to the conclusion $0 \ne 0$. Now metamathematics can attempt, using methods of reasoning borrowed from mathematics, to investigate the structure of such a formalized text, in the hope of “proving” that such a text cannot exist. In fact such “proofs” have been given for certain partial formalized languages, which are less rich than that which we propose to introduce, but rich enough to express a good part of classical mathematics. We may of course reasonably ask what in fact has been “proved” in this way : for, if mathematics were contradictory, then some of its applications to material objects, and in particular to formalized texts, would stand in danger of being illusory. To escape this dilemma, the consistency of a formalized language would have to be “proved” by arguments which could be formalized in a language less rich and consequently more worthy of confidence; but a famous theorem of metamathematics, due to Gödel, asserts that this is impossible for a language of the type we shall describe, which is rich enough in axioms to allow the formulation of the results of classical arithmetic.

On the other hand, in the proofs of “relative” consistency (that is to say, those which establish the consistency of a theory on the supposition that some other theory, for example set theory, is non-contradictory), the metamathematical part of the argument (cf. Chapter I, § 2, no. 4) is so simple that it seems hardly possible to deny it without renouncing all rational use of our intellectual faculties. Since the various mathematical theories are now logically attached to the Theory of Sets, it follows that any contradiction encountered in one or another of these theories must give rise to a contradiction in the Theory of Sets itself. Of course, this is not an argument from which we can infer the consistency of the Theory of Sets. Nevertheless, during the half-century since the axioms of this theory were first precisely formulated, these axioms have been applied to draw conclusions in the most diverse branches of mathematics without leading to a contradiction, so that we have grounds for hope that no contradiction will ever arise.

If it should turn out otherwise, it would be that the observed contradiction was inherent in the fundamental principles of the Theory of Sets; these principles would therefore require to be modified, if possible without compromising those parts of mathematics we wish most to retain, and it is clear that the task of modification would be made easier by the use of the axiomatic method and formalized language, which allow us to formulate these principles more precisely and to separate out their consequences more clearly. Indeed, this is more or less what has happened in recent times, when the “paradoxes” of the Theory of Sets were eliminated by adopting a formalized language essentially equivalent to that which we shall describe here; and a similar revision would have to be undertaken if this language in its turn should prove to be contradictory.

To sum up, we believe that mathematics is destined to survive, and that the essential parts of this majestic edifice will never collapse as a result of the sudden appearance of a contradiction; but we cannot pretend that this opinion rests on anything more than experience. Some will say that this is small comfort; but already for two thousand five hundred years mathematicians have been correcting their errors to the consequent enrichment and not impoverishment of their science; and this gives them the right to face the future with serenity.