General information

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.

News

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.

Lecture description

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.

Lectures

Week Tuesday dates Thursday dates
1 19.4.Introduction: Computational Metaphysics
(C. Benzmüller)
Location: T9/SR006
21.4. Logic Recap: Propositional, First-order, Higher-order, Classical- and Non-classical logic
(C. Benzmüller)
Location: T9/HS
2 26.4 Classical Higher-order Logic (HOL)
(C. Benzmüller)
Location: T9/HS
28.4. Interactive Proofs in Isabelle/HOL
(J. Blanchette, Inria Nancy and MPII Saarbrücken)
Location: T9/HS
3 3.5. Automatic Proofs and Models in Isabelle/HOL: Sledgehammer, Nitpick, Leo-II, Satallax and Friends
(J. Blanchette, Inria Nancy and MPII Saarbrücken)
Location: T9/SR006
4-6 Lecture break with many exercises e.g. on HOL and interactive/automated proofs in Isabelle/HOL
7 31.5. The Ontological Argument and Modal Higher-order Logics
(C. Benzmüller)
Location: T9/SR006
8 7.6. Automating Modal Higher-order Logics in HOL: The Logic Embeddings Approach
(C. Benzmüller)
Location: T9/SR006
9.6. Computational Analysis of Gödel's Ontological Argument
(C. Benzmüller)
Location: T9/SR006
9 No Lecture this week.
10 21.6. Computational Analysis of Further Variants of the Ontological Argument
(B. Woltzenlogel-Paleo, ANU Canberra)
Suggested reading: [40]
Location: T9/SR046
23.6. Logic Embeddings: Further Topics and Applications --- e.g. free logic, multivalued logic, paraconsistent logic, etc.
(B. Woltzenlogel-Paleo and C. Benzmüller)
Location: T9/SR006
11 28.6. Axiomatic Metaphysics: Two Applications
(E.N. Zalta, Stanford)
Suggested reading: [27] [28]
Location: T9/SR006
30.6. Computational Methods for Axiomatic Metaphysics
(E.N. Zalta, Stanford)
Suggested reading: [26] [25] [29]
Location: T9/SR006
12 5.7. Experiments:
(A) The Theory of Abstract Objects in Isabelle/HOL
(B) Free Logic (and Axiomatic Category Theory) in HOL
(C. Benzmüller)
Location: T9/SR006
13 12.7. Leibniz‘ Ontologischer Beweis der Existenz Gottes (Abstract)
(W. Lenzen, Osnabrück)
Location: T9/HS (lecture hall)
14 19.7. Final Lecture: Group presentations and final discusion
Preliminary talk schedule
Location: T9/SR006

Tutorial sessions

Tutorial sessions take place every week on wednesday 14-16 at Takustr. 9 (Institut für Informatik) at rooms K38 and K48 (computer pool rooms, basement). In the tutorial sessions, we will discuss details of the lecture topics, give examples and work on excercises (possibly in groups).

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.

No. Assignment sheet Hints and comments
1 [Ex. sheet as PDF] Due: Tuesday, April 26th, until the end of the lecture
2 [Ex. sheet as PDF] Due: Upload until Tuesday, May 3rd, until midnight into the KVV system under 'Excercise sheet 2'.
Additional material:
3 [Ex. sheet as PDF] Upload until Tuesday, May 10th, until midnight into the KVV system under 'Excercise sheet 3'.
4 [Ex. sheet as PDF] Upload until Tuesday, May 17th, until midnight into the KVV system under 'Excercise sheet 4'.
5 [Ex. sheet as PDF] Upload until Tuesday, May 24th, until midnight into the KVV system under 'Excercise sheet 5'.
Additional material:
6 [Ex. sheet as PDF] Upload until Tuesday, May 31st, until midnight into the KVV system under 'Excercise sheet 6'.
Additional material:
7 [Ex. sheet as PDF] Upload until Tuesday, June 7th, until midnight into the KVV system under 'Excercise sheet 7'.
8 [Ex. sheet as PDF] Upload the relevant parts until Tuesday, June 14th, until midnight into the KVV system under 'Excercise sheet 8', the rest may be handed in at our office (Arnimalle 7, room 113).
9 [Ex. sheet as PDF] Upload the relevant parts until Tuesday, June 21st, until midnight into the KVV system under 'Excercise sheet 9'.
Additional material:
  • QML theory, to be placed in the same directory where your current .thy file is (the one on which you are working).
  • Scott.thy -- formalization of Scott's variant of the Ontological Argument, with modal logic S5 used for the embedding. (To be placed in the same directory where the QML.thy file is located.)
n/a Thera are no more exercise sheets!

Resources

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

Satallax: Automated Theorem Prover for HOL

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

  1. Logic and Theism: Arguments for and Against Beliefs in God (J.H. Sobel), Cambridge U.Press, 2004.
  2. Appx. A: Notes in Kurt Gödel’s Hand (K. Gödel), pages 144-145. In Sobel, 2004.
  3. Appx. B: Notes in Dana Scott’s Hand (D. Scott), pages 145–146. In Sobel, 2004.
  4. Leibniz’s Ontological Proof of the Existence of God and the Problem of "Impossible Objects" (Wolfgang Lenzen), To appear.
  5. Some emendations of Gödel’s ontological proof (C.A. Anderson), Faith and Philosophy, 7(3), 1990.
  6. Gödel’s ontological proof (J.H. Sobel), In On Being and Saying. Essays for Richard Cartwright, pages 241-261. MIT Press, 1987.
  7. 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.
  8. 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.
  9. A New Small Emendation of Gödel's Ontological Proof (P. Hájek), Studia Logica 71(2):149-164, 2002.
  10. Types, Tableaux and Gödel’s God (M. Fitting), Kluwer, 2002.
  11. Modal collapse in Gödel’s ontological proof (S. Kovác), In Ontological Proofs Today, M. Szatkowski (ed.), Ontos Verlag, 2012.
  12. Understanding Gödel's Ontological Argument" (F. Bjørdal), The Logica Yearbook 1998. Ed. by T. Childers. Filosofia, 1999.
  13. Blogging Gödel: His ontological argument in the public eye (Fuhrmann), To appear.
  14. See also the list of papers available here.

Computational Metaphysics

  1. 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.
  2. Steps Toward a Computational Metaphysics (Fitelson, B., and E. Zalta), Journal of Philosophical Logic, 36/2 (April 2007): 227–247.
  3. Twenty-Five Basic Theorems in Situation and World Theory (Zalta, E.), Journal of Philosophical Logic, 22 (1993): 385-428.
  4. A (Leibnizian) Theory of Concepts (Zalta, E.), Philosophiegeschichte und logische Analyse / Logical Analysis and History of Philosophy, 3 (2000): 137-183.
  5. 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.
  6. The Theory of Abstract Objects (E.N. Zalta)
  7. Axiomatic Metaphysics (E.N. Zalta)
  8. Modal Logic as Metaphysics (T. Williamson), Oxford University Press, 2013
  9. Mere Possibilities: Metaphysical Foundations of Modal Semantics (R. Stalnaker), Princeton University Press, 2011.
  10. 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.
  11. The Inconsistency in Gödels Ontological Argument: A Success Story for AI in Metaphysics (C. Benzmüller and B. Woltzenlogel Paleo), IJCAI 2016.
  12. 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.
  13. Gödel’s God in Isabelle/HOL (C. Benzmüller and B. Woltzenlogel Paleo), Archive of Formal Proofs, 2013.
  14. A variant of Gödel’s ontological proof in a natural deduction calculus (A. Siders and B. Woltzenlogel Paleo)
  15. Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence (C. Benzmüller and B. Woltzenlogel Paleo), ArXiv e-prints, 2013.
  16. 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.
  17. 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

  1. Henkin Semantics for reasoning with natural language (Michael Hahn, Frank Richter), Journal of Language Modelling, Volume 3(2), 2015.
  2. 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.
  3. 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.
  4. Quantified Multimodal Logics in Simple Type Theory (C. Benzmüller, L. Paulson), Logica Universalis, 7(1):7-20, 2013.
  5. 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.
  6. HOL based First-order Modal Logic Provers, LPAR, 2013.
  7. Implementing and Evaluating Provers for First-order Modal Logics, ECAI, 2012.
  8. 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.
  9. 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

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

Further resources