Integrating ZermeloFraenkel set theory with higherorder logic
[ZFC_in_HOL
set theory
MJC Gordon
type classes
]
Many researchers, frustrated with the limited expressiveness of higherorder logic visàvis Zermelo Frankel set theory, have sought somehow to combine the two. The difficulty is to make the combination seamless, yielding a unified formal theory rather than two theories bolted together. We don’t want to keep transferring facts, constructions and proofs from one theory to the other.
Gordon’s HOLST
Higherorder logic was popularised by the late, great Mike Gordon (bio, also here), and it was he who first tried to extend it with ZFC. His HOLST simply introduced a type $V$ of all sets and a relation ${\in} : V\times V \to \textrm{bool}$, then asserted all the ZermeloFraenkel axioms. He remarks
The resulting theory has a consistency strength stronger than ZF, because one can define inside it a semantic function from a concrete type representing first order formulae to $V$ such that all the theorems of ZF can be proved. However, a model for higher order logic plus $V$ can be constructed in ZF with one inaccessible cardinal. Thus the strength of higher order logic augmented with ZFlike axioms for $V$ is somewhere between ZF and ZF plus one inaccessible cardinal.^{1}
He credits these claims to the equally legendary Ken Kunen. As a demonstration of the system’s power, Sten Agerholm formalised Dana Scott’s inverse limit construction of the set $D_\infty$, satisfying
\[\begin{align*} D_\infty \cong [D_\infty\to D_\infty] \end{align*}\]and yielding a model of the untyped $\lambda$calculus. Gordon also describes a construction of the list datatype using set theory. However, this experiment was not continued, with little attempt to integrate the set theory and higherorder logic worlds.
Oboa’s HOLZF
About 10 years later, Steven Obua performed a similar experiment with Isabelle/HOL. His paper on HOLZF begins with some amusing remarks:
The actual viability and howto of the approach was brought to the attention of the author by Bob Solovay who outlined HOLZF on the Isabelle mailing list and claimed that “for certain reasons he needed such a monster”, opposing Larry Paulson’s remark that HOLZF might be “too much of a good thing”. Bob Solovay also provided a proof of the consistency of HOLZF relative to the consistency of ZFC + ’there is an inaccessible cardinal’.^{2}
It seems that set theorists agree about the prooftheoretic strength of this “monster”. Obua adopted the same axioms and overall approach as Gordon, and demonstrated his system by formalising John H Conway’s partizan games, the basis of the socalled surreal numbers.
Importantly, Obua was able to rely on much of the existing infrastructure of Isabelle/HOL, such as its recursive function definitions.
He also made significant strides towards integrating ZFC with higherorder logic, introducing a function (like elts
below) to map a ZF set to the HOL set of its elements. Then he introduced the polymorphic type 'a zet
of typed sets that are “small”: i.e., embeddable into some ZF set.
HOLZF is the basis for one of the several formalisations of category theory in the Archive of Formal Proofs. Sadly, none of these formalisations have been used except to formalise even more category theory.
My own ZFC_in_HOL
My work in this area was inspired by Obua’s and is logically equivalent, but designed to develop ZFC with a minimum of additional vocabulary and maximum integration with higherorder logic. The presentation (refined by Dmitriy Traytel), introduces a type V
, a function elts
of type V set
and the ZF axioms for the construction of sets. Something is a set if it is an element of another set, i.e. if it is contained in the range of elts
. I also define the predicate small
, analogous to Obua’s 'a zet
but not a type: it characterises those sets (of the standard Isabelle/HOL set type, 'a set
that can be put in 11 correspondence with the elements of some ZF set.
No membership relation is required because one can simply write x ∈ elts y.
No symbols for union, intersection or the subset relation are required, since we can overload the type classes distrib_lattice
(distributive lattices, covering $\subseteq$, $\cup$, $\cap$) and conditionally_complete_lattice
(covering general unions and intersections).
The only penalty for using this overloading is a nonstandard syntax: $\le$ for subset, $\sqcup$ for union, etc. Further type class instantiations define 0 and 1 to denote the obvious natural numbers (0 is also the empty set).
Addition and multiplication of sets is also defined, allowing instantiation of the type classes stating that both $(0,{+})$ and $(1,{\times})$ are monoids.
These definitions extend the usual ordinal arithmetic, as I have mentioned earlier.
Also included, largely material borrowed from Isabelle/ZF: ordinal exponentiation and Cantor normal form, cardinals and cardinal arithmetic, $\aleph$notation for cardinals, transfinite induction and recursion, order types and many other odds and ends.
The class of ZFembeddable types
Type classes turn out to be a convenient means of integrating the ZF world with the rest of Isabelle/HOL. We’d like to be able to use existing constructions, such as the real and complex numbers, within ZF without having to construct them all over again. As I have pointed out before, the precise representation of mathematical objects as sets is generally unimportant; what matters simply is that they can be represented by sets, and we are happy to forget what that representation is.
Accordingly, the first type class identifies those types that can be embedded into V
:
class embeddable = assumes ex_inj: "∃V_of :: 'a ⇒ V. inj V_of"
There is already a class of all countable types. Those are types that can be embedded into the natural numbers, which (since they are finite ordinals) can in turn be embedded into V
. So all countable types are embeddable.
context countable begin subclass embeddable proof  have "inj (ord_of_nat ∘ to_nat)" if "inj to_nat" for to_nat :: "'a ⇒ nat" using that by (simp add: inj_compose inj_ord_of_nat) then show "class.embeddable TYPE('a)" by intro_classes (meson local.ex_inj) qed end
And hence the Booleans, natural numbers, integers and rationals are also embeddable. (We shall get to the reals later.)
instance bool :: embeddable .. instance nat :: embeddable .. instance int :: embeddable .. instance rat :: embeddable ..
The type V
is trivially embeddable into itself. It will follow that simple constructions over V
(such as lists) will also be embeddable into V
.
instance V :: embeddable by intro_classes (meson inj_on_id)
The (omitted) proofs the following instance declarations rely on routine constructions that uniquely represent, for example, a finite sequence of sets as a set.
instance prod :: (embeddable,embeddable) embeddable instance sum :: (embeddable,embeddable) embeddable instance list :: (embeddable) embeddable
In a previous post I stated that you risk inconsistency if you assume collections that are too big.
So what am I doing here? It’s simple: assuming the existence of a single model of ZFC, to be the interpretation of type V
, upon which further constructions can be built. By settheoretic standards, it’s a pretty weak assumption.
The class of small types
As noted above, a HOL set is small if it is equinumerous with a ZF set. It’s clear that all small types are embeddable and not conversely, the obvious exception being V
:
class small = assumes small: "small (UNIV::'a set)" begin subclass embeddable by intro_classes (meson local.small small_def) lemma TC_small [iff]: fixes A :: "'a set" shows "small A" using small smaller_than_small by blast end
Most constructions over small types yield other small types:
instance prod :: (small,small) small instance sum :: (small,small) small instance list :: (small) small instance set :: (small) small instance "fun" :: (small,small) small
The following inclusion may seem remarkable but simply reflects that all settheoretic functions are themselves sets.
instance "fun" :: (small,embeddable) embeddable
Finally, and most usefully, we can show that the real and complex number types are small. The proof is simply that they are represented in terms of other small types, in the case of the reals, by sequences of rationals.
instance real :: small instance complex :: small
Fully integrating ZFC with higherorder logic
In a previous post, I described some prior formalisations of set theoretic proofs using a variety of proof assistants. Shortly after writing the post, I became interested in Wetzel’s problem, a question about sets of analytic functions that turns out to be equivalent to the continuum hypothesis. The formalisation project revealed a number of major gaps in how ZFC_in_HOL interoperates with higherorder logic:
 in defining functions by transfinite recursion whether or not they are ZF sets
 in working with embeddings into the ZF universe
 in denoting the cardinality of infinite Isabelle/HOL sets (as opposed to ZF sets)
Fixing the first gap required nothing more than generalising the types in the relevant definition.
definition transrec :: "((V ⇒ 'a) ⇒ V ⇒ 'a) ⇒ V ⇒ 'a" where "transrec H a ≡ wfrec {(x,y). x ∈ elts y} H a"
The second was also easy enough to fix, by defining a new overloaded function:
definition V_of :: "'a::embeddable ⇒ V" where "V_of ≡ SOME f. inj f"
This definition gives us an arbitrary embedding. Had the embeddable
type class been defined to require an explicit definition of V_of
for each instance, we would have access to something resembling the actual embeddings arising from the definition of each type. Unfortunately, the type class countable
also hides the underlying map and would also have to be modified.
Fortunately, the precise embedding into the ZF universe really is of no importance. All that we need is the ability to designate something as the embedding of such constructions as $\mathbb R$ and $\mathbb C$.
definition "Real_set ≡ set (range (V_of::real⇒V))" definition "Complex_set ≡ set (range (V_of::complex⇒V))"
The third gap is also easily fixed by defining an overloaded function:
definition gcard :: "'a::embeddable set ⇒ V" where "gcard X ≡ vcard (set (V_of ` X))"
This general cardinality function accepts any Isabelle/HOL set of a type embeddable in the ZF world and returns a ZF cardinal number.
In particular we have an obvious identity, relating gcard
with its ZF analogue, vcard
, via the “elements of” function, elts
:
lemma gcard_eq_vcard: "gcard (elts x) = vcard x" by (metis cardinal_cong elts_set_V_of gcard_def small_elts)
Each of the definitions above required a little library of basic lemmas, and there were a number of other gaps in areas ranging from cardinalities to holomorphic functions. Filling all these gaps in the libraries seemed to involve more effort (and space in the theory file) than the Wetzel problem itself.
The project took 18 days and I hope to write more about it soon.

Mike Gordon. Set Theory, Higher Order Logic or Both? Theorem Proving in Higher Order Logics (1996), 192. ↩

S. Obua. Partizan games in Isabelle/HOLZF. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, Theoretical Aspects of Computing (Springer, 2006), p. 274. ↩