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.