Bonn Mathematical Logic Group

Ioanna Matilde Dimitriou Henríquez

my page at boole's rings:
office: Endenicher Allee 60, Room N1.007, tel: +49 (0) 228 73 62366
mailing address: Endenicher Allee 60, 53115 Bonn, Germany
email: dimitri at math dot uni - bonn dot de









I worked with Peter Koepke on formalising NBG set theory in Isabelle/HOL (Higher Order Logic) and in a "natural" way, that is, following the proving style and structure of a textbook. The textbook we chose is Mendelson's "Introduction to mathematical logic", chapter 4 ("An axiom system"), because it is considered a classic, and because it has a finite axiomatization of NBG set theory. During 2015, with the invaluable help of our students, we have created theory files with this formalisation, which can be found at this Github repository. We encountered difficulties to reason about first order logic (FOL) formulas in Isabelle's HOL, but Marek Broll and Thorben Tröbst have managed to create and connect a custom type FOL_Formula to Isabelle's HOL, which enables us to talk about definable classes. The bulk of the theory formalisation was done by Thekla Hamm, Uli Matzner, Lukas Meier, Robert Paßmann, Julian Schröteler, Jakob Speer, Benjamin Valdez, and Luisa Vogel. They used the proving language Isar (Intelligible semi-automatic reasoner), which resembles human style proofs (e.g., fix x y, assume "x = y + 1" thus "y = x - 1" by simp).

I am also a Common Lisper, and my pet project is the Choiceless Grapher, a program which creates diagrams of the implications between consequences of the axiom of choice. A sample diagram is below:

For more information about me, and my publications, please go to my boole's ring:

,,I hope the field of computer science never loses its sense of fun. Above all, I hope we don't become missionaries. Don't feel as if you're Bible salesmen. The world has too many of those already. What you know about computing other people will learn. Don't feel as if the key to successful computing is only in your hands. What's in your hands, I think and hope, is intelligence: the ability to see the machine as more than when you were first led up to it, that you can make it more.''
-- Alan J. Perlis