Hilbert II

Das mathematische Wissen dieses Projekts wird in sogenannten QEDEQ-Modulen organisiert. Solch ein Modul kann mit einem einfachen Texteditor gelesen und bearbeitet werden. Es kann Referenzen auf andere QEDEQ-Module besitzen, die irgendwo im WWW liegen können.

Ein QEDEQ-Modul ist wie ein mathematisches Textbuch aufgebaut. Es hat Kapitel, die in Paragraphen unterteilt sind und jeweils ein Axiom, Abkürzung, Definition oder Proposition enthalten. Jeder Paragraph besitzt ein Label und kann damit an anderer Stelle referenziert werden. Wesentlicher formaler Bestandteil eines Paragraphen sind Formeln. Die Formeln sind in einem Prädikatenkalkül erster Stufe formuliert, auch die Beweise sind in dieser formalen Sprache gehalten. Ein Beweisüberprüfer kann dann die formale Korrektheit der Formeln und Beweise feststellen. So können verlinkte mathematische Textbücher erzeugt werden. Und mit den erweiterten Analysemöglichkeiten durch die formale Sprache können wir beispielsweise auch eine Abhängigkeitsanalyse einfach durchführen.

Neben des Basisregeln können auch weitere abgeleitete Regeln, sogenannte Metaregeln zum Einsatz kommen. Ein Beweis, der sie benutzt, kann jedoch automatisch in einen Beweis, der nur die Basisregeln verwendet, umgewandelt werden. Es werden auch weitere Spracherweiterungen, wie zum Beispiel Abkürzungen, eingeführt um kürzer schreiben und bequemer argumentieren zu können. Auch dort ist eine automatische Entfernung der Erweiterungen und eine Rücktransformation in das Orginalsystem möglich.
Uns ist bewusst, dass dies Umwandlung nicht immer tatsächlich durchgeführt werden kann. Beispielsweise ist es nicht möglich. die natürliche Zahl 1000000000000000, vollständig in der Mengennotation aufzuschreiben: {{}, {{}}, {{}, {{}}}, {{}, {{}}, {{}, {{}}}}, ...}.

Mathematik wird nicht über formale Sprachen vermittelt. Deshalb sind die Beschreibungstexte, welche in der mathematischen "Umgangssprache LaTeX" verfasst werden, von großer Bedeutung. Diese Texte transportieren letztlich den mathematischen Gehalt der formal korrekten Sätze. In den Modulen von Hilbert II sind diese Texte integraler Bestandteil. Es könnnen auch für verschiedene Detaillierungssstufen Texte und Beweise angegeben werden. Die ersten Stufen können sollten dann nicht formale Beweise sondern übliche mathematische Texte sein, wie z. B. "trivial", "folgt direkt aus der Definition" oder etwas ausgearbeiteter sein. Die detailliertesten Stufen bestehen dann aus formal korrekten Beweisen. Es können auch verschiedene Beweise angegeben werden: beispielsweise ein eleganter und kurzer Beweis mit Fundierungsaxiom und ein längerer, umständlicher ohne Fundierungsaxiom.

Aus den Modulen können verlinkte LaTeX-, HTML- oder PDF-Dokumente generiert werden, die dann im wesentlichen wie ein normales mathematisches Dokument aussehen. Vor der Erzeugung muss der gewünschte Detaillierungsgrad angegeben werden.

Die aktuell in Entwicklung befindliche Spezifikation des QEDEQ-Formats liegt in Form einer XML-Schemadefinition vor und wird hier dokumentiert.

In Logical Language werden mehr Details über die formale Sprache für Formeln und Terme erklärt. Hier sind auch die elementaren formalen Beweismethoden aufgelistet.

Siehe Anfangsgründe der mathematischen Logik für den logischen Hintergrund für dieses Projekt..

Beim Prototypen kommt noch ein proprietäres Format zum Einsatz.