Computational Metaphysics

Time

April 18 - July 23, 2016, first lecture on tuesday, April 19

Dates

Lectures on tuesday (16-18), irregular additional lecture dates on thursday (16-18), tutorial sessions on wednesday (14-16)

Rooms (1)

Lectures: At Takustr. 9 ("Institut für Informatik"), room SR006 (seminar room, ground level -- also called T9/SR006).
Please look at the lecture schedule below for the exact rooms on each day!

Rooms (2)

Tutorials: At Takustr. 9 ("Institut für Informatik"), rooms K38 and K48 (basement)

Target audience

Advanced students of philosophy (within the 'Interdisziplinären Studienbereich'), computer science (module 'Spezielle Aspekte der praktischen Informatik' and 'Spezielle Aspekte der theoretischen Informatik'), and mathematics (module 'Ausgewählte Forschungsthemen')

Entry at course catalouge

VV Entry

Mailing list

CompMeta@lists.fu-berlin.de (Please subscribe to the mailing list: Important announcements will be published there.)

The module is designed for approx. 30 students.

12.07.16: Due to spontaneous construction work at SR006 we have to move our invited lecture on July 12th to the lecture hall.

21.06.16: The group work topic proposals have been added to the KVV system. Please prepare for the tutorial session on Wednesday, June 22nd, since we are assigned group work topics during the session. Also, the examination and group work guidelines are available at the KVV system.

15.06.16: The 1st International Grand Boolos Award has been awarded to the proud winners during the tutorial sessions! Congratulations!

15.06.16: The last assignment sheet in online. See assignments section.

26.04.16: The today's lecture and the lecture on thursday, April 28th, will take place at the great lecture hall (T9/HS großer Hörsaal).

21.04.16: The today's lecture will take place at the great lecture hall (T9/HS großer Hörsaal).

22.03.16: Due to room booking conflics, the lecture will now take place at the institute of computer science (Takustr. 9),mainly at seminar room SR006, please look at the detailed lecture schedule (below) for per-lecture room information.

15.02.16: A lot of literature resources have been added to this web site.

English

Formal logic (and formal reasoning) constitutes an substantial role in philosophy, mathematics and computer science. Topics such as basic reasoning in propositional and (first-order) predicate logic are often dealt with in early lecture of the aforementioned study programs. Unfortunately, other core topics are often omitted. This lecture addresses different advanced logic systems that are employed within modern studies in (theoretical) philosophy, mathematics and computer science. In conjunction therewith, a practical introduction to computer-assisted reasoning is given and their application to contemporary problems is demonstrated.

In the first part of the lecture we will retrace different variants of the Ontological Argument using computer deduction systems. Subsequently, we investigate the theory of abstract objects (by E.N. Zalta) as a logical foundation of metaphysics as well as means of representation in a computer system. Finally we discuss the interdisciplinary impact of these results and their influence on the young research area of computational metaphysics.

In student projects the learned techniques will be applied to similar arguments of metaphysics. Every promising project can be extended (with further supervision, if necessary) towards a publication in the field of logics or logical philosophy.

German

Die Formale Logik ist gleichermaßen beheimatet in der Philosophie, der Mathematik und der Informatik. Mit leicht unterschiedlicher Ausprägung ist sie in all diesen Disziplinen sowohl auf Anfänger- als auch auf Fortgeschrittenen-Niveau in Lehrveranstaltungen der jeweiligen Studiengänge vertreten. Kernthemen wie z.B. Aussagen- und Prädikatenlogik oder der Kalkül des natürlichen Schließens werden nicht selten mehrfach angesprochen, andere wichtige Themen aus Zeitgründen oft übergangen.

Mit unserer Lehrveranstaltung richten wir uns deshalb gleichzeitig an Studierende der Philosophie, Mathematik und Informatik. Ziel ist es, eine fachübergreifende Einführung in verschiedene (theoretische) Logikformalismen mit einer praktisch motivierten Einführung in moderne, computer-basierte Beweisassistenzsysteme zu kombinieren.

Zu Beginn werden wir die zentrale Idee der Veranstaltung näher beleuchten, in die theoretischen Grundlagen einführen und die zum praktischen Einsatz vorgesehenen Beweisassistenzsysteme vorstellen. Als einen ersten Höhepunkt werden wir dann Varianten des ontologischen Gottesbeweises mit einem Computersystem selbst nachvollziehen. Anschließend widmen wir uns weiteren relevanten Themen, beispielsweise Zalta's Theorie abstrakter Objekte als Grundlage für die Metaphysik, und untersuchen erneut die Formalisierbarkeit am Computer. Abschließend soll fachübergreifend die Bedeutung dieser Arbeiten diskutiert werden, insbesondere im Hinblick auf eine computationale Metaphysik und die sich andeutende (und zum Teil bereits nachgewiesene) Möglichkeit der formalen Verifikation von Publikationen in diesem Bereich.

In Projektarbeiten sollen die Studierenden versuchen, die erlernten Techniken auf weitere, ähnliche Argumente in der Metaphysik zu übertragen und anzuwenden. Dabei soll aber auch der enge übergeordnete Bezug zu verwandten, aber technisch weitaus komplexeren Arbeiten in der Mathematik (Beweis der Kepler'schen Vermutung) beleuchtet werden. Jede gute Arbeit kann potenziell in einer wissenschaftlichen Publikation münden, für dessen Veröffentlichung die Gruppen weiterführende Betreuung erhalten.

Instructors/Tutors

Alexander Steen, Max Wisniewski

Instructors for tutorial sessions, assignment organization.

E-Mail: a.steen@fu-berlin.de, Website: inf.fu-berlin.de/~lex // E-Mail: m.wisniewski@fu-berlin.de, Website: inf.fu-berlin.de/~mwisnie

Maximilian Claus, Hans-Jörg Schurr

Tutors for the wednesday tutorial session

E-Mail: m.claus@fu-berlin.de // E-Mail: hansjoerg@zedat.fu-berlin.de

Assignments

Assignments will be given out every week until approx. week 10. Thereafter, there will be group projects until the end of the lecture. Introductory problems are discussed in the tutorial session (on wednesday).

Assignment sheets are solved and submitted in pairs of two. Please find yourself a partner for the tutorial assignments.

Theses topics

There are a lot of interesting topics for bachelor and master theses. Check out the proposals and contact us, if you are interested.

Software-related resources

Isabelle Proof Assistant

• Website (download)
• Isabelle, Nitpick, Sledgehammer, etc.; Documentations and Tutorials
• Nitpick: A counterexample generator for higher-order logic based on a relational model finder (J.C. Blanchette and T. Nipkow), In Proc. of ITP 2010, number 6172 in LNCS, pages131-146. Springer, 2010.
• Extending Sledgehammer with SMT solvers (J.C. Blanchette, S. Böhme, and L.C. Paulson), Journal of Automated Reasoning, 51(1):109-128, 2013.

LEO-II: Automated Theorem Prover for HOL

• Website (download)
• The Higher-Order Prover LEO-II, (C. Benzmüller, N. Sultana, L. Paulson, and F. Theiss). Journal of Automated Reasoning, 2015.
• LEO-II Version 1.5, (C. Benzmüller, N. Sultana), In PxTP 2013, EasyChair, EPiC Series in Computing, volume 14, pp. 2-10, 2013.

Satallax: Automated Theorem Prover for HOL

• Website (download)
• Satallax: An Automatic Higher-Order Prover, (Chad E. Brown), In Proc. of IJCAR 2012, number 7364 in LNAI, pages 111-117. Springer, 2012.

Literature

Higher-Order Logic

1. The Seven Virtues of Simple Type Theory (William M. Farmer), Journal of Applied Logic, 6:267-286.
2. Church's Type Theory (Peter Andrews), The Stanford Encyclopedia of Philosophy (Spring 2014 Edition), E.N. Zalta (ed.)
3. Automation of Higher-Order Logic (Christoph Benzmüller, Dale Miller), Chapter in Handbook of the History of Logic, Volume 9 --- Logic and Computation (Jörg Siekmann, Dov Gabbay, John Woods, eds.), Elsevier, 2014.
4. Higher-Order Automated Theorem Provers, (Christoph Benzmüller), In All about Proofs, Proof for All (David Delahaye, Bruno Woltzenlogel Paleo, eds.), College Publications, Mathematical Logic and Foundations, pp. 171-214, 2015.
5. Completeness in the theory of types (L. Henkin), Journal of Symbolic Logic, 15(2):81-91, 1950.
6. Higher-Order Semantics and Extensionality, (Christoph Benzmüller, Chad Brown, Michael Kohlhase), Journal of Symbolic Logic, 69(4):1027-1088, 2004.
7. Cut-Simulation and Impredicativity, (Christoph Benzmüller, Chad Brown, Michael Kohlhase), Logical Methods in Computer Science, volume 5, number 1:6, pp. 1-21, 2009.
8. Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure, (Christoph Benzmüller, Geoff Sutcliffe), Journal of Formalized Reasoning, volume 3, number 1, pp. 1-27, 2010.
9. The Lambda Calculus (J. Alama), Stanford Encyclopedia of Philosophy, 2013.
10. Lambda Calculi with Types (Henk Barendregt), 1993.

Ontological Argument

11. Logic and Theism: Arguments for and Against Beliefs in God (J.H. Sobel), Cambridge U.Press, 2004.
12. Appx. A: Notes in Kurt Gödel’s Hand (K. Gödel), pages 144-145. In Sobel, 2004.
13. Appx. B: Notes in Dana Scott’s Hand (D. Scott), pages 145–146. In Sobel, 2004.
14. Leibniz’s Ontological Proof of the Existence of God and the Problem of "Impossible Objects" (Wolfgang Lenzen), To appear.
15. Some emendations of Gödel’s ontological proof (C.A. Anderson), Faith and Philosophy, 7(3), 1990.
16. Gödel’s ontological proof (J.H. Sobel), In On Being and Saying. Essays for Richard Cartwright, pages 241-261. MIT Press, 1987.
17. Magari and others on Gödel's ontological proof (P. Hájek), In Logic and algebra. A. Ursini and P. Agliano (eds.), Dekker, New York etc.,1996, pp. 125-135.
18. Der Mathematiker und die Frage der Existenz Gottes (P. Hájek), In Kurt Gödel. Wahrheit und Beweisbarkeit. B. Buldt, E. Köhler, M. Stöltzner, P. Weibel, C. Klein, and W. Depauli-Schimanowich-Göttig (eds.), ISBN 3-209- 03835-X. öbv&hpt, Wien, 2001, pp. 325-336.
19. A New Small Emendation of Gödel's Ontological Proof (P. Hájek), Studia Logica 71(2):149-164, 2002.
20. Types, Tableaux and Gödel’s God (M. Fitting), Kluwer, 2002.
21. Modal collapse in Gödel’s ontological proof (S. Kovác), In Ontological Proofs Today, M. Szatkowski (ed.), Ontos Verlag, 2012.
22. Understanding Gödel's Ontological Argument" (F. Bjørdal), The Logica Yearbook 1998. Ed. by T. Childers. Filosofia, 1999.
23. Blogging Gödel: His ontological argument in the public eye (Fuhrmann), To appear.
24. See also the list of papers available here.

Computational Metaphysics

25. Automating Leibniz's Theory of Concepts (J. Alama, P.E. Oppenheimer, E.N. Zalta), In CADE 2015, Springer LNCS, volume 9195, pp. 73-97, 2015.
26. Steps Toward a Computational Metaphysics (Fitelson, B., and E. Zalta), Journal of Philosophical Logic, 36/2 (April 2007): 227–247.
27. Twenty-Five Basic Theorems in Situation and World Theory (Zalta, E.), Journal of Philosophical Logic, 22 (1993): 385-428.
28. A (Leibnizian) Theory of Concepts (Zalta, E.), Philosophiegeschichte und logische Analyse / Logical Analysis and History of Philosophy, 3 (2000): 137-183.
29. Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations (Oppenheimer, P., and E. Zalta), Journal of Logic and Computation, 21 (2011): 351–374.
30. The Theory of Abstract Objects (E.N. Zalta)
31. Axiomatic Metaphysics (E.N. Zalta)
32. Modal Logic as Metaphysics (T. Williamson), Oxford University Press, 2013
33. Mere Possibilities: Metaphysical Foundations of Modal Semantics (R. Stalnaker), Princeton University Press, 2011.
34. On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Christoph Benzmüller, In TABLEAUX 2015, Springer, LNCS, volume 9323, pp. 209-216, 2015.
35. The Inconsistency in Gödels Ontological Argument: A Success Story for AI in Metaphysics (C. Benzmüller and B. Woltzenlogel Paleo), IJCAI 2016.
36. Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers (C. Benzmüller and B. Woltzenlogel Paleo), ECAI, 2014.
37. Gödel’s God in Isabelle/HOL (C. Benzmüller and B. Woltzenlogel Paleo), Archive of Formal Proofs, 2013.
38. A variant of Gödel’s ontological proof in a natural deduction calculus (A. Siders and B. Woltzenlogel Paleo)
39. Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence (C. Benzmüller and B. Woltzenlogel Paleo), ArXiv e-prints, 2013.
40. Computer-assisted analysis of the Anderson-Hájek ontological controversy (C. Benzmüller, L. Weber, and B. Woltzenlogel Paleo), Handbook of the 1st World Congress on Logic and Religion, Joao Pessoa, Brasil, 2015.
41. Interacting with Modal Logics in the Coq Proof Assistant (Benzmüller and B. Woltzenlogel Paleo), In Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015. Springer, LNCS, volume 9139, pp. 398--411, 2015.

Logic Embeddings and Applications

42. Henkin Semantics for reasoning with natural language (Michael Hahn, Frank Richter), Journal of Language Modelling, Volume 3(2), 2015.
43. Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In 21st European Conference on Artificial Intelligence (ECAI), 2014.
44. Higher-order Modal Logics: Automation and Applications (C. Benzmüller, B. Woltzenlogel Paleo), In Reasoning Web 2015 (Adrian Paschke, Wolfgang Faber, eds.), Springer, LNCS, number 9203, pp. 32-74, 2015.
45. Quantified Multimodal Logics in Simple Type Theory (C. Benzmüller, L. Paulson), Logica Universalis, 7(1):7-20, 2013.
46. Embedding and Automating Conditional Logics in Classical Higher-Order Logic (C. Benzmüller, D. Gabbay, V. Genovese, D. Rispoli), In Annals of Mathematics and Artificial Intelligence, volume 66, number 1-4, pp. 257-271, 2012.
47. HOL based First-order Modal Logic Provers, LPAR, 2013.
48. Implementing and Evaluating Provers for First-order Modal Logics, ECAI, 2012.
49. Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic (A. Steen, C. Benzmüller), In 7th International Conference Non-Classical Logic -- Theory and Applications, Toruń, Poland, 2015.
50. Embedding of First-Order Nominal Logic into HOL (Alexander Steen, Max Wisniewski), In Jean-Yves Beziau, Safak Ural, Arthur Buchsbaum, Iskender Tasdelen, Vedat Kamer (Eds.), 5th World Congress and School on Universal Logic (UNILOG'15), Handbook of abstracts, Istanbul, Turkey, pp. 337--339, 2015.

Further topics

51. First-Order Modal Logic (M. Fitting and R.L. Mendelsohn), volume 277 of Synthese Library. Kluwer, 1998.
52. Higher Order Modal Logic (R. Muskens), In P. Blackburn et al. (eds.), Handbook of Modal Logic, pages 621–653. Elsevier, Dordrecht, 2006.
53. Types, Tableaus, and Gödels God, (M. Fitting), Kluwer, 2002.
54. Interpolation for First Order S5 (M. Fitting), JSL, 67(2):621-634, 2002.
55. Notion of (Mathematical) Proof
56. Formal Proof of Kepler Conjecture, 2015
57. How to Write a 21st Century Proof (Leslie Lamport), 2011.

Further resources

• B. Woltzenlogel Paleo and C. Benzmüller. Formal theology repository.
• Lecture proposal