we moved to http://www.qedeq.org
In the famous "Principia Mathematica" A.N. Whitehead and B. Russell (London 1910, Cambridge University Press) tried to present mathematics in a fully formalized form. In D. Hilbert and W. Ackermann s "Grundzuege der theoretischen Logik" (Berlin 1928, Springer) an axiomatic system for predicate calculus was given, based on the "Principia Mathematica" with some improvements by P. Bernays. This logical system (a "first order predicate calculus" language) is the starting point for this project. (Another book to look into: Development of Mathematical Logic, R.L. Goodstein, 1971 London, Logos Press)
Goal of Principia Mathematica II (the title is a little bit arrogant.. ;-) is the creation of a system that enables a working mathematician to put theorems and proofs (in a formal language) into it. These proofs are automatically verified by a proof checker. Because this system is not centrally administrated and enables references to any location in the internet, a world wide mathematical knowledge base could be build. Any proof of sentence in this "mathematical web" could be drilled down to the very elementary rules and axioms. To make it more than a huge number of correct formulas, it should also contain information in "common mathematical language". Think of an incredible number of mathematical textbooks with hyperlinks and each of its proofs could be verified by pmii.
The formal language used here is a first order predicate calculus. But it differs slightly from the standard one. It is not allowed to quantify over a variable a second time. This is common mathematical practice anyway. Also it doesn't have all tautologies as an axiom schema: each tautology could be derived by the axioms and the rules. Also the extensions of the formal language should be oriented to the common mathematical practice. (Look at the description for the html modules: rules.)
Please take a look at the HTML modules: prophilbert1, prophilbert2 and predtheo1
To make the formal language practical, the original set of operators, abbreviations and rules will be expanded. These language enhancements could be automatically eliminated, so that each sentence and proof could be transferred into the pure old formal system. We know that there are certain limitations, so for complicated cases it would be impossible to actually do that transformation. (E.g. to write down the natural number that could be expressed as 9^9^9 in the set notation {{}, {{}}, {{}, {{}}}, {{}, {{}}, {{}, {{}}}}, ..)
Look at: prophilbert1, prophilbert2 for the result of an automatic transformation. (The loading time may be long: the greatest file has nearly two mega bytes of size.)
There results of converting a Qedeq module into LaTeX and PDF could be visited. Look at: prophilbert1, propaxiom, predtheo2 for the pdf representations. (You could also browse the directory: 0_00_51.)
There is a lot to do. The first programming goals are reached: the first order predicate calculus has a reference implementation. The proof verifier is working. After a validating and re factoring phase, the first mathematical work is done: proving the first elementary logical propositions. There are also some additional rules (e.g. the Hypothetical Syllogism). But there is a need for further rules and operators (for convenience only: each new rule or operator could be transformed automatically into the basic language). For example the logical "AND" with more than two arguments, usage of the deduction theorem, indirect proofs etc..
Then the language should be expanded to allow predicate constants and term functions. That leads to "DEFINITION"s that define predicate constants.
With this extension an elementary set theory (NBG) could be established. Look at: set for a first example of set theory (in German).
Elementary number theory would be next.
In future releases every creator of a module could define predicates (perhaps even new abbreviation operators) by herself - and determine the visual representation of them.
If you have any comments or questions please tell us!
This article must be full of errors and mistakes (English language, mathematical, historical, or whatever). You could correct them!
Could you write further modules? Either in an informal language or in the current syntax.
If you want to participate in this project, please make contact!
The whole project stands under the GPL. The reference implementation is programmed in Java. The mathematical knowledge of this project is organized in pieces that are called a modules. Such a module is a file, that could be easily read by any text editor. It could have references to other modules which are somewhere in the world wide web. It looks like a chapter of a textbook. It has paragraphs that contain an abbreviation, axiom, definition or proposition. Each paragraph is labeled and could be referenced by that label. The current programs could check a module ".qedeq" file and transform it into a clickable HTML file.
The module verification could be done by the program "com.meyling.principa.CheckModule" It uses the class "ModuleContext" to load a module file by its address. This address could be any URL. If the module wasn't loaded yet, the file buffer is searched for it. If the file buffer doesn't know about it, the URL is copied into a file buffer. Now the class "ModuleCreator" parses the file contents and will call the module constructor (with the "TextInput" parameter). If no "ArgumentException" occurs the module is ok and added to the Module HashMap.
Main data type is an Argument. This is a kind of list (like in LISP). There are two atomic arguments: Counter and Text. All other arguments are lists made of Counters and Text, these (Abstract)ArgumentLists (the classes) are called operators.
There are different packages. The important one for outside access is "com.meyling.principia.module". If you start the test program "com.meyling.principia.Main" it will try to copy some of the modules from this homepage into a new local directory "com/meyling/principia/buffer", then it tries to load them. It tries to compress some of them, to reduce the rule version of others and at last it will construct HTML files at the same location.
| Module | definition of a module |
| Proof | informal definition of a mathematical proof |
| Change history | history of program development |
| Module with axioms of propositional calculus | this is an example of a module |
| Module with proofs | this is an example of a module |
| Lib | java lib (jar), version 0.00.51 |
| javadoc | program documentation for version 0.00.51 |
| project plan | not very elaborated |
| rules | list of rule versions |
| full release 0.00.51 | includes source, java doc, modules, other documentation and a jar |
| development case log | project discussion/repository/log |
| links | look at these web pages |
Please take a look at the HTML modules: propaxiom, prophilbert1, prophilbert2 and predtheo1
Also see the following PDF modules: prophilbert1, propaxiom, predtheo2