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 one-step 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 directedcomplete 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 de nitions 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.

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

P. Aczel, Zorn's Lemma in CZF, unpublished, 2002.

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

P. Aczel and M. Rathjen, Notes on constructive set theory. Technical report, Institut Mittag-Leer, 2000/01. Report No. 40.

P. Aczel and M. Rathjen, Constructive set theory, book draft, 2010. 5The opinions expressed in this publication are those of the authors and do not necessarilyreect the views of the John Templeton Foundation.

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

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.

T. Coquand, Constructive topology and combinatorics, in: Constructivity in Computer Science (Summer Symposium San Antonio, TX, June 19{22, 1991 Proceeding), volume 613 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 1992, pp. 159-164.[8] R. Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51:1 (1975), 176-178.

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

M. Hendtlass and P. Schuster, A direct proof of Wiener's theorem, in: S. B. Cooper, A. Dawar, and B. Lowe, editors, How the World Computes. Turing Centenary Conference and Eighth Conference on Computability in Europe, volume 7318 of Lect. Notes Comput. Sci., Berlin and Heidelberg, 2012. Springer. Proceedings, CiE 2012, Cambridge, UK, June 2012, pp. 294-303,

K. Kuratowski, Une methode d'elimination des nombres trans nis des raisonnements mathematiques, Fundamenta Mathematicae 3:1 (1922), 76-108.

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

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

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

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

P. Schuster, Induction in algebra: a rst 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.

E. Szpilrajn, Sur l'extension de l'ordre partiel, Fundamenta Mathematicae 16:1 (1930), 386-389.

P. Vamos and D. W. Sharpe, Injective modules, Cambridge Tracts in Mathematics and Mathematical Physics, 62, Cambridge University Press, 1972.

M. Zorn, A remark on method in trans nite 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.