Pullbacks : pairing and matching

The prerequisite to read and understand most, if not all, of this top directory
is no more than a basic knowledge of sets and functions.

Example of a pullback

Here is a simple, elementary example of a pullback:
Suppose you have a set of men and a set of women, each with a political preference.

This situation can be expressed mathematically by
three sets, named Men, Women, and Parties,
connected by two functions,
named PolPref-Men and PolPref-Women (for Political Preference),
with a common target, Parties, but with sources Men and Women.
This situation is called, by categorists, a cospan in the category of sets,
and is usually represented most compactly in one or another of the two one-line formats,
which differ only in where the names of the functions are placed:

PolPref-Men PolPref-Women Men ------------> Parties <-------------- Women PolPref-Men: Men --------> Parties <-------- Women :PolPref-Women

but in preparation for the next step may be drawn as an angle:

Men Women \ / PolPref-Men \ / PolPref-Women \ / _| |_ Parties

You want to construct
a set of all pairs of men and women who have the same political preference.
That is called by categorists the pullback (@ncatlab, @Wikipedia)
(sometimes called "fibered product")
of the above diagram,
and is commonly denoted, for the situation above, as Men ×_Parties Women,
and diagrammed as follows:

Men ×_Parties Women / \ / \ / \ |_ _| Men Women \ / PolPref-Men \ / PolPref-Women \ / _| |_ Parties ,

where the arrows from Men ×_Parties Women are the evident projections.

The general case

For the general case (at least in the category of sets),
we replace the specific sets mentioned above by names representing arbitrary sets:

X ×_Z Y / \ / \ / \ |_ _| X Y \ / f \ / g \ / _| |_ Z

Some remarks on terminology

Two arrows that have the same source, such as the top two in the above diagram,
are called a span,
which is a special case of a cone,
which is any number (including, as a very special case, zero)
of arrows having a common source.
In both category theory and graph theory the common vertex is called the source.
(However, in category theory it has been common to call it the domain of the arrow,
based on the case of a function in the category of sets.)

Two arrows that have the same target, such as the bottom two in the above diagram,
are called a cospan (pronounced "co-span"),
which is a special case of a cocone,
which is any number (including, as a very special case, zero)
of arrows having a common target.
In category theory the common vertex is called the target
(or sometimes the codomain,
based on the case of a function in the category of sets).
In graph theory the common vertex is called the sink.

(As to the usefulness of the "span/cospan" terminology,
here is an example of its use in a more complex situation:
Cospans and spans of graphs:
a categorical algebra for the sequential and parallel composition of discrete systems
by L. de Francesco Albasini, N. Sabadini, R.F.C. Walters.)

Constructions of pullbacks

There are three valid and useful ways to construct the pullback.
In the first way, we first form the cartesian product set Men × Women,
then apply the comprehension principle to form the subset

{ (man, woman) ∈ Men × Women : PolPref(man) = PolPref(woman) }

Here "man" and "woman" are variables ranging over, respectively,
the sets Men and Women.
The second way is to form the triple cartesian product set Men × Parties × Women,
then to take the subset of that defined by

{ (man, party, woman) ∈ Men × Parties × Women : PolPref(man) = party = PolPref(woman) }

In the third way, the fibered product,
for each party ∈ Parties we form the subsets { man ∈ Men : PolPref(man) = party } and { woman ∈ Women : PolPref(woman) = party },
i.e. the fibers of PolPref : Men ----> Parties and PolPref : Women ----> Parties over party,
then take the cartesian product of those subsets.
After this is done for each party ∈ Parties
we take the sum (coproduct or disjoint union) of the cartesian products.

The kernel pair: when the two arrows of a cospan are equal

An important special case of the pullback is when
the two arrows that make up the cospan are equal.
Suppose, for example, we start with

PolPref-Men PolPref-Men Men ------------> Parties <------------ Men

to form

Men ×_Parties Men / \ / \ / \ |_ _| Men Men \ / PolPref-Men \ / PolPref-Men \ / _| |_ Parties ,

This is usually called by categorists the kernel pair,
although G.M. Kelly called it in a 1969 paper the discriminant.

Why it's called "pullback" and aligning the diagram horizontally and vertically

Drawing the pullback diagram as a diamond balanced on its lowest vertex
is useful in emphasizing that
the two arrows of the cospan play an equal role in defining the pullback, due to that facts that the binary cartesian product is pseudo-symmetric
(i.e., A × B is not equal to B × A, but isomorphic (or bijective)),
while equality is symmetric.
However, in some cases
the arrows play different roles before the pullback is created.
In particular, it often desired to view one of the arrows as being fixed,
while the other arrow is allowed to vary.
To emphasize those different roles,
and also to make drawing such diagrams a lot easier :-)
it is customary in most mathematical writing
to draw the pullback square with horizontal and vertical sides,
rather than sloping sides.
It is often the case that the arrow at the bottom of the square is viewed as fixed,
while the right arrow is viewed as varying.

Here is an example,
where we also use symbols intended to represent arbitrary sets and functions,
not those in the specific example presented above.
(The diagram is presented first using my home-brew HTML format, then using the American Mathematical Society's amsmath cd package.)

X ×_Y B --------> B | | | | g | | V V X -------------> Y f

\begin{equation}\begin{CD} X \times_Y B @>>> B\\ @VVV @VVgV\\ X @>>f> Y\\ \end{CD}\end{equation}

Here $f$ is viewed as a fixed arrow,
while $B \xrightarrow{g} Y$ varies over all the arrows into $Y$,
(called "objects over $Y$").
It is this point of view that caused the construction to be called “pullback”:
it “pulls-back” {objects over $Y$} to {objects over $X$}.

---

For a result about pullbacks which is used repeatedly in both the theory and applications of categories, see “The Pullback Lemma”.

The Pullback Lemma

A key lemma in category theory is the “pullback lemma”.
Here we prove it in the category $\Set$.
(The diagram in $\Set$ showing the situation) is in (the lower part of the box below); (the functions which implement the isomorphism) are shown (above the diagram).

$$\langle\eltx,\elty,\eltc\rangle \mapsto \langle\eltx,\eltc\rangle \mapsto \langle\eltx,\eltx\functionf,\eltc\rangle \mapsto \langle\eltx,\eltc\rangle$$ $$\begin{array}{} \boxed{ \begin{array}{} \\ (\functionf \functiong)\inv \gamma\\ \langle\eltx,\eltc\rangle \mid \eltx\functionf\functiong \xlongequal{\setZ} \eltc\gamma \\ \\ \\ \\ \end{array} } & \stackrel {\text{PBL}}\cong & \boxed{ \begin{array}{} \setX\times_\setY(\setY\times_\setZ\setC) \\ \functionf\inv\functiong\inv \gamma\\ \langle\eltx, \elty, \eltc\rangle \mid \eltx\functionf \xlongequal{\setY} \elty \wedge \elty\functiong \xlongequal{\setZ} \eltc\gamma \\ \langle\eltx,\eltc\rangle \mid \eltx\functionf\functiong \xlongequal{\setZ} \eltc\gamma \\ (\functionf\functiong)\inv\gamma \\ \setX\times_\setZ\setC \\ \end{array} } & \xrightarrow{\mkern3em} & \boxed{ \begin{array}{} \\ \\ \\ \langle\elty,\eltc\rangle \mid \elty\functiong \xlongequal{\setZ} \eltc\gamma \\ \functiong\inv \gamma \\ \setY\times_\setZ\setC \\ \end{array} } & \xrightarrow{\mkern3em} & \setC \\ && \big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \big\downarrow \rlap\gamma \\ && \setX & \xrightarrow[\textstyle \functionf]{} & \setY & \xrightarrow[\textstyle \functiong]{} & \setZ \\ \end{array}$$

A significant example of the use of this result is:

$$\langle\eltx,\elty\rangle \mapsto \eltx \mapsto \langle\eltx,\eltx\functionf\rangle \mapsto \eltx$$ $$\begin{array}{} \boxed{ \begin{array}{} \\ (\functionf \functionB)\inv \radjtop\\ \eltx \mid \eltx\functionf\functionB \xlongequal{\bftwo} \radjtop \\ \end{array} } & \stackrel {\text{PBL}}\cong & \boxed{ \begin{array}{} \functionf\inv\setB\\ \functionf\inv\functionB\inv \radjtop\\ \langle\eltx, \elty\rangle \mid \eltx\functionf \xlongequal{\setY} \elty \wedge \elty\functionB \xlongequal{\bftwo} \radjtop \\ \end{array} } & \xrightarrow{\mkern3em} & \boxed{ \begin{array}{} \setB \\ \functionB\inv \radjtop\\ \elty \mid \elty\functionB \xlongequal{\bftwo} \radjtop \\ \end{array} } & \xrightarrow{\mkern3em} & \bfone\\ && \big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \big\downarrow \rlap\radjtop\\ && \setX & \xrightarrow[\textstyle \functionf]{} & \setY & \xrightarrow[\textstyle \functionB]{} & \bftwo\\ \end{array}$$

This demonstrates the naturality of the predicate/subset bijection.

---

The diagram below is a two-dimensional generalization of the ordinary (one-dimensional) pullback lemma stated above:

\[\begin{array}{} && \boxed{\begin{array}{} (\setU \times_\setZ \setY) \times_{(\setV\times_\setZ\setY)}(\setV \times_\setZ \setX)\\ \eltu, \elty, \eltv, \eltx \mid \eltu\functions\functiont \xlongequal{\setZ} \elty\functiong \land \langle \eltu\functions,\elty \rangle \xlongequal{\setV\times_\setZ\setY} \langle \eltv, \eltx\functionf \rangle \land \eltv\functiont \xlongequal{\setZ} \eltx\functionf\functiong \\ \eltu,\eltx \mid \eltu\functions\functiont \xlongequal{\setZ} \eltx\functionf\functiong \\ \setU \times_\setZ \setX \\ \end{array} } & \xrightarrow{} & \boxed{\begin{array}{} (\setV\times_\setZ\setY) \times_\setY \setX \\ \eltv, \elty, \eltx \mid \eltv\functiont \xlongequal{\setZ} \elty\functiong \land \elty \xlongequal{\setY} \eltx\functionf \\ \eltv,\eltx \mid \eltv\functiong \xlongequal{\setZ} \eltx\functionf\functiong \\ \setV \times_\setZ \setX \\ \end{array} } & \xrightarrow{} & \setX & \ni & \eltx \\ && \Bigg\downarrow & \llap {{\raise2ex\hbox{$\lrcorner$}}\mkern1em} \searrow & \Bigg\downarrow & \mkern-2em{\raise2ex\hbox{$\lrcorner$}} & \Bigg\downarrow \rlap\functionf \\ && \boxed{\begin{array}{} \setU \times_\setV (\setV\times_\setZ\setY) \\ \eltu,\eltv,\elty \mid \eltu\functions \xlongequal{\setV} \eltv \land \eltv\functiont \xlongequal{\setZ} \elty\functiong \\ \eltu,\elty \mid \eltu\functionf\functiong \xlongequal{\setZ} \elty\functiong \\ \setU \times_\setZ \setY \\ \end{array} } & \xrightarrow{} & \boxed{\begin{array}{} \\ \\ \eltv,\elty \mid \eltv\functiont \xlongequal{\setZ} \elty\functiong \\ \setV \times_\setZ \setY \\ \end{array} } & \xrightarrow{} & \setY & \ni & \elty \\ && \Bigg\downarrow & \mkern-10em{\raise2ex\hbox{$\lrcorner$}} & \Bigg\downarrow & \llap { {\raise2ex\hbox{$\lrcorner$}} \mkern3em } \searrow & \Bigg\downarrow \rlap\functiong \\ && \setU & \xrightarrow[\textstyle \mkern.8em \functions \mkern.8em]{} & \setV & \xrightarrow[\textstyle \mkern.8em \functiont \mkern.8em]{} & \setZ \\ &&\eltu &&\eltv \\ \end{array} \]

Relations between limits in categories

2019-03-18 $\Newextarrow{\xrightrightarrows}{5,5}{0x21C9} \Newextarrow{\xRightarrow}{5,5}{0x21D2}$
The content starts on a new page, to keep the rather large diagram below on one page when printing in landscape mode.

$\equ$	$\begin{array}{} \boxed{ \begin{array}{} \boxed{ \begin{array}{} \setX\times_{(\setX\times\setY)}\setX \\ \eltx,\eltxp \mid \langle \eltx,\eltx\functionf \rangle \xlongequal{\setX\times\setY} \langle \eltxp,\eltxp\functiong \rangle \\ \eltx,\eltxp \mid \eltx \xlongequal{\setX} \eltxp \land \eltx\functionf \xlongequal{\setY} \eltxp\functiong \\ \eltx \mid \eltx\functionf \xlongequal{\setY} \eltx\functiong \\ \boxed{ \langle \functionf,\functiong \rangle \Equ} \\ \end{array} } & \xrightarrow{} & \setX \\ \llap{\langle \functionf,\functiong \rangle \equ} \Big\downarrow & \mkern-2em\smash{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow \rlap{\langle \setX,\functiong \rangle} \\ \setX & \xrightarrow{\smash{ \textstyle \langle \setX,\functionf \rangle }} & \setX\times\setY \\ \end{array} \mkern1.5em } \\ \boxed{ \begin{array}{} \boxed{ \begin{array}{} \eltx,\elty \mid \eltx\functionf = \elty = \eltx\functiong \\ \eltx \mid \eltx\functionf = \eltx\functiong \\ \boxed{ \langle \functionf,\functiong \rangle \Equ} \\ \end{array} } & \xrightarrow{} & \boxed { \begin{array}{} \eltx,\elty,\eltxp \mid \eltx\functionf = \elty = \eltxp\functiong \\ \eltx,\eltxp \mid \eltx\functionf = \eltxp\functiong \\ \end{array} } & \xrightarrow{} & \setY \\ \llap{\langle \functionf,\functiong \rangle \equ} \Big\downarrow & \mkern-2em\smash{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow & \mkern-2em\smash{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow \rlap{\Delta_\setY} \\ \setX & \xrightarrow{\smash {\textstyle \Delta_\setX}} & \setX\times\setX & \xrightarrow{\smash {\textstyle \functionf\times\functiong}} & \setY\times\setY \\ \Vert &&&& \Vert \\ \setX & {}\rlap{\mkern-2em\xrightarrow[\textstyle \mkern17em]{\smash {\textstyle \langle \functionf,\functiong \rangle }}} &&& \setY\times\setY \\ \end{array} } \\ \end{array} $		$ \boxed { \begin{array}{} \big(\setX \xrightrightarrows[\functiong]{\functionf}\setY\big)\Limit \\ \boxed{ \langle \functionf,\functiong \rangle \Equ } \\ \eltx \mid \eltx\functionf = \eltx\functiong \\ \end{array} } \xrightarrow{\textstyle \boxed{\langle \functionf,\functiong \rangle \equ}} \setX \xrightrightarrows[\textstyle\functiong]{\textstyle\functionf} \setY $
$\kp$	$\begin{array}{} \boxed{ \begin{array}{} \boxed{ \functionf\Kp} && \xrightrightarrows[\smash {\textstyle \functionf\kp}]{} && \setX \\ \Vert &&&& \Vert \\ \boxed{ \begin{array}{} \eltx,\elty,\eltxp \mid \eltx\functionf = \elty = \eltxp\functionf \\ \eltx,\eltxp \mid \eltx\functionf = \eltxp\functionf \\ \boxed{ \functionf\Kp} \\ \end{array} } & \xrightarrow{} & \setX\times\setX & \xrightrightarrows[\textstyle \pi_1]{\textstyle \pi_0} & \setX \\ \big\downarrow & \mkern-2em\smash{\raise2ex\hbox{$\lrcorner$}} & \smash{\Bigg\downarrow\rlap{\mkern-1.5em \functionf\times\functionf}} && \smash{\Bigg\downarrow \rlap\functionf} \\ \setY & \xrightarrow{\smash {\textstyle\Delta_\setY}} & \setY\times\setY & \xrightrightarrows[\textstyle \pi_1]{\smash{\textstyle \pi_0}} & \setY \\ \end{array} \mkern.5em} \\ \boxed{ \begin{array}{} \boxed{ \begin{array}{} \eltx,\eltxp \mid \eltx\functionf = \eltxp\functionf \\ \boxed{ \functionf\Kp} \\ \end{array} } & \xrightarrow{} & \setX \\ \Big\downarrow & \mkern-2em\smash{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow \rlap{\functionf} \\ \setX & \xrightarrow{\smash {\textstyle \mkern.5em\functionf\mkern.5em}} & \setY \\ \end{array} \mkern1.5em } \\ \end{array} $	$\begin{array}{} \boxed{ \begin{array}{} \big(\setX \xrightarrow{\functionf} \setZ \xleftarrow{\functionf} \setX\big)\Limit \\ \boxed{\functionf\Kp} \\ \eltx,\eltxp \mid \eltx\functionf = \eltxp\functionf \\ \end{array} } & \xrightrightarrows{\textstyle \boxed{\functionf\kp}} & \setX & \xrightarrow{\textstyle\functionf} & \setY \\ \end{array}$	$\begin{array}{} \boxed{ \begin{array}{} \langle \pi_0\functionf,\pi_1\functionf \rangle \Equ \\ \eltx,\eltxp \mid \langle \eltx,\eltxp \rangle \pi_0\functionf = \langle \eltx,\eltxp \rangle \pi_1\functionf \\ \eltx,\eltxp \mid \eltx\functionf = \eltxp\functionf \\ \boxed{\functionf\Kp} \\ \end{array} } \\ & \llap{\langle \pi_0\functionf,\pi_1\functionf \rangle \equ} \searrow \\ && \setX\times\setX & \xrightarrow{\textstyle \pi_1} & \setX \\ && \llap{\pi_0} \big\downarrow & \not= & \big\downarrow \rlap\functionf \\ && \setX & \xrightarrow[\textstyle \functionf]{} & \setY \\ \end{array}$
$\pb$	$\begin{array}{} \boxed{\begin{array}{} \big(\setX \xrightarrow{\functionf} \setZ \xleftarrow{\functiong} \setY\big)\Limit \\ \boxed{\setX\times_\setZ\setY} \\ \eltx,\eltz,\elty \mid \eltx\functionf = \eltz = \elty\functiong \\ \eltx,\elty \mid \eltx\functionf = \elty\functiong \\ \end{array} } & \xrightarrow{} & \setY \\ \bigg\downarrow & \mkern-2em\smash{\raise2ex\hbox{$\lrcorner$}} & \bigg\downarrow \rlap{\functiong} \\ \setX & \xrightarrow[\textstyle \mkern.5em\functionf\mkern.5em]{} & \setZ \\ \end{array} $		$\begin{array}{} \boxed{ \begin{array}{} \langle \pi_0\functionf,\pi_1\functiong \rangle \Equ \\ \eltx,\elty \mid \langle \eltx,\elty \rangle \pi_0\functionf = \langle \eltx,\elty \rangle \pi_1\functiong \\ \eltx,\elty \mid \eltx\functionf = \elty\functiong \\ \boxed{\setX\times_\setZ\setY} \\ \end{array} } \\ & \llap{\langle \pi_0\functionf,\pi_1\functiong \rangle \equ} \searrow \\ && \setX\times\setY & \xrightarrow{\textstyle \pi_1} & \setY \\ && \llap{\pi_0} \big\downarrow & \not= & \big\downarrow \rlap\functiong \\ && \setX & \xrightarrow{\smash {\textstyle \functionf}} & \setZ \\ \end{array}$
	$\pb$	$\kp$	$\equ$

---

What is below is a draft.

$\kp$ as a weighted limit

Let $\calK = \bftwo$ be a category with two objects, say $\objectK$ and $\objectL$, and only one non-identity arrow: $\objectK \xrightarrow{\textstyle \arrowk} \objectL$.
$\calK$ is purely an indexing category, with its objects and arrows having no significance beyond their use as indices.
Think of $\objectK,\objectL$ as analogous to $i,j$ as indices into sequences, and $\objectK \xrightarrow{\textstyle \arrowk} \objectL$ as analogous to $i \lt j$.

Let $2$ be a set with two elements, $0$ and $1$.
Let ($\setX\xrightarrow{\functionf}\setY$ be an arbitrary function in $\Set$), and ($2\xrightarrow{!_2}1$ be the only possible function).
Each of these (functions in $\Set$) defines (a functor $\bftwo\to\Set$), the "name" of (the function),
just as each (set in $\Set$) defines (a functor $\bfone\to\Set$), called the "name" of (the set).

$\begin{array}{} 2 & \xrightarrow{\textstyle !_2} & 1 \\ \big\downarrow && \big\downarrow \\ \setX & \xrightarrow[\textstyle \functionf]{} & \setY \\ \end{array}$ The "weighted limit" $\boxed{\{2\xrightarrow{!_2}1, \setX\xrightarrow{\functionf}\setY\}}$ of these two functors,
with (the first being the "weight") and (the second being that whose limit is being taken),
is (per (3.7) of Max Kelly's Basic Concepts of Enriched Category Theory) {the set of natural transformations from $2\xrightarrow{!_2}1$ to $\setX\xrightarrow{\functionf}\setY$}
i.e. the set $\hom {(2\xrightarrow[!_2]{}1)} {[\bftwo,\Set]} {( \setX \xrightarrow[\functionf]{} \setY )}$ of all possible ways of selecting vertical (downward) arrows (i.e., functions) to make the square at right commute.
But (arrows $2\to\setX$ on the left of the square) correspond to (pairs of elements $\eltx_0,\eltx_1$ of $\setX$),
while (arrows $1\to\setY$ on the right) correspond to (single elements $\elty$ of $\setY$).
The requirement that (the diagram commute) is that ($\eltx_0\functionf = \elty$ and $\eltx_1\functionf = \elty$).
But that is just the condition defining (the kernel pair of $\functionf$, $\functionf\Kp$).
Thus (the kernel pair) is a simple example of (a weighted limit).

---

Comparison of conical limits and weighted limits in $\Set$

	conical limit	weighed limit
		for specific weight and target functors	for general weight and target functors
	commuting triangles (two)	commuting squares (one)
indexing category $\calK$	$\objectK_0 \xrightarrow{\arrowk_0} \objectL \xleftarrow{\arrowk_1} \objectK_1$	$\objectK \xrightarrow{\arrowk} \objectL$
weighting functor $\functorF:\calK\to\Set$	$\big( 1 \xrightarrow{1_1} 1 \xleftarrow{1_1} 1 \big) = \big(!_\calK1\big)$	$2 \xrightarrow{!_2} 1$	$\objectK\functorF \xrightarrow{\arrowk\functorF} \objectL\functorF$
target functor $\functorG:\calK\to\Set$	$\setX \xrightarrow{\functionf} \setY \xleftarrow{\functionf} \setX$	$\setX \xrightarrow{\functionf} \setY$	$\objectK\functorG \xrightarrow{\arrowk\functorG} \objectL\functorG$
Diagrams	$ \begin{array}{} \cdot & \xrightarrow{} & \cdot & \xleftarrow{} & \cdot \\ \\ \\ && 1 \\ & \llap{\eltx_0} \swarrow & \llap\elty \downarrow & \searrow \rlap{\eltx_1} \\ \setX & \xrightarrow[\textstyle \functionf]{} & \setY & \xleftarrow[\textstyle \functionf]{} & \setX \\ \end{array} $	$ \begin{array}{} && \cdot & \xrightarrow{} & \cdot \\ \\ 1 & \xrightrightarrows[\textstyle 1]{\textstyle 0} & 2 & \xrightarrow{\textstyle !_2} & 1 \\ \Vert && \llap\eltx \downarrow && \downarrow \rlap\elty \\ 1 & \xrightrightarrows[\eltx_1 \xlongequal{\setX} 1\eltx ]{\eltx_0 \xlongequal{\setX} 0\eltx} & \setX & \xrightarrow[\textstyle \functionf]{} & \setY \\ \end{array} $	$ \begin{array}{} & \mkern1em & \objectK & \xrightarrow{\textstyle \arrowk} & \objectL \\ \\ \functorF && \objectK\functorF & \xrightarrow{\textstyle \arrowk\functorF} & \objectL\functorF \\ \llap\nattransalpha \Bigg\Downarrow && \llap{\objectK\nattransalpha} \Bigg\downarrow && \Bigg\downarrow \rlap{\objectL\nattransalpha} \\ \functorG && \objectK\functorG & \xrightarrow[\textstyle \arrowk\functorG]{} & \objectL\functorG \\ \end{array} $
Equations	$\eltx_0\functionf \xlongequal{\setY} \elty \xlongequal{\setY} \eltx_1\functionf$	$ \begin{array}{} && \eltx\functionf & \xlongequal{\textstyle [2,\setY]} & !_2\elty \\ \eltx_0\functionf & \xlongequal{\setY} & 0\eltx\functionf & \xlongequal{\setY} & 0!_2\elty & \xlongequal{\setY} & \elty \\ \eltx_1\functionf & \xlongequal{\setY} & 1\eltx\functionf & \xlongequal{\setY} & 1!_2\elty & \xlongequal{\setY} & \elty \\ \end{array} $	$ \begin{array}{} \objectK\nattransalpha \cdot \arrowk\functorG & \xlongequal{\textstyle [\objectK\functorF,\objectL\functorG]} & \arrowk\functorF \cdot \objectL\nattransalpha \\ \end{array} $
Notation	$\begin{array}{} \big( \setX \xrightarrow{\textstyle \functionf} \setY \xleftarrow{\textstyle \functionf} \setX \big)\Limit \\ \setX\times_\setY\setX \\ \end{array}$	$\big\{(2 \xrightarrow{\textstyle !_2} 1),\, (\setX \xrightarrow{\textstyle \functionf} \setY) \big\}$	$\big\{\functorF,\, \functorG \big\}$
as a set of natural transformations	$ \hom {(!_\calK1)} {[\bftwo\vee\bftwo,\Set]} {( \setX \xrightarrow[\functionf]{} \setY \xleftarrow[\functionf]{} \setX )} $	$ \hom {(2\xrightarrow[!_2]{}1)} {[\bftwo,\Set]} {( \setX \xrightarrow[\functionf]{} \setY )} = \hom {!_2} {[\bftwo,\Set]} {\functionf} $	$ \hom \functorF {[\calK,\Set]} \functorG $

In ordinary mathematics first we give explicit definitions of various categorical limits, most basically the product of two sets.
Then we show that (these definitions) satisfy (universal properties).
Analogous to that approach, for $\functorF,\functorG:\calK\to\Set$, we have given above an explicit definition of $\big\{\functorF,\, \functorG \big\}$ as $\hom \functorF {[\calK,\Set]} \functorG$.
Now we show that (that definition) satisfies (the universal property that Kelly uses, in (3.1), to characterize $\big\{\functorF,\, \functorG \big\}$).
\[\begin{array}{} \big[\objectT, \hom \functorF {[\calK,\Set]} \functorG \big] &&&& \hom \functorF {[\calK,\Set]} {[\objectT,\functorG]} & \buildrel \text{(3.1)} \over \cong & \big[\objectT,\{\functorF,\functorG\}\big]\\ \llap{(2.10)} \Vert &&&& \Vert \rlap{(2.10)} \\ \big[\objectT, \int_\objectK [\objectK\functorF,\objectK\functorG] \big] & \mathop\cong\limits^{\text{(2.3)}}_{\text{right adjoints preserve limits}} & \displaystyle\int_\objectK \big[\objectT, [\objectK\functorF,\objectK\functorG] \big] & \buildrel{\text{sym.}} \over \cong & \displaystyle\int_\objectK \big[\objectK\functorF, [\objectT,\objectK\functorG] \big] \\ \\ \text{$\objectT$-tuples} &&&& \text{matching pairs} \\ \text{of matching pairs} &&&& \text{of $\objectT$-tuples} \\ \end{array}\] Thus $\hom \functorF {[\calK,\Set]} \functorG$ satisfies (Kelly’s definition (3.1) of $\big\{\functorF,\, \functorG \big\}$), justifying $\big\{\functorF,\, \functorG \big\} \buildrel \text{(3.7)} \over \cong \hom \functorF {[\calK,\Set]} \functorG$.

(The counits $\boxed{ \calK \twocellctb \mu \functorF {\big[\{\functorF,\functorG\},\functorG {\big]}} \Set }$) of (the representation (3.1)),
for (the specific example above of $\big\{!_2,\,\functionf \big\} \cong \hom {!_2} {[\bftwo,\Set]} {\functionf}$) at the left, and (the general case $\big\{\functorF,\, \functorG \big\} \cong \hom \functorF {[\calK,\Set]} \functorG$) at the right, are then: \[\begin{array}{} 2 & \xrightarrow{\textstyle !_2} & 1 & \mkern8em & \objectK\functorF & \xrightarrow{\textstyle \arrowk\functorF} & \objectL\functorF \\ \llap{\objectK\mu} \bigg \downarrow \rlap{{} = \overline{\objectK\pi} = \overline{\objectK\lambda}} && \llap{\objectL\mu} \bigg \downarrow \rlap{{} = \overline{\objectL\pi} = \overline{\objectL\lambda}} && \llap{\objectK\mu} \bigg \downarrow \rlap{{} = \overline{\objectK\pi} = \overline{\objectK\lambda}} && \llap{\objectL\mu} \bigg \downarrow \rlap{{} = \overline{\objectL\pi} = \overline{\objectL\lambda}} \\ \big[ \hom {!_2} {[\bftwo,\Set]} {\functionf}, \setX \big] & \xrightarrow[\textstyle \big[ \hom {!_2} {[\bftwo,\Set]} {\functionf}, \functionf {\big]}]{} & \big[ \hom {!_2} {[\bftwo,\Set]} {\functionf}, \setY \big] && \big[ \hom {\functorF} {[\calK,\calV]} {\functorG}, \objectK\functorG \big] & \xrightarrow[\textstyle \big[ \hom {\functorF} {[\calK,\calV]} {\functorG}, \arrowk\functorG{\big]}]{} & \big[ \hom {\functorF} {[\calK,\calV]} {\functorG}, \objectL\functorG \big] \\ \end{array}\] $\objectK\mu$ sends $0\in2$ to the projection $\langle \eltx_0,\eltx_1,\elty \rangle \mapsto \eltx_0$, and $1\in2$ to the projection $\langle \eltx_0,\eltx_1,\elty \rangle \mapsto \eltx_1$.
$\objectL\mu$ sends the unique element of $1$ to the projection $\langle \eltx_0,\eltx_1,\elty \rangle \mapsto \elty$.
The commuting of (the naturality square for $\mu$) follows from (the naturality of each transformation $!_2 \xRightarrow{\textstyle \langle \eltx_0,\eltx_1,\elty \rangle } \functionf$); see (the diagram for it above).

---

The above has concerned the weighted limit of ordinary functors $\functorF,\functorG:\calK\to\Set$.
Perhaps unsurprisingly, weighted limits may be defined on more general classes of functors.
To wit, we have the following four possibilities for the targets of our weight ($\functorF$) and target ($\functorG$) functors,
from (the least general at the upper left) (the case $\calB=\calV=\Set$ already considered) to (the most general at the lower right):

		$\functorF:\calK\to\calV$
		$\calV=\Set$ (functors are $\Set$-functors)	$\calV$ (functors are $\calV$-functors)
$\functorG: \calK\to\calB$	$\calB=\calV$	$\begin{array}{}\functorF & : & \calK & \to & \Set \\ \functorG & : & \calK & \to & \Set \end{array}$ $\big\{\functorF,\functorG\} = \hom \functorF {[\calK,\Set]} \functorG$	$\begin{array}{}\functorF & : & \calK & \to & \calV \\ \functorG & : & \calK & \to & \calV \end{array}$ $\big\{\functorF,\functorG\} = \hom \functorF {[\calK,\calV]} \functorG$
	$\calB$	$\begin{array}{}\functorF & : & \calK & \to & \Set \\ \functorG & : & \calK & \to & \calB \end{array}$	$\begin{array}{}\functorF & : & \calK & \to & \calV \\ \functorG & : & \calK & \to & \calB \end{array}$

Here $\calV$ is an arbitrary base category (e.g. $\Set$), while $\calB$ is a category enriched in $\calV$.

Pushouts: uniting and identifying

C / \ f / \ g / \ |_ _| A B \ / \ / \ / _| |_ A +_C B

Given a span of sets as shown above
(i.e, sets A, B, C and functions f, g between them as shown above),
we "add", that is, take the disjoint union of, the sets A and B,
then, for each element c in C,
identify f(c) (in the union) with g(c) (in the union).
(Actually, we take the smallest equivalence relation which includes all such identifications,
and divide the A + B by that equivalence relation.)
The resulting cospan diagram (depicted above>
is called the pushout
of the span diagram determined by f and g.
As just defined,
it evidently combines both uniting (taking the disjoint union of) A and B
with identifying elements of A and B as determined by the span with vertex C.

Pushups, pullups and situps

Sorry, you have the wrong blog :-) !
Try a physical fitness blog.

Injection, full, monic, faithful, conservative in category theory

The concepts named in the subject line are related, even interdefinable, and provide examples of each other. $\Newextarrow{\xLeftarrow}{2,2}{0x21D0}$
The purpose of this post is to show some of those interrelations.

\[\begin{array}{cccl} \setX & \xrightarrow{\textstyle \mkern1em \functionf \mkern1em} & \setY && \text{a function in $\Set$} \\ (\eltx = \eltxp) & \xLeftarrow{} & (\eltx\functionf = \eltxp\functionf) && \text{$\functionf$ is $\textit{injective}$ iff, $\forall \eltx, \eltxp\in\setX$, this logical implication holds } \\ \hom \eltx \setX \eltxp & \xrightarrow {\textstyle \hom \eltx \functionf \eltxp} & \hom {\eltx\functionf} \setY {\eltxp\functionf} && \text{the arrow in $\calV$ between the hom-objects} \\ \end{array}\]

If we consider $\setX \xrightarrow{\textstyle \mkern1em \functionf \mkern1em} \setY$ as, not (a function in $\Set$), but as (a $\calV$-functor between discrete categories enriched in either $\calV=\bftwo$ or $\calV=\Set$),
then this condition amounts to saying that the arrow in the third line, in $\calV$, is invertible, i.e.,
that (the $\calV$-functor $\functionf$ between discrete $\calV$-categories) is not merely faithful, as it automatically is in those cases, but also full, i.e.,
that $\functionf$ is a full and faithful, or fully faithful $\calV$-functor.

Well-ordering and induction

$\Newextarrow{\xleftrightarrow}{10,10}{0x2194} \Newextarrow{\xRightarrow}{10,10}{0x21D2} \Newextarrow{\xLeftrightarrow}{10,10}{0x21D4}$ 2018-06-20 to ???

ABSTRACT: We define the four vertices and prove the seven implications of: \[\begin{array}{} && WO && \longrightarrow \atop \longleftarrow && DCC \\ & \swarrow && \searrow\nwarrow \\ SIND && \longrightarrow \atop \longleftarrow && PIND \mkern30mu . \\ \end{array}\] The proofs involve an interesting combination of first- and second-order logic.

---

Context:

$\N = \{0,1,2,\ldots\}$ is the set of natural numbers, and $\functions : \N \longrightarrow \N : \numbern \mapsto \numbern+1$ is its successor endofunction.
Let $\N$ also denote the corresponding discrete category, whose only arrows are its identity arrows, and let $\functions$ also denote the corresponding endofunctor.
Let $\bftwo$ be the category whose objects are $\leftadj\bot$ and $\rightadj\top$, whose only non-identity arrow is $\leftadj\bot \lt \rightadj\top$, also notated $\leftadj\bot \to \rightadj\top$ or $\leftadj\bot \Rightarrow \rightadj\top$
(an arrow realizing the ex falso sequitur quodlibet principle of logic).
Functions/functors $\functionA:\N \longrightarrow \bftwo : \numbern\mapsto\functionA_\numbern$ are called predicates on $\N$.

---

$ICON$, $SCON$, and $SIND$

The two conditions (on a predicate $\functionA:\N \rightarrow \bftwo$) for successor induction are:

initial condition ($ICON$):

$\functionA_0$ is true, i.e., there is an arrow in $\bftwo$, $ICON : \rightadj\top \xRightarrow{\textstyle ICON} \functionA_0$, i.e., there is a 2-cell in $\Cat$: $\mkern20mu$ \(\begin{array}{} \catI && { \xrightarrow[]{\textstyle 0} } && \N \\ & \llap{\rightadj\top} \searrow & \xRightarrow{\textstyle ICON} & \swarrow \rlap{\lower3pt\hbox{$\mkern-10mu\functionA$}} \\ && \bftwo \\ \end{array}\)

successor condition ($SCON$):

$SCON : (\forall\numbern\in\N) \Big[ \functionA_\numbern \xRightarrow{\textstyle SCON(\numbern)} \functionA_{\numbern+1} \Big]$
i.e., there is a transformation (automatically natural because $\N$ is discrete) in $\Cat$: \[\begin{array}{} &&&&&& \N \\ { \N } && { \xrightarrow[]{\textstyle \mkern10mu \functionA \mkern10mu} } && \bftwo &&& \mkern10mu \searrow \rlap{\raise3pt\hbox{$\mkern-10mu\functionA$}} &&&& \N && \xrightarrow{\textstyle \functions} && \N \\ & \llap{\lower3pt\hbox{$\functions \mkern{-10mu}$}} \searrow & \Big\Downarrow \rlap{\mkern-34mu SCON} & \nearrow \rlap{\lower3pt\hbox{$\mkern-10mu\functionA$}} && \mskip80mu \text{i.e.} \mskip80mu & \llap{\functions} \Bigg\downarrow & \mkern-20mu\Big\Downarrow\rlap{\mkern-34mu SCON} && \bftwo & \mskip80mu \text{i.e.} \mskip80mu && \llap{\functionA}\searrow & \xRightarrow{\textstyle SCON} & \swarrow\rlap{\functionA \mskip 60mu ,} \\ && \N &&&&& \mkern10mu \nearrow \rlap{\lower3pt\hbox{$\mkern-10mu\functionA$}} &&&&&& \bftwo \\ &&&&&& \N \\ \end{array}\] i.e., $\functorA$ is an opcoalgebra (equivalently, a co-opalgebra) for the endofunction/endofunctor $\functions$, i.e., an $\functions$-opcoalgebra or $\functions$-co-opalgebra.

The (initial condition $ICON$) and (successor condition $SCON$) form the antecedent in (successor induction $SIND$):

successor induction ($SIND$):

$SIND : (ICON \wedge SCON) \xRightarrow{\textstyle SIND} (\functionA = \top)$, i.e.,
$SIND : \bigg( \functionA_0 \wedge (\forall\numbern\in\N) \Big[ \functionA_\numbern \xRightarrow{\textstyle SCON(\numbern)} \functionA_{\numbern+1} \Big] \bigg) \xRightarrow{\textstyle SIND} (\functionA = \top)$.

This is generally called “the principle of mathematical induction” or “induction schema”,
however calling it “successor induction” makes more clear its relation to the “predecessors induction” (often called “complete induction”) defined below.

---

The predicate $\functionA$ generates a 2-diagram in $\Cat$:

The above data generate a 2-diagram in the 2-category $\Cat$, shown twice below
(where $\numbern_0$ and $\numbern_0-1$ are hypothetical elements of $\N$, and $\catI$ is the unit category):

\[\begin{array}{} \numbern_0-1 & \in & { \rightadj\top\downarrow\functionA } && { \xrightarrow[]{\textstyle \mkern40mu \llap{! \mkern20mu} {} \mkern40mu} } && \catI \\ && & \searrow & \raise6pt\hbox{$\Vert$} & { \nearrow \rlap{\lower3pt\hbox{${!}$}} } \\ && && { \rightadj\top\downarrow\functionA } \\ && { \Big\downarrow } && { \mkern{-50mu} \Big\Downarrow } && \rightadj{ \Big\downarrow \rlap\top } \\ && & \Big\Vert && { \Big\Downarrow } \\ && && { \Big\downarrow } \\ && { \N } && { \xrightarrow[]{\textstyle \mkern40mu \llap{\functionA\mkern20mu} {} \mkern40mu} } && \bftwo \\ & \llap{\raise3pt\hbox{$\numbern_0 - 1 \mkern{-10mu}$}} \nearrow & \Vert & \llap{\lower3pt\hbox{$\functions \mkern{-10mu}$}} \searrow & \Big\Downarrow \rlap{\mkern-34mu SCON} & { \nearrow \rlap{\lower3pt\hbox{$\mkern-10mu\functionA$}} } & \leftadj{ \Big\uparrow \rlap\bot } \\ \catI && \xrightarrow[\textstyle \numbern_0]{} && { \N } & \Big\Downarrow & \catI \\ &&&& \Big\uparrow & { \nearrow \rlap{\lower3pt\hbox{${!}$}} } \\ && \numbern_0 & \in & \functionA\downarrow\leftadj\bot \\ \end{array}\]

The same diagram rotated clockwise by a quarter-turn: (you have to add two long southwest-pointing diagonals yourself, instances of $\functionA$ and of ${!}$, and add three 2-cells, corresponding to the lower ($SCON$), back (universal), and top (equality) faces of the triangular prism in the diagram on the left).

\[\begin{array}{} && \catI \\ &&& \searrow \rlap{\numbern_0-1} \\ && \llap{\numbern_0} \Bigg\downarrow & = & \N & \leftarrow & \rightadj\top\downarrow\functionA \\ &&& \swarrow \rlap{\functions} & = & \swarrow\\ \functionA\downarrow\leftadj\bot & \xrightarrow{} & \N & \xleftarrow{} & \rightadj\top\downarrow\functionA \\ \llap{!} \Bigg\downarrow & \Leftarrow & \Bigg\downarrow \rlap{\mkern-14mu\functionA} & \Leftarrow & \Bigg\downarrow \rlap{!} \\ \catI & \xrightarrow[\textstyle \leftadj\bot]{} & \bftwo & \xleftarrow[\textstyle \rightadj\top]{} & \catI \\ \end{array}\]

---

Comparing (predicates on $\N$) and (subsets of $\N$)

In comparing induction, which is about (predicates on $\N$), to well-ordering, which is about (subsets of $\N$),
we will use a certain bijection between the two, the composite shown below: \[\begin{array}{} [\N,\bftwo] & \xleftrightarrow{\text{characteristic map}} & \Sub(\N) & \xleftrightarrow{\text{set-theoretic complement}} & \Sub(\N) \\ \functionA & \leftrightarrow & \top\downarrow\functionA & \leftrightarrow & \functionA\downarrow\bot \\ {?}\notin\setS = {?}\in\tilde\setS & \leftrightarrow & \tilde\setS & \leftrightarrow & \setS \\ \end{array}\]

---

$WO \Rightarrow SIND$

Suppose ($\functionA\downarrow\leftadj\bot$ is non-empty), i.e., ($\functionA\downarrow\leftadj\bot \not= \emptyset$), i.e., $(\exists\numbern\in\N)(\numbern\in\functionA\downarrow\leftadj\bot)$, i.e., $(\exists\numbern\in\N)(\functionA_\numbern \to \leftadj\bot)$, i.e., ($\functionA_\numbern$ is false for some $\numbern\in\N$).
If ($\N$ is well-ordered), then (the non-empty $\functionA\downarrow\leftadj\bot$) has (a least member, $\boxed{\numbern_0}$),
i.e., $(\numbern_0 \in \functionA\downarrow\leftadj\bot)$ and $(\forall \numbern \in \functionA\downarrow\leftadj\bot) (\numbern_0 \le \numbern)$.
Then we have \[\top \Rightarrow (\top \xRightarrow{ICON} \functionA_0) \Rightarrow (0 \in \rightadj\top\downarrow\functionA) \xRightarrow{\cap = \emptyset} (0 \notin \functionA\downarrow\leftadj\bot) \xRightarrow{\numbern_0 \in \functionA\downarrow\leftadj\bot} ( \numbern_0 \not= 0 ) \Rightarrow (\exists (\numbern_0 - 1) \in \N) \; . \] Then \[\top \Rightarrow (\numbern_0-1 \lt \numbern_0) \xRightarrow{\cap} (\numbern_0 \not\le \numbern_0-1) \xRightarrow[\text{contrapositive}]{\numbern_0 \text{ least}} (\numbern_0-1 \notin \functionA\downarrow\leftadj\bot) \xRightarrow{\cup} (\numbern_0-1 \in \rightadj\top\downarrow\functionA) \xRightarrow{SCON(\numbern_0 - 1)} ((\numbern_0-1)+1 = \numbern_0 \in \rightadj\top\downarrow\functionA) \xRightarrow{\cap} (\numbern_0 \notin \functionA\downarrow\leftadj\bot) \xRightarrow{\numbern_0 \in \functionA\downarrow\leftadj\bot} \bot \; . \] We have derived a contradiction, so one of our assumptions must be invalid.
If $\N$ is well-ordered and $\functionA$ satisfies $ICON$ and $SCON(\numbern_0 - 1)$,
this must mean that ($\functionA\downarrow\leftadj\bot$ is NOT non-empty).
By (the law of the excluded middle),
this means ($\functionA\downarrow\leftadj\bot$ is empty), i.e., (its complement $\rightadj\top\downarrow\functionA$ is all of $\N$).
So ($\functionA_\numbern$ is true for all $\numbern\in\N$).
Expressing this symbolically, and deriving the desired consequence, we have: \[\begin{array}{} WO \wedge (\functionA\downarrow\bot \not= \emptyset) \wedge ICON \wedge SCON \xRightarrow{WO} \big( (\exists\numbern_0\in\functionA\downarrow\bot)(\forall \numbern \in \functionA\downarrow\bot) (\numbern_0 \le \numbern) \big) \wedge ICON \wedge SCON \xRightarrow{\text{by the above}} \bot \\ WO \wedge ICON \wedge SCON \Longrightarrow \big[ \neg (\functionA\downarrow\bot \not= \emptyset) \big] \xlongequal{\text{excluded middle}} (\functionA\downarrow\bot = \emptyset) \xlongequal{\cup} (\top\downarrow\functionA = \N) = (\functionA=\top), \rlap{\mkern30mu \text{in short:}} \\ (WO \wedge ICON \wedge SCON) \Longrightarrow (\functionA = \top) \\ WO \Longrightarrow \big[ (ICON\wedge SCON) \Rightarrow (\functionA = \top) \big] = SIND \; .\\ \end{array}\]

---

$PCON$ and $PIND$

There is an alternative version of induction,
which replaces the two conditions, the initial condition ($ICON$) and the successor condition ($SCON$) of successor induction ($SIND$),
with a single induction condition, the predecessors condition ($PCON$) (note the plural):

predecessors condition ($PCON$):

$PCON : (\forall\numbern\in\N)\Big[(\forall\numberk\lt\numbern)\functionA_\numberk \xRightarrow[]{\textstyle PCON(\numbern)} \functionA_\numbern \Big]$, $\mkern40mu$ i.e., by the definition of relative quantification,
$PCON : (\forall\numbern\in\N)\Big[(\forall\numberk\in\N)[\numberk\lt\numbern \Rightarrow \functionA_\numberk] \xRightarrow[]{\textstyle PCON(\numbern)} \functionA_\numbern \Big]$.

In interpreting those logical statements, recall that the quantifiers “$\forall$” and “$\exists$” bind more tightly than binary connectives such as “$\Rightarrow$”,
so $(\forall\numberk\lt\numbern)\functionA_\numberk \Rightarrow \functionA_\numbern$ is equivalent to $\big((\forall\numberk\lt\numbern)\functionA_\numberk \big) \Rightarrow \functionA_\numbern$, NOT $(\forall\numberk\lt\numbern)[\functionA_\numberk \Rightarrow \functionA_\numbern]$.

(The predecessors condition for $\numbern=0$, $PCON(0)$), is equivalent to (the initial condition, $ICON$),
for the following are logically equivalent:

\(\begin{array}{r} PCON(0) \\ (\forall\numberk\lt 0)\functionA_\numberk \Rightarrow \functionA_0 \\ (\forall\numberk\in\N)[\numberk\lt 0 \Rightarrow \functionA_\numberk] \Rightarrow \functionA_0 \\ (\forall\numberk\in\N)[\bot \Rightarrow \functionA_\numberk] \Rightarrow \functionA_0 \\ (\forall\numberk\in\N)(\top) \Rightarrow \functionA_0 \\ \top \Rightarrow \functionA_0 \\ ICON \\ \end{array}\)

(The equivalence $(\forall\numberk\lt 0)\functionA_\numberk \Leftrightarrow \top$ demonstrated above) is sometimes described by (the phrase “$(\forall\numberk\lt 0)\functionA_\numberk$ is vacuously true”).

(The predecessors condition $PCON$) is the antecedent in (predecessors induction $PIND$):

predecessors induction ($PIND$):

$PIND : PCON \xRightarrow{\textstyle PIND} (\functionA = \top)$ , $\mkern40mu$ i.e.,
$PIND : (\forall\numbern\in\N)\Big[(\forall\numberk\lt\numbern)\functionA_\numberk \xRightarrow[]{\textstyle PCON(\numbern)} \functionA_\numbern \Big] \xRightarrow{\textstyle PIND} (\functionA = \top)$ .

---

$WO \Rightarrow PIND$

The proof above that $WO \Rightarrow SIND$ can be easily modified to show $WO \Rightarrow PIND$.
The key is to examine what it means to say that ($\numbern_0$ is least in $\functionA\downarrow\leftadj\bot$).
On the one hand, ($\numbern_0\in \functionA\downarrow\leftadj\bot$) means ($\functionA_{\numbern_0}$ is false).
On the other hand, we have a chain of logical equivalences:

\(\begin{array}{l} (\forall\numbern\in \functionA\downarrow\leftadj\bot) (\numbern_0\le\numbern)\\ (\forall\numbern\in\N) [\numbern\in \functionA\downarrow\leftadj\bot \Rightarrow \numbern_0\le\numbern] & \text{ (definition of relative quantifier)} \\ (\forall\numbern\in\N) [\numbern_0\not\le\numbern \Rightarrow \numbern\notin \functionA\downarrow\leftadj\bot] & \text{ (taking the contrapositive)} \\ (\forall\numbern\in\N) [\numbern\lt\numbern_0 \Rightarrow \numbern\in \rightadj\top\downarrow\functionA] & \text{ (the predicates $({?}\in\functionA\downarrow\leftadj\bot)$ and $(\numbern_0\le {?})$ each yield a partition of $\N$)} \\ (\forall\numberk\in\N) [\numberk\lt\numbern_0 \Rightarrow \functionA_\numberk] & \text{ (change of variable $\numbern\mapsto\numberk$, and semantics of $\rightadj\top\downarrow\functionA$)} \\ (\forall\numberk\lt\numbern_0) \functionA_\numberk & \text{ (definition of relative quantifier)} \\ \end{array}\)

\(\bbox[10px, border:4px black solid] { \begin{array}{} & (\numbern_0\not\leq{?}) = ({?} \lt \numbern_0) \\ & \bbox[10px, border:2px black solid] { \begin{array}{} \numbern_0 \leq {?} \\ \bbox[10px, border:2px cyan dashed] {(\functionA\downarrow\leftadj\bot) = \setS} \\ \end{array} } \\ \N \\ \end{array} } \)

But (the last) is precisely (the antecedent for $PCON(\numbern_0)$),
so if [($\numbern_0$ is least in $\functionA\downarrow\leftadj\bot$) and ($PCON(\numbern_0)$ is valid)], then ($\functionA_{\numbern_0}$ is true).
Thus we have derived a contradiction from the joint assumptions that ($\numbern_0$ is least in $\functionA\downarrow\leftadj\bot$) and ($PCON(\numbern_0)$ is valid).
The rest of the argument is the same, viz: \[\begin{array}{} WO \wedge (\functionA\downarrow\bot \not= \emptyset) \wedge PCON \xRightarrow{WO} \big( (\exists\numbern_0\in\functionA\downarrow\bot)(\forall \numbern \in \functionA\downarrow\bot) (\numbern_0 \le \numbern) \big) \wedge PCON(\numbern_0) \xRightarrow{\text{by the above}} \bot \\ WO \wedge PCON \Longrightarrow \neg\neg(\functionA\downarrow\bot = \emptyset) \xRightarrow{\text{excluded middle}} (\functionA\downarrow\bot = \emptyset) \Leftrightarrow (\functionA = \top) \\ WO \Longrightarrow \big[ PCON \Rightarrow (\functionA = \top) \big] = PIND \\ \end{array}\]

---

$PIND \Rightarrow WO$
Suppose (a subset $\setS\subseteq\N$) has NO least element.
Then we claim the predicate $({?}\notin\setS) : \N \longrightarrow \bftwo : \numbern \mapsto (\numbern\notin\setS)$ satisfies the $PCON$.
Suppose ($\numbern\in\N$) is such that $(\forall\numberk\lt\numbern)(\numberk\notin\setS)$.
Then if ($\numbern\in\setS$), $\numbern$ is the least element of $\setS$. But $\setS$ has no least element. So ($\numbern\notin\setS$).
Thus the predicate satisfies $PCON$.
$PIND$ then implies $(\forall\numbern\in\N)(\numbern\notin\setS)$, i.e., $\setS$ is empty.
Taking the contrapositive, and applying (the law of the excluded middle), we have shown that $PIND$ implies:

$\N$ is well-ordered ($WO$):

$WO:{}$ Any (subset $\setS\subseteq\N$ which is non-empty) must have (a least element $\numbern_0$, i.e., $(\numbern_0\in\setS) \wedge (\forall\numbern\in\setS)(\numbern_0\leq\numbern)$).

The above argument may be expressed with more extensive use of logical notation: \[\begin{array}{} \neg(\text{$\setS$ has a least element}) \xRightarrow{\text{by the above}} PCON({?}\notin\setS) \xRightarrow{PIND({?}\notin\setS)} \big((\forall\numbern\in\N)(\numbern\notin\setS)\big) \Leftrightarrow (\setS=\emptyset) \\ PIND({?}\notin\setS) \wedge \neg(\text{$\setS$ has a least element}) \Longrightarrow (\setS=\emptyset) \\ PIND({?}\notin\setS) \Longrightarrow \Big[ \neg(\text{$\setS$ has a least element}) \Rightarrow (\setS=\emptyset) \Big] \xRightarrow{\text{contrapositive}} \Big[ (\setS\not=\emptyset) \Rightarrow \neg\neg(\text{$\setS$ has a least element}) \xLeftrightarrow{\text{excluded middle}} (\text{$\setS$ has a least element}) \Big] = WO(\setS) \\ \end{array}\]

---

$WO \Leftrightarrow PIND$

It is possible to give an “if and only if”-style proof of the equivalence of $WO$ and $PIND$.
First, we establish an “if and only if” relation between the “has a least element” and predecessors conditions.
The statements in the left column below, for an arbitrary (subset $\setS\subseteq\N$), and those in the right column below, for an arbitrary (predicate $\functionA : \N\to\bftwo$),
are logically equivalent.
(Here we use a briefer notation: unrestricted quantifiers are presumed to vary over all of $\N$.
The tautology referenced is between $A \Rightarrow B$ and $\neg(A \wedge \neg B)$, or a variant. The generic version of (the tautology used) is shown at the extreme left or right.
A $*$ or $\text{*}$ in a comment simply indicates the step is a key one.
At (the bottom of each column) is (a small 2-diagram in $\Cat$) showing (the logical equivalence) as (a 2-cell in $\Cat$), and giving (a name) to (that logical equivalence).
(The relations between these 2-cells are best explained in terms of the “mates calculus” in the 2-category $\Cat$.) )

\(\begin{array}{l} & \neg (\setS \text{ has a least element}) && \neg (\functionA\downarrow\bot \text{ has a least element}) \\ & \neg (\exists\numbern\in\setS) (\forall\numberk\in\setS) (\numbern\leq\numberk) & \text{(definition of least)} & \neg (\exists\numbern\in\functionA\downarrow\bot) (\forall\numberk\in\functionA\downarrow\bot) (\numbern\leq\numberk)\\ & (\forall\numbern\in\setS) (\exists\numberk\in\setS) (\numbern\not\leq\numberk) & \text{(negation and quantification)} \mkern20mu & (\forall\numbern\in\functionA\downarrow\bot) (\exists\numberk\in\functionA\downarrow\bot) (\numbern\not\leq\numberk)\\ & (\forall\numbern\in\setS) (\exists\numberk\in\setS) (\numberk\lt\numbern) & \text{(* $(\N,\leq)$ is a total order)} & (\forall\numbern\in\functionA\downarrow\bot) (\exists\numberk\in\functionA\downarrow\bot) (\numberk\lt\numbern) \\ & \forall\numbern \big[ \numbern\in\setS \Longrightarrow \exists\numberk(\numberk\lt\numbern \wedge \numberk\in\setS) \big] & \text{(definition of relative $\forall$, $\exists$)} & \forall\numbern \big[ \neg\functionA_\numbern \Longrightarrow \exists\numberk(\numberk\lt\numbern \wedge \neg\functionA_\numberk) \big] \\ & \forall\numbern \big[ \neg\exists\numberk(\numberk\lt\numbern \wedge \numberk\in\setS) \Longrightarrow \numbern\notin\setS \big] & \text{(* taking the contrapositive)} & \forall\numbern \big[ \neg\exists\numberk(\numberk\lt\numbern \wedge \neg\functionA_\numberk) \Longrightarrow \functionA_\numbern \big] \\ \neg(A \wedge B) & \forall\numbern \big[ \forall\numberk\neg(\numberk\lt\numbern \wedge \numberk\in\setS) \Longrightarrow \numbern\notin\setS \big] & \text{(negation and quantification)} & \forall\numbern \big[ \forall\numberk\neg(\numberk\lt\numbern \wedge \neg\functionA_\numberk) \Longrightarrow \functionA_\numbern \big] & \neg (A \wedge \neg B) \\ A \Rightarrow \neg B & \forall\numbern \big[ \forall\numberk [\numberk\lt\numbern \Rightarrow \numberk\notin\setS] \Longrightarrow \numbern\notin\setS \big] & \text{(* tautology for $\Rightarrow$)} & \forall\numbern \big[ \forall\numberk [\numberk\lt\numbern \Rightarrow \functionA_\numberk] \Longrightarrow \functionA_\numbern \big] & A \Rightarrow B \\ & \forall\numbern \big[ (\forall\numberk\lt\numbern)(\numberk\notin\setS) \Longrightarrow \numbern\notin\setS \big] & \text{(definition of relative $\forall$)} & \forall\numbern \big[ (\forall\numberk\lt\numbern)\functionA_\numberk \Longrightarrow \functionA_\numbern \big] \\ & PCON({?}\notin\setS) & \text{(definition of $PCON$)} & PCON(\functionA) \\ \\ & \begin{array}{} \llap{ \catI \xrightarrow{\textstyle \setS} {} \mkern8mu } \Sub (\N) & \xrightarrow{\textstyle \text{least}} & \bftwo^\op \\ & \llap{{?}\notin{?}'} \searrow & \Bigg\Updownarrow \rlap{\mkern-57mu \text{least}{+}{+}PCON} & \searrow \rlap\neg \\ && [\N,\bftwo] & \xrightarrow[\textstyle PCON]{} & \bftwo \\ \end{array} && \mkern-40mu \begin{array}{} && \Sub (\N) & \xrightarrow{\textstyle \text{least}} & \bftwo^\op \\ & \llap{{?''}\downarrow\bot} \nearrow && \Bigg\Updownarrow \rlap{\mkern-57mu \text{least}{-}{+}PCON} && \searrow \rlap\neg \\ \llap{ \catI \xrightarrow{\textstyle \functionA} {} \mkern8mu } [\N,\bftwo] &&& \xrightarrow[\textstyle PCON]{} &&& \bftwo \\ \end{array} \\ \end{array}\)

Then, for the (subset $\setS\subseteq\N$), we have:

\(\begin{array}{} PCON({?}\notin\setS) & \xleftrightarrow{\textstyle (\text{least}{+}{+}PCON)(\setS)} & \neg (\setS \text{ has a least element}) && (\setS \text{ has a least element}) \\ \llap{PIND({?}\notin\setS)} \Bigg\downarrow & \xLeftrightarrow{} & \Bigg\downarrow & \xLeftrightarrow[\textstyle \text{double negation}]{\textstyle \text{contrapositive plus}} & \Bigg\uparrow\rlap{WO(\setS)} \\ ({?}\notin\setS) = \top & \xleftrightarrow[\textstyle \text{definition of $\emptyset$}]{} & \setS=\emptyset && \setS\not=\emptyset \\ \end{array}\)

Thus, for every (subset $\setS\subseteq\N$), we have \(PIND({?}\notin\setS) \xLeftrightarrow{PIND{-}WO(\setS)} WO(\setS)\),
so if ($PIND$ is valid for all predicates on $\N$, e.g., ${?}\notin\setS$) then ($WO$ is valid for all subsets $\setS$ of $\N$).

To get the converse implication, the most efficient way is to use the bijection between (predicates $\functionA$ on $\N$) and (subsets $\setS$ of $\N$) described above.
For an arbitrary (predicate $\functionA:\N\to\bftwo$), let ($\setS = \functionA\downarrow\bot$), so that ($\functionA = {?}\notin\setS$).
Then we have $PIND(\functionA) = PIND({?}\notin\setS) \xLeftrightarrow{PIND{-}WO(\setS)} WO(\setS) = WO(\functionA\downarrow\bot)$,
so if ($WO$ is valid for all subsets of $\N$, e.g., $\setS = \functionA\downarrow\bot$) then ($PIND$ is valid for all predicates $\functionA$ on $\N$),
So $WO \Leftrightarrow PIND$.

An alternative (but equivalent) method is to redo the whole argument, replacing the (subset $\setS\subseteq\N$) with a (predicate $\functionA : \N \rightarrow \bftwo$).
For each (predicate $\functionA : \N \rightarrow \bftwo$) we use the logical equivalence ($\text{least}{-}{+}PCON$) at right above to get:

\(\begin{array}{} PCON(\functionA) & \xleftrightarrow{\textstyle (\text{least}{-}{+}PCON)(\functionA)} & \neg (\functionA\downarrow\bot \text{ has a least element}) && (\functionA\downarrow\bot \text{ has a least element}) \\ \llap{PIND(\functionA)} \Bigg\downarrow & \xLeftrightarrow{} & \Bigg\downarrow & \xLeftrightarrow[\textstyle \text{double negation}]{\textstyle \text{contrapositive plus}} & \Bigg\uparrow\rlap{WO(\functionA\downarrow\bot)} \\ \functionA = \top & \xleftrightarrow[]{} & \functionA\downarrow\bot = \emptyset && \functionA\downarrow\bot\not=\emptyset \\ \end{array}\)

Thus $PIND(\functionA) \Leftrightarrow WO(\functionA\downarrow\bot)$, and so on.

For comparison and reference, here are logical equivalents for the positive statements ($\setS$ has a least element) and ($\functionA\downarrow\bot$ has a least element).

\(\begin{array}{l} & (\setS \text{ has a least element}) && (\functionA\downarrow\bot \text{ has a least element}) \\ & (\exists\numbern\in\setS) (\forall\numberk\in\setS) (\numbern\leq\numberk) & \text{(definition of least)} & (\exists\numbern\in\functionA\downarrow\bot) (\forall\numberk\in\functionA\downarrow\bot) (\numbern\leq\numberk)\\ & (\exists\numbern\in\setS) (\forall\numberk\in\setS) (\numberk\not\lt\numbern) & \text{(* $(\N,\leq)$ is a total order)} & (\exists\numbern\in\functionA\downarrow\bot) (\forall\numberk\in\functionA\downarrow\bot) (\numberk\not\lt\numbern)\\ & (\exists\numbern\in\setS) \forall\numberk [\numberk\in\setS \Rightarrow \numberk\not\lt\numbern] & \text{(definition of relative $\forall$)} & (\exists\numbern\in\functionA\downarrow\bot) \forall\numberk [ \neg\functionA_\numberk \Rightarrow \numberk\not\lt\numbern] \\ & (\exists\numbern\in\setS) \forall\numberk [\numberk\lt\numbern \Rightarrow \numberk\notin\setS] & \text{(* taking the contrapositive)} & (\exists\numbern\in\functionA\downarrow\bot) \forall\numberk [ \numberk\lt\numbern \Rightarrow \functionA_\numberk ] \\ & (\exists\numbern\in\setS) (\forall\numberk\lt\numbern) (\numberk\notin\setS) & \text{(definition of relative $\forall$)} & (\exists\numbern\in\functionA\downarrow\bot) (\forall\numberk\lt\numbern) \functionA_\numberk \\ A \wedge B & \exists\numbern \big( (\forall\numberk\lt\numbern)(\numberk\notin\setS) \wedge \numbern\in\setS \big) & \text{(definition of relative $\exists$)} & \exists\numbern \big( (\forall\numberk\lt\numbern) \functionA_\numberk \wedge \neg\functionA_\numbern \big) & A \wedge \neg B \\ \neg [A \Rightarrow \neg B] & \exists\numbern \neg\big[ (\forall\numberk\lt\numbern)(\numberk\notin\setS) \Longrightarrow \numbern\notin\setS \big] & \text{(* tautology for $\Longrightarrow $)} & \exists\numbern \neg\big[ (\forall\numberk\lt\numbern)\functionA_\numberk \Longrightarrow \functionA_\numbern \big] & \neg [A \Rightarrow B] \\ & \neg\forall\numbern \big[ (\forall\numberk\lt\numbern)(\numberk\notin\setS) \Longrightarrow \numbern\notin\setS \big] & \text{(negation and quantification)} \mkern20mu & \neg\forall\numbern \big[ (\forall\numberk\lt\numbern)\functionA_\numberk \Longrightarrow \functionA_\numbern \big] \\ & \neg PCON({?}\notin\setS) & \text{(definition of $PCON$)} & \neg PCON(\functionA) \\ \\ & \mkern-80mu \begin{array}{} \llap{ \catI \xrightarrow{\textstyle \setS} {} \mkern8mu } \Sub (\N) &&& \xrightarrow{\textstyle \text{least}} &&& \bftwo^\op \\ & \llap{{?}\notin{?}'} \searrow && \Bigg\Updownarrow \rlap{\mkern-57mu \text{least}{+}{-}PCON} && \nearrow \rlap\neg \\ && [\N,\bftwo] & \xrightarrow[\textstyle PCON]{} & \bftwo \\ \end{array} && \mkern-40mu \begin{array}{} && \Sub (\N) & \xrightarrow{\textstyle \text{least}} & \bftwo^\op \\ & \llap{{?''}\downarrow\bot} \nearrow & \Bigg\Updownarrow \rlap{\mkern-57mu \text{least}{-}{-}PCON} & \nearrow \rlap\neg \\ \llap{ \catI \xrightarrow{\textstyle \functionA} {} \mkern8mu } [\N,\bftwo] & \xrightarrow[\textstyle PCON]{} & \bftwo \\ \end{array} \end{array}\)

---

$WO \Leftrightarrow DCC$

The well-ordering condition, in turn, is equivalent to the

Descending chain condition ($DCC$):

Every descending chain $\numbern_0 \gt \numbern_1 \gt \numbern_2 \gt \cdots$ of natural numbers (i.e., in $\N$) terminates, i.e.,
there are no infinite descending chains of natural numbers.

$WO \Rightarrow DCC$:
Given a descending chain $\numbern_0 \gt \numbern_1 \gt \numbern_2 \gt \cdots$,
let $\setS = \{\numbern_0, \numbern_1, \numbern_2, \ldots \}$.
By $WO$, $\setS$ has a least element, $\numbern_{\text{least}}$, such that $\forall\numberi (\numbern_{\text{least}} \leq \numbern_\numberi)$.
So the chain is finite and terminates with $\numbern_{\text{least}}$.

$DCC \Rightarrow WO$:
Let $\setS \subseteq \N$ be non-empty, so there exists a number, say $\numbern_0$, in $\setS$.
If $\numbern_0$ is least in $\setS$, we are done.
If not, there exists $\numbern_1\in\setS$ such that $\numbern_1 \lt \numbern_0$.
Continue.
By $DCC$, the chain generated must terminate, with say, $\numbern_0 \gt \cdots \gt \numbern_{\numberk-1} \gt \numbern_\numberk$.
The termination condition means $\neg(\exists\numbern\in\setS)(\numbern \lt \numbern_\numberk)$,
for otherwise the chain could have continued with $\numbern$.
Hence $(\forall\numbern\in\setS) \neg (\numbern \lt \numbern_\numberk)$, hence $(\forall\numbern\in\setS) (\numbern_\numberk \leq \numbern)$.
Hence $\numbern_\numberk$ is a (the) least element in $\setS$.
So $DCC \Rightarrow WO$.

Finally, we claim $DCC$ is clearly true for $\N$,
for a descending chain starting at $\numbern\in\N$ can have at most $\numbern+1$ elements:
$\numbern \gt \numbern-1 \gt \numbern-2 \gt \cdots \gt 2 \gt 1 \gt 0$.

---

$PIND \Rightarrow SIND$

We switch some of the arrows from double arrows to single arrows in this section, because of the lack of diagonal double arrows.

For all $\numbern\gt0$ we have:

\(\begin{array}{} (\forall\numberk\lt\numbern)\functionA_\numberk && \xrightarrow{\textstyle \pi_{\numbern-1}} && \functionA_{\numbern-1} \\ & \llap{PCON(\numbern)} \searrow & \Longleftarrow & \swarrow \rlap{SCON(\numbern-1) } \\ && \functionA_\numbern \\ \end{array}\)

i.e.

\(\begin{array}{} (\forall\numberk\lt\numbern)\functionA_\numberk \xRightarrow{\textstyle \pi_{\numbern-1}} \functionA_{\numbern-1} \xRightarrow{\textstyle SCON(\numbern-1)} \functionA_\numbern \\ SCON(\numbern-1) \wedge (\forall\numberk\lt\numbern)\functionA_\numberk \Longrightarrow \functionA_\numbern \\ SCON(\numbern-1) \Longrightarrow \big[(\forall\numberk\lt\numbern)\functionA_\numberk \Rightarrow \functionA_\numbern \big] = PCON(\numbern) \\ \end{array}\)

so $(\forall\numbern\gt0)\big[PCON(\numbern) \leftarrow SCON(\numbern-1)\big]$.
Also, $PCON(0) \leftarrow ICON$.
Thus $PCON \longleftarrow ICON \wedge SCON$.
Then we have:

\(\begin{array}{} PCON && \xleftarrow{} && ICON \wedge SCON \\ & \llap{PIND} \searrow & \Longrightarrow & \swarrow \rlap{SIND} \\ && (\functionA = \top) \\ \end{array}\)

i.e.

\(\begin{array}{} ICON \wedge SCON \xRightarrow{\text{by the above}} PCON \xRightarrow{\textstyle PIND} (\functionA=\top) \\ PIND \wedge ICON \wedge SCON \Longrightarrow (\functionA=\top) \\ PIND \Longrightarrow \big[(ICON \wedge SCON) \Rightarrow (\functionA=\top) \big] = SIND \\ \end{array}\)

---

$SIND \Rightarrow PIND$

Finally, one may show that (successor induction $SIND$) implies (predecessors induction $PIND$).
This follows from contemplation of the diagram (for arbitrary $\numbern\geq0$):
\[\begin{array}{} (\forall\numberk\lt\numbern+1)\functionA_\numberk & \xlongequal{} & (\forall\numberk\leq\numbern)\functionA_\numberk & = & AP_\numbern \\ \llap{PCON(\numbern+1,\functionA)}\bigg\downarrow & \searrow & \bigg\uparrow \rlap{\pi_{0 .. \numbern}} && \bigg\downarrow\rlap{SCON(\numbern,AP)} \\ \functionA_{\numbern+1} & \xleftarrow[\textstyle \pi_{\numbern+1}]{} & (\forall\numberl\leq\numbern+1)\functionA_\numberl & = & AP_{\numbern+1} \\ \end{array}\] (The diagonal arrow) is induced by [(the right universal property) of (the two arrows out of its target)].
Given (the indicated equalities between the objects), we may also consider (the diagonal) as [(an arrow) between (the two objects on the right)].
With these as (its source and target), it becomes (the desired $SCON(\numbern,AP)$).
Thus $(\forall\numbern\geq0)\big[PCON(\numbern+1,\functionA) \Rightarrow SCON(\numbern,AP)\big]$.
Also, $PCON(0,\functionA) = ICON(\functionA) = \functionA_0 = AP_0 = ICON(AP)$.
Then we have successively \[\begin{array}{} PCON(\functionA) \xRightarrow{\text{by the above}} \big(ICON(AP) \wedge SCON(AP)\big) \xRightarrow{\textstyle SIND(AP)} (\forall\numbern)AP_\numbern \xRightarrow{\textstyle (\forall\numbern)(AP_\numbern\xRightarrow{\textstyle \pi_\numbern} \functionA_\numbern)} (\forall\numbern)\functionA_\numbern \\ SIND(AP) \wedge PCON(\functionA) \Longrightarrow (\forall\numbern)\functionA_\numbern \\ SIND(AP) \Longrightarrow \big[PCON(\functionA) \Rightarrow (\forall\numbern)\functionA_\numbern\big] = PIND(\functionA) \; . \\ \end{array}\] So if ($SIND$ holds for all predicates on $\N$), then ($PIND$ does also).

---

In summary, we have proved the following implications regarding $\N$, its predicates, and its subsets: \[\begin{array}{} && WO && \longrightarrow \atop \longleftarrow && DCC \\ & \swarrow && \searrow\nwarrow \\ SIND && \longrightarrow \atop \longleftarrow && PIND \mkern30mu . \\ \end{array}\] Thus $WO$, $SIND$, $PIND$ and $DCC$ are logically equivalent.

---

References:

Induction Tutorial, 2011-09-29, CS221, University of Chicago
Ascending chain condition, Wikipedia web page
A Well Ordering Is A Consistent Choice Function, by Tom Leinster, 2018-11-12

Topics in logic and set theory

2018-08-17 $\Newextarrow{\xleftrightarrow}{10,10}{0x2194} \Newextarrow{\xRightarrow}{10,10}{0x21D2} \Newextarrow{\xLeftrightarrow}{10,10}{0x21D4}$

The arguments used in the post on “Well-ordering and induction” use, repeatedly, an argument in logic and set theory (which I call negation interchange).
It seems worthwhile to highlight and discuss this in a general setting, and its three variants (which hold when the setting is Boolean).

	${} =\emptyset$		${} \not=\emptyset$
$\setA \cap \setB$	\( \bbox[10px, border:4px black solid] { \begin{array}{l} \bbox[4px, border:2px black solid] {\setA} \subseteq \tilde\setB \\ \setA \cap \setB = \emptyset \\ \bbox[4px, border:2px black solid] {\setB} \subseteq \tilde\setA \\ \end{array} } \ \\ \)	\(\begin{array}{l} \forall\eltx [ \functionA_\eltx \Rightarrow \neg\functionB_\eltx ] \\ \forall\eltx \neg ( \functionA_\eltx \wedge \functionB_\eltx ) \\ \forall\eltx [ \functionB_\eltx \Rightarrow \neg\functionA_\eltx ] \\ \end{array}\)	\( \bbox[10px, border:4px black solid] { \begin{array}{l} \bbox[4px, border:2px black solid] {\setA} \not\subseteq \tilde\setB \\ \setA \cap \setB \not= \emptyset \\ \bbox[4px, border:2px black solid] {\setB} \not\subseteq \tilde\setA \\ \end{array} } \ \\ \)	\(\begin{array}{l} \neg\forall\eltx [ \functionA_\eltx \Rightarrow \neg\functionB_\eltx ] \\ \neg\forall\eltx \neg ( \functionA_\eltx \wedge \functionB_\eltx ) \\ \neg\forall\eltx [ \functionB_\eltx \Rightarrow \neg\functionA_\eltx ] \\ \end{array}\)	\(\begin{array}{l} \exists\eltx \neg [ \functionA_\eltx \Rightarrow \neg\functionB_\eltx ] \\ \exists\eltx ( \functionA_\eltx \wedge \functionB_\eltx ) \\ \exists\eltx \neg [ \functionB_\eltx \Rightarrow \neg\functionA_\eltx ] \\ \end{array}\)
$\setA \cap \tilde\setB$	\( \bbox[10px, border:4px black solid] { \begin{array}{l} \bbox[4px, border:2px black solid] {\setA} \subseteq \setB \\ \setA \cap \tilde\setB = \emptyset \\ \bbox[4px, border:2px black solid] {\tilde\setB} \subseteq \tilde\setA \\ \end{array} } \ \\ \)	\(\begin{array}{l} \forall\eltx [ \functionA_\eltx \Rightarrow \functionB_\eltx ] \\ \forall\eltx \neg ( \functionA_\eltx \wedge \neg\functionB_\eltx ) \\ \forall\eltx [ \neg\functionB_\eltx \Rightarrow \neg\functionA_\eltx ] \\ \end{array}\)	\( \bbox[10px, border:4px black solid] { \begin{array}{l} \bbox[4px, border:2px black solid] {\setA} \not\subseteq \setB \\ \setA \cap \tilde\setB \not= \emptyset \\ \bbox[4px, border:2px black solid] {\tilde\setB} \not\subseteq \tilde\setA \\ \end{array} } \ \\ \)	\(\begin{array}{l} \neg\forall\eltx [ \functionA_\eltx \Rightarrow \functionB_\eltx ] \\ \neg\forall\eltx \neg ( \functionA_\eltx \wedge \neg\functionB_\eltx ) \\ \neg\forall\eltx [ \neg\functionB_\eltx \Rightarrow \neg\functionA_\eltx ] \\ \end{array}\)	\(\begin{array}{l} \exists\eltx \neg [ \functionA_\eltx \Rightarrow \functionB_\eltx ] \\ \exists\eltx ( \functionA_\eltx \wedge \neg\functionB_\eltx ) \\ \exists\eltx \neg [ \neg\functionB_\eltx \Rightarrow \neg\functionA_\eltx ] \\ \end{array}\)

Discussion: (The following is a draft, containing several alternative texts.)

Consider first (the thickly(4 pixels)-bordered box) in (the upper left quadrant).
This is (an enhanced Venn diagram) showing (a set $\setX$) containing (two disjoint subsets, $\setA$ and $\setB$), shown as (smaller boxes) within (the enveloping set $\setX$).
(Their disjointness) is declared explicitly by (the statement $\setA \cap \setB = \emptyset$).
Superimposed on (the Venn diagram) are (three set-theoretic relations) (two inclusions and an equality).
(Each of these) is, by definition, equivalent to (the statement in predicate logic to its right).
(Thus, e.g., (the disjointness of subsets $\setA$ and $\setB$ of $\setX$) is equivalent to
(the incompatibility of predicates (i.e. properties) $\setA$ and $\setB$ on $\setX$).)
(The three statements in predicate logic) are logically equivalent, hence (all six statements are logically equivalent).

$A$ and $B$ as (subsets of $\setX$) determine (predicates on $\setX$):
(${?}\in\setA : \setX \longrightarrow \bftwo: \eltx \mapsto \eltx\in\setA$), and (${?}\in\setB : \setX \longrightarrow \bftwo: \eltx \mapsto \eltx\in\setB$).
We commit an abuse of notation by using the same letter to denote both (the subset) and (the predicate) it determines.
Thus $\eltx\in\setA \Longleftrightarrow (\functionA_\eltx = \top) \Longleftrightarrow \functionA_\eltx$, and similarly for $B$.

In the above we use (the same letter “$A$”) to denote both (a subset $\setA\subseteq\setX$) and the corresponding (predicate $\functionA:\setX\to\bftwo$), and likewise for $B$.
Thus: $\eltx\in\setA \Longleftrightarrow (\functionA_\eltx = \top) \Longleftrightarrow \functionA_\eltx$.
The reason is that the Boolean algebras of (subsets of $\setX$, $\Sub(\setX)$), and of (predicates of $\setX$, $[\setX,\bftwo]$), are isomorphic Boolean algebras.
(The equivalences in the displays above) hold in both Boolean algebras; we want to make that fact explicit and show how one may easily switch between the two BAs.

The other three quadrants are variations.
The right column changes (the assumption of disjointness) to (the assumption of overlap), introducing the existential quantifier,
which yields (nine logically equivalent (in a Boolean setting) statements).
The lower row changes $\setB$ to $\tilde\setB$, exhibiting equivalent ways of expressing the inclusion relation and the contrapositive.

---

Lower bounds in total orders

For a simple but significant example of negation interchange, we show that, in a total order, there are six equivalent conditions for being a lower bound.
For concreteness, we consider the total order $(\N,\leq)$, but the argument generalizes to arbitrary total orders.
So, in the above “negation interchange” setting,
let $\setX=\N$ and $\setA = \boxed\setS\subseteq\N$, an arbitrary subset of the natural numbers (so $\functionA_\numberk \Leftrightarrow \numberk\in\setS$).
Let $\boxed\numbern\in\N$ be an arbitrary natural number, and let
$\setB = [0,\numbern) = \{\numberk\in\N \mid \numberk\lt\numbern \}$, the strict predecessors of $\numbern$, i.e., $\numbern$’s strict initial segment (so $\functionB_\numberk \Leftrightarrow \numberk\lt\numbern$); so that
$\tilde\setB = \widetilde{[0,\numbern)} = \{ \numberk\in\N \mid \numberk \not\lt \numbern \} \xlongequal{(\N,\leq) \text{ total order}} \{\numberk\in\N \mid \numbern\leq\numberk \} = [\numbern,\infty)$, the (weak) successors of $\numbern$, i.e., $\numbern$’s final segment
(so $(\tilde\functionB)_\numberk \Leftrightarrow \neg(\functionB_\numberk) \Leftrightarrow \numberk\not\lt\numbern \xLeftrightarrow {(\N,\leq) \text{ total order}} \numbern\leq\numberk$).
Then negation interchange, together with some definitions and the fact that $(\N,\leq)$ is a total i.e. linear order, gives:

\( \bbox[10px, border:4px black solid] { \begin{array}{l} \bbox[4px, border:2px black solid] {\setS} \subseteq [\numbern,\infty) \xlongequal{(\N,\leq) \text{ total order}} \widetilde {[0,\numbern)} \\ [0,\numbern) \cap \setS = \emptyset \\ \bbox[4px, border:2px black solid] {[0,\numbern)} \subseteq \tilde\setS \\ \end{array} } \ \\ \)

\(\begin{array}{l} \numbern\in LB(\setS\subseteq\N) & (\numbern\in\N \text{ is a lower bound for } \setS\subseteq\N) \\ (\forall\numberk\in\setS)(\numbern\leq\numberk) \\ \forall\numberk [ \numberk\in\setS \Rightarrow \numbern\leq\numberk \xLeftrightarrow {(\N,\leq) \text{ total order}} \numberk\not\lt\numbern ] \\ \forall\numberk \neg ( \numberk\lt\numbern \wedge \numberk\in\setS ) \\ \forall\numberk [ \numberk\lt\numbern \Rightarrow \numberk\notin\setS ] \\ (\forall\numberk\lt\numbern)(\numberk\notin\setS) \\ (\forall\numberk\lt\numbern)(\numberk\in\tilde\setS) \\ \end{array}\)

Thus we have (six equivalent conditions for being a lower bound for a subset $\setS\subseteq\N$): \[\begin{array}{l} LB(\setS\subseteq\N) & = & \big\{ \numbern \bigm| (\forall\numberk\in\setS)(\numbern\leq\numberk) \big\} & = & \big\{ \numbern \bigm| \setS\subseteq [\numbern,\infty) \big\} \\ & = & \big\{ \numbern \bigm| \forall\numberk \neg ( \numberk\lt\numbern \wedge \numberk\in\setS ) \big\} & = & \big\{ \numbern \bigm| [0,\numbern) \cap \setS = \emptyset \big\} \\ & = & \big\{ \numbern \bigm| (\forall\numberk\lt\numbern)(\numberk\notin\setS) \big\} & = & \big\{ \numbern \bigm| [0,\numbern) \subseteq \tilde\setS \big\} \\ \end{array}\]

---

The following is material for the post “Well-ordering and induction”, two alternative double applications of negation interchange.
$\setS$ is an arbitrary subset of the natural numbers: $\setS\subseteq\N$. $LB(\setS\subseteq\N)$ is the set of lower bounds of $\setS$: $LB(\setS\subseteq\N) = \{ \numbern\in\N \mid (\forall\numberk\in\setS)(\numbern\leq\numberk) \}$.
In this situation (the logical statements in the center three columns below) are equivalent.
(The columns on the outside of those columns) are equivalent statements about sets. The outermost columns are simply comments. \[\begin{array}{cllcl} &&& \neg ( \setS \text{ has a least element} ) \\ &&& \neg (\exists\numbern\in\setS) (\forall\numberk\in\setS)(\numbern\leq\numberk) \\ &&& (\forall\numbern\in\setS) \neg (\forall\numberk\in\setS)(\numbern\leq\numberk) && \mkern12mu \numbern\notin LB(\setS\subseteq\N) \\ &&&&& \mkern32mu \updownarrow \\ & \bbox[4px, border:2px black solid] {\setS} \subseteq \widetilde{LB(\setS)} & \forall\numbern \big[ \numbern\in\setS \Longrightarrow \neg (\forall\numberk\in\setS)(\numbern\leq\numberk) \big] && (\forall\numbern\in\setS) \neg \forall\numberk [\numberk\in\setS \Rightarrow \numbern\leq\numberk] & \bbox[4px, border:2px black solid] {\setS} \not\subseteq [\numbern,\infty) \rlap{{} = \widetilde{[0,\numbern)} } \\ \forall\numbern \mkern24mu & LB(\setS\subseteq\N) \cap \setS = \emptyset & \forall\numbern \neg \big( \numbern\in\setS \wedge (\forall\numberk\in\setS)(\numbern\leq\numberk) \big) && (\forall\numbern\in\setS) \neg \forall\numberk \neg ( \numberk\lt\numbern \wedge \numberk\in\setS ) & [0,\numbern) \cap \setS \not= \emptyset & \mkern16mu \forall\numberk \\ & \llap{\numbern\in{}} \bbox[4px, border:2px black solid] {LB(\setS\subseteq\N)} \subseteq \tilde\setS & \forall\numbern \big[ (\forall\numberk\in\setS)(\numbern\leq\numberk) \Longrightarrow \numbern\notin\setS \big] && (\forall\numbern\in\setS) \neg \forall\numberk [ \numberk\lt\numbern \Rightarrow \numberk\notin\setS ] & \bbox[4px, border:2px black solid] {[0,\numbern)} \not\subseteq \tilde\setS \\ &&&& (\forall\numbern\in\setS) \neg (\forall\numberk\lt\numbern) (\numberk\notin\setS) \\ {}\rlap{\mkern60mu \raise2ex\hbox{$\nwarrow \mkern-20mu \searrow$}} \\ & \bbox[4px, border:2px black solid] {\setS} \subseteq [\numbern,\infty) = \widetilde{[0,\numbern)} & \forall\numbern \big[ \forall\numberk [\numberk\in\setS \Rightarrow \numbern\leq\numberk] \Longrightarrow \numbern\notin\setS \big] && \forall\numbern \big[ \numbern\in\setS \Longrightarrow \neg(\forall\numberk\lt\numbern) (\numberk\notin\setS) \big] & \bbox[4px, border:2px black solid] {\setS} \subseteq \widetilde{LB(\setS)} \\ \forall\numberk \mkern24mu & [0,\numbern) \cap \setS = \emptyset & \forall\numbern \big[ \forall\numberk \neg ( \numberk\lt\numbern \wedge \numberk\in\setS ) \Longrightarrow \numbern\notin\setS \big] && \forall\numbern \neg \big( \numbern\in\setS \wedge (\forall\numberk\lt\numbern) (\numberk\notin\setS) \big) & LB(\setS\subseteq\N) \cap \setS = \emptyset & \mkern16mu \forall\numbern \\ & \bbox[4px, border:2px black solid] {[0,\numbern)} \subseteq \tilde\setS & \forall\numbern \big[ \forall\numberk [ \numberk\lt\numbern \Rightarrow \numberk\notin\setS ] \Longrightarrow \numbern\notin\setS \big] && \forall\numbern \big[ (\forall\numberk\lt\numbern)(\numberk\notin\setS) \Longrightarrow \numbern\notin\setS \big] & \bbox[4px, border:2px black solid] {LB(\setS\subseteq\N)} \subseteq \tilde\setS \\ && \forall\numbern \big[ (\forall\numberk\lt\numbern)(\numberk\notin\setS ) \Longrightarrow \numbern\notin\setS \big] \\ \\ &&& PCON({?}\notin\setS) \\ \end{array}\]

---

Comparing (least in $\setS$) to (greatest lower bound for $\setS$)

\[\begin{array}{l} &&\big( \numbern = \text{least}(\setS\subseteq\N) \big) & \Longleftrightarrow & \numbern\in\setS \wedge \numbern\in LB(\setS\subseteq\N) & \mkern10mu | \mkern8mu B \wedge A \\ &&& \Longleftrightarrow & \numbern\in\setS \wedge (\forall\numberk\in\setS)(\numbern\leq\numberk) \\ \\ \big( \numbern = \text{glb}(\setS\subseteq\N) \big) & \Longleftrightarrow & \Big( \numbern = \text{greatest}\big(LB(\setS\subseteq\N) \subseteq \N\big) \Big) & \Longleftrightarrow & \numbern\in LB(\setS\subseteq\N) \wedge \numbern\in UB\big(LB(\setS\subseteq\N)\subseteq\N\big) & \mkern10mu | \mkern8mu A \wedge E \\ &&& \Longleftrightarrow & \numbern\in LB(\setS\subseteq\N) \wedge \big(\forall\numberm\in LB(\setS\subseteq\N)\big)(\numberm\leq\numbern) \\ &&& \Longleftrightarrow & \numbern\in LB(\setS\subseteq\N) \wedge \forall\numberm\big[\numberm\in LB(\setS\subseteq\N) \Rightarrow \numberm\leq\numbern \big] \\ &&& \Longleftrightarrow & (\forall\numberk\in\setS)(\numbern\leq\numberk) \wedge \forall\numberm\big[\numberm\in LB(\setS\subseteq\N) \Rightarrow \numberm\leq\numbern \big] \\ &&& \Longleftrightarrow & (\forall\numberk\in\setS)(\numbern\leq\numberk) \wedge \forall\numberm\big[(\forall\numberk\in\setS)(\numberm\leq\numberk) \Rightarrow \numberm\leq\numbern \big] \\ \end{array}\]

Proposition. If $\setS\subseteq\N$, then $\text{least}(\setS\subseteq\N) = \text{glb}(\setS\subseteq\N)$.

Proof:
We must show $\numbern\in LB(\setS\subseteq\N) \Longrightarrow \Big[ \numbern\in\setS \Leftrightarrow \numbern\in UB\big(LB(\setS\subseteq\N)\subseteq\N\big) \Big]$ $\mkern128mu | \mkern8mu A \Longrightarrow [B \Leftrightarrow E]$ .

First, we have \[\begin{array}{l} \numberm\in LB(\setS\subseteq\N) \xRightarrow{\text{definition of lower bound}} [\numbern\in\setS \Rightarrow \numberm\leq\numbern] & \mkern10mu | \mkern8mu \hom \numberm A {} \Longrightarrow [B\Rightarrow \hom \numberm C {} ] \\ \numberm\in LB(\setS\subseteq\N) \wedge \numbern\in\setS \Longrightarrow \numberm\leq\numbern & \mkern10mu | \mkern8mu \hom \numberm A {} \wedge B \Longrightarrow \hom \numberm C {} \\ \numbern\in\setS \Longrightarrow \big[ \numberm\in LB(\setS\subseteq\N) \Rightarrow \numberm\leq\numbern \big] & \mkern10mu | \mkern8mu B \Longrightarrow [\hom \numberm A {} \Rightarrow \hom \numberm C {}] \\ \numbern\in\setS \Longrightarrow \forall\numberm\big[ \numberm\in LB(\setS\subseteq\N) \Rightarrow \numberm\leq\numbern \big] & \mkern10mu | \mkern8mu B \Longrightarrow \forall\numberm [\hom \numberm A {} \Rightarrow \hom \numberm C {}] \\ \numbern\in\setS \Longrightarrow \big(\forall\numberm\in LB(\setS\subseteq\N)\big)(\numberm\leq\numbern) \\ \numbern\in\setS \Longrightarrow \numbern\in UB\big(LB(\setS\subseteq\N)\subseteq\N\big) \; . & \mkern10mu | \mkern8mu B \Rightarrow E \\ \end{array}\] This holds for an arbitrary $\numbern\in\setS$, not even requiring that $\numbern\in LB(\setS\subseteq\N)$, and is true for a subset $\setS$ of an arbitrary partial order.

To get the other direction, $\numbern\in LB(\setS\subseteq\N) \Longrightarrow \Big[ \numbern\in UB\big(LB(\setS\subseteq\N)\subseteq\N\big) \Rightarrow \numbern\in\setS \Big]$, consider the following sequence of valid statements: \[\begin{array}{l} \numbern\in LB(\setS\subseteq\N) \wedge \numberk\in\setS \xRightarrow{\text{definition of lower bound}} \numbern\leq\numberk & \mkern10mu | \mkern8mu A \wedge \hom {} C \numberk \Rightarrow \numbern\leq\numberk \\ \numbern\notin\setS \wedge \numberk\in\setS \wedge \numbern = \numberk \xRightarrow{\text{substitution}} \numbern\notin\setS \wedge \numbern\in\setS \Longrightarrow \bot & \mkern10mu | \mkern8mu \neg B \wedge \hom {} C \numberk \wedge \numbern=\numberk \Rightarrow \bot \\ \numbern\notin\setS \wedge \numberk\in\setS \Longrightarrow \numbern \not= \numberk & \mkern10mu | \mkern8mu \neg B \wedge \hom {} C \numberk \Rightarrow \numbern \not=\numberk \\ \numbern\in LB(\setS\subseteq\N) \wedge \numbern\notin\setS \wedge \numberk\in\setS \Longrightarrow \numbern\leq\numberk \wedge \numbern \not= \numberk \Longleftrightarrow \numbern\lt\numberk \xLeftrightarrow{\text{property of $\N$}} \numbern+1 \leq\numberk & \mkern10mu | \mkern8mu A \wedge \neg B \wedge \hom {} C \numberk \Rightarrow \hom {} D \numberk \\ \numbern\in LB(\setS\subseteq\N) \wedge \numbern\notin\setS \Longrightarrow [\numberk\in\setS \Rightarrow \numbern+1 \leq\numberk] & \mkern10mu | \mkern8mu A \wedge \neg B \Rightarrow [\hom {} C \numberk \Rightarrow \hom {} D \numberk] \\ \numbern\in LB(\setS\subseteq\N) \wedge \numbern\notin\setS \Longleftrightarrow \forall\numberk[\numberk\in\setS \Rightarrow \numbern+1 \leq\numberk] \Longleftrightarrow \numbern+1 \in LB(\setS\subseteq\N) \xRightarrow{\numbern\lt\numbern+1 \; \Rightarrow \; \numbern+1\not\leq\numbern} \numbern\not\in UB\big(LB(\setS\subseteq\N)\subseteq\N\big) & \mkern10mu | \mkern8mu A \wedge \neg B \Rightarrow \neg E \\ \numbern\in LB(\setS\subseteq\N) \wedge \numbern\notin\setS \wedge \numbern\in UB\big(LB(\setS\subseteq\N)\subseteq\N\big) \Longrightarrow \bot & \mkern10mu | \mkern8mu A \wedge \neg B \wedge E \Rightarrow \bot \\ \numbern\in LB(\setS\subseteq\N) \wedge \numbern\in UB\big(LB(\setS\subseteq\N)\subseteq\N\big) \Longrightarrow \neg\neg (\numbern\in\setS) \xRightarrow[\text{double negation}]{\text{Boolean}} \numbern\in\setS & \mkern10mu | \mkern8mu A \wedge E \Rightarrow \neg \neg B \Rightarrow B \\ \big( \numbern = \text{glb}(\setS\subseteq\N) \big) \Longrightarrow \numbern\in\setS \; . \end{array}\] The proposition is proved.
(By the way, each implication after a “$|$” symbol is a generic version of one of the implications before the “$|$” symbol, i.e., a schematic representation or template for it.)

---

An alternative proof of the last result, using one of the equivalent conditions for lower bound of subsets in $\N$, gives further insight into the situation: \[\begin{array}{c} [0,\numbern)\cap\setS = \emptyset \wedge \numbern\notin\setS & \Longleftrightarrow & [0,\numbern] \cap \setS = \emptyset & \xLeftrightarrow{\numberk\leq\numbern \; \Leftrightarrow \; \numberk\lt\numbern+1} & [0,\numbern+1)\cap\setS = \emptyset \\ \Bigg\Updownarrow &&&& \Bigg\Updownarrow \\ \numbern\in LB(\setS\subseteq\N) \wedge \numbern\notin\setS && \xLeftrightarrow{} && \numbern+1 \in LB(\setS\subseteq\N) \\ \end{array}\]

The biimplications in the top row are properties of intervals and sets in $\N$;
the two vertical biimplications are given by the equivalent condition for being a lower bound in $\N$;
the biimplication in the bottom row is the composite of those above it in the diagram.
The rest of the proof is as above, i.e., largely a parameterized version of negation interchange, followed by the Boolean double negation law.

---

Remark:

The implication $\numbern+1 \in LB(\setS\subseteq\N) \xRightarrow{\numbern\lt\numbern+1 \Rightarrow \numbern+1\not\leq\numbern} \numbern\not\in UB\big(LB(\setS\subseteq\N)\subseteq\N\big)$ above in fact is a biimplication.
We prove this via a (widely useful) minilemma and a (more specialized) lemma:

Minilemma.

$LB(\setS\subseteq\N)$ is a downdeal,	i.e.,	$\numberm'\leq\numberm\in LB(\setS\subseteq\N)$	$\Rightarrow$	$\numberm'\in LB(\setS\subseteq\N)$,	i.e., $LB(\setS)$ is downwards closed
$UB(\setS\subseteq\N)$ is an updeal,	i.e.,	$UB(\setS\subseteq\N)\ni\numbern\leq\numbern'$	$\Rightarrow$	$\numbern'\in UB(\setS\subseteq\N)$,	i.e., $UB(\setS)$ is upwards closed.

This is a direct consequence of the transitivity property of $\leq$.
(The “deal” terminology is due to Peter Freyd, emphasizing the analogy to ideals in algebra.)

Lemma.

For an arbitrary	$\setT\subseteq\N$,	$\numbern+1 \in \setT$	$\Rightarrow \numbern\notin UB(\setT\subseteq\N)$.
For a downdeal	$\setD\subseteq\N$,	$\numbern+1 \in \setD$	$\Leftarrow \numbern\notin UB(\setD\subseteq\N)$.

Proof:
$\Rightarrow$: \[\begin{array}{l} \numbern+1\in\setT \wedge \numbern\in UB(\setT\subseteq\N) \xRightarrow{\text{definition of upper bound}} \numbern+1 \leq \numbern \Rightarrow \bot \\ \numbern+1\in\setT \Rightarrow \numbern\notin UB(\setT\subseteq\N) \end{array} \] $\Leftarrow$:
We have a sequence of equivalent statements: \begin{array}{l} \numbern\not\in UB\big(\setD\subseteq\N\big) \\ \neg\big(\forall\numberd\in \setD\big)(\numberd\leq\numbern) \\ \big(\exists\numberd\in \setD\big)(\numberd\not\leq\numbern) \\ \big(\exists\numberd\in \setD\big)(\numbern\lt\numberd) & \text{(trichotomy property of total orders, in this case, $\N$)} \\ \big(\exists\numberd\in \setD\big)(\numbern+1\leq\numberd) & \text{(property of $\N$)} \\ \numbern+1\in \setD & \text{($\setD$ a downdeal)} \\ \end{array}