Formalising set theoretic proofs with Isabelle/HOL in Isar.
Workshop during FOMUS: Foundations of Mathematics: Univalent Foundations and Set Theory - What are Suitable Criteria for the Foundations of Mathematics?
This workshop will take place on Monday July 18 at 5:30 - 7:00pm, and on Tuesday July 19 at 14:00 - 15:30. The participants are required to bring along laptops with Isabelle2016 installed, and at least once opened. This is because Isabelle builds the logical core the first time it runs after installation.
Also please download the GitHub repository NBG_HOL, which contains the files we will use. There is a button on the right side which says "clone or download". The README.md file there (visible on the link above if you scroll down) contains more detailed information about these files.
We shall work with a "natural" formalisation of NBG set theory in Isabelle/HOL, "natural" here meaning following a textbook, namely Mendelson's classic textbook "Introduction to mathematical logic", Chapter 4: "An axiom system" (Chapman & Hall, 4th edition, 1997). This formalisation is based on this textbook, mainly because it presents the finite axiomatisation of NBG set theory, which simplifies setting up the basics of our theory.
I will only shortly talk about other set theories in Isabelle, the reasons for choosing our theory, and the obstacles we encountered during this formalisation. More details will be given during my talk on Friday. In this workshop, we shall concentrate on formalising set theoretic proofs in this system, in Isabelle's human readable proving language Isar (Intelligible semi-automatic reasoning).
An example set theoretic proof in our theory, written with Isar in Isabelle/HOL:
Note that the proofs (by ...) above, were found automatically with Isabelle's tool "Sledgehammer".
The same lemma is proven in Mendelson, very similarly, as follows:
lemma Prop4_8_b: "(Ord(X) ∧ Y ⊂ X ∧ Trans(Y)) ⟶ Y ∈ X"
assume 1: "Ord(X)" and 2: "Y ⊂ X" and "Trans(Y)"
hence "Sect ℰ X Y" by (metis Ex4_30_b Section_def segment_lemma mem_rel_lemma2 strict_subclass_def)
thus "Y ∈ X" using Ex4_30_c Ex4_30_b 1 2 ordinal_def strict_subclass_def by force
Proof. Assume Ord(X) ∧ Y ⊂ X ∧ Trans(Y).
It is easy to see that Y is a proper ℰ-section of X.
Hence, by Exercise 4.30(b,c), Y∈X.