Begriffsschrift is not only the direct ancestor of contemporary systems of mathematical logic, but also the ancestor of all formal languages including computer programming languages. (Citation.)
Frege's reason for creating this "ideography" or "concept script" is essentially the reason behind creating formal verification systems; that is, he wanted to leave no gaps in his reasoning. He said,
Its first purpose, therefore, is to provide us with the most reliable test of the validity of a chain of inferences and to point out every pre-supposition that tries to sneak in unnoticed, so that its origin can be investigated.
It is worth reading more of the introduction to Begriffsschrift to see how Frege was led to this revolutionary new idea, the idea underlying all the work we do on this project. (Citation.)
David Hilbert was led to the idea of a formal system for similar but distinct reasons. He developed this notion with increasing precision and clearer purpose in the 1920s, at the same time that Emil Post was coming to them in his 1920 PhD thesis in the United States. Hilbert understood the idea of removing the meaning from an axiom system from his work on the foundations of geometry.
Hilbert eventually (in the 1920s) based his famous "program" for "saving mathematics" from its foundational crisis on the idea of studying formal systems as mathematical objects using a highly constructive, even finitistic, mathematics which he called metamathematics. In this view, mathematics is considered to be a meaningless game, like chess. The only important property of the game is that it be free from contradiction. His bold idea for a program of salvation was to show, using finitary means, that the game was safe. Some of the results would be meaningful, at least the finitistic ones and perhaps the constructive ones if Brouwer had a say (See Constructive Mathematics); while other results were only "ideal." They lacked meaning in themselves, but could be used as shortcuts to deriving the meaningful ones in the game.
Hilbert's program was so bold and promising that it even won over Brouwer's disciple, Arend Heyting, who saw it as a way to reconcile classical and intuitionistic mathematics. But Gödel detected a flaw in this program. His incompleteness theorem essentially said that no formal system was strong enough to guarantee that the game would not allow results that were false or meaningless. That is, since there are true theorems that can not be proved in the game, it is possible to add false axioms and still have a safe (consistent) but meaningless system of mathematics. Here is what Gödel said at a small meeting on Foundations at Konigsberg in September, 1930.
On the contrary it would be, for example, entirely possible that one could prove with the transfinite methods of classical mathematics a sentence of the form Exists x F(x) where F is a finite property of the natural numbers ... and on the other hand recognize through conceptual considerations that all numbers have the property not F; and what I want to indicate is that this remains possible even if one had verified the consistency of the formal system of classical mathematics. (Citation.)
Gödel had already realized that "one cannot claim with certainty of any formal system that all conceptual considerations are representable in it." The questions motivating Gödel's theorem are still being asked about physical theories. For example, E. O. Wilson in Consilience asks whether there might be an interpretation of mathematical physics which is completely different from the physical world as we know it.
Automath
The idea to use computers in carrying out a massive formalization of mathematics is well articulated in Wang. But the first sustained project to do this was N. G. deBruijn's Automath Project. The copious work done by the Automath project is now collected in a 1024-page 1994 North-Holland publication, Selected Papers on Automath. (Citation.) The style and scope of the work can be seen in this quote from the first publication about the project in the book.Technical Contributions
Our contributions can be understood by comparison to the pioneering and brilliant work of N. G. de Bruijn on Automath. It was this project along with Edinburgh LCF that directly inspired us, and in some ways we have not yet achieved the total breadth of the Automath conception, especially in regard to the structure of a "library" of formal on-line texts into a "tree of knowledge." But in some respects we have gone well beyond Automath, as we indicate.
First, the formal text we produce is directly readable as ordinary mathematics. Moreover, we can change the display of all the text with the trivial operation of changing the display form of an object. This powerful mechanism was introduced in PRL by Joe Bates and brought to the state-of-the-art by Stuart Allen and Richard Eaton.
Second, we can generate formal text from rigorous text at rates ten times faster than the Automath user.
Third, the expansion factor from rigorous text to Automath text was nearly 50 to 1 whereas for us it is more like 5 to 1. We have the tools to make the expansion close to 1 for completely rigorous proofs into formal proofs. We aim to create a situation where the normal display of formal argument is shorter than rigorous proof.
Fourth, we can incorporate proofs from other systems such as HOL. We can produce multiple logic arguments and keep track of the logical dependencies.
Fifth, we have tools to formally manipulate entire theories. So it is possible to generate a variant of a theory automatically as Chet Murthy showed by producing a constructive account of Higmann's Lemma from a classical one.
Sixth, our text is formal hypertext so that concepts are automatically linked. This makes our library into a semantic net. The naming convention for library objects is used to guide automatic search for content.
Seventh, our text can be automatically displayed on the Web.
Citations
- Davis, M., ed. The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems, and Computable Functions, Raven Press, 1965, New York.
- Davis, M. "The Prehistory and Early History of Automated Deduction," in Automation of Reasoning 1, edited by J. Siekmann and G. Wrightson, Springer-Verlag, NY, 1983, pages 1-28.
- DeBruijn, N. G. "The Mathematical Language Automath, its Usage, and Some of its Extensions," in Selected Papers on Automath, edited by R. P. Nederpelt, J. H. Geuvers, and R.C. de Vrijer, Vol. 133, Studies in Logic and The Foundations of Mathematics, 1994, pages 73-100. Reprinted from: Laudet, M., Lacombe, D. and Schuetzenberger, M., eds., Symposium on Automatic Deduction, pages 26-61, by courtesy of Springer-Verlag, Heidelberg.
- Frege, G. Grundgesetze der Arithmetik, begriffsschriftlich abgeleitet, Olms, 1962, Vol. 1, Hildesheim.
- Frege, G. "Begriffsschrift, A Formula Language, Modeled upon that for Arithmetic for Pure Thought," In From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, 1967, Cambridge, MA, pages 1-82.
- Godel, K. "On Intuitionistic Arithmetic and Number Theory," in The Undecidable, edited by M. Davis, Raven Press, 1965, pages 75-81.
- Murthy, C. "Extracting Constructive Content for Classical Proofs," PhD Thesis, Department of Computer Science, Cornell University, 1990, published as TR 89-1151.
- Murthy, C. "Classical Proofs as Programs: How, What, and Why" Constructivity in Computer Science, Lecture Notes in Computer Science 613, edited by J. P. Myers and M. J. O'Donnell, June, 1991, Springer-Verlag, pages 71-88.
- Nederpelt, R. P., J. H. Geuvers and R. C. De Vrijer, editors. Selected Papers in Automath, Elsevier, 1994, Vol. 133, Studies in Logic and the Foundations of Mathematics, Amsterdam.
- Russell, J. and Chetan Murthy. "A Direct Constructive Proof of Higman's Lemma," in Proceedings of the Fifth Symposium on Logic in Computer Science, IEEE, 1990, pages 257-269.
- Smorynski, C. Self-Reference and Modal Logic, Springer-Verlag, 1985.
- Wang, H. "Toward Mechanical Mathematics", IBM Journal of Research and Development, 1960, pages 2-22.