It is a great honour and at the same time a necessity for me to round out and develop my thoughts on the foundations of mathematics, which was expounded here one day five years ago and which since then have constantly kept me most actively occupied. With this new way of providing a foundation for mathematics, which we may appropriately call a proof theory, I pursue a significant goal, for I should like to eliminate once and for all the questions regarding the foundations of mathematics, in the form in which they are now posed, by turning every mathematical proposition into a formula that can be concretely exhibited and strictly derived, thus recasting mathematical definitions and inferences in such a way that they are unshakeable and yet provide an adequate picture of the whole science. I believe that I can attain this goal completely with my proof theory, even if a great deal of work must still be done before it is fully developed.

No more than any other science can mathematics be founded by logic alone; rather, as a condition for the use of logical inferences and the performance of logical operations, something must already be given to us in our faculty of representation, certain extra-logical concrete objects that are intuitively present as immediate experience prior to in thought. If logical inference is to be reliable, it must be possible to survey these objects completely in all their parts, and the fact that they occur, that they differ from one another, and that they follow each other, or are concatenated, is immediate, given intuitively, together with the objects, is something that neither can be reduced to anything else nor requires reduction. This is the basic philosophical position that I regard as requisite for mathematics and, in general, for all scientific thinking, understanding, and communication. And in mathematics, in particular, we consider is the concrete signs themselves, whose shape, according to the conception we have adopted, is immediately, clear and recognisable. This is the very least that must be presupposed; no scientific thinker can dispense with it, and therefore everyone must maintain it, consciously, or not.

I shall now present the fundamental idea of my proof theory.

All the propositions that constitute in mathematics are converted into formulas, so that mathematics proper becomes all inventory of formulas. These differ from the ordinary formulas of mathematics only in that, besides the ordinary signs, the logical signs

⇒	&	v	~	∀ (x)	(∃x)
implies	and	or	not	for all	there exists

also occur in them. Certain formulas, which serve as building blocks for the formal edifice of mathematics, are called axioms. A proof is an array that must be given as such to our perceptual intuition of it of inferences according to the schema

Š

Š ⇒ Ý

Ý

where each of the premises, that is, the formulae, Š and Š ⇒ Ý in the array either is an axiom or directly from an axiom by substitution, or else coincides with the end formula of an inference occurring earlier in the proof or results from it by substitution. A formula is said to be provable if it is either an axiom or the end formula of a proof.

The axioms and provable propositions, that is, the formulas resulting from this procedure, are copies of the thoughts constituting customary mathematics as it has developed till now.

Through the program outlined here the choice of axioms for our proof theory is already indicated; we arrange them as follows.

I. Axioms of implication,

1. A ⇒ (B ⇒ A) (introduction of an assumption)

2. (A ⇒ (A ⇒ B) ) ⇒ (A ⇒ B) (omission of an assumption)

3- (A ⇒ (B ⇒ C) ) ⇒ (B ⇒ (A ⇒ C) ) (interchange of assumptions)

4. (B ⇒ C) ⇒ ( (A ⇒ B) ⇒ (A ⇒ C) ) (elimination of a proposition).

II. Axioms about & and v

5. A & B ⇒ A;

6. A & B ⇒ B;

7. A ⇒ (B ⇒ A & B)

8. A ⇒ A v B;

9. B ⇒ A v B;

10. ((A ⇒ C) & (B ⇒ C)) ⇒ ((A v B) ⇒ C)).

III. Axioms of negation,

11. (A ⇒ B & ~B) ⇒ ~A (principle of contradiction);

12. ~(~A)) ⇒ A (principle of double negation).

The axioms of groups I, II, and III are nothing but the axioms of the propositional calculus. From 11 and 12 there follows, in particular, the formula

(A & ~(A)) ⇒ B

and further the logical principle of excluded middle,

((A ⇒ B) & (~A ⇒ B) ) ⇒ B.

IV. The logical e-axiom

13. A(a) ⇒ A (e(A)).

Here e(A) stands for an object of which the proposition A(a) certainly holds if it holds of any object at all; let us call e the logical e-function. To elucidate the role of the logical E-function let us make the following remarks.

In the formal system the e-function is used in three ways.

1. By means of e "all" and "there exists " can be defined, namely, as follows:

∀(a) A (a) ⇔ A (e(~A)),

(∃a)A(a) ⇔ A (e(A)),

Here the double arrow ( ⇔ ) stands for a combination of two implication formulas; in its place we shall henceforth use the "equivalence" sign ≡ .

On the basis of this definition the e-axiom IV 13 yields the logical relations that hold for the universal and the existential quantifier, such is

∀(a)A(a) ⇒ A(b) (Aristotle's dictum),

and ~(∀(a)A(a) ) ⇒ (∃a)(~A(a)) (principle of excluded middle).

2. If a proposition Y holds of one and only one object, then e(Y) is the object of which Y(a) holds.

The e-function thus enables us to resolve t proposition such as Y(a), when it holds of only one object, so as to obtain

a = e(Y)

3. Beyond this, e takes on the role of the choice function; that is, in case A(a) holds of several objects, e(Y) is some one of the objects a of which Y(a) holds.

In addition to these purely logical axioms we have the following specifically mathematical axioms.

V. Axioms of equality

14. a = a;

15. (a = b) ⇒ (A(a) ⇒ A(b)).

VI. Axioms of Number

16. a' ≠ 0; (≠ for "not=")

17. (A(0) & ∀(a)(A(a) ⇒ A(a'))) ⇒ A(b) (principle of mathematical induction).

Here a' denotes the number following and the integers 1, 2, 3, . . . can be written in the form 0', 0'', 0''',..

For the numbers of the second number class and of Cantor's higher number classes the corresponding induction axioms must be added; they would have to be combined, however, into a schema in agreement with Cantor's theory.

Finally, we also need explicit definitions, which introduce the notions of mathematics and have the character of axioms, as well as certain recursion axioms, which result from a general recursion schema. Before we discuss the formulation of these axioms, we must first lay down the rules that govern the use of axioms in general. For in my theory contentual inference is replaced by manipulation of signs according to rules; in this way the axiomatic method attains that reliability, and perfection that it can and must reach if it is to become the basic instrument of .all theoretical research.

First, the following stipulations hold.

For mathematical variables we always use lower-case italic Latin letters, but for constant mathematical objects (specific functions) lower-case Greek letters.

For variable atomic propositions (indeterminate formulas) we always use capital italic Latin letters, but for constant atomic propositions capital Greek letters, for example,

Z(a) [a is a natural number]

and

N(a) [a is a number of the second number class].

Concerning the procedure of substitution, the following general conventions hold.

For propositional variables we may substitute only formulas, that is, arrays constructed from elementary formulas by means of the logical signs

⇒

&

v

~

∀

(x)

(∃x)

The elementary formulas are the formula variables, possibly with arguments

attached, and the signs for constant propositions, such as

Z, N, = , <

with the associated argument places filled.

Any array may be substituted for a mathematical variable; however, when a mathematical variable occurs in a formula, the constant proposition that states of what kind the variable is, followed by the implication sign, must always precede, for example,

Z(a) ⇒ a + 1 = 1 + a,

N(a) ⇒ N(a').

This convention has the effect that only substituends that are ordinary numbers or numbers of the second number class come into consideration after all. In Axioms V and VI the propositions Z(a) and Z(b), which should precede, were omitted for the sake of brevity.

German capital and lower-case letters have reference and are used only to convey information.

The mathematical variables are of two kinds: (1) the primitive variables and (2) the variable-sorts.

1. Now while in all of arithmetic and analysis the ordinary integer suffices as sole primitive variable, with each of Cantor's transfinite number classes there is associated a primitive variable that ranges over precisely the ordinals of that class. Hence to each primitive variable there corresponds a proposition that states of what kind it is; this proposition is implicitly characterised by axioms.

With each primitive variable there is associated one kind of recursion, by means of which we define functions whose argument is that primitive variable. The recursion associated with the number-theoretic variable is "ordinary recursion", by means of which t function of t number-theoretic variable n is defined when we indicate what value it has for n = 0 and how the value for n' is obtained from that for n. The generalisation of ordinary recursion is transfinite recursion; it rests upon the general principle that the value of the function for a value of the variable is determined by means of the preceding values of the function.

2. From the primitive variables we derive further kinds of variables by applying logical connectives to the propositions associated with the primitive variables, for example, to Z. The variables thus defined are called variable-sorts, and the propositions defining them are called sort-propositions; for each of these a new particular sign is introduced. Thus the formula

F(f) ≡ ∀(a)(Z(a) - Z(f (a)))

offers the simplest instance of a variable-sort; this formula defines the sort of the function variable (" being-a-function "). A further example is the formula

F(g) - (f)((P(f) - Z(g(f)));

it defines the "being-a-function-of-a-function"; the argument g is the new function-of-a-function variable.

To produce the higher variable-sorts we must provide the sort-propositions themselves with subscripts, thus making a recursion procedure possible.

We can now characterise what is to be understood by explicit definitions and by recursion axioms: An explicit definition is an equivalence or identity that on its left side has the sign to be defined (capital or lower-case Greek [bold] letter), along with certain variables as arguments, and on its right side has an array in which only these arguments occur as free variables and in which no signs for constants occur except those that have already been introduced.

In a corresponding way, the recursion axioms are formula systems that are modelled upon the recursive procedure.

These are the general foundations of my theory. To familiarise you with the way in which it is applied I would like to adduce some examples of particular functions as they are defined by recursion.

...

If we now begin to construct mathematics, we shall first set our sights upon elementary number theory; we recognise that we can obtain and prove its truths through contentual intuitive considerations. The formulas that we encounter when we take this approach are used only to impart information. Letters stand for numerals, and an equation informs us of the fact that two signs stand for the same thing.

The situation is different in algebra ; in algebra we consider the expressions formed with letters to be independent objects in themselves, and the propositions of number theory, which are included in algebra, are formalised by means of them. Where we had numerals, we now have formulas, which themselves are concrete objects that in their turn are considered by our perceptual intuition, and the derivation of one formula from another in accordance with certain rules takes the place of the number-theoretic proof based on content.

Thus algebra already goes considerable, beyond centennial number theory. Even the formula 1 + a = a + 1, for example, in which a is a genuine number-theoretic variable, in algebra no longer merely imparts information about something contentual but is a certain formal object, a provable formula, which in itself means nothing and whose proof cannot be based on content but requires appeal to the induction axiom.

The formulas 1 + 3 = 3 + 1 and 1 + 7 = 7 + 1, which can be verified by contentual considerations, can be obtained from the algebraic formula above only by a proof procedure, such as formal substitution of the numerals 3 and 7 for a, that is, by the use of a rule of substitution.

Hence even elementary mathematics contains, first, formulas to which correspond contentual communications of finitary propositions (mainly numerical equations or inequalities, or more complex communications composed of these) and which .we may call the real propositions of the theory, and second, formulas that - just like the numerals of contentual number theory - in themselves mean nothing but are merely things that are governed by our rules and must be regarded as the ideal objects of the theory.

These considerations show that, to arrive at the conception of formulas as ideal propositions, we need only pursue in a natural and consistent way the line of development that mathematical practice has already followed till now. And it is then natural and consistent for us to treat henceforth not only the mathematical variables but also the logical signs, v, &, etc, and the logical variables, namely, the propositional variables, A, B, C, . . ., just like the numerals and letters in algebra and to consider them, too, as signs that in themselves mean nothing but are merely building blocks for ideal propositions.

Indeed, we have an urgent reason for thus extending the formal point of view of algebra to all of mathematics. For it is the means of relieving us of a fundamental difficulty that already makes itself felt in elementary number theory. Again I take as an example the equation

a + 1 = 1 + a;

if we wanted to regard it as imparting the information that

a + 1 = 1 + a,

where a stands for any given number, then this communication could not be negated, since the proposition that there exists a number a for which

a + 1 ≠ 1 + a

holds has no finitary meaning; one cannot, after all, try out all numbers. Thus, if we adopted the finitist attitude, we could not make use of the alternative according to which an equation, like the one above, in which an unspecified numeral occurs either is satisfied for every numeral or can be refuted by a counter-example. For, as an application of the "principle of excluded middle", this alternative depends essentially on the assumption that it is possible to negate the assertion that the equation in question always holds.

But we cannot relinquish the use either of the principle of excluded middle or of any other law of Aristotelian logic expressed in our axioms, since the construction of analysis is impossible without them.

Now the fundamental difficulty that we face here can be avoided by the use of ideal propositions. For, if to the real propositions we adjoin the ideal ones, we obtain a system of propositions in which all the simple, rules of Aristotelian logic hold and all the usual methods of mathematical inference are valid. Just as, for example, the negative numbers are indispensable in elementary number theory and just as modern number theory and algebra become possible only through the Kummer-Dedekind ideals, so scientific mathematics becomes possible only through the introduction of ideal propositions.

To be sure, one condition, a single but indispensable one, is always attached to the use of the method of ideal elements, and that is the proof of consistency; for, extension by the addition of ideal elements is legitimate only if no contradiction is thereby brought about in the old, narrower domain, that is, if the relations that result for the old objects whenever the ideal objects are eliminated are valid in the old domain.

In the present situation, however, this problem of consistency is perfectly amenable to treatment. For the point is to show that, when ideal objects are introduced, it is impossible for us to obtain two logically contradictory propositions, Y and ~Y. Now, as I remarked above, the logical formula

(A & ~A) ⇒ B

follows from the axioms of negation. If in it we substitute the proposition Y for A and the inequality 0 ≠ 0 for B, we obtain

(Y & ~Y) ⇒ (0 ≠ 0).

And, once we have this formula, we can derive the, formula 0 # 0 from Y and ~Y. To prove consistency we therefore need only show that 0 ≠ 0 cannot be obtained from our axioms by the rules in force as the end formula of a proof, hence that 0 ≠ 0 is not a provable formula. And this is a task that fundamentally lies within the province of intuition just as much as does in contentual number theory the task, say, of proving the irrationality of sqrt(2), that is, of proving that it is impossible to find two numerals a and b satisfying the relation a² = 2b², a problem in which it must be shown that it is impossible to exhibit two numerals having a certain property. Correspondingly, the point for us is to show, that it is impossible to exhibit a proof of a certain kind. But a formalised proof, like a numeral, is a concrete and surveyable object. It can be communicated from beginning to end. That the end formula has the required structure, namely " 0 ≠ 0 ", is also a property of the proof that can be concretely ascertained. The demonstration can in fact be given, and this provides us with a justification for the introduction of our ideal propositions. At the same time we recognise that this also gives us the solution of a problem that became urgent long ago, namely, that of proving the consistency of the arithmetic axioms.

Wherever the axiomatic method is used it is incumbent upon us to prove the consistency of the axioms. In geometry and the physical theories this proof is successfully carried out by means of a reduction to the consistency of the arithmetic axioms. This method obviously fails in the case of arithmetic itself. By making this important final step possible through the method of ideal elements, our proof theory forms the necessary keystone of the axiomatic system.

The final test of every new theory is its success in answering pre-existent questions that the theory was not specifically created to answer. As soon as Cantor had discovered his first transfinite numbers, the numbers of the second number class as they are called, the question arose whether by means of this transfinite counting one could actually enumerate the elements of sets known in other contexts but not denumerable in the ordinary sense. The line segment was the first and foremost set of this kind to come under consideration. This question, whether the points of the line segment, that is, the real numbers, can be enumerated by means of the numbers of the second number class, is the famous problem of the continuum, which was formulated but not solved by Cantor. In my paper "On the infinite" (1925) I showed how through our proof theory this problem becomes amenable to successful treatment.

In order to show that this continuum hypothesis of Cantor's constitutes a perfectly concrete problem of ordinary analysis, I mention further that it can be expressed as a formula in the following way:

∀(∃h)((f)(F(f) ⇒ N(h(f))) & ∀(f,g)[F(f) & F(g) ⇒ ((h(f) = h(g)) ⇒ (f, g))]),

where, to abbreviate, we have put

F(f) for ∀(a)(Z(a) ⇒ Z(f (a)))

and

(f, g) for ∀(a)(Z(a) ⇒ (f (a) = g(a))).

In this formula there still occurs the proposition N, which is associated with the primitive variable of the second number class. But this can be avoided, since, as is well known, the numbers of the second number class can be represented by well-orderings of the number sequence-that is, by certain functions that have two number-theoretic variables and take the values 0 and 1-in such a way that the proposition in question takes the form of a proposition purely about functions.

I have already set forth the basic features of this proof theory of mine on different occasions, in Copenhagen [1922], here in Hamburg [1922], in Leipzig [1922], and in Munster [1925]; in the meantime much fault has been found with it, and objections of all kinds hive been raised against it, all of which I consider just as unfair as it can be. I would now like to elucidate some of these points.

Poincaré already made various statements that conflict with my views; above all, he denied from the outset the possibility of a consistency proof for the arithmetic axioms, maintaining that the consistency of the method of mathematical induction could never be proved except through the inductive method itself. But, as my theory shows, two distinct methods that proceed recursively come into play when the foundations of arithmetic are established, namely, on the one hand, the intuitive construction of the integer as numeral (to which there also corresponds, in reverse, the decomposition of any given numeral, or the decomposition of any concretely given array constructed just as a numeral is), that, is, contentual induction, and, on the other hand, formal induction proper, which is based on the induction axiom and through which alone the mathematical variable can begin to play its role in the formal system.

Poincaré arrives at his mistaken conviction by not distinguishing between these two methods of induction, which are of entirely different kinds. Regrettably Poincaré, the mathematician who in his generation was the richest in ideas and the most fertile, had a decided prejudice against Cantor's theory, which prevented him from forming a just opinion of Cantor's magnificent conceptions. Under these circumstances Poincaré had to reject my theory, which, incidentally, existed at that time only in its completely inadequate early stages. Because of his authority, Poincaré often exerted a one-sided influence on the younger generation.

My theory is opposed on different grounds by the adherents of Russell and Whitehead's theory of foundations, who regard Principia Mathematica as a definitively satisfying foundation for mathematics.

Russell and Whitehead's theory of foundations is a general logical investigation of wide scope. But the foundation that it provides for mathematics rests, first, upon the axiom of infinity and, then, upon what is called the axiom of reducibility, and both of these axioms are genuine contentual assumptions that are not supported by a consistency proof they are assumptions whose validity in fact remains dubious and that, in any case, my theory does not require.

In my theory Russell's axiom of reducibility has its counterpart in the rule for dealing with function variables. But reducibility is not presupposed in my theory rather, it is recognised as something that can be compensated for: the execution of the reduction would be required only in case a proof of a contradiction were given, and then, according to my proof theory, this reduction would always be bound to succeed.

Now with regard to the most recent investigations, the fact that research on foundations has again come to attract such lively appreciation and interest certainly gives me the greatest pleasure. When I reflect on the content and the results of these investigations, however, I cannot for the most part agree with their tendency; I feel. rather, that they are to a large extent behind the times, as if they came from a period when Cantor's majestic world of ideas had not yet been discovered.

In this I see the reason, too, why these most recent investigations in fact stop short of the great problems of the theory of foundations, for example, the question of the construction of functions, the proof or refutation of Cantor's continuum hypothesis, the question whether all mathematical problems are solvable, and the question whether consistency and existence are equivalent for mathematical objects.

Of today's literature on the foundations of mathematics, the doctrine that Brouwer advanced and called intuitionism forms the greater part. Not because of any inclination for polemics, but in order to express my views clearly and to prevent misleading, conceptions of my own theory, I must look more closely into certain of Brouwer's assertions.

Brouwer declares (just as Kronecker did in his day) that existence statements, one and all, are meaningless in themselves unless they also contain the construction of the object asserted to exist; for him they are worthless scrip, and their use causes mathematics to degenerate into a game.

The following may serve as an example showing that a mere existence proof carried out with the logical e-function is by no means a piece of worthless scrip.

In order to justify a remark by Gauss to the effect that it is superfluous for analysis to go beyond the ordinary complex numbers formed with sqrt(-1), Weierstrass and Dedekind undertook investigations that also led to the formulation and proof of certain theorems. Now some time ago I stated a general theorem (1896) on algebraic forms that is a pure existence statement and by its very nature cannot be transformed into a statement involving constructibility. Purely by use of this existence theorem I avoided the lengthy and unclear argumentation of Weierstrass and the highly complicated calculations of Dedekind, and in addition. I believe, only my proof uncovers the inner reason for the validity of the assertions adumbrated by Gauss and formulated by Weierstrass and Dedekind.

But even if one were not satisfied with consistency and had further scruples, he would at least have to acknowledge the significance of the consistency proof as a general method of obtaining finitary proofs from proofs of general theorems - say of the character of Fermat's theorem - that are carried out by means of the e-function.

Let us suppose, for example, that we had found, for Fermat's great theorem, a proof in which the logical function e was used. We could then make a finitary proof out of it in the following way.

Let us assume that numerals

p, a, b, c (p > 2)

satisfying Fermat's equation

a^v + b^v = c^v

are given; then we could also obtain this equation as a provable formula by giving the form of a proof to the procedure by which we ascertain that-the numerals a^v + b^v and c^v coincide. On the other hand, according to our assumption we would have a proof of the formula

(Z(a) & Z(b) & Z(c) & Z(p) & (p > 2)) ⇒ (ap + bp ≠ cp),

from which

a^v + b^v ≠ c^v

is obtained by substitution and inference. Hence both

a^v + b^v = c^v and

a^v + b^v ≠ c^v

would be provable. But, as the consistency proof shows in a finitary way, this cannot be the case.

The examples cited are, however, only arbitrarily selected special cases. In fact, mathematics is replete with examples that refute Brouwer's assertions concerning existence statements.

What, now, is the real state of affairs with respect to the reproach that mathematics would degenerate into a game?

The source of pure existence theorems is the logical c-axiom, upon which in turn the construction of all ideal propositions depends. And to what extent has the formula game thus made possible been successful? This formula game enables us to express the entire thought-content of the science of mathematics in a uniform manner and develop it in such a way that, at the same time, the interconnections between the individual propositions and facts become clear. To make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable; on the contrary, a theory by its very nature is such that we do not need to fall back upon intuition or meaning in the midst of some argument. What the physicist demands precisely of a theory is that particular propositions be derived from laws of nature or hypotheses solely by inferences, hence on the basis of a pure formula game, without extraneous considerations being adduced. Only certain combinations and consequences of the physical laws can be checked by experiment-just as in my proof theory only the real propositions are directly capable of verification. The value of pure existence proofs consists precisely in that the individual Construction is eliminated by them and that many different constructions are subsumed under one fundamental idea, so that only what is essential to the proof stands out clearly; brevity and economy of thought are the raison d'étre of existence proofs. In fact, pure existence theorems have been the most important landmarks in the historical development of our science. But such considerations do not trouble the devout intuitionist.

The formula game that Brouwer so deprecates has, besides its mathematical value, an important general philosophical significance. For this formula game is carried out according to certain definite rules, in which the technique of our thinking is expressed. These rules form a closed system that can be discovered and definitively stated. The fundamental idea of my proof theory is none other than to describe the activity of our understanding, to make a protocol of the rules according to which our thinking actually proceeds. Thinking, it so happens, parallels speaking and writing: we form statements and place them one behind another. If any totality of observations and phenomena deserves to be made the object of a serious and thorough investigation, it is this one-since, after all, it is part of the task of science to liberate us from arbitrariness, sentiment, and habit and to protect us from the subjectivism that already made itself felt in Kronecker's views and, it seems to me, finds its culmination in intuitionism.

Intuitionism's sharpest and most passionate challenge is the one it flings at the validity of the principle of excluded middle, for example, in the simplest case, at the validity of the mode of inference according, to which, for any assertion containing a number-theoretic variable, either the assertion is correct for all values of the variable or there exists a number for which it is false. The principle of excluded middle is a consequence of the logical c-axiom and has never yet caused the slightest error. It is, moreover, so clear and comprehensible that misuse is precluded. In particular, the principle of excluded middle is not to be blamed in the least for the occurrence of the well-known paradoxes of set theory; rather, these paradoxes are due merely to the introduction of inadmissible and meaningless notions, which are automatically excluded from my proof theory. Existence proofs carried out with the help of the principle of excluded middle usually are especially attractive because of their surprising brevity and elegance. Taking the principle of excluded middle from the mathematician would be the same, proscribing the telescope to the astronomer or to the boxer the use of his fists. To prohibit existence statements and the principle of excluded middle is tantamount to relinquishing the science of mathematics altogether. For, compared with the immense expanse of modern mathematics, what would the wretched remnants mean, the isolated results, incomplete and unrelated, that the intuitionists naive obtained without the use of the logical e-axiom ? The theorems of the theory of functions, such as the theory of- conformal mapping and the fundamental theorems in the theory of partial differential equations or of Fourier series - to single out only a few examples from our science, are merely ideal propositions in my sense and require the logical e-axiom for their development.

In these circumstances I am astonished that a mathematician should doubt that the principle of excluded middle is strictly valid as a mode of inference. I am even more astonished that, as it seems, a whole community of mathematicians who do the same has now constituted itself. I am most astonished by the fact that even in mathematical circles the power of suggestion of a single man, however full of temperament and inventiveness, is capable of having the most improbable and eccentric effects.

Not even the sketch of my proof of Cantor's continuum hypothesis has remained uncriticised. I would therefore like to make some comments on this proof. ...

From my presentation you will recognise that it is the consistency proof that determines the effective scope of my proof theory and in general constitutes its core. The method of W. Ackermann permits a further extension still. For the foundations of ordinary analysis his approach has been developed so far that only the task of carrying out a purely mathematical proof of finiteness remains. Already at this time I should like to assert what the final outcome will be: mathematics is a presuppositionless science. To found it I do not need God, as does Kronecker, or the assumption of a special faculty of our understanding attuned to the principle of mathematical induction, as does Poincaré, or the primal intuition of Brouwer, or, finally, as do Russell and Whitehead, axioms of infinity, reducibility, or completeness, which in fact are actual, contentual assumptions that cannot be compensated for by consistency proofs.

I would like to note further that P. Bernays has again been my faithful collaborator. He has not only constantly aided me by giving advice but also contributed ideas of his own and new points of view, so that I would like to call this our common work. We intend to publish a detailed presentation of the theory soon.