Machine Logic

Integrating Zermelo-Fraenkel set theory with higher-order logic

06 Apr 2022

Many researchers, frustrated with the limited expressiveness of higher-order 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 HOL-ST

Higher-order 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 HOL-ST simply introduced a type $V$ of all sets and a relation ${\in} : V\times V \to \textrm{bool}$, then asserted all the Zermelo-Fraenkel 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 ZF-like axioms for $V$ is somewhere between ZF and ZF plus one inaccessible cardinal.¹

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

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 higher-order 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 how-to 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’.²

It seems that set theorists agree about the proof-theoretic 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 so-called 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 higher-order 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 higher-order 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 1-1 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 non-standard 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 ZF-embeddable 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 set-theoretic 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 set-theoretic 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 higher-order 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 higher-order logic:

1. in defining functions by transfinite recursion whether or not they are ZF sets
2. in working with embeddings into the ZF universe
3. 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.