|
|
Mathematics
In Hilbert II a formal language is used which enables us to describe most domains of mathematics. It is a first order predicate calculus based on the text Elements of Mathematical Logic from P. S. Novikov. The logical axioms and basic rules originate from the book Principles of Mathematical Logic (Grundzüge der theoretischen Logik) (1928) by D. Hilbert and W. Ackermann.
Beside logical ones the only axioms in Hilbert II are those of axiomatic set theory. As usual for mathematics the axioms of all other theories could be expressed as simple predicate constant definitions. With common mathematical practice in mind, the set theory used here is not ZFC but Morse-Kelley (an impredicative Neumann-Bernays-Gödel extension). Our mathematical basis text is E. J. Lemmon's wonderful Introduction to Axiomatic Set Theory.
The prototype implements already a bigger part of the denoted predicate calculus, only predicate constants function variables and function constants are not supported.
Also only the basic rules and simple extensions are implemented by the prototype, so that the proofs are still very detailed and bulky.
An overview about the used logic in Hilbert II can be found in the script Elements of Mathematical Logic. There are all rules, axioms, definitions and propositions assembled. The propositions are not complete and currently proofs are missing, but the mathematical orientation becomes clear. A better part of it is described in the document Language and Rules of Predicate Calculus that describes the logical basis of the prototype.
See the following sections:
| propositional calculus |
Logical rules, axioms, definitions and propositional theorems of the prototype. |
| predicate calculus |
Predicate logic theorems of the prototype. |
| Axiomatic Set Theory |
Construction of set theory. This is a living document and is updated from time to time. Especially at the locations marked with "+++" additions or changes will be made. See also under planning. |
Literature
- D. Hilbert und W. Ackermann, Grundzüge der theoretischen Logik, Berlin: Springer, 1928.
- P. S. Novikov, Elements of Mathematical Logic, Edinburgh: Oliver and Boyd, 1964.
- A. N. Whitehead und B. Russell, Principia Mathematica, London: Cambridge University Press, 1910.
- E. J. Lemmon, Introduction to Axiomatic Set Theory, London: Routledge & Kegan Paul Ltd, 1968.
- J. Schmidt, Mengenlehre I, Mannheim: BI, 1966.
- J. D. Monk, Introduction to Set Theory, New York: McGraw-Hill, 1996.
- G. Takenti, W. M. Zaring, Introduction to Axiomatic Set Theory, New York: Springer, 1971.
|