Towards a theory of symmetric extensions

TL;DR

This paper develops a comprehensive framework for iterating symmetric extensions, enhancing understanding of models without the Axiom of Choice and extending the theoretical tools available since the 1960s.

Contribution

It introduces a general theory of symmetric extensions including iterations, quotients, and structural results, filling a gap in the understanding of the technique.

Findings

Developed a theory of symmetric extensions with various iteration types

Proved that every set lies in a symmetric extension of HOD under ZF

Extended classical results of Grigorieff within the new framework

Abstract

The technique of symmetric extensions is derived from forcing and it is one of the most important tools for studying models without the Axiom of Choice. Despite being incredibly successful since the 1960s, our understanding of the technique remained fairly limited compared to the theory of forcing. Whereas forcing developed products and iterations, no serious attempts at developing any general framework for iterating symmetric extensions were presented before [10], where only finite support iterations are treated. In this paper we develop the theory of symmetric extensions including different types of iterations, quotients, equivalents, and the structural results that can be described in this language. In particular, we give a modern exposition to some of the important theorems of Grigorieff [3], study Kinna--Wagner Principles in symmetric extensions, and show that it is provable from $\mathsf{ZF}$ that every set lies in a symmetric extension of $\operatorname{HOD}$.