On the conservativity of the axiom of choice over set theory (Q647343)

In this very interesting and well-written paper, the author shows that for various set theories \(\mathsf{T}\), including \(\mathsf{ZF}\), \(\mathsf{T + AC}\) (\(\mathsf{AC}\) is the axiom of choice: For every family \(\mathcal{A}\) of non-empty sets, there is a function \(f\) with domain \(\mathcal{A}\) such that, for every \(x\in\mathcal{A}\), \(f(x)\) is an element of \(x\)) is conservative over \(\mathsf{T}\) for sentences of the form \(\forall x\exists! y\) \(\mathsf{A}(x,y)\) where \(\mathsf{A}(x,y)\) is a \(\Delta_0\)-formula. (If \(\mathsf{T}\) and \(\mathsf{T}'\) are theories in the languages \(L\) and \(L'\), then \(\mathsf{T}'\) is a conservative extension of \(\mathsf{T}\) if \(\mathsf{T}\subseteq\mathsf{T}'\) and \(\mathsf{T}'\cap L=\mathsf{T}\), that is, all theorems of \(\mathsf{T}'\) in the language \(L\) are already theorems of \(\mathsf{T}\). A formula of set theory is a \(\Delta_0\)-formula if it has no quantifiers, or it is \(\phi\wedge\psi\), \(\phi\vee\psi\), \(\neg\phi\), \(\phi\rightarrow\psi\) or \(\phi\leftrightarrow\psi\), where \(\phi\) and \(\psi\) are \(\Delta_0\)-formulas, or it is \((\exists x\in y)\phi\) or \((\forall x\in y)\phi\), where \(\phi\) is a \(\Delta_0\)-formula). More specifically, the research in this paper is centered at the following themes: P. Aczel conjectured in 2009 at the Leeds Symposium on Proof Theory and Constructivism that the \(\Delta_0\)-definable functions of \(\mathsf{ZFC}\) are the same as those of \(\mathsf{ZF}\). In particular: Assume \(\mathsf{A}(x,y)\) is a \(\Delta_0\)-formula in the language of set theory. If \(\mathsf{ZFC}\vdash\forall x\exists!y\;\mathsf{A}(x,y)\), then \(\mathsf{ZF}\vdash\forall x\exists!y\;\mathsf{A}(x,y)\). The author proves Aczel's conjecture in Section 2 of his paper. The argument can be modified for weaker theories that the author considers later on in his paper. In Section 3 of the paper, the author discusses aspects of forcing over theories like \(\mathsf{KP}_{\Sigma_{1}}\omega\) (the subtheory of Kripke-Platek set theory with infinity obtained by restricting induction to \(\Sigma_1\)-formulas, i.e., formulas of the form \(\exists x\phi\) where \(\phi\) is \(\Delta_0\)) needed to generalize the proof of Aczel's conjecture. In Section 4, Aczel's conjecture is generalized to various subtheories of \(\mathsf{ZF}\). In addition, the author supplies, in Section 1, a concise and well-organized account of the background, which is very helpful to the reader.