``To prevent anything intuitive from penetrating [into an argument] unnoticed, I had to bend every effort to keep the chain of inferences free of gaps. In attempting to comply with this requirement in the strictest possible way I found the inadequacy of language to be an obstacle. This deficiency led me to the present ideography...Leibniz, too, recognized -- and perhaps overrated the advantages of adequate notation. His idea of a...calculus philosophicus... was so gigantic that the attempt to realize it could not go beyond the bare preliminaries. The enthusiasm that seized its originator when he contemplated the immense increase in intellectual prover of mankind that [the calculus would bring] caused him to underestimate the difficulties.... But even if this worthy goal cannot be reached in one leap, we need not despair of a slow step by step approximation.''
So Frege began with very limited goals and took what he characterized as ``small steps'' (like creating all of predicate logic!). He did not include a study of computation and its language; he limited his study of notation to logical operators, and he ruled out creating a natural expression of proofs or classifying them based on how ``obvious'' they are.
In addition, Frege focused on understanding the most fundamental types, natural numbers, sequences, functions, and classes. He adopted a very simple approach to the domain of functions, forcing them all to be total. He said (in his Collected Papers) ``the sign a + b should always have a reference, whatever signs for definite objects may be inserted in place of `a' and `b'.'' Principia took a different approach to functions, introducing types, but also it excluded from consideration an analysis of computation or natural proofs or the notational practices of working mathematics. It too developed only basic mathematics with no attempt to treat abstract algebra or computational parts of analysis.
Principia Mathematica, the monumental work of [116], was indeed the first comprehensive rendering of mathematics in symbolic logic. Gödel's celebrated 1931 paper ``On Formally Undecidable Propositions of Principia Mathematica and Related Systems'' begins:
``The development of mathematics toward greater precision has led, as is well known, to the formalization of large tracts of it, so that one can prove any theorems using nothing but a few mechanical rules. The most comprehensive formal systems that have been set up hither to are the system of Principia Mathematica (PM) on the one hand and the Zermelo-Fraenkel axiom system of set theory...on the other.''
Principia presents a logic based on types and derives in it a theory of classes, while ZF set theory provided informal axioms and, logic was incidental.6 Principia deals with the topics that I find fundamental in my own work of ``implementing mathematics'' in the Nuprl system, [28]. Thus much of what I say here is related to PM. Indeed, in a sense Nuprl is a modern style Principia suitable for computational mathematics.
Hilbert introduced a greater degree of formalization, essentially banishing semantics, and he began as a result to deal with computation in his metalanguage. But he took a step backwards from Principia in terms of analyzing when expressions are meaningful. He reduced this to an issue of parsing and ``decidable type checking'' of formulas as opposed to the semantic judgments of Principia.
It wasn't until Gentzen that the notion of proofs as they occur in practice was analyzed, first in natural deduction and then in sequent calculi. It wasn't until Herbrand, Gödel, Church, Markov, and Turing that computation was analyzed and not until de Bruijn that the organization of knowledge (into a ``tree of knowledge'' with explicit contexts) was considered. De Bruijn's Automath project also established links to computing, like those simultaneously being forged from computer science.
Recently Martin-Löf has widened the logical investigation to reintroduce a semantic approach to logic, to include computation as part of the language, and to make manifest the connections to knowledge. [81, p.30] says:
``to have proved = to know = to have understood, comprehended, grasped, or seen. It is now manifest, from these equations, that proof and knowledge are the same. Thus, if proof theory is construed, not in Hilbert's sense, as metamathematics but simply as the study of proofs in the original sense of the word, then proof theory is the same as theory of knowledge...''
We are now in a position where mathematical logic can consider all of these elements: an analysis of the basic judgments of typing, truth, and computational equality; an analysis of natural proofs and their semantics; the integration of computational concepts into the basic language; an analysis of the structure of knowledge and its role in practical inference; and classification of inference according to its computational complexity.
We will attempt a consideration of logic that takes all this into account and is linked to computing practice, and yet is accessible. I begin the article with an account of typed logic that relates naturally to the Automath conception. The connection is discussed explicitly in Section 2.12.
The article stresses the nature of the underlying logical language because that is so basic -- everything else is built upon it. The structures built are so high that a small change in the foundation can cause a large movement at the top of the structure. So any discoveries that improve the foundation for formal mathematics are among the most profound in their effect. As it is, we are standing on the shoulders of giants. I take the time in section 2 to review this heritage that is so crucial to everything else.