Hilbert II 



Mathematics
LogicIn 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. 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. Meanwhile we have a script with the axioms and inference rule of firstorder predicate calculus which contains the beginning propositions of propositional calculus inclusive formal proofs: see qedeq_formal_logic_v1. Set TheoryBeside 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 MorseKelley (an impredicative NeumannBernaysGödel extension). Our mathematical basis text is E. J. Lemmon's wonderful Introduction to Axiomatic Set Theory. In Axiomatic Set Theory we construct systematically our 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
