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)$.
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}\]
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]$.
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} } \) |
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)$).
$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:
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:
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).
$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}\) |
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
No comments:
Post a Comment