Prof. (em.) Dr. Peter Koepke

Axiomatic Set Theory, General Logic, and Formal Mathematics

Research profile

• Axiomatic set theory: determination of consistency strengths of infinitary combinatorial principles, using forcing and core models; determination of consistency strengths without assuming the axiom of choice, characterizations of large cardinal axioms by embeddings of models of set theory.
• Constructibility theory and ordinal computability theory: new fine structure theories for constructible models of set theory, with applications; generalized machines with tapes of arbitrary ordinal lengths or registers working on ordinal numbers.
• Descriptive set theory and infinitary games.
• Formal mathematics: the language of mathematics and designing a natural proof checking system Naproche with natural language interfaces, in collaboration with linguistics.

Teaching Winter 2026/27:
Praktikum Mathematische Logik (P2A1) and Practical Project in Mathematical Logic (P4A1)
Axiomatic Set Theory, Formalized in Natural Language

Lecturer Peter Koepke

Time and Place Tuesdays 16-18, Wednesdays 16-18, N 0.008

Contents

The practical project will focus on two themes: a standard introduction to Morse-Kelley set theory and a formalization of that theory in the Naproche interactive theorem prover.

Morse-Kelley set theory was introduced in the Appendix: Elementary Set Theory of the classic textbook General Topology by John L. Kelley (1955). It is built on first-order axioms about classes, whose elements are sets. In Morse-Kelley set theory one can conveniently introduce the fundamental notions of relations, functions and numbers and prove their usual properties. In this way, Morse-Kelley set theory can serve as a general foundation of mathematics.

Naproche (Natural Proof Checker) is distinguished from other interactive theorem provers like Lean or Isabelle/HOL by using natural mathematical language input (in LaTeX) instead of formal code. Naproche proofs are intended to read and function like standard mathematical proofs. Strong first-order automated theorem proving is employed to fill in mathematical details that are left implicit like in ordinary mathematical discourse. There are readable Naproche formalizations of a variety of theories and results.

The course will be based on an existing Naproche formalization of Kelley's Appendix. The course will meet weekly for four hours. Initially three hours will be devoted to lectures by me on the Appendix and on Naproche. Mathematically this will lead up ordinal and cardinal numbers and to infinitary cardinal arithmetic. One hour will be devoted to practical exercises and work with Naproche. After getting acquainted with Naproche, practical projects will be assigned which may extend the formalization of the Appendix or examine and improve the Naproche software. The second half of the course will continue the lectures but will concentrate more on the projects.

Naproche is part of the current Isabelle prover platform. After installing and opening Isabelle one can click “Documentation” in the left margin and then $ISABELLE_NAPROCHE/Intro.thy to get further instructions and Naproche formalization examples, including a tutorial. For the practical project we shall use Isabelle2026 to be released in October. Kelley's General Topology can be downloaded here.

Participants are supposed to have a reasonably powerful laptop which can run Isabelle. You can apply for a practical slot by email to koepke@math.uni-bonn.de. Please state your

– name, matriculation number, email address, subject, Bachelor or Master and study semester, completed logic modules, programming experience, and optional further information.

The practical project will be organized via email and appointment.

Contact

• Mathematisches Institut
  Rheinische Friedrich-Wilhelms-Universität Bonn
  Endenicher Allee 60
  D-53115 Bonn
  Germany
  
• E-mail: koepke [emailsymbol] math.uni-bonn.de
• Sprechstunden nach Vereinbarung per Email.