Krull Without Zorn

Joint work with Davide Rinaldi, University of Leeds

Zorn's Lemma (ZL) is without doubt the most common incarnation of the Axiom of Choice in algebra. The use of ZL, however, allegedly obscures the algorithmic content of proofs, and therefore is generally despised as non-constructive. Yet ZL often leads to arguments shorter and more elegant than those involving explicit computations, especially when ZL is used within a proof by contradiction. 

We can rephrase Krull's Lemma (KL), one the frequent forms of ZL in commutative algebra, as a syntactic conservation theorem: the theory of integral domains is conservative, for definite Horn clauses, over the theory of reduced rings. In this sense, KL is in fact constructive! Apart from addressing the dual case, we briefly compare our result with the ones from dynamical algebra.