Hilbert II 
Formal Correct Mathematical Knowledge 

Overview  quick start and feature summary 
Project Goals  about this project 
Mathematics  mathematical contents 
Installing, Starting and Working  preconditions and other stuff about starting and working with the application 
Release Contents  detailed directory description of this release 
Further Installation  some more or less optional adjustments 
Licenses  these licenses apply 
Future Development  short range project plan 
This is an unstable development release of Hilbert II. In the tradition of Hilbert's program the project creates a formal correct (checkable by a proof verifier) but readable (like an ordinary LaTeX textbook) mathematical knowledge base which is freely accessible within the internet. The mathematical axioms, definitions and propositions are combined to so called QEDEQ modules. Such a module could be seen as a mathematical textbook which includes formal correct proofs. The project started with logic and set theory.
This release contains a program suite that can produce LaTeX and UTF8 files out of QEDEQ XML files. The QEDEQ files can be checked for syntactic correctness. Simple formal proofs can also be validated. For set theory we provide some small finite models. Checks for model validity are also available. The following files were mostly generated out of QEDEQ modules and contain more information. Some files are also available in German and not in our terribly, awfully bad English...
qedeq_set_theory_v1_en.pdf 
Script with the beginning of axiomatic set theory. Currently all given proofs are non formal. 
qedeq_logic_v1_en.pdf 
Logical background of this project. Contains main logical axioms, definitions, rules and propositions. 
qedeq_logic_language_en.pdf 
Explains more formal details. 
qedeq_formal_logic_v1_en.pdf 
Here are all propositional calculus axioms and propositions with formal proofs. The corresponding QEDEQ module was successfully checked with the application proof checker. Will be expanded. 
changes.txt 
Change history to know the difference to the previous release. 
qedeq_basic_concept_en.pdf 
QEDEQ basic concept for more project details. 
sample 
Directory with sample QEDEQ modules. These can be automatically be loaded within the application by selecting File / Load all from QEDEQ.org. 
A convenient way to start this application is via Java Web Start. Just click on: START. There should be a splash screen for Java Web Start, asking you to trust the signature. Although it will be not recommended you must trust the signature of Hilbert II to start the application. If you already started an older program version via Web Start you should remove the files in the config
directory. In this case you must also empty the local buffer directory by selecting File / Clear Buffer in the menu.
The goal of Hilbert II is decentralized access to verified and readable mathematical knowledge. The knowledge base contains mathematical texts in different languages and detail levels, axioms, definitions, propositions and their proofs. Beside common non formal proofs the system includes formal proofs that were verified by a proof checker.
The mathematical axioms, definitions and propositions are combined to socalled QEDEQ modules. Such a module could be seen as a mathematical textbook. At least all proposition formulas are written in a formal language and each proposition can also have a formal correct proof. The proposition is verified iff it has a formal proof and all required propositions are also verified.
Hilbert II will provide a program suite that enables a mathematician to put data into that knowledge base and retrieve various documents and analyze results out of the system. This includes the generation of LaTeX files that look like a common mathematical textbook and the answer to questions like "assumes this theorem the axiom of choice?" for verified propositions. As it's name already suggests, this project is in the tradition of Hilbert's program.
Because this system is not centrally administered and references to any location in the internet are possible, a world wide mathematical knowledge base could be build. Any proof of a theorem in this "mathematical web" could be drilled down to the very elementary rules and axioms. Think of an incredible number of mathematical textbooks with hyperlinks and each of its proofs could be verified by Hilbert II. For each theorem the dependency of other theorems, definitions and axioms could be easily derived.
See also under QEDEQ basic concept for more project details. This document was generated out of the following XML file: qedeq_basic_concept.xml.
The mathematical knowledge of this project is organized in so called QEDEQ modules. Such a module can be read and edited with a simple text editor. It could contain references to other QEDEQ modules which lay anywhere in the world wide web. A QEDEQ module is structured like a mathematical text book. It contains chapters which are composed of paragraphs each with an axiom, abbreviation, definition or proposition. Every paragraph has a label and could be referenced by that label. Essential formal element of a paragraph are formulas. The formulas are written in a first order predicate calculus, also the proofs are in this language. Therefore a proof verifier can check the formulas and their proofs for formal correctness. We can create linked mathematical text books. And with the extended analytic possibilities of the formal language we can easily do for example a dependency analysis.
In addition to the basic rules also other derived rules, so called meta rules, could be used. A proof that uses meta rules could be automatically transformed into a proof which only uses the basis rules. Some other language extensions, for example defined predicate constants, are established for shorter writing and convenient argumentation. These extensions can also be automatically removed and transformed into the original system.
We are aware of the fact that this transformation is not in each case practically realizable. For example it is not possible to write down the natural number 1000000000000000 completely in set notation: {{}, {{}}, {{}, {{}}}, {{}, {{}}, {{}, {{}}}}, ...}.
The QEDEQ XML files have a formal structure that is defined here or here. The logical language is described in qedeq_logic_language_en.pdf (in development).
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. They are presented in qedeq_logic_v1.pdf. The propositions are not complete and proofs are missing, but the mathematical orientation becomes clear.
Recently we changed the logical structure along the lines of Vilnis Detlovs and Karlis Podnieks Introduction to Mathematical Logic to have a fully formalized presentation. Please take a look at qedeq_formal_logic_v1.pdf to see the current state. This document contains all axioms and rules for predicate calculus. It also has some propositions with formal proofs (checkable by our proof checker).
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 MorseKelley (an impredicative NeumannBernaysGödel extension). Our mathematical basis text is E. J. Lemmon's wonderful Introduction to Axiomatic Set Theory. Along these lines, we wrote a script about axiomatic set theory. This script is also available in German. It contains already some non formal proofs. In the XML source all formulas of axioms and propositions are already written in the formal language. The main goal is the completion through the addition of formal proofs. New proof methods are necessary to accomplish this.
Precondition is a Java Runtime Environment, at least version 1.4. From Download Java 2 Platform you could get the Java Runtime Environment J2SE v 1.4.2 JRE. To work with the created LaTeX documents you need an appropriate LaTeX environment.
You can start the application by the script qedeq_se.bat
or qedeq_se.sh
in the main directory. If you connect to the internet via a proxy server you should start the preferences dialog via the menu Tools / Preferences. There you can enter the appropriate proxy parameters.
To start the application more manually call via java:
org.qedeq.gui.se.main.QedeqMainFrame
The classpath must include the files in the lib directory..
You also can start the applicaton via Java Web Start. Just click on: START.
Sample XML files can be found in the sample directory. The main structure of an QEDEQ XML file looks like the LaTeX book format. There is a special kind of subsections called node
that contain an axiom, definition or proposition. Each node is labeled and could be referenced by that label. Here is the XSD and here it's documentation. The root element is called QEDEQ.
So what can we do? You can load existing QEDEQ modules from the local file system or via http. Files loaded from web are stored in a local buffer directory. Even after successfully buffering a QEDEQ module loading it might fail due to XML validation or elementary application errors. In such a case the tree icon changes its color to red. A successfully loaded module looks dark grey. To get some modules we just select File / Load all from QEDEQ.org. Depending from your internet connection you will see new modules appearing in the tree at the left side. They will successive change their color from baby pink into dark grey. Some modules even get a little bit of red color. The log panel lists all module states changes.
By selecting a red module at the three the state panel will show more details about the selected module. If you select the error module qedeq_error_sample_00 and activate the pane labeled Errors you will see an entry like cvccomplextype.2.4.a: Invalid content was found starting with element 'XOR'. One of '{"":FORMULATYPE}' is expected. This list entry describes am XML parsing error that occurs in line 36. If you click on this entry the XML source will open at the error location in the QEDEQ panel. The error location is marked and we see the usage of the unknown element 'XOR'.
If you look at qedeq_error_sample_12 you can see an application error. This module has two Nodes that have the same id. This is a violation of the uniqueness of nodes and leads to an loading error. By the way, the state of the module is loading into memory failed the other red modules have the state loading from local buffer failed.
Now we have various plugins to work on a loaded module. Firstly you can select a module and choose Show module as UTF8 text in the context menu. This plugin transforms a QEDEQ module into an UTF8 text and displays the result in an extra window. We try that on module qedeq_sample3 and see same axioms, propositions and their proofs. The layout and format of the displayed text is not satisfying but you get a visual impression of the QEDEQ module.
Now we test the generation of UTF8 text files by selecting the appropriate context menu entry on qedeq_sample2. We notice that three modules change their color to green. First qedeq_logic_v1 second qedeq_set_theory_v1 and last qedeq_sample2. The green color is a signal for the state well formed. This means all imported modules are well formed too and that all formulas passed the syntax checker. This check was initiated by the UTF8 text plugin because the plugin has to know the LaTeX representation of every imported operator. If loading an imported module fails then the plugin tries to use backup definitions for unknown operators. We see the location of the generated UTF8 text files in the log pane and can open such a file within a web browser. (Perhaps you must change the encoding to UTF8.)
If we generate UTF8 files for qedeq_sample1 or qedeq_logic_language the modules turns yellow and we get some warnings because the LaTeX texts contain not supported constructs. To remove plugin errors and warnings you can select Remove Plugin Results in the context menu for the appropiate module.
Now we come to the important features. We take qedeq_sample3 and start Check WellFormdness. Firstly all imported modules are checked for being well formed. Then the rest of the module is sequentially analyzed. Formulas are checked for beeing well formed and that their operators are all defined. There should be no problems with qedeq_sample3 and the module status color should change to green. Now we want to know if the module is fully correct  that is all propostions have correct formal proofs. So we start the Check Proof plugin and the state changes to well formed; Check Proofs successful. All other QEDEQ modules (beside qedeq_formal_logic_v1) with propositions will get errors. We test that with qedeq_sample1. We see that qedeq_logic_v1 and qedeq_sample1 both change their colors to red. qedeq_logic_v1 has still no formal proofs and neither has qedeq_sample1.
To get an impression of the logical basis for this project we check the proofs of qedeq_formal_logic_v1. It contains the logical axioms and rules of inference for our predicate calculus and some basic propositions with formal proofs. It even uses the derived rule conditional proof. Just look at the UTF8 text to get an impression of the logical roots. For further information you should visit Introduction to Mathematical Logic by V. Detlovs and K. Podnieks.
We now try proof checking with qedeq_sample4 and get also errors for missing formal proofs. But now we try the new (experimental!) plugin Find Proofs. If you start it directly it will search for much to long. You have to restrict the substitution usage. Just go to the plugin preferences dialog and the Find Proofs tab. There you should change the weight values for the operators from implication to equivalence from 1 to 0. Now after quite a while (ten minutes on an an Intel Celeron with 2 GHz) the plugin can find the missing proofs. It works only for propositional proofs and uses bruteforce. If we execute Check Proof now the color changes to green. The plugin changes only the buffered file so you loose these findings after executing Clear Buffer. By the way: the blue color signals that all neccessary imports were done.
During a plugin execution (proof finding is a good example) one could check the execution status by selecting the menu entry Plugins / Threads. The new window shows all plugin processes that were executed. If you select a running process you can see the current element the plugin works on. The proof finder plugin shows you even the last generated proof line.
We still provide no further tools to create new QEDEQ modules. You still have to copy an existing QEDEQ file and modify its content. A file modification that takes place after the module is already loaded is not recognized. You must Remove the module and then Load local file. If you modified an already buffered file you must do even more. The application takes the local buffered file when reloading such a file. The buffer location can be found under Tools / Preferences. You have to clear the buffer via File / Clear Buffer.
For propositional calculus we included a small tool that helped us to integrate new formal proofs into our system. You can start it via the menu entry Tools / Proof Text to QEDEQ. You can add a proof in text form at the left upper window. Just click Transform / Proof Text to QEDEQ in the menu when you are ready. At the bottom you see the generated XML snippet for the proposition including the formal proof. At the upper right window you see the generated UTF8 text. Just compare it to the original at the left side if you want to be shure everthing got parsed correctly. There is still no syntax description for the format. You have to look at the sample and you might want to change the file "config/proofTextMathOperators.xml" according to your needs.
Modules without errors are reloaded automatically when the application is restarted. This behavior can be changed in the Tools / Preferences menu.
This release includes the source code and the JUnit test classes. The code coverage results of these tests where produced by clover .
Directory  Description 

bin 
executable files, currently containing script for finding simple propositional proofs 
config 
configuration files 
log4j.xml 
log4j property file, change "error" to "debug" to get a little more log output; change it to "fatal" to reduce the logging events. To enable logging you also have to mark "Tools / Preferences / Enable trace output generation" 
latexMathOperators.xml 
LaTeX operator information, used from the parser to transform LaTeX formulas into QEDEQ XML; can be manually edited 
textMathOperators.xml 
text operator information, used from the parser to transform text formulas into QEDEQ XML; can be manually edited 
doc 
documentation 
project 
project specific 
qedeq_basic_concept_en.pdf 
basic concept of Hilbert II 
qedeq_logic_language_en.pdf 
explanation of the logical language of Hilbert II (in development) 
projektbeschreibung.pdf 
project description (in German, a little bit outdated) 
changes.txt 
change history to previous versions 
math 
mathematical texts 
qedeq_set_theory_v1_en.pdf 
beginning of axiomatic set theory, this is already a QEDEQ module 
axiomatic_set_theory.txt 
beginning of set theory as non formal (ASCII text) file, it shows the intention of this project (parts in German) 
qedeq_logic_v1_en.pdf 
logical background 
qedeq_formal_logic_v1_en.pdf 
logical derivations in formal correct form 
lib 
libraries for running the application 
commonscodec1.3.jar 
apache commons codec component 
commonshttpclient3.1.jar 
apache commons httpclient component 
commonsio1.4.jar 
apache commons io component 
commonslang2.4.jar 
apache commons lang component 
commonslogging1.1.1.jar 
apache commons logging component 
forms1.1.0.jar 
JGoodies Forms GUI support 
jh2.0.5.jar 
Java Help help file creation and display 
log4j1.2.14.jar 
log4j logging implementation 
looks2.1.4.jar 
JGoodies Looks GUI support 
qedeq_gui_se0.04.04.jar 
binary GUI release of Hilbert II 
qedeq_kernel0.04.04.jar 
binary kernel release of Hilbert II 
xercesImpl.jar 
apache XML parser xerces 
xmlapis.jar 
XML standard API definition 
license 
various license files 
license/apache_license.txt 
apache software license 
license/fdl.html 
GNU Free Documentation License 
license/gpl.html 
GNU General Public License 
license/forms_license.txt 
BSD license for JGoodies Forms 
license/looks_license.txt 
BSD license for JGoodies Looks 
license/oil_licenses_full.txt 
Licenses for the Open Icon Library 
license/tango_license.txt 
Creative Commons Attribution ShareAlike license for the tango theme 
log 
log files are written herein 
sample 
sample XML files 
qedeq_basic_concept.xml 
qedeq basic concept as QEDEQ XML document 
qedeq_logic_v1.xml 
logical foundation of project 
qedeq_formal_logic_v1.xml 
axioms and rules of predicate calculus and propositions with formal proofs (will be expanded) 
qedeq_set_theory_v1.xml 
axiomatic set theory script 
qedeq_sample1.xml 
mathematical sample module 
qedeq_sample2.xml 
We just use the two main QEDEQ modules and show a simple proposition. 
qedeq_sample3.xml 
this module contains simple proofs that are formally correct which can b checked by the application 
qedeq_sample4.xml 
here are some propositional calculus axioms and propositions without formal proofs  but these proofs can be automatically generated by the application 
qedeq_error_sample_00.xml 
usage of an unknown logical operator 
qedeq_error_sample_01.xml 
too many arguments for logical implication operator 
qedeq_error_sample_02.xml 
second quantification over same variable 
qedeq_error_sample_03.xml 
subject variable occurs free and bound 
qedeq_error_sample_04.xml 
subject variable occurs bound and free 
qedeq_error_sample_05.xml 
import of a QEDEQ module that has errors 
qedeq_error_sample_12.xml 
semantic error in QEDEQ file, a node id is used twice 
qedeq_error_sample_13.xml 
syntax error in XML file, violates XML syntax 
qedeq_error_sample_14.xml 
syntax error in XML file, violates XSD 
qedeq_error_sample_15.xml 
logic error in XML file, quantify over already bound subject variable 
qedeq_error_sample_16.xml 
logic error in XML file, "unknown" is an unknown predicate 
qedeq_error_sample_17.xml 
logic error in XML file, a subject variable occurs free and bound 
qedeq_error_sample_18.xml 
semantic error in XML file, duplicate language entries 
src 
source code of Hilbert II 
eclipse 
all needed eclipse projects 
maven 
project structure in maven format 
reports 
various project reports 
qedeq_kernel 
QEDEQ kernel 
qedeq_kernel/checkstyle 
checkstyle report 
qedeq_kernel/clover 
code coverage report 
qedeq_kernel/findbugs/ 
findbugs report 
qedeq_kernel/jdepend/ 
jdepend report 
qedeq_kernel/junit 
JUnit report 
qedeq_kernel/junitpest 
JUnit pest report 
qedeq_gui_se 
QEDEQ GUI 
xml 
XML schemata and their documentation 
qedeq.xsd 
XSD for QEDEQ format 
qedeq.html 
documentation of QEDEQ XSD 
parser.xsd 
XSD for operator definition for text parser 
parser.html 
documentation of parser XSD 
qedeq 

index.html 
another documentation of QEDEQ XSD 
Beside the steps mentioned in Overview you should install a correction for the buggy LaTeX package longtable. One possibility is this patch from Chungchieh Shan. It was used to produce the provided PDF files.
The QEDEQ XML files stand under the GNU Free Documentation License (GFDL), the software of this project under the GNU General Public License (GPL).
For XML parsing the apache parser is used which falls under the apache license. This license applies also to the class com.sun.syndication.io.XmlReader
which was taken on 20080306 from project Rome (see https://rome.dev.java.net/../XmlReader.java
). The GUI uses the tango theme that is under the Creative Commons Attribution ShareAlike license.
There are also some icons of the Open Icon Library included. These icons stand under different licenses.
Hilbert II uses JGoodies Looks and JGoodies Forms, distributed by JGoodies under the terms of the BSD License see looks license and forms license for details. Also included are three additional classes (SimpleInternalFrame, Factory and UIFSplitPane) by Karsten Lentzsch, which are distributed under these terms.
We also used some great work of Santhosh Kumar. This code is distributed under the GNU Lesser General Public License.
For the current source code you could browse the subversion tree.
Here are descriptions of the next minor releases. Subversions are not listed. All these releases are characterised as "unstable" and are only of interest for developers.
0.01 brigand 
First XSD releases. XML could be parsed and value objects are created. Very simple generation of LaTeX files is possible. There are two QEDEQ modules: the project handbook and a mathematical example. Beside the XSD verification no checking is done. The LaTeX generation works directly on the value objects. 
0.02 moster 
Some elements of the BO (business object) layer exist. The script of axiomatic set theory includes at least most of the axioms. First attempts of a small LaTeX to QEDEQ XML converter. 
0.03 mongaga 
Formal checks for single formulas could be done ("is this formula well formed"). 
0.04 gaffsie 
QEDEQ modules and the referenced modules are loaded from the web. The formula checking incorporates also all required QEDEQ modules and handles external definitions. External predicate and function constants are resolved. 
0.05 toffle 
Simple formal proofs can be written down in QEDEQ syntax. 
0.06 misabel 
Simple formal proofs can be checked. 
0.07 joxter 
All needed formal proof methods for Axiomatic Set Theory can be written down in QEDEQ syntax. 
0.08 hodgkins 
All proof methods that can be expressed within the QEDEQ syntax can be checked. 