A General Extension Theorem for Directed-Complete Partial Orders

Peter Schuster,

Daniel Wessel


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.


Received 27 June 2017

AMS subject classification: 03E25, 03F65

Słowa kluczowe: Extension theorems, Kuratowski-Zornlemma, transfinite methods

[1] P. Aczel, Zorn’s Lemma in CZF, unpublished, 2002.

[2] P. Aczel, Aspects of general topology in constructive set theory, Annals of Pure and Applied Logic 137:1–3 (2006), 3–29.

[3] P. Aczel and M. Rathjen, Notes on constructive set theory. Technical report, Instiut Mittag-Leffler, 2000/01. Report No. 40.

[4] P. Aczel and M. Rathjen, Constructive set theory, book draft, 2010.

[5] J.L. Bell, Zorn’s lemma and complete Boolean algebras in intuitionistic type theories, The Journal of Symbolic Logic 62:4 (1997), 1265–1279.

[6] U. Berger, A computational interpretation of open induction, In: F. Titsworth, editor, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 2004, pp. 326–334.

[7] T. Coquand, Constructive topology and combinatorics, In: Constructivity in Computer Science (Summer Symposium San Antonio, TX, June 19–22, 1991 Proceeding), vol. 613 of Lecture Notes in Computer Science, Springer, Berlin and Heidelberg, 1992, pp. 159–164.

[8] R. Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51:1 (1975), 176–178.

[9] N.D. Goodman and J. Myhill, Choice implies excluded middle, Mathematical Logic Quarterly 24:461 (1978), 25–30.

[10] M. Hendtlass and P. Schuster, A direct proof of Wiener’s theorem, In: S.B. Cooper, A. Dawar and B. L¨owe, editors, How the World Computes. Turing Centenary Conference and Eighth Conference on Computability in Europe, vol. 7318 of Lecture Notes in Computer Science, Springer, Berlin and Heidelberg, 2012. Proceedings, CiE 2012, Cambridge, UK, June 2012, pp. 294–303,

[11] K. Kuratowski, Une méthode d’élimination des nombres transfinis des raisonnements mathématiques, Fundamenta Mathematicae 3:1 (1922), 76–108.

[12] D.G. Northcott, An Introduction to Homological Algebra, Cambridge University Press, 1960.

[13] H. Perdry, Strongly Noetherian rings and constructive ideal theory, Journal of Symbolic Computation 37:4 (2004), 511–535.

[14] J.-C. Raoult, Proving open properties by induction, Information Processing Letters 29:1 (1988), 19–23.

[15] G. Sambin, Some points in formal topology, Theoretical Computer Science 305:1-3 (2003), 347–408.

[16] P. Schuster, Induction in algebra: a first case study, In: 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE Computer Society Publications, 2012. Proceedings, LICS 2012, Dubrovnik, Croatia, pp. 581–585.

[17] E. Szpilrajn, Sur l’extension de l’ordre partiel, Fundamenta Mathematicae 16:1 (1930), 386–389.

[18] P. V´amos and D.W. Sharpe, Injective modules, Cambridge Tracts in Mathematics and Mathematical Physics 62, Cambridge University Press, 1972.

[19] M. Zorn, A remark on method in transfinite algebra, Bulletin of the American Mathematical Society 41:10 (1935), 667–670.

Czasopismo ukazuje się w sposób ciągły on-line.
Pierwotną formą czasopisma jest wersja elektroniczna.