Daniel Kirchner verteidigt seine Doktorarbeit in Mathematik an der FU Berlin mit summa cum laude
Titel: Computer-verifizierte Grundlagen der Metaphysik und eine Ontologie der natürlichen Zahlen in Isabelle/HOL
Zusammenfassung: Wir nutzen und erweitern die Methode der flachen (shallow) semantischen Einbettungen (SSEs) in der klassischen Logik höherer Ordnung (HOL), um eine maßgeschneiderte Theorembeweisumgebung für die Theorie abstrakter Objekte (AOT) auf der Basis von Isabelle/HOL zu konstruieren. SSEs sind ein Mittel für universelle logische Schlussfolgerungen durch die Übersetzung einer Ziellogik in HOL unter Verwendung einer Darstellung ihrer Semantik. AOT ist eine grundlegende metaphysische Theorie, die von Edward Zalta entwickelt wurde und die Objekte, die von den Wissenschaften vorausgesetzt werden, als abstrakte Objekte erklärt, die Eigenschaftsmuster verdinglichen. Die AOT hat insbesondere den Anspruch, eine philosphisch fundierte Grundlage für die Konstruktion und Analyse der Objekte der Mathematik zu liefern. Wir können diese Behauptung untermauern, indem wir Uri Nodelmans und Edward Zaltas Rekonstruktion von Freges Theorem überprüfen: Wir können bestätigen, dass die Dedekind-Peano-Postulate für die natürlichen Zahlen in der AOT mit Freges Methode konsistent ableitbar sind. Darüber hinaus können wir Verallgemeinerungen und Varianten der Konstruktion vorschlagen und diskutieren und so theoretische Einsichten in die Konstruktion liefern und zu ihrer philosophischen Rechtfertigung beitragen. Dabei können wir zeigen, dass unsere Methode einen nahezu transparenten Austausch von Ergebnissen zwischen der traditionellen, auf Papier basierenden Argumentation und der computergestützten Implementierung ermöglicht, die ihrerseits die für Isabelle/HOL verfügbaren Automatisierungsmechanismen beibehalten kann.
Während unserer Arbeit konnten wir wesentlich zur Entwicklung unserer Zieltheorie selbst beitragen und gleichzeitig die technische Herausforderung lösen, eine SSE zur Implementierung einer Theorie zu verwenden, die auf logischen Grundlagen basiert, die sich deutlich von der Metalogik HOL unterscheiden. Im Allgemeinen zeigen unsere Ergebnisse die Fruchtbarkeit der Praxis der Computational Metaphysics, d.h. der Anwendung von Berechnungsmethoden auf metaphysische Fragen und Theorien.