A General Extension Theorem for Directed-Complete Partial Orders
Peter M. Schuster, Daniel Wessel · Reports on Mathematical Logic · 2018
A b s t r a c t.The typical indirect proof of an abstract extension theorem, by the Kuratowski-Zorn lemma, is based on a onestep extension argument.While Bell has observed this in case of the axiom of choice, for subfunctions of a given relation, we now consider such extension patterns on arbitrary directed-complete partial orders.By postulating the existence of so-called total elements rather than maximal ones, we can single out an immediate consequence of the Kuratowski-Zorn lemma from which quite a few abstract extension theorems can be deduced more directly, apart from certain definitions by cases.Applications include Baer's criterion for a module to be injective.Last but not least, our general extension theorem is equivalent to a suitable form of the Kuratowski-Zorn lemma over constructive set theory.