www.qedeq.org

 Hilbert II

English   Deutsch
Hilbert II bei SourceForge
Einführung
News
Mathematik
QEDEQ
Planung
Download
Glossar
Entwicklung
Prototyp
Links
Kontakt
Sitemap
Planung

Einen Überblick über die Planung bietet auch das Grobkonzept: Projektbeschreibung. Eine neuere Version in Englisch liegt unter basic concept.

Die Planung für dieses Projekt kann am Besten anhand des mathematischen Inhalts beschrieben werden. Mit dem Blick auf die mathematische Praxis ist die in Hilbert II verwendete Mengenlehre nicht ZFC, sondern MK (eine imprädikative Erweiterung von NBG). Unser mathematische Ausgangspunkt ist E. J. Lemmons großartiger Text Introduction to Axiomatic Set Theory.

Wir haben begonnen ein Skript über axiomatische Mengenlehre zu schreiben. Dieses Skript ist in einem XML-Format gehalten, welches LaTeX-Texte und Formeln enthalten kann. Das Dokumentformat wird QEDEQ genannt. Wärend der Vervollständigung des Mengenlehreskripts wird das QEDEQ-Format angepaßt und erweitert um die formal korrekten Schreibweisen und Beweise aufnehmen zu können. Der Parser zum Lesen solcher QEDEQ-Dokumente und Erzeugen eines entsprechenden Java-Objekts wird gleichzeitig mitentwickelt. Weiterhin sollte die Erzeugung von LaTeX-Dateien in jeder Phase immer möglich sein. Für unserer aktuelles Skript siehe: Axiomatische Mengenlehre.

Wir haben die folgenden Ziele identifiziert.

1.
 Emma
Syntax für elementare Mengenlehre Die formale Syntax ist so reichhaltig, dass die notwendigen Schreibweisen und Formeln der elementaren Mengenlehre ausgedrückt werden können.
2.
 Mymble
Formaler Inhalt elementarer Mengenlehre Wir haben ein Mengenlehreskript, welches alle Axiome, Definitionen und Propositionen in formaler Form besitzt. Daher sind auch alle Propositionen als Formeln geschrieben.
3.
 Fillyjonk
Elementare Mengenlehre informell komplett Unser Mengenlehreskript ist fertig. Jeder Satz besitzt einen informellen Beweis wie sonst auch. Wir haben ein einfaches LaTeX-Dokument, das wie jedes andere mathematische Textbuch über axiomatische Mengenlehre aussieht. Idealerweise liegen die mathematischen Beschreibungstexte in verschiedenen Detaillierungsstufen und in den Sprachen English und Deutsch vor.
4.
 Snork
Alle Formeln sind überprüfbar Es gibt einen Kernel, der QEDEQ-Module auf syntaktische Fehler hin überprüfen kann. Beispielsweise sollte er feststellen können, dass eine Formel nicht korrekt gebildet ist, weil über dieselbe Subjektvariable zweimal quantifiziert wurde. Der Kernel kann noch keine Beweise kontrollieren (d. h. er kann nicht entscheiden, ob eine Formel logisch aus anderen folgt).
5.
 The Groke
Elementare Mengenlehre komplett formalisiert Wir haben nun auch formale Beweise in dem Skript über elementare Mengenlehre und können sie auch überprüfen.
6.
 Little My
Logik dokumentiert Die zugrundeliegende Logik ist in dem Skript Anfangsgründe der mathematischen Logik umfänglich dokumentiert.

Aktuell haben wir Emma fast vollständig erfüllt und mehr als die Hälfte von Mymble fertig. Wir haben Snork umgesetzt und müssen den Kernel erweitern, wenn neue Beweismethoden hinzukommen. Auch die Basis von Little My ist bereits fertig. Wir haben einige Beweise fertig, damit ist auch Fillyjonk in Arbeit.
Sogar The Gorke hat begonnen - die ersten formalen Beweise liegen in qedeq_sample3.xml vor und können von unser Anwendung auf Korrektheit geprüft werden. Mehr noch: es gibt bereits ein Skript mit den Axiomen und Ableitungsregeln der Predikatenlogik erste Stufe, welches die Anfangspropositionen der Aussagenlogik inklusive formaler Beweise enthält: qedeq_formal_logic_v1.

Nach der letzten Phase werden wir mit einem Skript über Zahlentherie erneut alle Phasen durchlaufen.

Bei Interesse an einer Projektteilnahme bitte einfach Kontakt aufnehmen.


update 2014-01-20 09:20:48+0100