Historical perspective on a grand enterprise 1875-1995

>From Begriffsschrift [44] onwards until Grundgesetze [45], logic was re-surveyed by Gottlob Frege, and the ground was cleared to provide a firm foundation for mathematics.³ In Principia Mathematica, [116] revised Frege's flawed architectural plans, and then using these plans, [63] laid out a formalist program to build the completely formal theories which would be used to explain and justify the results and methods of mathematics. His program would defend mathematical practice against critics like Brouwer who saw the need to place the foundation pilings squarely on the natural numbers and build with constructive methods.⁴

Hilbert called for workers, training some himself, and began with them the task which proved to be so compelling and attractive to many talented mathematicians like Church, von Neumann, Herbrand, Gentzen, Skolem, Turing, Tarski, Gödel, and many more. Boring deep into the bedrock to explore the foundation site, Kurt Gödel [51] unexpected limitations to the planned activity. It could never be completed as envisioned by Hilbert.⁵ His surprising discovery changed expectations, but the tools Gödel created transformed the field and stimulated enormous interest in the enterprise. More remarkable discoveries followed.

Within two decades, computer science was providing new ``power tools'' to realize in software the formal structures needed to support mathematics. By 1960 computer hardware could execute programming languages like LispLisp, c.f. [84], designed for the symbolic processing needed to build formal structures. Up in the scaffolding computer scientists began to encounter their own problems with ``wiring and communications,'' control of resource expenditure, design of better tools, etc. But already even in the 1970's poised over the ground like a giant drilling rig, the formal structures supported still deeper penetration into the bedrock designed to support mathematics (and with it the mathematical sciences and much of our technical knowledge). The theory of computational complexity, arising from [58], led to further beautiful discoveries like Cook's P=NPproblem, and to a theory of algorithms needed for sophisticated constructions, and to a theory of feasible mathematics (see [21,75,74,76]), and to ideas for the foundations of computational mathematics.

By 1970 the value of the small formal structure already assembled put to rest the nagging questions of earlier times about why mathematics should be formalized. The existing structure provided economic benefit to engineering, just as Leibniz dreamed, Frege foresaw, McCarthy planned [85], and many are realizing. ([55,17,53,33,64,91]).

Even without the accumulating evidence of economic value, and without counting the immediate utility of the software artifacts, scientists in all fields recognized that the discoveries attendant on this ``grand enterprise'' illuminate the very nature of knowledge while providing better means to create and manage it. The results of this enterprise have profound consequences because all scholars and scientists are in the business of processing information and contributing to the accumulation and dissemination of knowledge.