This paper was converted on www.awesomepapers.org from LaTeX by an anonymous user.
Want to know more? Visit the Converter page.

\newdateformat

UKvardate \monthname[\THEMONTH] \THEYEAR

A Dedekind-style axiomatization and the corresponding universal property of an ordinal number system

Zurab Janelidze and Ineke van der Berg
Abstract

In this paper, we give an axiomatization of the ordinal number system, in the style of Dedekind’s axiomatization of the natural number system. The latter is based on a structure (N,0,s)(N,0,s) consisting of a set NN, a distinguished element 0N0\in N and a function s:NNs\colon N\to N. The structure in our axiomatization is a triple (O,L,s)(O,L,s), where OO is a class, LL is a class function defined on all ss-closed ‘subsets’ of OO, and ss is a class function s:OOs\colon O\to O. In fact, we develop the theory relative to a Grothendieck-style universe (minus the power set axiom), as a way of bringing the natural and the ordinal cases under one framework. We also establish a universal property for the ordinal number system, analogous to the well-known universal property for the natural number system.

Introduction

The introduction and study of ordinal numbers goes back to the pioneering works of Cantor in set theory [2, 3]. In modern language, Cantor’s ordinal numbers are isomorphic classes of well-ordered sets, see e.g. [5]. There is also a ‘concrete’ definition of an ordinal number as a transitive set which is well-ordered under the element relation – see e.g. [7]. Such sets are usually called von Neumann ordinals. Natural numbers can be seen concretely as the finite ordinal numbers. In Dedekind’s approach to the natural number system described in [4], the natural numbers are not defined as concrete objects, but rather as abstract entities organized in a certain structure; namely, a triple (N,0,s)(N,0,s) consisting of a set NN (a set of ‘abstract’ natural numbers), a distinguished element 0 of NN (in [4], the distinguished element is 1), and a function s:NNs\colon N\to N, which names the ‘successor’ of each natural number. The axioms that such a system should satisfy were formulated by Dedekind, but are often referred to as Peano axioms today (see e.g. [13] for some historical background):

  • 0 does not belong to the image of ss.

  • ss is injective.

  • X=NX=N for any subset XX of NN that is closed under ss and contains 0.

It is an observation due to Lawvere [10] that these axioms identify the natural number systems as initial objects in the category of all triples (X,x,t)(X,x,t) where XX is a set, xXx\in X and tt is a function t:XXt\colon X\to X. This ‘universal property’ of the natural number system, freed from its category-theoretic formulation, is actually the ‘definition by induction’ theorem already contained in [4]. A morphism (N,0,s)(X,x,t)(N,0,s)\to(X,x,t) of such triples is defined as a function f:NXf\colon N\to X such that:

  • f(0)=xf(0)=x,

  • f(s(n))=t(f(n))f(s(n))=t(f(n)) for all nNn\in N.

The ‘definition by induction’ theorem states that there is exactly one morphism to any other triple (X,x,t)(X,x,t) from the triple (N,0,s)(N,0,s) satisfying the axioms stated above. This theorem is of course well known because of its practical use: it says that recursively defined functions exist and are uniquely determined by the recursion. Intuitively, the theorem can be understood as follows. A triple (X,x,t)(X,x,t) can be viewed as an abstraction of the concept of counting – XX is the set of figures used in counting, xx is where counting begins and the function tt names increments when counting. Without further restrictions on such ‘counting systems’, there are many non-isomorphic ones, some of which are quite different from the natural number system, but still useful; for instance, hours on a clock, where counting loops back to 11 once we pass 1212. A morphism of these triples can be viewed as a ‘translation’ of one counting system to another. The universal property of the natural number system presents it as a ‘universal’ counting system, in the sense that it has a unique translation to any other counting system. Incidentally, such intuition is not particular to the natural number system: many structures in mathematics can be defined by natural universal properties – see [11].

Ordinal numbers exhibit a similar structure to natural numbers – there is a ‘starting’ ordinal (the natural number 0), and every ordinal number has a successor. The natural numbers 0,1,2,3,0,1,2,3,\ldots are the first ordinal numbers. This set is closed under succession. The ordinal number system allows for another type of succession that can be applied to sets of ordinal numbers closed under succession, giving rise to the so-called ‘limit’ ordinal numbers. The infinite sequence of natural numbers is succeeded by a limit ordinal number, usually denoted by ω\omega. Now, we can take the ‘usual’ successor of ω\omega, call it ω+1\omega+1, and keep taking its successors until we get another set that is closed under succession, after which we introduce another limit ordinal number – it will be ω+ω=ω2\omega+\omega=\omega\cdot 2. The next limit ordinal number will be ω3\omega\cdot 3. At some point, we reach ωω=ω2\omega\cdot\omega=\omega^{2}, then ω3\omega^{3}, and so on until we reach ωω\omega^{\omega}, then ωω+1\omega^{\omega}+1, and so on…The process is supposed to continue until all ordinal numbers that we have named no longer form a set. Let us also recall that von Neumann ordinals are defined as sets of preceding ordinals. Thus the first ordinal number, the number 0, is defined as 0=0=\varnothing and the successor of an ordinal number nn is defined as 𝖴{n,{n}}\mathsf{U}\{n,\{n\}\}. A limit ordinal number is one that is the union of all preceding ordinal numbers. We can, in particular, think of 0 as a limit ordinal number given by the union of its predecessors, since the empty union equals the empty set. Equivalently, limit ordinal numbers are those whose sets of predecessors are closed under succession.

We may also think of the ordinal number system in terms of a triple (O,L,s)(O,L,s) – this time, OO is a class (since the collection of all ordinal numbers is no longer a set), LL is a (class) function that specifies limit ordinals and is defined for those subclasses of OO which form sets closed under the class function ss, which specifies the successor of each ordinal. In this paper we show that the following three axioms on such a triple are suitable as analogues of the three Dedekind-Peano axioms for the ordinal number system:

  • L(I)L(I) does not belong to the image of ss, and also s(L(I))Is(L(I))\notin I, for any II such that L(I)L(I) is defined.

  • ss is injective and L(I)=L(J)L(I)=L(J) if and only if I¯=J¯\overline{I}=\overline{J} and L(I),L(J)L(I),L(J) are defined, where I¯\overline{I} and J¯\overline{J} denote closures of II and JJ, respectively, under ss and LL predecessors.

  • X=OX=O for any subclass XX of OO that is closed under ss and that contains L(I)L(I) for each IXI\subseteq X such that L(I)L(I) is defined.

In particular, we prove that:

  • The system of von Neumann ordinals constitutes a triple (O,L,s)(O,L,s) satisfying the three axioms above. There is nothing surprising here, as the result relies on the well-known properties of ordinal numbers.

  • Any triple (O,L,s)(O,L,s) satisfying these three axioms has an order which makes it order-isomorphic to the system of ordinal numbers. The order, in fact, is the specialization order of the topology given by the closure operator in the second axiom (without those axioms, this order is merely a preorder).

  • The triple (O,L,s)(O,L,s) satisfying the three axioms above is an initial object in the category of all triples (O,L,s)(O^{\prime},L^{\prime},s^{\prime}) such that I¯=J¯\overline{I^{\prime}}=\overline{J^{\prime}} implies L(I)=L(J)L(I^{\prime})=L(J^{\prime}), whenever those are defined (with the domain of LL^{\prime} being the class of all ss^{\prime}-closed subsets of OO^{\prime}).

The idea for defining an ordinal number system abstractly goes back to Zermelo (see ‘Seven notes on ordinal numbers and large cardinals’ in [15]). His approach is to define it as a particular type of well-ordered class (O,)(O,\leqslant). The following axioms would suffice:

  • For every xOx\in O, the class {x}>={yOy<x}\{x\}^{>}=\{y\in O\mid y<x\} is a set.

  • For each subset XX of OO, the class X<={yOxX[x<y]}X^{<}=\{y\in O\mid\forall_{x\in X}[x<y]\} is non-empty.

There is, of course, an analogous presentation (although less known than the one given by Peano axioms) of the natural number system as a well-ordered set (N,)(N,\leqslant) satisfying the following conditions:

  • For each xNx\in N, the set {x}>\{x\}^{>} is finite.

  • For each xNx\in N, the set {x}<\{x\}^{<} is non-empty.

This is an alternative approach to that of Dedekind, where there is greater emphasis on the order structure. The difference between our approach to ordinal numbers and the traditional approaches is similar, where in our approach we try to make minimal use of the order structure. Universal properties of the ordinal number system emerging from the more order-based approach have been established in [8]. Our universal property is different from those.

The main new results of the paper are given in the last two sections. Before that, we redevelop the basic theory of ordinal numbers relative to the set-theoretic context in which these results are proved, ensuring that the paper is self-contained.

1 The context

There are a number of alternatives for a context in which the theory that we lay down in this paper could be developed. Elaboration of those contexts and comparison of results across the contexts as a future development of our work would certainly be worthwhile. In this paper, we have decided to stick to what we believe to be technically the most simple and intuitive context, given by a ‘universe’ inside the standard Zermelo-Fraenkel axiomatic set theory, including the axioms of foundation and choice (see e.g. [7]). Developing mathematics relative to a universe is typical in those subjects where sets of different sizes are needed. For instance, this is the approach followed in the exposition of category theory in [11]. The universes we work with, however, are slightly more general than the more commonly used Grothendieck universes [1, 6, 14]. The main difference is that our universes do not require closure under power sets and can be empty. Our context is in fact a particular instance of the quite general category-theoretic context used in [8]. Generalization of our results to that context is left for future work.

We remark that the definitions, theorems and their proofs contained in this paper could be adapted, after a straightforward modification to their formulation to ‘absolute’ set theory, where our ‘sets’ could be replaced with ‘classes’ and elements of the fixed universe with ‘sets’. We would then get the form of the definitions and theorems given in the Introduction.

For a set XX, by 𝖯X\mathsf{P}X we denote the power set of XX, and by 𝖴X\mathsf{U}X we denote the union of all elements of XX. By \mathbb{N} we denote the set of natural numbers. While we do not rely on any prior knowledge of facts about ordinal numbers (proofs of all needed facts are included in the paper), we do rely on knowledge of basic set-theoretic properties of the natural number system. In particular, we will make use of mathematical induction, definition by recursion, as well as the fact that any infinite set has a subset bijective to \mathbb{N}.

Recall that a set XX is said to be transitive when X𝖯XX\subseteq\mathsf{P}X, or equivalently, when 𝖴XX\mathsf{U}X\subseteq X. For a function f:XYf\colon X\to Y and a set A𝖯XA\in\mathsf{P}X, we write fAfA to denote the image of AA under ff:

fA={f(a)aA}.\displaystyle fA=\{f(a)\mid a\in A\}.
Definition 1.

A universe is a set 𝔘\mathfrak{U} satisfying the following:

  • (U1)

    𝔘\mathfrak{U} is a transitive set.

  • (U2)

    If X,Y𝔘X,Y\in\mathfrak{U} then {X,Y}𝔘\{X,Y\}\in\mathfrak{U}.

  • (U3)

    𝖴fI𝔘\mathsf{U}fI\in\mathfrak{U} for any I𝔘I\in\mathfrak{U} and any function f:I𝔘f\colon I\to\mathfrak{U}.

These axioms imply that 𝔘\mathfrak{U} is closed under the following standard set-theoretic constructions:

  • Singletons. Trivially, since {x}={x,x}\{x\}=\{x,x\}.

  • Union. Because 𝖴X=𝖴1XX\mathsf{U}X=\mathsf{U}1_{X}X.

  • Subsets. Let XYX\subseteq Y. If Y𝔘Y\in\mathfrak{U} and X=X=\varnothing, then X𝔘X\in\mathfrak{U} because 𝔘\mathfrak{U} is a transitive set (thanks to the axiom of foundation). If XX\neq\varnothing then let x0Xx_{0}\in X. Consider the function f:Y𝔘f\colon Y\to\mathfrak{U} defined by

    f(y)={{y},yX,{x0},yX,\displaystyle f(y)=\begin{cases}\{y\},&y\in X,\\ \{x_{0}\},&y\notin X,\end{cases}

    Then X=𝖴fYX=\mathsf{U}fY and so X𝔘X\in\mathfrak{U}.

  • Cartesian products (binary). Let X𝔘X\in\mathfrak{U} and Y𝔘Y\in\mathfrak{U}. Then

    {(x,y)}={{{x,y},{x}}}𝔘\displaystyle\{(x,y)\}=\{\{\{x,y\},\{x\}\}\}\in\mathfrak{U}

    for each xXx\in X and yYy\in Y. For each xXx\in X define a function fx:Y𝔘f_{x}\colon Y\to\mathfrak{U} by fx(y)={(x,y)}f_{x}(y)=\{(x,y)\}. Then {(x,y)yY}=𝖴fxY𝔘\{(x,y)\mid y\in Y\}=\mathsf{U}f_{x}Y\in\mathfrak{U} for each xXx\in X. Now define a function g:X𝔘g\colon X\to\mathfrak{U} by g(x)={{(x,y)yY}}g(x)=\{\{(x,y)\mid y\in Y\}\}. Then, X×Y=𝖴gX𝔘X\times Y=\mathsf{U}gX\in\mathfrak{U}.

  • Disjoint union. Given X𝔘X\in\mathfrak{U}, the disjoint union ΣX\Sigma X can be defined as

    ΣX=𝖴{x×{x}xX}.\displaystyle\Sigma X=\mathsf{U}\{x\times\{x\}\mid x\in X\}.

    Then ΣX=𝖴fX\Sigma X=\mathsf{U}fX where f:X𝔘f\colon X\to\mathfrak{U} is defined by f(x)=x×{x}f(x)=x\times\{x\}.

  • Quotient sets. Let X𝔘X\in\mathfrak{U} and let EE be an equivalence relation on XX. Then X/E=𝖴qXX/E=\mathsf{U}qX, where qq is the function q:X𝔘q\colon X\to\mathfrak{U} defined by q(x)={[x]E}q(x)=\{[x]_{E}\}.

From this it follows of course that when 𝔘\mathfrak{U} is not empty, it contains all natural numbers, assuming that they are defined by the recursion

0\displaystyle 0 =,\displaystyle=\varnothing,
n+1\displaystyle n+1 =𝖴{n,{n}}.\displaystyle=\mathsf{U}\{n,\{n\}\}.

Furthermore, when 𝔘\mathfrak{U} contains at least one infinite set, it also contains the set \mathbb{N} of all natural numbers (as defined above).

The empty set \varnothing is a universe. The sets whose transitive closure have cardinality less than a fixed infinite cardinal κ\kappa form a universe in the sense of the definition above (by Lemma 6.4 in [9]). In particular, hereditarily finite sets form a universe, as do hereditarily countable sets. The so-called Grothendieck universes are exactly those universes in our sense, which are closed under power sets, i.e. if X𝔘X\in\mathfrak{U}, then 𝖯X𝔘\mathsf{P}X\in\mathfrak{U}.

For any two sets AA and BB, we write

AB\displaystyle A\approx B

when there is a bijection from AA to BB. The restricted power set of a set XX relative to a universe 𝔘\mathfrak{U} is the set

𝖯𝔘X={AXB𝔘[AB]}.\displaystyle\mathsf{P}_{\mathfrak{U}}X=\{A\subseteq X\mid\exists_{B\in\mathfrak{U}}[A\approx B]\}.

The following lemmas will be useful.

Lemma 2.

When 𝔘\mathfrak{U} is non-empty, for any set XX and its finite subset YXY\subseteq X, we have Y𝖯𝔘XY\in\mathsf{P}_{\mathfrak{U}}X.

Proof.

This follows from the fact that when 𝔘\mathfrak{U} is non-empty, it contains a set of each finite size. ∎

Lemma 3.

If ABA\subseteq B and B𝖯𝔘XB\in\mathsf{P}_{\mathfrak{U}}X, then A𝖯𝔘XA\in\mathsf{P}_{\mathfrak{U}}X.

Proof.

If ABC𝔘A\subseteq B\approx C\in\mathfrak{U}, then AA is bijective to a subset of CC. ∎

Lemma 4.

If A,B𝖯𝔘XA,B\in\mathsf{P}_{\mathfrak{U}}X then 𝖴{A,B}𝖯𝔘X\mathsf{U}\{A,B\}\in\mathsf{P}_{\mathfrak{U}}X. Also, if I𝖯𝔘XI\in\mathsf{P}_{\mathfrak{U}}X, then for any function f:I𝖯𝔘Xf\colon I\to\mathsf{P}_{\mathfrak{U}}X, we have: 𝖴fI𝖯𝔘X\mathsf{U}fI\in\mathsf{P}_{\mathfrak{U}}X.

Proof.

Let AAA\approx A^{\prime} and BBB\approx B^{\prime} where A,B𝔘A^{\prime},B^{\prime}\in\mathfrak{U}. Then 𝖴{A,B}\mathsf{U}\{A,B\} is bijective to a suitable quotient set of a disjoint union of AA^{\prime} and BB^{\prime}. Next, to prove the second part of the lemma, suppose IJ𝔘I\approx J\in\mathfrak{U} and for each xIx\in I, suppose f(x)g(x)𝔘f(x)\approx g(x)\in\mathfrak{U}. Let hh denote a bijection h:JIh\colon J\to I. Define a function f:J𝔘f^{\prime}\colon J\to\mathfrak{U} by f(x)={gh(x)}f^{\prime}(x)=\{gh(x)\}. Then fI𝖴fJfI\approx\mathsf{U}f^{\prime}J. The union 𝖴fI\mathsf{U}fI will then be bijective to a suitable disjoint union of 𝖴fJ\mathsf{U}f^{\prime}J. ∎

Lemma 5.

Given a function f:XYf\colon X\to Y,

A𝖯𝔘XfA𝖯𝔘Y.\displaystyle A\in\mathsf{P}_{\mathfrak{U}}X\quad\Rightarrow\quad fA\in\mathsf{P}_{\mathfrak{U}}Y.
Proof.

If AA𝔘A\approx A^{\prime}\in\mathfrak{U}, then fAfA is bijective to a suitable quotient of AA^{\prime}. ∎

Lemma 6.

If A𝖯𝔘XA\in\mathsf{P}_{\mathfrak{U}}X and B𝖯𝔘YB\in\mathsf{P}_{\mathfrak{U}}Y, then A×B𝖯𝔘(X×Y)A\times B\in\mathsf{P}_{\mathfrak{U}}(X\times Y).

Proof.

This follows from the fact that 𝔘\mathfrak{U} is closed under cartesian products. ∎

Lemma 7.

𝖯𝔘𝔘𝔘\mathsf{P}_{\mathfrak{U}}\mathfrak{U}\subseteq\mathfrak{U}.

Proof.

Let ABA\approx B, A𝔘A\subseteq\mathfrak{U} and B𝔘B\in\mathfrak{U}. Write ff for a bijection f:BAf\colon B\to A. Consider the function g:B𝔘g\colon B\to\mathfrak{U} defined by g(b)={f(b)}g(b)=\{f(b)\}. Then A=𝖴gBA=\mathsf{U}gB and so A𝔘A\in\mathfrak{U}. ∎

2 Abstract ordinals

In this section we introduce an abstract notion of an ordinal number system relative to a universe and establish its basic properties. Consider a partially ordered set (X,)(X,\leqslant). The relation << for the partial order, as a relation from XX to XX, induces a Galois connection from 𝖯X\mathsf{P}X to itself given by the mappings

SS>\displaystyle S\mapsto S^{>} ={xXyS[x<y]}, and\displaystyle=\{x\in X\mid\forall_{y\in S}[x<y]\},\text{ and}
SS<\displaystyle S\mapsto S^{<} ={xXyS[y<x]}.\displaystyle=\{x\in X\mid\forall_{y\in S}[y<x]\}.

We call S>S^{>} the lower complement of SS, and S<S^{<} the upper complement of SS. Note that by ‘a<ba<b’ above we mean ‘ababa\leqslant b\land a\neq b’, as usual. Since the two mappings above form a Galois connection, we have

S(S>)< and S(S<)>\displaystyle S\subseteq(S^{>})^{<}\textrm{ and }S\subseteq(S^{<})^{>}

for any SXS\subseteq X. We define the incremented join

+

S
\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S
of a subset SS of XX (when it exists) as follows:

+S=min(S<).\displaystyle\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S=\min(S^{<}).

Note that since SS<=S\cap S^{<}=\varnothing, the incremented join of SS is never an element of SS. It will be convenient to use the following abbreviations (where xXx\in X and SXS\subseteq X):

x+=+{x},S+={x+xS}.\displaystyle x^{+}=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}\{x\},\quad S^{+}=\{x^{+}\mid x\in S\}.

Note that for any SXS\subseteq X such that x+x^{+} exists for all xSx\in S,

+S\displaystyle\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S =min{xyS[y<x]}\displaystyle=\min\{x\mid\forall_{y\in S}[y<x]\}
=min{xyS[y+x]}\displaystyle=\min\{x\mid\forall_{y\in S}[y^{+}\leqslant x]\}
=min{xyS+[yx]}\displaystyle=\min\{x\mid\forall_{y\in S^{+}}[y\leqslant x]\}
=S+.\displaystyle=\bigvee S^{+}.

Furthermore, the following basic laws are self-evident:

  1. (L1)

    x<x+x<x^{+},

  2. (L2)

    there is no zz such that x<z<x+x<z<x^{+},

  3. (L3)

    x<yx+yx<y\;\Leftrightarrow\;x^{+}\leqslant y,

  4. (L4)

    x=

    +

    {x}>
    x=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}\{x\}^{>}
    (for a total order),

  5. (L5)

    x<y+xyx<y^{+}\;\Leftrightarrow\;x\leqslant y (for a total order),

  6. (L6)

    x+=y+x=yx^{+}=y^{+}\;\Leftrightarrow\;x=y (for a total order),

  7. (L7)

    x<yx+<y+x<y\;\Leftrightarrow\;x^{+}<y^{+} (for a total order).

The following (easy) lemma will also be useful:

Lemma 8.

Let (X,)(X,\leqslant) be a poset and let SXS\subseteq X. Then:

  1. (i)

    If SS does not have a largest element, then S\bigvee S exists if and only if

    +

    S
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S
    exists, and when they exist they are equal, S=

    +

    S
    \bigvee S=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S
    . Conversely, if S=

    +

    S
    \bigvee S=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S
    then SS does not have a largest element.

  2. (ii)

    If SS has a largest element x=maxSx=\max S, then

    +

    S
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S
    exists if and only if x+x^{+} exists, and when they exist,

    +

    S
    =x+
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S=x^{+}
    . Conversely, when \leqslant is a total order, if

    +

    S
    =x+
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S=x^{+}
    then x=maxSx=\max S.

  3. (iii)

    If

    +

    S>
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S^{>}
    exists then

    +

    S>
    =minS
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S^{>}=\min S
    . Conversely, when \leqslant is a total order, if minS\min S exists, then minS=

    +

    S>
    \min S=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S^{>}
    .

Proof.
  1. (i)

    If SS has no largest element, then

    {xXyS[yx]}={xXyS[y<x]}\displaystyle\{x\in X\mid\forall_{y\in S}[y\leqslant x]\}=\{x\in X\mid\forall_{y\in S}[y<x]\}

    and so

    S=min{xXyS[yx]}\displaystyle\bigvee S=\min\{x\in X\mid\forall_{y\in S}[y\leqslant x]\}

    exists if and only if

    +S=min{xXyS[y<x]}\displaystyle\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S=\min\{x\in X\mid\forall_{y\in S}[y<x]\}

    exists, and when they exist, they are equal. Now suppose S=

    +

    S
    \bigvee S=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S
    . Since

    +

    S
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S
    is never an element of SS, we conclude that SS does not have a largest element.

  2. (ii)

    Let x=maxSx=\max S. Then {x}<=S<\{x\}^{<}=S^{<}, and so x+=min({x}<)x^{+}=\min(\{x\}^{<}) exists if and only if

    +

    S
    =min(S<)
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S=\min(S^{<})
    exists, and when they exist, they are equal. Now suppose, in the case of total order, that

    +

    S
    =x+
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S=x^{+}
    for some xXx\in X. Then SS can only have elements that are strictly smaller than x+x^{+}, and thus each element of SS is less than or equal to xx (L5). Also, since x+=

    +

    S
    =min(S<)
    x^{+}=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S=\min(S^{<})
    , it does not hold that xS<x\in S^{<}, and thus xx is not strictly larger than every element of SS. We can conclude that x=max(S)x=\max(S).

  3. (iii)

    Suppose

    +

    S>
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S^{>}
    exists. Since S(S>)<S\subseteq(S^{>})^{<}, we must have

    +

    S>
    x
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S^{>}\leqslant x
    for each xSx\in S. This together with the fact that

    +

    S>
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S^{>}
    cannot be an element of S>S^{>} forces

    +

    S>
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S^{>}
    to be an element of SS. Hence

    +

    S>
    =minS
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S^{>}=\min S
    . Suppose now that \leqslant is a total order and minS\min S exists. Consider an element x(S>)<x\in(S^{>})^{<}. Then xx is not an element of S>S^{>} and so we cannot have x<minSx<\min S. Therefore, minSx\min S\leqslant x. This proves minS=

    +

    S>
    \min S=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}S^{>}
    . ∎

Definition 9.

An ordinal system relative to a universe 𝔘\mathfrak{U} is a partially ordered set 𝒪=(𝒪,)\mathcal{O}=(\mathcal{O},\leqslant) satisfying the following axioms:

  • (O1)

    For all X𝒪X\subseteq\mathcal{O}, if XX\neq\varnothing, then X>𝖯𝔘𝒪X^{>}\in\mathsf{P}_{\mathfrak{U}}\mathcal{O}.

  • (O2)

    +

    X
    \operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}X
    exists for each X𝖯𝔘𝒪X\in\mathsf{P}_{\mathfrak{U}}\mathcal{O}.

We refer to elements of 𝒪\mathcal{O} as ordinals.

Note that if 𝒪\mathcal{O} is non-empty, then Axiom (O1) forces the universe 𝔘\mathfrak{U} to be non-empty as well. So for any ordinal x𝒪x\in\mathcal{O} we have {x}𝖯𝔘𝒪\{x\}\in\mathsf{P}_{\mathfrak{U}}\mathcal{O} (Lemma 2). Note also that Axiom (O1) is equivalent to its weaker form (the equivalence does not require (O2) and relies on Lemma 3):

  1. (O1)

    {x}>𝖯𝔘𝒪\{x\}^{>}\in\mathsf{P}_{\mathfrak{U}}\mathcal{O} for all x𝒪x\in\mathcal{O}.

Axiom (O2) implies that the mapping xx+x\mapsto x^{+} is a function 𝒪𝒪\mathcal{O}\to\mathcal{O}. We call this function the successor function of the ordinal system 𝒪\mathcal{O}. For each x𝒪x\in\mathcal{O}, an element of 𝒪\mathcal{O} that has the form x+x^{+} is called a successor ordinal and the successor of xx. We call an ordinal that is not a successor ordinal a limit ordinal.

Recall that a poset is a well-ordered set when each of its nonempty subsets has smallest element.

Theorem 10.

A poset (𝒪,)(\mathcal{O},\leqslant) is an ordinal system relative to a universe 𝔘\mathfrak{U} if and only if it is a well-ordered set (and consecutively, a totally ordered set) satisfying (O1) and such that X<X^{<}\neq\varnothing for all X𝖯𝔘(𝒪)X\in\mathsf{P}_{\mathfrak{U}}(\mathcal{O}).

Proof.

Consider an ordinal system 𝒪\mathcal{O} relative to a universe 𝔘\mathfrak{U}. Let XX be a non-empty subset of 𝒪\mathcal{O}. Then X>𝖯𝔘𝒪X^{>}\in\mathsf{P}_{\mathfrak{U}}\mathcal{O} by (O1), and thus

+

X>
\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}X^{>}
exists by (O2). By Lemma 8(iii),

+

X>
=minX
\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}X^{>}=\min X
. This proves the ‘only if’ part of the theorem. Note that any well-ordered set is totally ordered: having a smallest element of a two-element subset {x,y}\{x,y\} forces xx and yy to be comparable. The ‘if’ part is quite obvious. ∎

We will use this theorem often without referring to it. One of its consequences is that each non-empty ordinal system has a smallest element. We denote this element by 0. Note that 0 is a limit ordinal. Since by the same theorem an ordinal system is a total order, the properties (L4–7) above apply to an ordinal system. In particular, we get that the successor function is injective. We also get the following:

Lemma 11.

In an ordinal system, for an ordinal xx the following conditions are equivalent:

  1. (i)

    xx is a limit ordinal.

  2. (ii)

    {x}>\{x\}^{>} is closed under successors.

  3. (iii)

    x={x}>x=\bigvee\{x\}^{>}.

Proof.

We have x=

+

{x}>
x=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}\{x\}^{>}
for any ordinal xx (L4). If xx is a limit ordinal then for each y<xy<x we have y+<xy^{+}<x (L3). So (i){}\Rightarrow{}(ii). If (ii) holds, by by (L1), we get that {x}>\{x\}^{>} does not have a largest element. So

+

{x}>={x}>
\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}\{x\}^{>}=\bigvee\{x\}^{>}
(Lemma 8). This gives (ii){}\Rightarrow{}(iii). Suppose now x={x}>x=\bigvee\{x\}^{>}. If xx were a successor ordinal x=y+x=y^{+}, then by (L5), yy would be the join of {x}>\{x\}^{>}. However, xyx\neq y by (L1), and therefore, xx must be a limit ordinal. Thus, (iii){}\Rightarrow{}(i). ∎

The following theorem gives yet another way of thinking about an abstract ordinal number system.

Theorem 12.

A poset (𝒪,)(\mathcal{O},\leqslant) is an ordinal system relative to a universe 𝔘\mathfrak{U} if and only if (O1) holds along with the following axioms:

  • (O22a)

    For all X𝖯𝔘𝒪X\in\mathsf{P}_{\mathfrak{U}}\mathcal{O}, the join X\bigvee X exists.

  • (O22b)

    x+x^{+} exists for each x𝒪x\in\mathcal{O}.

Proof.

This can easily be proved using (i) and (ii) of Lemma 8. ∎

Transfinite induction and recursion are well known for well-ordered sets. We formulate them here (in one particular form, out of many possibilities) in the case of ordinal systems, since we will use them later on in the paper. We have included our own direct proofs, for the sake of completeness, but we do not expect these proofs to have any new arguments that do not already exist in the literature.

Theorem 13 (transfinite induction).

Let 𝒪\mathcal{O} be an ordinal system and let X𝒪X\subseteq\mathcal{O} satisfy the following conditions:

  • (I1)

    X+XX^{+}\subseteq X;

  • (I2)

    for every limit ordinal xx, if {x}>X\{x\}^{>}\subseteq X then xXx\in X.

Then X=𝒪X=\mathcal{O}.

Proof.

Since 𝒪\mathcal{O} is well-ordered, if 𝒪X\mathcal{O}\setminus X is non-empty then it has a smallest element yy. By (I1), yy cannot be a successor of any z<yz<y in XX. By (I2), it also cannot be a limit ordinal. This is a contradiction since a limit ordinal is defined as one that is not a successor ordinal. ∎

Here is one of the immediate consequences of transfinite induction (the proof will require also the total order of an ordinal system, as well as the properties (L3) and (L4)):

Corollary 14.

Let 𝒪\mathcal{O} be an ordinal system relative to a universe 𝔘\mathfrak{U} and let X𝒪X\subseteq\mathcal{O} satisfy the following conditions:

  • (S1)

    XX is down-closed in 𝒪\mathcal{O}, i.e., if x<yXx<y\in X then xXx\in X, for all x,y𝒪x,y\in\mathcal{O};

  • (S2)

    XX is an ordinal system relative to 𝔘\mathfrak{U} under the restriction of the order of 𝒪\mathcal{O}.

Then X=𝒪X=\mathcal{O}.

Theorem 15 (transfinite recursion).

Let 𝒪\mathcal{O} be an ordinal system and let X=(X,V,T)X=(X,V,T), where XX is a set, TT is a function XXX\to X and VV is a function 𝖯𝔘XX\mathsf{P}_{\mathfrak{U}}X\to X. Then there exists a unique function f:𝒪Xf\colon\mathcal{O}\to X that satisfies the following conditions:

  • (R1)

    f(x+)=T(f(x))f(x^{+})=T(f(x)) for any x𝒪x\in\mathcal{O},

  • (R2)

    f(x)=V({f(y)y<x})f(x)=V(\{f(y)\mid y<x\}) for any limit ordinal xx.

Proof.

For each ordinal x𝒪x\in\mathcal{O}, let FxF_{x} be the set consisting of all functions

fx:{y𝒪yx}X\displaystyle f_{x}\colon\{y\in\mathcal{O}\mid y\leqslant x\}\to X

that satisfy the following conditions:

  1. (i)

    f(y+)=T(f(y))f(y^{+})=T(f(y)) for any successor ordinal y+xy^{+}\leqslant x, and

  2. (ii)

    f(y)=V({f(z)z<y})f(y)=V(\{f(z)\mid z<y\}) for any limit ordinal yxy\leqslant x.

Note that any function ff satisfying (R1–2) must have a subfunction in each set FxF_{x}. Also, for any x𝒪x\in\mathcal{O}, a function fxFxf_{x}\in F_{x} must have a subfunction in each set FyF_{y} where y<xy<x. We prove by transfinite induction that for each x𝒪x\in\mathcal{O}, the set FxF_{x} contains exactly one function fxf_{x}.

Successor case.

Suppose that for some ordinal xx and each yxy\leqslant x there exists a unique function fyFyf_{y}\in F_{y}. Then g=𝖴{fx,{(x+,T(fx(x)))}}g=\mathsf{U}\{f_{x},\{(x^{+},T(f_{x}(x)))\}\} satisfies (i,ii) and thus gFx+g\in F_{x^{+}}.

Now consider any function gFx+g^{\prime}\in F_{x^{+}}. Since gg and gg^{\prime} must both have the unique function fxFxf_{x}\in F_{x} as a subfunction, gg and gg^{\prime} are identical on the domain {yyx}\{y\mid y\leqslant x\}. But since gg and gg^{\prime} both satisfy condition (i), we get that g(x+)=T(fx(x))=g(x+)g^{\prime}(x^{+})=T(f_{x}(x))=g(x^{+}) and thus g=gg^{\prime}=g.

Limit case.

Suppose that for some limit ordinal xx and each y<xy<x there exists a unique function fyFyf_{y}\in F_{y}. Then for any two ordinals y<y<xy<y^{\prime}<x, the function fyf_{y} is a subfunction of fyf_{y^{\prime}}, which is in turn a subfunction of every function in FxF_{x}. The relation

g=𝖴{{(x,V({fy(y)y<x}))},𝖴{fyy<x}}\displaystyle g=\mathsf{U}\{\{(x,V(\{f_{y}(y)\mid y<x\}))\},\mathsf{U}\{f_{y}\mid y<x\}\}

is then a function over the domain {yyx}\{y\mid y\leqslant x\} and moreover, it is easy to see that gFxg\in F_{x}.

Now consider any function gFxg^{\prime}\in F_{x}. Since for each ordinal y<xy<x the unique function fyFyf_{y}\in F_{y} is a subfunction of both gg and gg^{\prime}, we see that they are identical on the domain {yy<x}\{y\mid y<x\}, and since they both satisfy condition (ii), the following holds:

g(x)=V({g(y)y<x})=V({g(y)y<x})=g(x).\displaystyle g(x)=V(\{g(y)\mid y<x\})=V(\{g^{\prime}(y)\mid y<x\})=g^{\prime}(x).

We can conclude that g=gg^{\prime}=g and thus gg is the unique function in FxF_{x}.

We showed that for each ordinal xx, exactly one function fxFxf_{x}\in F_{x} exists. Construct a function f:𝒪Xf\colon\mathcal{O}\to X as follows: for each ordinal xx,

f(x)=fx(x).\displaystyle f(x)=f_{x}(x).

It satisfies (R1–2) because each fxf_{x} satisfies (i,ii). Since any function satisfying (R1–2) must have a subfunction in each set FxF_{x}, we can conclude that ff is the unique function satisfying (R1–2). ∎

3 Concrete ordinals

For a universe 𝔘\mathfrak{U}, define a 𝔘\mathfrak{U}-ordinal to be a transitive set that belongs to the universe 𝔘\mathfrak{U} and is a well-ordered set under the relation

xy[xy][x=y].\displaystyle x\mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}y\quad\Leftrightarrow\quad[x\in y]\lor[x=y].

Thus, a 𝔘\mathfrak{U}-ordinal is nothing but a usual von Neumann ordinal number [12] that happens to be an element of 𝔘\mathfrak{U}. In other words, it is a von Neumann ordinal number internal to the universe 𝔘\mathfrak{U}. Thus, at least one direction in the following theorem is well known. We include a full proof for completeness.

Theorem 16.

A set OO is the set of all 𝔘\mathfrak{U}-ordinals if and only if the following conditions hold:

  1. (i)

    O\varnothing\in O provided 𝔘\varnothing\in\mathfrak{U} (𝔘\Leftrightarrow\mathfrak{U}\neq\varnothing), and O𝔘O\subseteq\mathfrak{U},

  2. (ii)

    OO is a transitive set,

  3. (iii)

    OO is an ordinal system relative to 𝔘\mathfrak{U} under the relation \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}.

When these conditions hold, the incremented join of X𝖯𝔘OX\in\mathsf{P}_{\mathfrak{U}}O is given by

+

X
=𝖴{𝖴X,X}
\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}X=\mathsf{U}\{\mathsf{U}X,X\}
.

Proof.

Let OO be the set of all 𝔘\mathfrak{U}-ordinals. Then (i) follows easily from the definition of a 𝔘\mathfrak{U}-ordinal. To show (ii), let yxOy\in x\in O. We want to show that yy is a 𝔘\mathfrak{U}-ordinal. Since x𝔘x\in\mathfrak{U} also y𝔘y\in\mathfrak{U} by (U1). Since yxy\subseteq x and xx is well-ordered (under \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}), so is yy. Next, we must prove that yy is transitive. Let zyz\in y. Then zxz\in x since xx is transitive. We want to show zyz\subseteq y, so suppose tzt\in z. Then txt\in x. By the fact that \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}} is an order on xx, we must have tyt\mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}y. We cannot have t=yt=y, since tzyt\in z\in y, and so tyt\in y. Next, we prove (iii). It is easy to see that the relation \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}} is a partial order on OO: reflexivity is obvious, while transitivity follows from each element of OO being a transitive set. To prove (O1), consider xOx\in O. Then we have:

{x}>={yOyx}x.\displaystyle\{x\}^{>}=\{y\in O\mid y\in x\}\subseteq x.

Since xx is a 𝔘\mathfrak{U}-ordinal, x𝖯𝔘Ox\in\mathsf{P}_{\mathfrak{U}}O and so {x}>𝖯𝔘O\{x\}^{>}\in\mathsf{P}_{\mathfrak{U}}O (Lemma 3). Note that by (ii) we actually have x={x}>x=\{x\}^{>}, although we did not need this to establish (O1).

For what follows, we will first establish the following:

Fact 1.

xy=min(yx)x\cap y=\min(y\setminus x) for any two 𝔘\mathfrak{U}-ordinals xx and yy such that yxy\setminus x\neq\varnothing.

Let axya\in x\cap y. Then ayxa\notin y\setminus x. Hence amin(yx)a\neq\min(y\setminus x). By the well-ordering of yy, we then get that either amin(yx)a\in\min(y\setminus x) or min(yx)a\min(y\setminus x)\in a. By transitivity of xx and the fact that min(yx)x\min(y\setminus x)\notin x, the second option is excluded. So amin(yx)a\in\min(y\setminus x). This shows xymin(yx)x\cap y\subseteq\min(y\setminus x). Now suppose amin(yx)a\in\min(y\setminus x). Then aya\in y, by transitivity of yy. If axa\notin x, then ayxa\in y\setminus x which would give min(yx)a\min(y\setminus x)\mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}a, which is impossible. So axa\in x. This proves min(yx)xy\min(y\setminus x)\subseteq x\cap y. Hence min(yx)=xy\min(y\setminus x)=x\cap y.

From Fact 1 we easily get the following:

Fact 2.

xyx\mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}y if and only if xyx\subseteq y, for any two 𝔘\mathfrak{U}-ordinals xx and yy.

This in turn implies that OO is totally ordered under \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}. Indeed, consider x,yOx,y\in O. If xyx\neq y then either xyx\setminus y or yxy\setminus x is non-empty. Without loss of generality, suppose yxy\setminus x is non-empty. By Fact 1, min(yx)x\min(y\setminus x)\subseteq x. Then, by Fact 2, either min(yx)x\min(y\setminus x)\in x or min(yx)=x\min(y\setminus x)=x, and since min(yx)yx\min(y\setminus x)\in y\setminus x we can conclude that x=min(yx)x=\min(y\setminus x) and thus xyx\in y.

We now show that OO is well-ordered under the relation \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}. Let YOY\subseteq O be nonempty. Take any yYy\in Y. If yY=y\cap Y=\varnothing, then for all xYx\in Y we have xyx\notin y and thus y=minYy=\min Y by total ordering. If yYy\cap Y\neq\varnothing, then min(yY)\min(y\cap Y) exists, since yYyy\cap Y\subseteq y. For all xYyx\in Y\setminus y, it holds that xyx\notin y and thus yxy\subseteq x (by total ordering and Fact 2), which in turn implies min(yY)x\min(y\cap Y)\in x. We can conclude that min(yY)x\min(y\cap Y)\in x for all xYx\in Y, and thus minY=min(yY)\min Y=\min(y\cap Y).

We will now complete the proof of (iii) and prove the last statement of the theorem simultaneously. Consider X𝖯𝔘OX\in\mathsf{P}_{\mathfrak{U}}O. By (i) and Lemma 7, X𝔘X\in\mathfrak{U}. Then 𝖴{𝖴X,X}𝔘\mathsf{U}\{\mathsf{U}X,X\}\in\mathfrak{U}. To show that 𝖴{𝖴X,X}\mathsf{U}\{\mathsf{U}X,X\} is a 𝔘\mathfrak{U}-ordinal, we need to prove that it is a transitive set, well-ordered under the relation \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}. Since each element of XX is transitive, we have 𝖴𝖴X𝖴X\mathsf{U}\mathsf{U}X\subseteq\mathsf{U}X, which implies transitivity of 𝖴{𝖴X,X}\mathsf{U}\{\mathsf{U}X,X\}:

𝖴𝖴{𝖴X,X}=𝖴{𝖴𝖴X,𝖴X}=𝖴X𝖴{𝖴X,X}.\displaystyle\mathsf{U}\mathsf{U}\{\mathsf{U}X,X\}=\mathsf{U}\{\mathsf{U}\mathsf{U}X,\mathsf{U}X\}=\mathsf{U}X\subseteq\mathsf{U}\{\mathsf{U}X,X\}.

It follows from (ii) that each element of 𝖴{𝖴X,X}\mathsf{U}\{\mathsf{U}X,X\} is a 𝔘\mathfrak{U}-ordinal. So the fact that 𝖴{𝖴X,X}\mathsf{U}\{\mathsf{U}X,X\} is well-ordered under the relation \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}} follows from the fact that OO is well-ordered under the same relation, as we have already proved. Thus, 𝖴{𝖴X,X}\mathsf{U}\{\mathsf{U}X,X\} is a 𝔘\mathfrak{U}-ordinal. Any 𝔘\mathfrak{U}-ordinal yy such that xyx\in y for every element xXx\in X will have 𝖴{𝖴X,X}y\mathsf{U}\{\mathsf{U}X,X\}\subseteq y and thus 𝖴{𝖴X,X}y\mathsf{U}\{\mathsf{U}X,X\}\mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}y by Fact 2. To conclude that 𝖴{𝖴X,X}\mathsf{U}\{\mathsf{U}X,X\} is the incremented join of XX, it remains to make a trivial remark that for each xXx\in X we have x𝖴{𝖴X,X}x\in\mathsf{U}\{\mathsf{U}X,X\}.

It remains to prove that if (i–iii) hold then OO is the set of all 𝔘\mathfrak{U}-ordinals. Let OO be any set satisfying (i–iii). First we prove that every element of OO is a 𝔘\mathfrak{U}-ordinal. Let xOx\in O. By (iii), the set OO is ordered under the relation \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}}. In this ordered set, the set {x}>\{x\}^{>} consists of those elements of xx which are also elements of OO. By (ii), this is all elements of xx and so x={x}>x=\{x\}^{>}. By (i) and (iii), x𝔘x\in\mathfrak{U}. Furthermore, for any yxy\in x the following holds:

y={y}>{x}>=x.\displaystyle y=\{y\}^{>}\subseteq\{x\}^{>}=x.

This shows that xx is transitive. Since OO is well-ordered under \mathrel{\text{\oalign{$\in$\cr\nointerlineskip\kern 4.30554pt\cr$\smash{-}$\cr\nointerlineskip\kern-2.15277pt\cr}}} (by (iii) and Theorem 10) and xOx\subseteq O, xx is also well-ordered under the same relation. Thus, every element of OO is a 𝔘\mathfrak{U}-ordinal. Now we need to establish that every 𝔘\mathfrak{U}-ordinal is in OO. We already proved that the set 𝒪\mathcal{O} of all 𝔘\mathfrak{U}-ordinals is an ordinal system, and since OO is a set of 𝔘\mathfrak{U}-ordinals, O𝒪O\subseteq\mathcal{O}. The equality O=𝒪O=\mathcal{O} then follows from Corollary 14. ∎

4 A Dedekind-style axiomatization

A limit-successor system is a triple X=(X,L,s)X=(X,L,s) where XX is a set, LL is a partial function L:𝖯XXL\colon\mathsf{P}X\to X called the limit function and ss is a function s:XXs\colon X\to X called the successor function. A successor-closed subset of a limit-successor system XX is a subset II of XX such that sIIsI\subseteq I. For such subset, write s1Is^{-1}I to denote

s1I={xXs(x)I}\displaystyle s^{-1}I=\{x\in X\mid s(x)\in I\}

and L1IL^{-1}I to denote

L1I={A𝖽𝗈𝗆LL(A)I}.\displaystyle L^{-1}I=\{A\in\mathsf{dom}L\mid L(A)\in I\}.

A subset IXI\subseteq X is said to be closed when

s1II and 𝖴L1II.\displaystyle s^{-1}I\subseteq I\textrm{ and }\mathsf{U}L^{-1}I\subseteq I.

It is not difficult to see that closed subsets form a topology on XX; in fact, an Alexandrov topology. We denote the closure of a subset II in this topology by I¯\overline{I}. Recall that the corresponding ‘specialization preorder’ given by

xyx{y}¯\displaystyle x\leqslant y\quad\Leftrightarrow\quad x\in\overline{\{y\}}

is a preorder (as it is for any Alexandrov topology) and that xI¯x\in\overline{I} if and only if xyx\leqslant y for some yIy\in I.

We abbreviate the operator s1s^{-1} composed with itself mm times as sms^{-m}, with the m=0m=0 case giving the identity operator. We write ss^{-\infty} for the operator defined by

sI=𝖴{smIm}\displaystyle s^{-\infty}I=\mathsf{U}\{s^{-m}I\mid m\in\mathbb{N}\}

and 𝖴L1\mathsf{U}{L^{-1}} for the operator I𝖴L1II\mapsto\mathsf{U}L^{-1}I. It is easy to see that the closure of a subset IXI\subseteq X can be computed as

I¯=𝖴{s[𝖴L1s]kIk}.\displaystyle\overline{I}=\mathsf{U}\{s^{-\infty}\left[\mathsf{U}{L^{-1}}s^{-\infty}\right]^{k}I\mid k\in\mathbb{N}\}.

This means that the specialization preorder ‘breaks up’ into two relations s\leqslant_{s} and L\leqslant_{L}, each determined by ss and LL alone, as explained in what follows. These relations are defined by:

xsy\displaystyle x\leqslant_{s}y m[sm(x)=y]\displaystyle\quad\Leftrightarrow\quad\exists_{m\in\mathbb{N}}[s^{m}(x)=y] (xs{y})\displaystyle(\Leftrightarrow x\in s^{-\infty}\{y\})
xLy\displaystyle x\leqslant_{L}y I[[xI][L(I)=y]]\displaystyle\quad\Leftrightarrow\quad\exists_{I}[[x\in I]\wedge[L(I)=y]]\qquad (x𝖴L1{y})\displaystyle(\Leftrightarrow x\in\mathsf{U}{L^{-1}}\{y\})

We then have xyx\leqslant y if and only if

x=z0sz1Lz2sz3Lz2ksy\displaystyle x=z_{0}\leqslant_{s}z_{1}\leqslant_{L}z_{2}\leqslant_{s}z_{3}\leqslant_{L}\dots z_{2k}\leqslant_{s}y

for some z0,,z2kXz_{0},\dots,z_{2k}\in X, where kk can be any natural number k0k\geqslant 0. Note that s\leqslant_{s} is both reflexive and transitive, although the same cannot be claimed for L\leqslant_{L}.

Definition 17.

Given a universe 𝔘\mathfrak{U}, a 𝔘\mathfrak{U}-counting system is a limit-successor system (X,L,s)(X,L,s) satisfying the following conditions:

  • (C1)

    The domain of LL is the set of all successor-closed subsets I𝖯𝔘XI\in\mathsf{P}_{\mathfrak{U}}X.

  • (C2)

    If II and JJ belong to the domain of LL and I¯=J¯\overline{I}=\overline{J}, then L(I)=L(J)L(I)=L(J).

The structure above is the one that will be used for formulating the universal property of an ordinal system in the next section. In this section we give a characterization of ordinal systems as counting systems having further internal properties.

Lemma 18.

Let 𝔘\mathfrak{U} be a universe and let (X,L,s)(X,L,s) be a 𝔘\mathfrak{U}-counting system. Then L\leqslant_{L} is transitive and furthermore,

xsyLzxLz\displaystyle x\leqslant_{s}y\leqslant_{L}z\quad\Rightarrow\quad x\leqslant_{L}z

for all x,y,zXx,y,z\in X.

Proof.

To prove transitivity, suppose xLyx\leqslant_{L}y and yLzy\leqslant_{L}z. Then xIx\in I, L(I)=yL(I)=y, yJy\in J and L(J)=zL(J)=z for some successor-closed I,J𝖯𝔘XI,J\in\mathsf{P}_{\mathfrak{U}}X. Then the union 𝖴{I,J}𝖯𝔘X\mathsf{U}\{I,J\}\in\mathsf{P}_{\mathfrak{U}}X (Lemma 4) is also successor-closed, and hence it belongs to the domain of LL by (C1). Since L(I)JL(I)\in J, we get that IJ¯I\subseteq\overline{J}. This implies that 𝖴{I,J}¯=J¯\overline{\mathsf{U}\{I,J\}}=\overline{J}. By (C2), L(𝖴{I,J})=L(J)L(\mathsf{U}\{I,J\})=L(J). Having x𝖴{I,J}x\in\mathsf{U}\{I,J\} and L(𝖴{I,J})=zL(\mathsf{U}\{I,J\})=z means that xLzx\leqslant_{L}z. This completes the proof of transitivity. To prove the second property, suppose xsyLzx\leqslant_{s}y\leqslant_{L}z. Then sm(x)=ys^{m}(x)=y and yJy\in J with L(J)=zL(J)=z, for some mm\in\mathbb{N} and successor-closed J𝖯𝔘XJ\in\mathsf{P}_{\mathfrak{U}}X. This proof follows a similar idea where we expand JJ, this time adding to it all elements of the form sk(x)s^{k}(x), where k{0,,m1}k\in\{0,\dots,m-1\}. The resulting set

K=𝖴{{x,s(x),,sm1(x)},J}\displaystyle K=\mathsf{U}\{\{x,s(x),\dots,s^{m-1}(x)\},J\}

is clearly successor-closed and belongs to 𝖯𝔘X\mathsf{P}_{\mathfrak{U}}X (Lemmas 2 and 4). Then, since K¯=J¯\overline{K}=\overline{J}, we get that L(K)=L(J)L(K)=L(J) by (C2). This implies xLzx\leqslant_{L}z. ∎

This lemma gives that in a 𝔘\mathfrak{U}-counting system (X,L,s)(X,L,s), for any x,zXx,z\in X we have

xz[xsz]y[xLysz]\displaystyle x\leqslant z\quad\Leftrightarrow\quad[x\leqslant_{s}z]\vee\exists_{y}[x\leqslant_{L}y\leqslant_{s}z]

and hence the closure of a subset IXI\subseteq X is given by

I¯=𝖴{sI,𝖴L1sI}.\displaystyle\overline{I}=\mathsf{U}\{s^{-\infty}I,\mathsf{U}{L^{-1}}s^{-\infty}I\}.
Theorem 19.

The specialization preorder of a 𝔘\mathfrak{U}-counting system (X,L,s)(X,L,s) makes XX an ordinal system relative to 𝔘\mathfrak{U}, provided the following conditions hold:

  • (C3)

    s1{L(I)}==I{s(L(I))}s^{-1}\{L(I)\}=\varnothing=I\cap\{s(L(I))\} for all II such that L(I)L(I) is defined.

  • (C4)

    ss is injective and LL has the property that if L(I)=L(J)L(I)=L(J) then I¯=J¯\overline{I}=\overline{J}.

  • (C5)

    J=XJ=X for any successor-closed set JJ having the property that IJL(I)JI\subseteq J\Rightarrow L(I)\in J every time L(I)L(I) is defined.

When these conditions hold, ss is the successor function of the ordinal system and L(I)=I=

+

I
L(I)=\bigvee I=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I
whenever L(I)L(I) is defined; moreover, the limit ordinals are exactly the elements of XX of the form L(I)L(I). Furthermore, the closure of I𝖯𝔘XI\in\mathsf{P}_{\mathfrak{U}}X is given by I¯={

+

I
}
>
\overline{I}=\left\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I\right\}^{>}
. Finally, any ordinal system relative to 𝔘\mathfrak{U} arises this way from a (unique) 𝔘\mathfrak{U}-counting system satisfying (C3–5).

Before proving the theorem, let us illustrate axioms (C1–5) in the case when 𝔘\mathfrak{U} is the universe of hereditarily finite sets (i.e., sets which are elements of a finite transitive set). Then LL is only defined on finite successor-closed sets. Injectivity of ss in (C4) forces every element xx of such set to have the property m{0}[sm(x)=x]\exists_{m\in\mathbb{N}\setminus\{0\}}[s^{m}(x)=x]. At the same time, by (C3), such xx cannot lie in the image of LL. So

J={xXm{0}[sm(x)x]}\displaystyle J=\{x\in X\mid\forall_{m\in\mathbb{N}\setminus\{0\}}[s^{m}(x)\neq x]\}

has the second property in (C5). Moreover, by injectivity of ss again, JJ is also successor-closed. Then, by (C5), J=XJ=X and so LL can only be defined on the empty set. With this provision, the triple (X,L,s)(X,L,s) becomes a triple (X,0,s)(X,0,s) where 0 is the unique element in the image of LL, 0=L()0=L(\varnothing). The axioms (C1–2) then trivially hold, while (C3–5) take the form of the axioms of Dedekind for a natural number system:

  • The first equality in (C3) states that 0 does not belong to the image of ss, while the second equality holds trivially.

  • (C4) just states that ss is injective.

  • (C5) becomes the usual principle of mathematical induction.

Proof of Theorem 19.

Suppose the conditions (C1–5) hold.


Step 1. As a first step, we prove that the specialization preorder is antisymmetric, i.e., that it is a partial order.

For this, we first show that L\leqslant_{L} is ‘antireflexive’: it is impossible to have xLxx\leqslant_{L}x. Indeed, suppose xIx\in I and L(I)=xL(I)=x. Since II is successor-closed by (C1), s(x)Is(x)\in I. But then s(x)I{s(L(I))}s(x)\in I\cap\{s(L(I))\}, which is impossible by (C3).

Next, we show antisymmetry of s\leqslant_{s}. Suppose xszsxx\leqslant_{s}z\leqslant_{s}x and xzx\neq z. Then we get that sk(x)=xs^{k}(x)=x for k>1k>1. We will now show that this is not possible. In fact, we establish a slightly stronger property, which will be useful later on as well:

Property 0.

sk(x)xs^{k}(x)\neq x for all k>0k>0 and xXx\in X.

Actually, we have already established this property in the remark after the theorem. Here is a more detailed argument. Consider the set JJ of all xXx\in X such that sk(x)xs^{k}(x)\neq x for all k>0k>0. We will use (C5) to show that J=XJ=X. First, we show that JJ is successor-closed. Let yJy\in J. Suppose sk(s(y))=s(y)s^{k}(s(y))=s(y) for some k>0k>0. Then by injectivity of ss (which is required in (C4)), sk1(s(y))=ys^{k-1}(s(y))=y, which is impossible. So s(y)Js(y)\in J, showing that JJ is successor-closed. Now let IJI\subseteq J be successor-closed I𝖯𝔘XI\in\mathsf{P}_{\mathfrak{U}}X (by (C1), II is such if and only if L(I)L(I) is defined). Then L(I)sk(L(I))L(I)\neq s^{k}(L(I)) for all k>0k>0 by the first equality in (C3). So L(I)JL(I)\in J and we can apply (C5) to get J=XJ=X, as desired.

Antisymmetry of s\leqslant_{s} has thus been established.

We are now ready to prove the antisymmetry of \leqslant. Suppose xzx\leqslant z and zxz\leqslant x. There are four cases to consider:

Case 1.

xszsxx\leqslant_{s}z\leqslant_{s}x. Then x=zx=z by antisymmetry of s\leqslant_{s}.

Case 2.

xLyszsxx\leqslant_{L}y\leqslant_{s}z\leqslant_{s}x for some yy. By transitivity of s\leqslant_{s} and Lemma 18, in this case we get yLyy\leqslant_{L}y, which we have shown not to be possible.

Case 3.

xszLysxx\leqslant_{s}z\leqslant_{L}y\leqslant_{s}x for some yy. Similar to the previous case, in this case we get yLyy\leqslant_{L}y, which is impossible.

Case 4.

xLyszLysxx\leqslant_{L}y\leqslant_{s}z\leqslant_{L}y^{\prime}\leqslant_{s}x for some y,yy,y^{\prime}. In this case too we get the impossible yLyy\leqslant_{L}y (this case relies in addition on transitivity of L\leqslant_{L}, established also in Lemma 18).

We have thus shown that the specialization preorder is antisymmetric. We will now establish the following two properties, which will be useful later on.

Property 1.

If x<yx<y then s(x)ys(x)\leqslant y, for all x,yXx,y\in X.

Property 2.

If y<s(x)y<s(x) then yxy\leqslant x, for all x,yXx,y\in X.

To prove the first property, suppose x<yx<y. There are two cases:

Case 1.

xsyx\leqslant_{s}y; then clearly s(x)ys(x)\leqslant y (as xyx\neq y).

Case 2.

xLysyx\leqslant_{L}y^{\prime}\leqslant_{s}y for some yy^{\prime}. Then xIx\in I and L(I)=yL(I)=y^{\prime} for a successor-closed II, by (C1). So s(x)Is(x)\in I and thus s(x)Lys(x)\leqslant_{L}y^{\prime}. With ysyy^{\prime}\leqslant_{s}y this gives s(x)ys(x)\leqslant y.

So in both cases we get s(x)ys(x)\leqslant y, as required. To prove Property 2, suppose y<s(x)y<s(x). We have again two cases:

Case 1.

yss(x)y\leqslant_{s}s(x). This with ys(x)y\neq s(x) gives yxy\leqslant x by injectivity of ss from (C4).

Case 2.

yLyss(x)y\leqslant_{L}y^{\prime}\leqslant_{s}s(x). Since ys(x)y^{\prime}\neq s(x) by the first equality in (C3), by injectivity of ss from (C4) we must have ysxy^{\prime}\leqslant_{s}x. This will give yxy\leqslant x.

We get the required conclusion in both cases.


Step 2. Next, we want to prove that the specialization order is a total order.

We will prove this by simultaneously establishing the following:

Property 3.

Let yXy\in X. If x<yx<y for all xIx\in I such that L(I)L(I) is defined, then necessarily L(I)yL(I)\leqslant y.

Let JJ be the set of all xXx\in X such that for every yXy\in X either yxy\leqslant x or xyx\leqslant y. We will use (C5) to show that J=XJ=X. For this, we first prove that JJ is successor-closed. Let xJx\in J. Consider any yXy\in X. Since xs(x)x\leqslant s(x), if yxy\leqslant x then ys(x)y\leqslant s(x). If x<yx<y then by Property 1, s(x)ys(x)\leqslant y. This proves that JJ is successor-closed. Consider now L(I)L(I), where IJI\subseteq J. To prove that L(I)JL(I)\in J, we proceed as follows. Let xXx\in X. If xyx\leqslant y for at least one yIy\in I, then xL(I)x\leqslant L(I), since yLL(I)y\leqslant_{L}L(I). Thus, it suffices to prove that the set KIK_{I} of all xXx\in X such that if y<xy<x for all yIy\in I then L(I)xL(I)\leqslant x, is the entire KI=XK_{I}=X. This we prove using (C5). First, we show that KIK_{I} is successor-closed. Suppose xKIx\in K_{I}. If y<s(x)y<s(x) for all yIy\in I, then by Property 2, yxy\leqslant x for all yIy\in I. If xIx\in I then, since II is successor-closed by (C1), we will have s(x)Is(x)\in I, which will violate the assumption that y<s(x)y<s(x) for all yIy\in I. So we get that y<xy<x for all yIy\in I. Then L(I)xL(I)\leqslant x, since xKIx\in K_{I}. This implies L(I)s(x)L(I)\leqslant s(x), thus proving that KIK_{I} is successor-closed. Now let HKIH\subseteq K_{I} be such that L(H)L(H) is defined. Suppose y<L(H)y<L(H) for all yIy\in I. From the first equality in (C3) we get that yLL(H)y\leqslant_{L}L(H) for each yIy\in I. So for each yIy\in I, there is GyG_{y} such that yGyy\in G_{y} and L(Gy)=L(H)L(G_{y})=L(H). This implies that Gy¯=H¯\overline{G_{y}}=\overline{H} for each yIy\in I (by (C4)), and so IH¯I\subseteq\overline{H}. Since IJI\subseteq J, each element of HH is comparable with each element of II. If for every hHh\in H we have yhIy_{h}\in I such that hyhh\leqslant y_{h}, then HI¯H\subseteq\overline{I}. This would then give I¯=H¯\overline{I}=\overline{H}, and so by (C2), L(I)=L(H)L(I)=L(H), showing that L(I)L(H)L(I)\leqslant L(H), as desired. In contrast, if there is hHh\in H such that y<hy<h for every yIy\in I, then (since HKIH\subseteq K_{I}) L(I)<hL(I)<h. This together with hLL(H)h\leqslant_{L}L(H) will give L(I)L(H)L(I)\leqslant L(H). We have thus shown that KIK_{I} has the required properties in order for us to apply (C5) to conclude that KI=XK_{I}=X. This then shows that L(I)JL(I)\in J, and so JJ has the required properties to conclude that J=XJ=X. The proof of the specialization order being a total order is then complete. At the same time, since J=XJ=X and for each IJI\subseteq J such that L(I)L(I) is defined, KI=XK_{I}=X, we have also established Property 3.


Step 3. We now show that L(I)=I=

+

I
L(I)=\bigvee I=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I
whenever L(I)L(I) is defined and s(x)=x+s(x)=x^{+} for all xXx\in X.

Properties 0 and 3 show that L(I)L(I) is the join of II, for any II such that L(I)L(I) is defined. Indeed, if xyx\leqslant y for all xIx\in I, then for each xIx\in I, also s(x)ys(x)\leqslant y. Since x<s(x)x<s(x), as clearly xs(x)x\leqslant s(x) and by Property 0, xs(x)x\neq s(x), we get: x<yx<y for all xIx\in I. Then by Property 3, L(I)yL(I)\leqslant y thus showing that L(I)L(I) is a join of II. Furthermore, the property x<s(x)x<s(x) together with Property 1 implies that s(x)=x+s(x)=x^{+}, for each xXx\in X. Thus, once we prove that XX is an ordinal system under the specialization order, we have that ss is its successor function and LL is given by join. Furthermore, when L(I)L(I) is defined, II is successor-closed and so it cannot have a largest element, by Property 0. Then the join L(I)L(I) of II must also be the incremented join of II (Lemma 8).


Step 4. We show that XX is an ordinal system under the specialization order where limit ordinals are exactly the elements of the form L(I)L(I).

Consider the set JJ of all xXx\in X such that {x}>𝖯𝔘X\{x\}^{>}\in\mathsf{P}_{\mathfrak{U}}X. If xJx\in J, then by Property 2, {s(x)}>=𝖴{{x}>,{x}}𝖯𝔘X\{s(x)\}^{>}=\mathsf{U}\{\{x\}^{>},\{x\}\}\in\mathsf{P}_{\mathfrak{U}}X (Lemmas 2 and 4) and so s(x)Js(x)\in J. Suppose IJI\in J is such that L(I)L(I) is defined. Since the specialization order is a total order and L(I)L(I) is the join of elements in II, we have

{L(I)}>=𝖴{{x}>xI}𝖯𝔘X ((C1) & Lemma 4)\displaystyle\{L(I)\}^{>}=\mathsf{U}\{\{x\}^{>}\mid x\in I\}\in\mathsf{P}_{\mathfrak{U}}X\quad\textrm{ ((C1) \& Lemma \ref{lem:unio})}

and so L(I)JL(I)\in J. By (C5), J=XJ=X.

To prove that XX is an ordinal system under the specialization order, it remains to prove that for any Y𝖯𝔘XY\in\mathsf{P}_{\mathfrak{U}}X, the incremented join of YY exists in XX. If YY has a largest element, then the successor of that element is the incremented join of YY (Lemma 8). If 𝔘\mathfrak{U} does not contain an infinite set, then YY is finite and so it has a largest element. Now consider Y𝖯𝔘XY\in\mathsf{P}_{\mathfrak{U}}X that has no largest element, with 𝔘\mathfrak{U} containing an infinite set. We define:

sY={sn(x)[xY][n]}.\displaystyle s^{\infty}Y=\{s^{n}(x)\mid[x\in Y]\wedge[n\in\mathbb{N}]\}.

This is of course the closure of YY under ss. Then sY𝖯𝔘Xs^{\infty}Y\in\mathsf{P}_{\mathfrak{U}}X (Lemmas 5 and 6) and so L(sY)L(s^{\infty}Y) is defined by (C1). Since YsYY\subseteq s^{\infty}Y, it holds that y<L(sY)y<L(s^{\infty}Y) for all yYy\in Y. Let yYy\in Y. We prove by induction on nn that for each nn\in\mathbb{N}, we have sn(y)<zs^{n}(y)<z for some zYz\in Y. For n=0n=0, this follows from the fact that YY does not have a largest element. Suppose sn(y)<zs^{n}(y)<z for some zYz\in Y. Then sn+1(y)=s(sn(y))zs^{n+1}(y)=s(s^{n}(y))\leqslant z. Since zz cannot be the largest element of YY, we must have z<zz<z^{\prime} for some zYz^{\prime}\in Y. Then sn+1(y)<zs^{n+1}(y)<z^{\prime}. What we have shown implies that the incremented join L(sY)L(s^{\infty}Y) of sYs^{\infty}Y is also the incremented join of YY.

We have thus proved that the specialization (pre)order of a 𝔘\mathfrak{U}-counting system satisfying (C3–5) makes it an ordinal system relative to 𝔘\mathfrak{U}, with ss as its successor function and LL given equivalently by join and by incremented join. This also establishes that if an ordinal system relative to 𝔘\mathfrak{U} arises this way from a 𝔘\mathfrak{U}-counting system satisfying (C3–5), then this 𝔘\mathfrak{U}-counting system is unique. We now prove the existence of such a 𝔘\mathfrak{U}-counting system. Actually, before doing that, note that by (C3), no element of XX of the form L(I)L(I) can be a successor ordinal, and so it must be a limit ordinal. Conversely, for a limit ordinal xx we have x=L({x}>)x=L(\{x\}^{>}) (Lemma 11). This shows that limit ordinals are precisely the ordinals of the form L(I)L(I).

For an ordinal system 𝒪\mathcal{O} relative to 𝔘\mathfrak{U}, consider the limit-successor system (𝒪,,_+)(\mathcal{O},\bigvee,\_^{+}), where \bigvee is the usual join restricted on a domain as required by (C1).


Step 5. We show that (C1–5) hold for the limit-successor system (𝒪,,_+)(\mathcal{O},\bigvee,\_^{+}) and that the corresponding specialization order matches with the order of 𝒪\mathcal{O}. In this step we show as well that I¯={

+

I
}
>
\overline{I}=\left\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I\right\}^{>}
holds for each I𝖯𝔘𝒪I\in\mathsf{P}_{\mathfrak{U}}\mathcal{O}.

By Theorem 12, LL is indeed defined over the entire domain required in (C1). To prove (C2), first we establish that

I¯={+I}>\displaystyle\overline{I}=\left\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I\right\}^{>}

for each I𝖯𝔘𝒪I\in\mathsf{P}_{\mathfrak{U}}\mathcal{O}. It is easy to see that {

+

I
}
>
\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I\}^{>}
is closed, so I¯{

+

I
}
>
\overline{I}\subseteq\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I\}^{>}
. To show {

+

I
}
>
I¯
\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I\}^{>}\subseteq\overline{I}
, let x{

+

I
}
>
x\in\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I\}^{>}
. We have well-ordering and hence total order by Theorem 10. Then x<

+

I
x<\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I
and so xyIx\leqslant y\in I for some yy. Consider

y=min{yI¯xy}.\displaystyle y^{\prime}=\min\{y\in\overline{I}\mid x\leqslant y\}.

We consider two cases:

Case 1.

yy^{\prime} is a successor ordinal. Then y=y′′+y^{\prime}=y^{\prime\prime+} for some ordinal y′′y^{\prime\prime}. Since yI¯y^{\prime}\in\overline{I}, we must have y′′I¯y^{\prime\prime}\in\overline{I}. Then y′′<xy^{\prime\prime}<x and so yxy^{\prime}\leqslant x (L3). This gives x=yx=y^{\prime} and so xI¯x\in\overline{I}.

Case 2.

yy^{\prime} is a limit ordinal. Then {y}>\{y^{\prime}\}^{>} is successor-closed. Furthermore, we have

y=+{y}>=({y}>)+={y}>.\displaystyle y^{\prime}=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}\{y^{\prime}\}^{>}=\bigvee(\{y^{\prime}\}^{>})^{+}=\bigvee\{y^{\prime}\}^{>}.

By closure of I¯\overline{I}, we get {y}>I¯\{y^{\prime}\}^{>}\subseteq\overline{I}. Since y<xy<x for all y<yy<y^{\prime}, we get yxy^{\prime}\leqslant x. This gives x=yx=y^{\prime} and so xI¯x\in\overline{I}.

We have thus established that the equality I¯={

+

I
}
>
\overline{I}=\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I\}^{>}
holds for each I𝖯𝔘𝒪I\in\mathsf{P}_{\mathfrak{U}}\mathcal{O}. From this it follows that the specialization preorder matches with the order of 𝒪\mathcal{O}. We then get that (C2) holds by the fact that if down-closures of two subsets of a poset are equal, then so are their joins. Thus (𝒪,,_+)(\mathcal{O},\bigvee,\_^{+}) is a 𝔘\mathfrak{U}-counting system.

It remains to show that (C3–5) hold. Consider a successor-closed I𝖯𝔘𝒪I\in\mathsf{P}_{\mathfrak{U}}\mathcal{O}. II has no maximum element thanks to (L1) and thus, I=

+

I
\bigvee I=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I
by Lemma 8. By the same lemma,

+

I
\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I
cannot be a successor if II has no maximum. Thus we have (_+)1{I}=(\_^{+})^{-1}\{\bigvee I\}=\varnothing, which is the first part of (C3). Since (I)+>Ix(\bigvee I)^{+}>\bigvee I\geqslant x for each xIx\in I, we have that (I)+I(\bigvee I)^{+}\notin I, which means the second part of (C3) also holds, i.e. I{(I)+}=I\cap\{(\bigvee I)^{+}\}=\varnothing.

We already know that _+\_^{+} is injective, so to see that (C4) holds, consider another successor-closed J𝖯𝔘𝒪J\in\mathsf{P}_{\mathfrak{U}}\mathcal{O}. If I=J\bigvee I=\bigvee J, then

I¯={+I}>={I}>={J}>={+J}>=J¯.\displaystyle\overline{I}=\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}I\}^{>}=\{\bigvee I\}^{>}=\{\bigvee J\}^{>}=\{\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}J\}^{>}=\overline{J}.

Thus (C4) holds. Finally, consider a successor-closed subset JJ of 𝒪\mathcal{O} where IJ\bigvee I\in J for all successor-closed subsets II of JJ such that I𝖯𝔘𝒪I\in\mathsf{P}_{\mathfrak{U}}\mathcal{O}. Then J=𝒪J=\mathcal{O} if it satisfies (I1) and (I2) in our formulation of transfinite induction. We check both:

  • (I1)

    J+JJ^{+}\subseteq J follows from the fact that JJ is successor-closed.

  • (I2)

    Let xx be a limit ordinal such that {x}>J\{x\}^{>}\subseteq J. Then x={x}>Jx=\bigvee\{x\}^{>}\in J (Lemma 11).

Since both of these conditions hold, we can conclude that J=𝒪J=\mathcal{O}, and thus (C5) holds. This completes the proof. ∎

5 The corresponding universal property

Given two 𝔘\mathfrak{U}-counting systems (X1,L1,s1)(X_{1},L_{1},s_{1}) and (X2,L2,s2)(X_{2},L_{2},s_{2}), a function f:X1X2f\colon X_{1}\to X_{2} that preserves the successor function (fs1=s2ffs_{1}=s_{2}f) automatically preserves successor-closed subsets, so for any successor-closed I𝖯𝔘X1I\in\mathsf{P}_{\mathfrak{U}}X_{1}, both sides of the equality

L2(fI)=f(L1(I))\displaystyle L_{2}(fI)=f(L_{1}(I))

are defined (Lemma 5). When this equality holds for any such II, we say that ff is a morphism of 𝔘\mathfrak{U}-counting systems and represent ff as an arrow

f:(X1,L1,s1)(X2,L2,s2).\displaystyle f\colon(X_{1},L_{1},s_{1})\to(X_{2},L_{2},s_{2}).

It is not difficult to see that 𝔘\mathfrak{U}-counting systems and morphisms between them form a category, under the usual composition of functions. Isomorphisms in this category are bijections between 𝔘\mathfrak{U}-counting systems which preserve both succession and limiting. Call a 𝔘\mathfrak{U}-counting system an ordinal 𝔘\mathfrak{U}-counting system when conditions (C3–5) hold. Clearly, the property of being an ordinal 𝔘\mathfrak{U}-counting system is stable under isomorphism of 𝔘\mathfrak{U}-counting systems. By Theorems 16 and 19, an ordinal 𝔘\mathfrak{U}-counting system exists and is given by the 𝔘\mathfrak{U}-ordinals. We will now see that ordinal 𝔘\mathfrak{U}-counting systems are precisely the initial objects in the category of 𝔘\mathfrak{U}-counting systems.

Theorem 20.

For any universe 𝔘\mathfrak{U}, a 𝔘\mathfrak{U}-counting system is an initial object in the category of 𝔘\mathfrak{U}-counting systems if and only if it is an ordinal 𝔘\mathfrak{U}-counting system.

Proof.

Since we know that an ordinal 𝔘\mathfrak{U}-counting system exists (Theorem 16) and that the property of being an ordinal 𝔘\mathfrak{U}-counting system is stable under isomorphism, it suffices to show that any ordinal 𝔘\mathfrak{U}-counting system is an initial object in the category of 𝔘\mathfrak{U}-counting systems. By Theorem 19, an ordinal 𝔘\mathfrak{U}-counting system has the form (𝒪,,_+)(\mathcal{O},\bigvee,\_^{+}), where 𝒪\mathcal{O} is an ordinal system relative to 𝔘\mathfrak{U} and \bigvee is the join defined for exactly the successor-closed subsets I𝖯𝔘𝒪I\in\mathsf{P}_{\mathfrak{U}}\mathcal{O} in the 𝔘\mathfrak{U}-counting system.

For any 𝔘\mathfrak{U}-counting system (X,L,s)(X,L,s), if a morphism (𝒪,,_+)(X,L,s)(\mathcal{O},\bigvee,\_^{+})\to(X,L,s) exists, it must be the unique function ff defined by the transfinite recursion

  1. (i)

    f(x+)=s(f(x))f(x^{+})=s(f(x)) for any x𝒪x\in\mathcal{O};

  2. (ii)

    f(x)=L({f(y)y<x})f(x)=L(\{f(y)\mid y<x\}) for any limit ordinal xx (Lemma 11).

We now prove that the function ff defined by the recursion above is a morphism. It preserves succession by (i). Consider I𝖯𝔘𝒪I\in\mathsf{P}_{\mathfrak{U}}\mathcal{O} closed under successors. Then I\bigvee I is a limit ordinal and I¯={I}>\overline{I}=\{\bigvee I\}^{>}, by Theorem 19. By definition of ff, we then have

f(I)=L({f(y)y<I})=L(fI¯).\displaystyle f(\bigvee I)=L(\{f(y)\mid y<\bigvee I\})=L(f\overline{I}).

We will now prove fI¯¯=fI¯\overline{f\overline{I}}=\overline{fI}. We clearly have fIfI¯¯fI\subseteq\overline{f\overline{I}}, so it suffices to show that fI¯fI¯f\overline{I}\subseteq\overline{fI}. This is equivalent to showing I¯f1fI¯\overline{I}\subseteq f^{-1}\overline{fI}, which would follow if we prove f1fI¯f^{-1}\overline{fI} is closed. If x+f1fI¯x^{+}\in f^{-1}\overline{fI}, then s(f(x))=f(x+)fI¯s(f(x))=f(x^{+})\in\overline{fI}. Therefore, f(x)fI¯f(x)\in\overline{fI} and so xf1fI¯x\in f^{-1}\overline{fI}. If Jf1fI¯\bigvee J\in f^{-1}\overline{fI}, then (as J\bigvee J is a limit ordinal by Theorem 19)

L({f(y)y<J})=f(J)fI¯,\displaystyle L(\{f(y)\mid y<\bigvee J\})=f(\bigvee J)\in\overline{fI},

which implies {f(y)y<J}fI¯\{f(y)\mid y<\bigvee J\}\subseteq\overline{fI}. This gives J{J}>f1fI¯J\subseteq\{\bigvee J\}^{>}\subseteq f^{-1}\overline{fI}. Note that we have the first of these two subset inclusions due to the fact that J=

+

J
\bigvee J=\operatorname{\mathchoice{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{6.0pt}{\tiny+}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.5}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}{\mathchoice{{\ooalign{$\displaystyle\bigvee$\cr\hfil$\displaystyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\textstyle\bigvee$\cr\hfil$\textstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptstyle\bigvee$\cr\hfil$\scriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle\bigvee$\cr\hfil$\scriptscriptstyle\raisebox{5.0pt}{\scalebox{0.4}{+}}$\hfil\cr}}}}}J
thanks to Theorem 19. This proves that f1fI¯f^{-1}\overline{fI} is closed. So fI¯¯=fI¯\overline{f\overline{I}}=\overline{fI}. We therefore get f(I)=L(fI¯)=L(fI)f(\bigvee I)=L(f\overline{I})=L(fI), showing that ff is indeed a morphism (𝒪,,_+)(X,L,s)(\mathcal{O},\bigvee,\_^{+})\to(X,L,s). ∎

Consider the case when every element in 𝔘\mathfrak{U}\neq\varnothing is a finite set (e.g., 𝔘\mathfrak{U} could be the universe of hereditarily finite sets). Then every triple (X,0,s)(X,0,s), where XX is a set, ss is a function s:XXs\colon X\to X, and 0X0\in X, can be seen as a 𝔘\mathfrak{U}-counting system for the same ss, with L(I)=0L(I)=0 for each finite II. A morphism f:(X1,01,s1)(X2,02,s2)f\colon(X_{1},0_{1},s_{1})\to(X_{2},0_{2},s_{2}) between such 𝔘\mathfrak{U}-counting systems is a function f:X1X2f\colon X_{1}\to X_{2} such that s2f=fs1s_{2}f=fs_{1} and f(01)=02f(0_{1})=0_{2}. The natural number system (,0,s)(\mathbb{N},0,s), with its usual successor function s(n)=n+1s(n)=n+1, is an initial object in the category of such 𝔘\mathfrak{U}-counting systems. The theorem above presents the natural number system as an initial object in the category of all 𝔘\mathfrak{U}-counting systems. It is not surprising that the natural number system is initial in this larger category too, since the empty set is the only finite successor-closed subset of \mathbb{N}.

References

  • [1] M. Artin, A. Grothendieck, and J.-L. Verdier. Théorie des topos et cohomologie etale des schémas: Séminaire de géométrie algébrique du Bois Marie (SGA 4), Tome 1. 1963–1964.
  • [2] G. Cantor. Beiträge zur Begründung der transfiniten Mengenlehre(erster Artikel). Math. Ann., 46(4):481–512, 1895.
  • [3] G. Cantor. Beiträge zur Begründung der transfiniten Mengenlehre (zweiter Artikel). Math. Ann., 49(2):207–246, 1897.
  • [4] R. Dedekind. Was sind und was sollen die Zahlen? Vieweg, Braunschweig, 1888.
  • [5] A. H. Fraenkel. Abstract set theory. Bull. Amer. Math. Soc, 59:584–585, 1953.
  • [6] P. Gabriel. Des catégories abéliennes. Bull. Soc. Math. France, 90:323–448, 1962.
  • [7] T. Jech. Set theory. Springer, Berlin, Heidelberg, 2003.
  • [8] A. Joyal and I. Moerdijk. Algebraic set theory, volume 220. Cambridge University Press, 1995.
  • [9] K. Kunen. Set theory: an introduction to independence proofs. Elsevier Science Publishers, 1980.
  • [10] F. W. Lawvere. An elementary theory of the category of sets. Proc. Nat. Acad. Sci. U.S.A., 52(6):1506–1511, 1964.
  • [11] S. Mac Lane. Categories for the working mathematician, volume 5 of Graduate Texts in Mathematics. Springer, second edition, 1998.
  • [12] J. von Neumann. Zur einführung der transfiniten Zahlen. Acta Litterarum ac Scientiarum Regiae Universitatis Hungaricae Francisco-Josephinae, sectio scientiarum mathematicarum, 1:199–208, 1923.
  • [13] H. Wang. The axiomatization of arithmetic. J. Symb. Log., 22(2):145–158, 1957.
  • [14] N. H. Williams. On Grothendieck universes. Compos. Math., 21(1):1–3, 1969.
  • [15] E. Zermelo. Ernst Zermelo: Collected Works/Gesammelte Werke: Volume I/Band I – Set Theory, Miscellanea/Mengenlehre, Varia, volume 21 of Schriften der Mathematisch-naturwissenschaftlichen Klasse. Springer, 2010.