The term ”Hilbert’s Programme” is used in the literature on the foundations of mathematics to denote the set of ideas which Hilbert, either alone or together with Paul Bernays, developed mainly from the 1920’s onwards until the publication of Grundlagen der Mathematik in 1934. The strategic aim was to restore to classical mathematical reasoning the kind of confidence it reached before it was shaken by the paradoxes.

The system of thought which arose from this work is sometimes also known as Formalism. In relation to Hilbert (and to Bernays) this term is misapplied, because Hilbert was not a formalist in the sense that this term had in Frege’s vocabulary, to be found when he refers to the formalists of his day, in particular around his position in the dispute over the existence of the complex number system. And Hilbert was also not a formalist in the sense that this term came to have in the language of modern mathematical formalists like Haskell Curry.

Before the publication of Grundlagen der Mathematik we can follow the maturing of Hilbert’s thought in essays like ”Neubegründung der Mathematik”, and ”Die logischen Grundlagen der Mathematik” both from 1922 and the three sources together will be used to define Hilbert’s outlook.

In contrast with Russell’s well known dictum in his Principles of Mathematics that pure mathematics is the class of all propositions of the form ”$p$ implies $q$”, where $p$ and $q$ contain only logical constants, Hilbert conceived mathematics as an autonomous intellectual creation irreducible to anything else, logic or otherwise. In his philosophy he reconciles both the bias of his time towards extensionality and empiricism with the efforts to rediscover the axiomatic method. In his mature period Hilbert was able to characterize with formal rigour the differences between the classical axiomatic method and his own conception of what this method ought to be.

In Grundlagen I we find the fundamental criterion to distinguish between these two senses of the term ”axiomatic”. In his distinction there is an echo of the scholastic dichotomy between form and content, but it is fully captured by Hilbert’s own use of the words ”formal” and ”concrete”.

An axiomatic system is proposed in a concrete sense when, relative to a well established body of mathematical theory one tries to idealize the concepts that it contains and to single out a small number of propositions from which the whole theory can be logically derived. The classical example is the axiomatic formulation of Euclid’s geometry, in the form that dominated the English school system until the 1960’s.

In contrast to this, an axiomatic system is proposed in a formal sense when one begins by constructing an abstract theory, unrelated to any body of accepted doctrine. Primitive concepts and extensionally definable propositions have to be proposed, the consequences of which do not depend on making an appeal to the meaning of the expressions in which they are represented.

Without trying to minimize the theoretical interest of the problem of formulating suitable applications for a formal axiomatic system, Hilbert’s crucial question however was that of establishing whether an axiomatic system, even in the form of an abstract theory, is in itself, an sich, meaningful.

An abstract theory, as we saw above, is merely a sequence of propositions, which we deduce from another other sequence of propositions, called the axioms,using previously stipulated methods of inference. Such a theory then will not be meaningful in the same sense in which an axiomatic system proposed in a concrete sense is meaningful, since the meaning of this latter theory is provided by the body of experience which the theory is supposed to explain.

Thus to prove, against simple minded formalism, that a formal axiomatic system is not an arbitrary and futile game, one needs to show that the theory’s own conceptual structure exists in a specifiable domain of objects. In short one has to show that the theory has what one calls today a model.

Now it turns out that a considerable number of mathematical theories do not have an immediate translation in empirical experience accessible to spacio-temporal sense perceptions. This implies that the model which will provide the theory with its meaning will not always be actually specifiable. One then requires that it be specifiable at least in principle. But the question becomes then how can we know for sure that the primitive concepts of the theory can be interpreted as being the concepts involved in a certain domain of objects, and indeed interpreted in such a way that all the axioms in which they occur become true in the domain.

Such an interpretation of the primitive concepts amounts to a realization of the abstract theory. And just like one says in first order predicate calculus that a formula is satisfiable in a given model if the predicate, the functional and the individual variables, when interpreted, produce a true statement, one says likewise that a theory is realizable if one can specify a model in which, when interpreted, all the axioms result in true statements.

It is important to underline the qualitative difference between specifying a model actually and only in principle, since only for a restricted class of cases is it possible to actually specify a model, namely that class of cases in which the domain of the interpretation is finite.

Thus it is possible to actually produce a realization of the abstract structure of a group, by choosing a finite group specifiable by a product table that one can actually compute. Such a model shows that the structure has a realization. The problem arises first when one meets with relatively simple systems of axioms for which a finite model can not be specified.

Let us take as example a well known system, $O$, with one binary relation $R$, individual variables and the usual quantifiers:

Axiom 1: $(\forall x)\neg R(x,x)$

Axiom 2: $(\forall x)(\forall y)(\forall z)[R(x,y)\wedge R(y,z)\rightarrow R(x,z)]$

Axiom 3: $(\forall x)(\exists y)R(x,y)$

To see that this axiom system can not be satisfied in a finite domain $D$ of objects one reasons as follows. Assuming that $D$ is not empty we secure the existence of an object, which we can denote by a symbol like ”1”. Then by Axiom 3 there exists another object, to be denoted by ”11”, and the two together let the binary relation $R$ (”1”, ”11”) be satisfied in $D$.

But by Axiom 1, ”11” is different from ”1”. Another application of Axiom 3 secures the existence of another object, to be denoted by ”111”, which together with ”11” let the binary relation $R$ (”11”, ”111”) be satisfied in $D$. Therefore by Axiom 2 the binary relation $R$ (”1”, ”111”) is satisfied in $D$ and by Axiom 1 ”111” is different from ”11”. Since $D$ is finite the reiteration of this argument stops when the cardinal of $D$ is reached. Thus to satisfy O we have to introduce an infinite domain.

As an example we can immediately see that if we let $D$ be the set $\mathbb{Z}$ of integers and the binary relation $R$ the ordering $m<n$ in $\mathbb{Z}$, then O can be satisfied.

But an infinite domain is not a concrete totality which we can consider to be an immediate object of perception, and so its introduction needs to be justified as much as the abstract theory that it was supposed to justify.

It would seem prima facie that the implicit definition of the integers, by means of axioms such as de Dedekind-Peano axioms, would be a paradigm case for the introduction of infinite totalities. But such a definition would be in turn dependent on an abstract axiomatic theory. A model for such a theory would again be required and we would be therefore unable to justify the introduction of an infinite totality.

Hilbert’s Ansatz was then that if one has to use an infinite totality to provide a domain for the realiztion of an abstract theory, one has to require that this domain be itself the object of a direct and concrete perception. It is of course not possible to produce an infinite domain in such a way that we have a spacio-temporal simultaneous perception of all its elements. But we can have at any given time the perception of an initial segment of this totality.

To construct such an initial segment we start by having the elements of the domain to be represented by symbols like ”1”, ”11”, ”111”, $\ldots$, which we can obtain by starting with a first symbol ”1” and then obtaining a second simply by juxtaposing to the right the same symbol and then reiterating the process again.

We shall call these symbols ”numerals” and we can introduce variables, like small roman letters, which denote an numeral: $m$, $n$, $\ldots$

The order relation betweem two numerals $m$ and $n$ can thus be reduced to the inspection of the comparative length of $m$ and $n$. In a finite number of steps we can decide which is longer, or whether they have the same length, just by counting the number of symbols that each is composed of.

By the same token if $m$ and $n$ are two numerals their sum, to be denoted in the usual way by $m+n$, is the numeral that we obtain by juxtaposing $n$ to the right of $m$. Likewise the product of two numerals, to be denoted by $m\cdot n$, is the numeral that we obtain if we substitute each symbol of $n$ by $m$.

Thus for Hilbert mathematical insight is conceived as a thought-experiment performed on objects of which we can have a concrete and immediate perception, examples of which are the numerals in arithmetic, or the symbolic expressions with numerical coefficients in algebra. For this new kind of reasoning Hilbert coined the expression ”finitist inference”, where the term ”finitist” is supposed to express the fact that mathematical insight arises within the boundaries imposed on one side by the effective computability of all processes, and on the other by the concrete content of the validating perceptions.

We can therefore characterize finitist reasoning by the following three clauses:

F1. The objects about which inferences are made are not merely postulated but actually constructed;

F2. The computation and definition rules are only legitimate if one can secure a bound on the finite number of steps needed to terminate them.

F3. This bound has to be specified in advance.

As an example we want to describe the finitist meaning of two fundamental and well known processes.

Starting with induction let us assume that $P$ is a proposition which embodies some concrete and intuitive content about numerals. We assume that $P$ is valid for 1 and that if it is valid for $n$ then it is also valid for $n+1$. We conclude then that $P$ is valid for any numeral $k$. The finitist meaning of the induction rule consists in the recognition that $k$ is constructed from 1 by the reiterated juxtaposition of the same symbol. If we can verify that $P$ is valid for 1 and that by each juxtaposition of the symbol 1 $P$ remains valid for the new symbol, then when the construction of $k$ is terminated we can also verify that $P$ is valid for $k$.

Under this interpretation one immediately sees that the induction rule is not an autonomous axiom, but rather a corollary that follows from the principle used in the concrete construction of the symbolism.

The second example is definition by recursion where the purpose of the definition is the introduction of a new functional symbol $f$ by means of the equations:

where $k$ is a numeral and $g$ a binary function previously constructed and in such a way that $g(a,b)$ can be always computed and has a numeral as value.

And so, just as in the case of the induction rule, we recognize that the definition of a function by recursion is not an autonomous principle but rather a compressed description of a construction procedure, by means of which from one or more numerals a new numeral is again obtained. A certain amount of deductive detail would be involved in showing that this interpretation can be extended to reveal the finitist content of the well known properties of addition and product of integers, of the concept of prime number and the unique representation of an integer as a product of prime factors.

We want instead to delineate the principles of logic that follow from the adoption of the finitist point of view and begin by sketching the underlying theory of meaning.

We assume to be in contact with a sequence of quantifier-free propositions $P_{1}$, $P_{2}$, $\ldots$ about numerals and their relations and want to know what is the meaning of a statement like, for example, $m+n=k$. An answer is reached as soon as we establish the truth-value of the judgement expressed by the statement. We do this by direct inspection of the numerals to the left and to the right of ”=”, and the judgment is of course true when $m+n$ denotes the same numeral as $k$ and false otherwise.

On the other hand a simply quantified statement of the general form ($\forall x$) $F(x)$ is to be interpreted as having the meaning of a hypothetical judgment about each numeral, just as when we say that every prime greater than 2 is odd we mean to say that every prime is odd only if it is greater than 2.

The universal quantifier articulates a general law which can effectively be verified for each individual case, adequately expressed by the classical principle of the Dictum de Omni.

The meaning of a proposition of the form ($\exists x$) $F(x)$ is interpreted as being that of a partial judgment, in the sense that it is an incomplete segment of a statement yet to be more accurately determined. Such a determination may consist either in the immediate construction of a numeral $m$ such that $F(m)$ or in the specification of a procedure which allows the construction of a numeral $m$ such that $F(m)$.

It will be required that, according to F3, with the specification of the procedure which allows the construction, the bound on the number of steps of the construction also has to be given.

If we now turn to double quantification, the meaning of an assertion of the general form

is to be regarded as being that of an incomplete segment of a fuller statement which secures the existence of a procedure such that for every numeral $k$ such that $A(k)$, the procedure allows the construction of a numeral $m$ which stands with $k$ in the relation $B(k,m)$.

Negation in its finitist sense does not always coincide with negation in the classical sense. In quantifier-free statements, which in the literature are called elementary propositions, negation consists in the fact that we can establish by direct inspection that a given statement is false, like in $m+n=1$. The negation of this statement, expressed by the formula $\neg(m+n=1)$ is then true and asserts that the result of direct inspection and the result expressed by the formula are not the same.

Thus for decidable propositions the disjunction

is intuitively evident and can be used without restrictions.

The same can not be said of propositions in which negation precedes quantifiers and, from the finitist point of view, it is not immediately obvious how the negation of a quantified statement is to be understood.

We can interpret the negation of the existencial statement as meaning that an $x$ such that $F(x)$ is not known. But since such an interpretation expresses only a contingent state of knowledge, we have to improve it to an assertion about the impossibility of a construction of $x$.

This is the motivation to introduce the concept of the finitist negation of a proposition $A$, $\neg A$, which nevertheless is no longer the exact contradictory of the proposition $A$.

The pair of propositions ($\exists x$) $F(x)$ and $\neg(\exists x)$ $F(x)$ do not exactly behave like the pair $m+n=k$ and $\neg(m+n=k)$. And the difference is the following: whereas both elementary propositions represent one and the same decision about the numerals involved, the quantified statements represent two different kinds of knowledge.

In the case of the positive existential statement the knowledge obtained by contact with an $x$ such that $F(x)$ and, in the case of the negative existential statement, the knowledge by inference from some general law on numerals, showing the impossibility of the construction of $x$. And whereas it is intuitively evident that in the case of the elementary propositions the direct inspection of the construction will decide the statement one way or the other, it is not intuitively evident that in the case of the quantified statements the two kinds of knowledge must be expressed by mutually contradictory propositions. In this sense the general validity of

has to be rejected.

There are similar difficulties interpreting the negation of the universal statement, $\neg(\forall x)A(x)$, so that it is not immediately evident how it should be conceived.

On one hand we can interpret it as being a refutation of the universal statement by means of a counter-example but, on the other hand, we are commited to the interpretation of the universal statement as an incomplete assertion about a general principle of construction, verifiable for every instance. Here we have a parallel difficulty to the one found with existential quantification: it is not intuitively evident that either a general law about numerals $x$ such that $F(x)$ or the existence of a counter example must be expressed by mutually contradictory propositions. In this sense the general validity of the disjunction

has to be rejected.

One could argue that the universal statement can be refuted not only by a counter example but also by deriving from it a contradiction. But the above mentioned difficulty would also arise, since it is equally not intuitively evident that either a general law about numerals or the derivation of the contradiction which allows its refutation must be expressed by mutually contradictory propositions.

We return now to the initially mentioned problem of the intrinsic meaning of a mathematical theory. We have seen that an abstract axiomatic theory is to be considered meaningful only if we can produce a model of the theory, that is an interpretation in which all the axioms became true and the rules of inference preserve truth.

If we have a finite model then the meaning of the theory is immediately given, namely in the direct inspection of the model from which we obtain the truth values of the statements whose meaning we want to know. This applies even if the model is infinite,in which case the interpretation has to be formulated by means of definitions that conform to finitist principles i.e., F1, F2 and F3.

The crucial question is that these principles, as definied in Section 6, have a very restricted range, as we can see from the fact that already in elementary first order arithmetic we have to go beyond it to state, for example, that if a property $P$ is satisfied by a positive integer $k$, then there is a least positive integer that satisfies $P$. Under these circumstances the method by means of which we have secured the meaning of an abstract mathematical theory has to be subject to a revision, and Hilbert’s idea was that the source of meaning has to be now the consistency proof of the theory.

Accordingly an abstract mathematical theory has meaning, i.e., is able to describe a structure, if we have a proof that from the axioms, by means of the rules of inference, a contradiction can not be derived. At this point the focus of Hilbert’s programme shifts to the task of ensuring, for any given mathematical theory, a proof that the methods of inference used in the theory do not give rise to a contradiction.

For the new outlook Hilbert coined the names Proof-Theory and Metamathematics, to be defined as the systematic study of the range of validity of the several methods of inference used in mathematics.

However, as it was to be expected, for the consistency proof it was required that the metamathematical argument used had to conform to finitist principles. And whereas at the time of Grundlagen der Geometrie Hilbert was only interested in proving the consistency of Euclidean geometry, in Grundlagen der Mathematik his horizon was the validation of the whole body of classical mathematics by means of finitist metamathematical arguments.

To achieve that purpose Hilbert was to led to represent a given mathematical theory in a formalized deductive system, i.e., a system with a fixed syntax and its associated semantics.

The syntactical point of view consisted in:

i) Describing the alphabet of the theory and its well-formed formulas.

ii) Grounding the theory in a postulated non empty domain of objects.

iii) Isolating a finite number of initial well-formed formulas as being the set of axioms of the theory.

iv) Formulating the rules of inference explicitly.

In such a system the derivable formulas are those well-formed formulas which we can obtain from the initial formulas or axioms by a finite number of applications of the rules of inference. It was to be expected that each theorem of the underlying (informal) theory would be represented by a derivable formula of the formal system, in which case the system would be called complete. Thus if we then have a consistency proof of the formal theory, the meaning of the underlying (informal)theory is fully established.

It turns out that the frequent use of non-finitist reasoning in ”real” (i.e., pre-formal) mathematical theories forces the introduction, in the formal theories which are supposed to justify real mathematics, of rules of inference which represent that non-finitist segment of the real theory.

Is this paradoxical? Let us assume that a formal system $f$ represents a real theory $T$ which contains one or several non-finitist arguments. They will have to be represented in $F$ and Hilbert’s argument is that the situation is not paradoxical because $F$ conforms to our principles F1, F2, F3, so that in the end the representation is again a sequence of well-formed formulas which have to be built according to finitist principles.

Finitism and intuitionism have some features in common, like the belief that mathematical objects do not exist prior to their construction and the rejection of basic laws of classical logic like the tertium non datur. But intuitionism is in general less restrictive than finitism, and so Brouwer allows general abstract arguments even if their scope is narrower than in classical realism.

But in intuitionism, in spite of the role played by combinatorial experience, reigns the notion that a mathematical construction is essentially an act of awareness and that such an experience is better understood by taking the intensional point of view. In contrast Hilbert’s finitism emphasizes the notion that a mathematical insight is a synthetic judgement about the outcome of an experience on concrete objects, conceived as formed by discrete parts inserted in the space-time continuum.

In this sense intuitionism includes finitism since the experience of a concrete object can be the content of an intensional act. But intuitionism goes beyond finitism in that it allows arguments about all possible constructions, and this is not a meaningful finitist totality.

Another essential difference is that in Brouwer’s intuitionism no single formal theory can ever represent the the fullness of real mathematical reasoning.

It was to be expected, after the successful formalization of the essential parts of first order logic, that the formalization of first order arithmetic would also be possible. A theorem by Kurt Gödel proves that it not possible to represent in a formal theory for arithmetic all the truths of real arithmetic. In another related result Gödel also shows that the required consistency proof for a formal system for arithmetic can not be carried out within the formal system itself.

Gödel devoted some of his later work to define the boundaries between intuitionism and finitism and in his epoch-making 1958 work Ãœber eine bisher noch nicht benützte Erweiterung des finiten Stanpunktes he formulated the mathematical-philosophical conditions to be required in order to extend finitism beyond incompleteness.