Varie indagini metamatematiche, a partire dalla storica dimostrazione di Fraenkel del- l’indipendenza dell’assioma di scelta, necessitavano il ricorso alla definizione di universi gerarchici di insiemi. Ci`o ha portato alla scoperta di importanti strutture cumulative, tra cui quella indivi- duata da von Neumann (generalmente indicata come l’universo di tutti gli insiemi) e l’universo dei cosiddetti construibili di G ̈odel. Varianti di tali strutture tornano utili anche in studi riguardan- ti i fondamenti dell’analisi (secondo l’approccio di Abraham Robinson), o riguardanti gli insiemi non-ben-fondati. Mossi dunque dalla loro rilevanza e pervasivit`a nella matematica, offriamo qui una presentazione sistematica di queste molte strutture. Riporteremo come numerose propriet`a di nozioni inerenti le gerarchie di insiemi, quale ad esempio la nozione di rango, siano state controllate grazie all’assistenza del verificatore di dimostrazioni ÆtnaNova. Illustreremo poi, tramite procedure per la manipolazione efficace degli insiemi ereditariamente finiti di Ackermann, implementate in SETL e in Maple, un caso particolarmente significativo fra i tanti in cui le entita` costitutive di un universo di insiemi possono venire costruite e trattate algoritmicamente: per questa via, il fruttuoso impiego delle gerarchie cumulative di insiemi viene ad estendersi dalla matematica pura agli ambiti dell’informatica teorica e dell’algoritmica
