Cumulative hierarchies and computability over universes of sets

  • Domenico Cantone Università di Catania
  • Claudio Chiaruttini Università di Trieste
  • Marianna Nicolosi Asmundo Università di Catania
  • Eugenio G. Omedeo Università di Trieste
Keywords: Set theory, Computable set theory, Cumulative hierarchies, Superstructures, Hereditarily finite sets, Constructible sets, Hypersets, Proof verification, Syllogistics


Various metamathematical investigations, beginning with Fraenkel’s historical proof of the independence of the axiom of choice, called for suitable definitions of hierarchical universes of sets. This led to the discovery of such important cumulative structures as the one singled out by von Neumann (generally taken as the universe of all sets) and Godel’s universe of the so-called constructibles. Variants of those are exploited occasionally in studies concerning the foundations of analysis (according to Abraham Robinson’s approach), or concerning non-well-founded sets. We hence offer a systematic presentation of these many structures, partly motivated by their relevance and pervasiveness in mathematics. As we report, numerous properties of hierarchy-related notions such as rank, have been verified with the assistance of the ÆtnaNova proof-checker.

Through SETL and Maple implementations of procedures which effectively handle the Ackermann’s hereditarily finite sets, we illustrate a particularly significant case among those in which the entities which form a universe of sets can be algorithmically constructed and manipulated; hereby, the fruitful bearing on pure mathematics of cumulative set hierarchies ramifies into the realms of theoretical computer science and algorithmics.

Author Biographies

Domenico Cantone, Università di Catania
Dipartimento di Matematica e Informatica
Claudio Chiaruttini, Università di Trieste
Dipartimento di Matematica e Informatica
e Centro Interdipartimentale per le Scienze Computazionali
Marianna Nicolosi Asmundo, Università di Catania
Dipartimento di Matematica e Informatica
Eugenio G. Omedeo, Università di Trieste
Dipartimento di Matematica e Informatica