Logic & Set Theory seminar: Formalising NBG set theory in Isabelle/HOL
Ioanna Dimitriou, University of Bonn
Howard House 4th floor seminar room
Last semester in the mathematical logic group of Bonn, Peter Koepke and I supervised a group of 11 students, who began formalising NBG set theory, in Isabelle's higher order logic (HOL) and in a "natural style", i.e., with the structure and proofs of a textbook. We used Mendelson's classic textbook "Introduction to Mathematical Logic", also because it presents NBG's finite axiomatisation. We encountered two main obstacles in formalising a first order logic (FOL) theory in Isabelle/HOL. First, we had to express FOL formulas and connect them to the internal HOL logic of Isabelle. The second was that the axiom of choice is included in Isabelle/HOL, while we wanted to add it to our theory only later, and in a controlled fashion.
This was a first step towards a larger project that we are considering in Bonn, that is, formalising set theoretic techniques in a "natural" style, and in HOL, which is the preferred logic for most theorem provers, and which will help simplify formal metamathematical arguments. To follow the style of the proofs in Mendelson, we used Isabelle's proving language Isar (Intelligible semi-automatic reasoning), which uses keywords such as "fix x y", "assume ...", "thus ...", etc., to create human-readable proofs.
I will present this formalisation, the issues we encountered, and the solutions we used, and I will discuss our plans for the future of this project.