Supplement to Proof Theory
A. Formal Axiomatics: Its Evolution and Incompleteness
In this somewhat extended appendix, we are going to discuss the evolution of the formal axiomatic standpoint in Hilbert’s foundational thinking. To begin with we articulate in greater detail than we did in section 1 of the main article Dedekind’s way of defining abstract concepts, like that of a simply infinite system. Dedekind had seen very clearly that such a structural definition raises a fundamental issue: How can we ensure that such a definition does not contain internal contradictions?
- A.1 Structural definitions
- A.2 Consistency: no internal contradictions
- A.3 Formal proofs
- A.4 Gödel’s incompleteness results
A.1 Structural definitions
In the three volumes of Dedekind’s Gesammelte mathematische Werke, there are exactly two occurrences of the word “Axiom”. The main substantive occurrence is found in section 3 of Dedekind 1872, where Dedekind refers to his principle of continuity as an axiom. The second occurrence, in the preface to the same essay, points to Cantor’s 1872, where a corresponding principle is also called an axiom. To emphasize, the word “Axiom” is neither used in his work on algebraic number theory, nor in his second foundational essay on natural numbers (Dedekind 1888). And yet, Emmy Noether is right when she asserts in her brief remark on Stetigkeit und irrationale Zahlen that Dedekind’s axiomatic standpoint is articulated very clearly in this essay and in his letters to Lipschitz from June and July 1876 that comment on the essay (her remarks can be found in Dedekind 1932: 334). In his letter of July 1876, Dedekind makes a striking remark concerning Euclid’s Elements and continuity:
Let’s analyze all the assumptions, that have been made explicitly or tacitly, on which the entire edifice of Euclid’s geometry is built, let’s admit the truth of all his theorems as well as the feasibility of all his constructions …: as far as I have investigated matters, one never reaches in this way the continuity of space as a condition that is inseparably connected with Euclid’s geometry; his whole system remains valid even without continuity—a result that is certainly surprising for many and thus seemed to me to be worth mentioning. (Dedekind 1932: 479)
Where we indicated the ellipsis, Dedekind inserted a remarkable statement, in parentheses, that pertains to his theory of real numbers:
(an absolutely reliable method of such an analysis consists for me in the replacement of all Kunstausdrücke [technical terms or terms of art] by arbitrary newly invented (up to now meaningless words): the edifice, if properly constructed, must not collapse, and I claim for example that my theory of real numbers passes this test).
What is Dedekind’s theory of real numbers?—It is
best understood as the theory of complete (or continuous)
ordered fields. The notion of a field, prominent in
Dedekind’s work on algebraic number theory, was introduced in a
supplement to Lejeune Dirichlet et al. 1871.
It is highlighted in the 1872
essay already in section 1, entitled “Properties of rational
numbers”. The system
-
is a subset of N, - N is the chain of the system
, - 1 is not an element of
, and - the mapping
is injective.[35]
Using this approach, any system R of things is a complete ordered field just in case there is an ordering O and there are four operations on R, such that (1) R with O is a continuous ordered system (in Dedekind’s sense) and (2) R with the four operations is a field (and the operations are compatible with the ordering). Dedekind’s theory of real numbers is thus given as a “structural definition”.
Hilbert’s theory of real numbers is formulated in Hilbert 1900a also as a structural definition. It is assumed that a system exists whose elements satisfy the conditions Hilbert calls axioms. Hilbert points out the parallelism with the method of geometry.
Here [in geometry] one begins customarily by assuming the existence of all the elements, i.e., one postulates at the outset three systems of things (namely, the points, lines, and planes), and then—essentially after the model of Euclid—brings these elements into relationship with one another by means of certain axioms of linking, order, congruence, and continuity. (Hilbert 1900a: 1092)
These geometric ways are taken over for arithmetic when Hilbert introduces a system of real numbers as follows:
We think a system of things, and we call them numbers and denote them by a, b, c…. We think these numbers in certain mutual relations, whose precise and complete description is obtained through the following axioms. (Hilbert 1900a: 1092)
Then the axioms for an ordered field are formulated and “completed” by the requirement of continuity via the Archimedean axiom and the axiom of completeness. This formulation is in the spirit of Hilbert’s geometric ways, but how is it connected to Dedekind’s way?
The connection is illuminated through the correspondence with Frege in late 1899 when Hilbert responds to Frege’s complaint about his use of the word “axiom”; he points out that the Erklärung of the concept “between” provides a proper definition, as its characteristic conditions (Merkmale) are given by the five axioms II 1 through II 5 that involve “between”. He writes, if one wanted to take “definition” in exactly the traditional sense, then one would have to say:
“Between” is a relation for the points of a line that satisfies the following characteristic conditions: II 1 … II 5. (Gabriel et al. 1980: 11)
He emphasizes that he has absolutely no objection, if Frege called his axioms simply characteristic conditions. He asserts most clearly:
The renaming of “axioms” as “characteristic conditions” etc. is a pure formality and, in addition, a matter of taste—in any event, it is easily accomplished. (Gabriel et al. 1980: 12)
Let us see briefly how this perspective allows us to understand properly the completeness axiom that is frequently criticized as being metamathematical and, to boot, a statement of a peculiar sort.[36]
The completeness axiom requires in both the geometric and arithmetic case that the assumed structure is maximal, i.e., any extension satisfying the remaining axioms must already be contained in it. In the case of the arithmetic of real numbers, we can proceed as follows: Call a field continuous when it satisfies the axioms of an ordered field and the Archimedean axiom; a system A is called fully continuous or complete if and only if A is continuous and for any system B, if A is a subfield of B and B is continuous, then B is a subfield of A. Hilbert’s arithmetic axioms are equivalent to Dedekind’s characteristic conditions for a complete ordered field and characterize the fully continuous systems up to isomorphism.
A.2 Consistency: no internal contradictions
In the 1920s, Hilbert and Bernays called this way of proceeding, because it assumes the existence of a suitable system, existential axiomatics. Hilbert’s view of axioms as characterizing a system of things is complemented by the traditional one, namely, that the axioms must allow to establish, purely logically, all geometric facts and laws. It is reflected for arithmetic in the Paris lecture, where he states that the totality of real numbers is
… a system of things whose mutual relations are governed by the axioms set up and for which all propositions, and only those, are true which can be derived from the axioms by a finite number of logical inferences. (Hilbert 1900a: 1092)
It is Hilbert’s firm view that “the concept of the continuum is strictly logically tenable in this sense only” and that the axiomatic method has to confront two fundamental problems, formulated in 1900 at first for geometry and then for arithmetic:
The necessary task then arises of showing the consistency and the completeness of these axioms, i.e., it must be proved that the application of the given axioms can never lead to contradictions, and, further, that the system of axioms suffices to prove all geometric propositions. (Hilbert 1900a: 1092–1093)
It is not clear, whether completeness requires the proof of all true geometric, or arithmetic, statements or of just those that are part of the established corpus; the latter would be a quasi-empirical notion of completeness. Turning to the central topic of consistency, we observe that the notion was viewed as a “semantic” one not only by Dedekind, but also by logicians in the nineteenth century more generally. In the essay (1888) and his letter to Keferstein (1890), Dedekind sharply expresses a crucial requirement for a structural definition; namely, one has to logically prove the existence of a system of things falling under the notion in order to ensure that it does not contain “internal contradictions”. The considerations in 1872 that pertain to cuts of rational numbers establish that the system of cuts falls under the concept of a complete ordered field; in more modern terms, the system of cuts is a complete ordered field, as it satisfies the Merkmale of the notion. If one views these Merkmale as axioms formulated in an appropriate language, then the system of cuts provides a model of these axioms.
This is a pre-Tarskian notion of semantics introduced in Hilbert
1917/18, but rooted—via the indicated connection to satisfying
the conditions of a structural definition—in the mathematical
practice of the late nineteenth century. It is used in Hilbert &
Ackermann 1928 and also in Gödel’s dissertation (1929) that
is following, as Gödel himself emphasizes, Hilbert and
Ackermann’s terminology. Of course, in Gödel’s thesis
this is done only for the language of first-order logic or the
“restricted function calculus”. The formulae of the
latter, logische Ausdrücke, are built up from individual
variables
Let A be any logical expression that contains the function variables
, ,…, , the free individual variables , ,…, and the statement variables , ,…, and otherwise only bound variables. Let , ,…, be functions (all defined in the same domain of thought), , ,…, individuals (belonging also to the same domain of thought), and , ,…, statements; of this system we say that it satisfies the logical expression, if it yields, when placed into it [the expression], a true proposition ([true] in the domain of thought under consideration). (Gödel 1929 [1986: 66–68])[37]
There is no further explication of “true proposition”. Let us note that Gödel later discusses a language expanded by individual constants (names) and function constants (relation symbols). He distinguishes logische Ausdrücke from Zählausdrücke: the latter contain neither function nor statement variables and all individual variables are bound. Zählaxiomensysteme are defined as consisting only of Zählausdrücke. As an example of such an axiom system he mentions in note 10 Hilbert’s system for geometry without the continuity axioms, i.e., the Archimedean principle and the completeness axiom. For the metamathematical investigation the axioms “with a fixed interpretation” are replaced by corresponding logical expressions: Gödel solves the completeness problem for Zählaxiomensysteme by reducing it by this technique to the solution for the corresponding axiom system. But let us return to Hilbert’s earlier work.
In 1899 and 1900a,b, Hilbert formulated a (quasi-) syntactic notion of consistency: no finite number of logical steps lead (from given axioms) to a contradiction. That does not mean, however, he sought to prove consistency by syntactic methods. The (relative) consistency proofs in 1899 are all semantic. In 1900a, Hilbert expected to prove the consistency of arithmetic by “a suitable modification of familiar methods of inference”. In the Paris Lecture he suggests finding a direct method of proof; but he still thought that such a method would emerge from a suitable modification of known methods. Hilbert believed, it seems, that the genetic build-up of the real numbers could somehow be exploited to yield the blueprint for a consistency proof in Dedekind’s logicist style. That impression is supported by his treatment of arithmetic in contemporaneous lectures, but also by a more programmatic statement from the Introduction to the notes for the lectures Elemente der Euklidischen Geometrie that were given in the winter term 1898/99. He maintains there,
It is important to fix precisely the starting-point of our investigations: as given we consider the laws of pure logic and in particular all of arithmetic. (Hilbert 1898/99: 303).
Hilbert adds then parenthetically, “On the relation between logic and arithmetic cf. Dedekind, Was sind und was sollen die Zahlen?” and, for Dedekind, arithmetic is clearly part of logic.
Hilbert changed his attitude only after the discovery of the elementary contradiction of Russell and Zermelo.[38] That paradox convinced him that there was a deep problem, that difficulties appeared already at an earlier stage, and that the issue had to be addressed in a different way. In early 1904 Hilbert sent a letter to Adolf Hurwitz writing:
It has been my view for a long time that exactly the most important and most interesting questions have not been settled by Dedekind and Cantor (and a fortiori not by Weierstrass and Kronecker). In order to be forced into the position to reflect on these matters systematically, I announced a seminar on the “logical foundations of mathematical thought” for next semester. (Dugac 1976: 271)
The notes from the following summer term contain complimentary remarks on Dedekind’s achievements, but insist pointedly that basic difficulties remain.
He [Dedekind] arrived at the view that the standpoint of considering the integers as obvious [selbstverständlich] cannot be sustained; he recognized that the difficulties Kronecker saw in the definition of irrationals arise already for integers; furthermore, if they are removed here, they disappear there. This work [Was sind und was sollen die Zahlen?] was epochal, but it did not yet provide something definitive, certain difficulties remain. These difficulties are connected, as for the definition of the irrationals, above all to the concept of the infinite; … (Hilbert 1904: 166)
This set the stage for Hilbert’s Heidelberg talk in August of that year, 1904, in which he indicates a novel way of solving the consistency problem for arithmetic. The sense in which he takes arithmetic now is more restricted, namely, as dealing with just the natural numbers.
A.3 Formal proofs
Hilbert’s Heidelberg talk takes on the consistency problem with a striking syntactic approach. The goal is still securing the existence of a suitable model, that means here “the consistent existence of the so-called smallest infinite”. The system consists of axioms for identity and Dedekind’s conditions for a simply infinite system; the induction principle is mentioned, but neither formulated nor treated in the consistency argument. In modern notation the axioms can be given in this way, where W is a “formula”:
The rules, implicit in Hilbert’s description of “consequence”, are modus ponens and a substitution rule allowing the replacement of variables by arbitrary sign combinations. Other “modes of logical inferences” are alluded to but not stated, and they are consequently not incorporated into the consistency proof. The view that the problem for the real numbers is resolved once matters are settled for the natural numbers is strongly emphasized.
For the consistency proof Hilbert calls an equation
The considerations just sketched constitute the first case in which a direct proof of consistency has been successfully carried out for axioms, whereas the method of a suitable specialization, or of the construction of examples, which is otherwise customary for such proofs—in geometry in particular—necessarily fails here. (Hilbert 1905 [1967: 135])
Hilbert stressed the programmatic goal of developing logic and mathematics simultaneously, but the actual work has real shortcomings: as to the logical work, there is no calculus for sentential logic and there is no proper treatment of quantification; as to the mathematical work, not even the induction principle is formulated. In sum, there is an important shift from “semantic” to “syntactic” arguments, but the formal set-up is woefully inadequate as a frame for mathematics.
The foundational import of Hilbert’s considerations was challenged by Poincaré, interpreting the results in a very generous way as including the treatment of induction. As the consistency proof proceeded by induction, Poincaré raised not only the question, how it could be viewed as justifying induction, but also brought out additional methodological shortcomings (Poincaré 1905 [1996: 1026–7]).[39] His incisive analysis shifted Hilbert’s attention not away from foundational concerns—they are documented by lectures given throughout the period from 1905 to 1921—but rather from the “proof-theoretic” approach advocated in the Heidelberg talk. Indeed, under the impact of a detailed study of Principia Mathematica beginning in 1913, Hilbert flirted again with logicism.[40] What resulted from this study were the lectures Prinzipien der Mathematik. Hilbert gave them in the winter term of 1917/18 with the assistance of Paul Bernays; these lectures present modern mathematical logic and provide a comprehensive formalism for representing mathematical practice, in particular, for developing analysis in ramified type theory with the axiom of reducibility.
The programmatic logicism in Hilbert’s Zürich talk and these lectures was abandoned in the following years. A radical constructivism for developing mathematics from the ground up replaced it, but was abandoned as well, because even basic logical laws were seen not to hold, e.g., the law of the excluded middle. The finitist consistency program, as we think of it, was only formulated towards the end of lectures given in the winter term 1921/22. The elementary character of the formalisms for mathematics allowed viewing the metamathematical studies as part of constructive mathematics. This new, still tentative perspective was connected to Hilbert’s approach in his Heidelberg talk; indeed, that approach had been reviewed and modified in 1920/21. The broad considerations and preliminary results were presented in talks in Copenhagen and Hamburg given in the spring and summer of 1921. In his 1922 paper, based on these talks, Hilbert claimed that induction had been avoided by restructuring the consistency proof and that Poincaré’s objection had consequently been met.
In September of 1921, Bernays presented a paper at the meeting of the German Association of Mathematicians (DMV) in Jena. The paper was published as Bernays 1922 and starts out with a discussion of existential axiomatics that presupposes, as we saw in A.2, a system of objects satisfying the structural conditions formulated by the axioms. As the assumption of such a system contains “something so-to-speak transcendent for mathematics”, the question arises, “which principled position with respect to it should be taken”. Bernays remarks that it might be perfectly coherent to appeal to an intuitive grasp of the natural number sequence or even of the manifold of real numbers. However, that could not be an intuition in any primitive sense, and one should take seriously the tendency of the exact sciences to use only restricted means to acquire knowledge, as far as that can be done. He was led to the question,
whether it is not possible to give a foundation to these transcendent assumptions in such a way that only primitive intuitive knowledge is used. (Bernays 1922: 11)
Contentual mathematics is to be based on primitive intuitive knowledge and includes for Bernays, at this stage, induction—both as a proof and definition principle concerning the natural numbers. In the outline (Disposition) for the lectures to be given in the winter term 1921/22, Bernays discusses “constructive arithmetic” (konstruktive Arithmetik) and then the “broader formulation of constructive thought” (konstruktiver Gedanke):
Construction of the proofs, by means of which the formalization of the higher inferences is made possible and the consistency problem is becoming accessible in a general way. (Bernays 1921: 123–124)
A.4 Gödel’s incompleteness results
On 26 August 1930, Gödel met with Rudolf Carnap and Friedrich Waismann at the Café Reichsrat; the main topic of conversation was their upcoming trip to Königsberg, from Vienna of course. Reflecting a dramatic shift away from travel preparations, Carnap noted that the discussion turned to “Gödel’s discovery: Incompleteness of the system of Principia Mathematica; difficulty of the consistency proof”.[41] In Königsberg the three attended the Conference for Epistemology of the Exact Sciences that was held there from 5 to 7 September. On the very first day of the conference, Carnap and Waismann gave plenary lectures on the foundations of mathematics presenting the logicist position and Wittgenstein’s views, respectively; von Neumann and Heyting gave complementary lectures on the formalist and intuitionist standpoints. On the next day Gödel presented the results of his thesis claiming at the very end of his talk[42] that the completeness result for first-order logic cannot be extended to “the higher parts of logic (the extended functional calculus)”. After all, together with the categorical characterization of natural and real numbers, such a result would imply the “solvability of every problem of arithmetic and analysis expressible in Principia Mathematica”. That conclusion, he argued, conflicts with a fact he had recently established, namely, that
… there are mathematical problems which can be expressed in Principia Mathematica but cannot be solved by the logical devices of Principia Mathematica.
The latter fact, Gödel asserted, can also be expressed as follows:
The Peano axiom system, with the logic of Principia Mathematica as superstructure, is not syntactically complete.
Carnap, Heyting, von Neumann, Waismann and Gödel were among the participants of a roundtable discussion “Zur Grundlegung der Mathematik” that took place on 7 September, the last day of the conference, and was chaired by Gödel’s thesis advisor Hans Hahn. At that occasion, Gödel presented his result in greater detail, but also with a different emphasis. (The stenographic notes of Gödel’s remarks were published in the 1931 issue of the journal Erkenntnis together with a Postscriptum (Nachtrag, 1931b) that summarizes the mathematical results of Gödel 1931a.) Now he connects his considerations closely with Hilbert’s program and argues, the consistency of a formal theory A for classical mathematics does not guarantee that all theorems of A are “contentually correct” (inhaltlich richtig). At first he views it as “quite possible” that
… one might prove a statement of the form
, where F is a finitist property of natural numbers (the negation of Goldbach’s conjecture, e.g., has this form) by the transfinite means of classical mathematics and yet ascertain by contentual considerations that all numbers have the property not-F; this remains possible, and that’s what I would like to point out, even if the consistency of the formal system for classical mathematics had been proved. For of no formal system can one claim that all contentual considerations are representable in it. (Gödel 1931b: 200)
In a second remark, he strengthens the claim that “one might
prove a statement” to the assertion, “one can indeed give
examples of statements” that are contentually correct but
unprovable in A, if the latter is consistent. He concludes: Thus, if
one adjoins the negation of such a statement to the axioms of
classical mathematics, then one obtains a consistent system in which a
contentually false statement is provable. Let us explore now, how
Gödel seems to have convinced himself of that state of
mathematical affairs. This reconstruction is based on Wang 1981 and
the long first section of Gödel 1931a that sketches the
“main idea of the proof” and assumes the semantic
soundness of classical mathematics; in the core of the paper,
soundness is replaced by the weaker syntactic conditions of
consistency and
Ironically, the main idea exploits two features that made
Hilbert’s finitist program plausible: (1) strong formal theories
T, like Principia Mathematica or Zermelo-Fraenkel set theory,
allow the formalization of mathematics, and (2) the formal theories
can be described in a very elementary part of mathematics, finitist
mathematics. The latter descriptions are precise and can be involved
in rigorous mathematical arguments; after all, a finitist proof of the
consistency of formal theories was sought and actually given for a
fragment of arithmetic. It was also clear that elementary
combinatorial concepts could be defined in the formal theories.
Gödel observed that metamathematical notions like FORM(ULA)
and PROOF
can be provably (in
metamathematics) represented by formulae in the language of
T; that amounts, say for FORM,
to having a formula form in the language of T such
that: If FORM(
One way of achieving such a naming scheme is to require that T
have names for natural numbers, i.e., numerals, and allow for
the formation of sequences (of sequences) of numerals. The numerals
can be used, non-standardly, as names or codes for the basic
symbols of T’s language; the numeral used, for example,
as the code for the conjunction symbol
This way of “internalizing” the syntactic description of
T in T allows us, in particular, to formulate a
self-referential statement G that expresses its own
unprovability in
T.[46]
If T is sound, G is seen to be independent of T
as follows. Assuming that T proves G, soundness
guarantees the truth of G and consequently the unprovability of
G; thus, T does not prove G. Assuming that
T proves
One thus obtains a proof for the existence of undecidable propositions in that system, but no individual instance of an undecidable proposition. (1934 [1986: 363])
All of this concerns the first incompleteness theorem. At the end of the first section of his 1931a, Gödel remarks that the formally undecidable sentence G can be decided by metamathematical considerations and continues:
The precise analysis of this curious situation leads to surprising results concerning the consistency proofs of formal theories, that will be presented in greater detail in section 4 (Theorem XI). (Gödel 1931a: 150)
Gödel discovered this theorem only after the Königsberg
congress; it is his second incompleteness theorem, asserting that the
formal statement cons expressing the consistency of a theory
cannot be proved in the theory. For its proof, Gödel suggested
formalizing the argument for the first incompleteness theorem in order
to obtain the statement
In this discussion, von Neumann asked whether number theoretical undecidable propositions could also be constructed, in view of the fact that the combinatorial objects can be mapped onto the integers, and expressed the belief that it could be done. In reply, Gödel said, “Of course undecidable propositions about integers could be so constructed, but they would contain concepts quite different from those occurring in number theory like addition and multiplication”. Shortly afterward Gödel, to his own astonishment, succeeded in turning the undecidable proposition into polynomial form preceded by quantifiers (over natural numbers).
Von Neumann was very enthusiastic about the result Gödel had found and was preoccupied with it during the following months. We get a sense of that from Herbrand’s letter to his friend Claude Chevalley, when he writes from Berlin on 3 December 1930:
Mathematicians are a strange bunch; I have been here for two weeks, and each time I see von Neumann, we talk about a paper by a certain Gödel, who has produced quite curious statements; and all this destroys some very solidly anchored ideas.[47]
This sentence opens the letter. Having sketched Gödel’s arguments, Herbrand concludes the metamathematical discussion with, “Please excuse this long beginning; but all of this haunts me, and by writing about it I can exorcise it a bit”.
Von Neumann communicated the outcome of his reflections to Gödel in a letter of 20 November 1930 announcing as a “new result” that the consistency of classical mathematics is unprovable. The reasoning for von Neumann’s result was articulated more sharply in a letter of 12 January 1931, which he wrote after having received the galleys of Gödel’s 1931a paper with its dramatic expansion of methods and results. Metamathematically von Neumann claimed—in contrast to Gödel’s sketch of a formal proof of the first incompleteness theorem—the equivalence of the sentence G with the consistency statement cons assuming general properties of the theorem predicate for formal theories. (That’s what Hilbert and Bernays would do in great detail and precisely in their 1939 through representability and derivability conditions.) Methodologically he argued—in opposition to Gödel’s conjecture—that intuitionist or, synonymously at the time, finitist proofs can be formally captured in elementary arithmetic or, if not there, then certainly in analysis or set theory.[48]