Hilbert II - 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.

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. Der grösste Anteil von Snork ist ebenfalls umgesetzt. Auch die Basis von Little My ist bereits fertig. Wir haben gerade begonnen Beweise aufzuschreiben, damit ist auch Fillyjonk gestartet. Nach der letzten Phase werden wir mit einem Skript über Zahlentherie erneut alle Phasen durchlaufen.