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