Ordinal Subtraction when Possible is Unique

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x$ and $y$ be ordinals such that $x \le y$.

Then there exists a unique ordinal $z$ such that $x + z = y$.


That is:

$x \le y \implies \exists! z \in \On: x + z = y$


Proof

By transfinite induction on $y$.


Base Case

\(\ds x\) \(\le\) \(\ds \O\)
\(\ds \leadsto \ \ \) \(\ds x\) \(=\) \(\ds \O\) Subset of Empty Set
\(\ds \leadsto \ \ \) \(\ds x + z\) \(=\) \(\ds z\) Definition of Ordinal Addition
\(\ds \leadsto \ \ \) \(\ds x + z = \O\) \(\iff\) \(\ds z = \O\) Equality is Equivalence Relation


Inductive Case

\(\ds x\) \(\le\) \(\ds y^+\)
\(\ds \leadsto \ \ \) \(\ds x\) \(\le\) \(\ds y\) Ordinal is Subset of Successor
\(\, \ds \lor \, \) \(\ds x\) \(=\) \(\ds y^+\)
\(\ds x\) \(\le\) \(\ds y\)
\(\ds \leadsto \ \ \) \(\ds \exists ! z \in \On: \, \) \(\ds x + z\) \(=\) \(\ds y\) by hypothesis
\(\ds \leadsto \ \ \) \(\ds \exists ! z \in \On: \, \) \(\ds \paren {x + z}^+\) \(=\) \(\ds y^+\) Equality of Successors
\(\ds \leadsto \ \ \) \(\ds \exists ! w \in \On: \, \) \(\ds x + w\) \(=\) \(\ds y^+\) Equality of Successors

The last step is justified because of:

$x + z^+ = y^+$

which guarantees existence, and by Ordinal Addition is Left Cancellable:

$x + w = x + z^+ \implies w = z^+$

which guarantees uniqueness.


Limit Case

\(\ds \forall w \in y: \, \) \(\ds x\) \(\le\) \(\ds w\)
\(\ds \leadsto \ \ \) \(\ds \exists ! z: \, \) \(\ds x + z\) \(=\) \(\ds w\) by hypothesis
\(\ds x\) \(\le\) \(\ds y\)
\(\ds \leadsto \ \ \) \(\ds x\) \(=\) \(\ds y\)
\(\, \ds \lor \, \) \(\ds x\) \(<\) \(\ds y\)
\(\ds x\) \(=\) \(\ds y\)
\(\ds \leadsto \ \ \) \(\ds x + \O\) \(=\) \(\ds y\) Definition of Ordinal Addition
\(\ds \leadsto \ \ \) \(\ds x + z = y\) \(\iff\) \(\ds x + \O = x + z\) Equality is Equivalence Relation
\(\ds \leadsto \ \ \) \(\ds x + z = y\) \(\iff\) \(\ds z = \O\) Ordinal Addition is Left Cancellable
\(\ds \leadsto \ \ \) \(\ds \exists ! z: \, \) \(\ds x + z\) \(=\) \(\ds y\) $z$ must be equal to $\O$
\(\ds x\) \(<\) \(\ds y\)
\(\ds \leadsto \ \ \) \(\ds \exists w < y: \, \) \(\ds x\) \(<\) \(\ds w\) Union of Limit Ordinal

Set $A = \set {w : x < w \land w < y}$.

The above statement shows that $A$ is nonempty.


Then:

$\forall w \in A: \exists ! z: x + z = w$

Create a mapping $F$, that sends each $w \in A$ to the unique $z$ that satisfies $x + z = w$.



\(\ds x\) \(<\) \(\ds w\)
\(\, \ds \land \, \) \(\ds w\) \(<\) \(\ds y\)
\(\ds \leadsto \ \ \) \(\ds x + \map F w\) \(=\) \(\ds w\) Definition of $F$ above
\(\ds \leadsto \ \ \) \(\ds \bigcup_{w \mathop \in A} \paren {x + \map F w}\) \(=\) \(\ds \bigcup_{w \mathop \in A} w\) Indexed Union Equality
\(\ds \leadsto \ \ \) \(\ds \bigcup_{w \mathop \in A} \paren {x + \map F w}\) \(=\) \(\ds y\) Union of Limit Ordinal


Finally, we must prove that:

$\ds \bigcup_{w \mathop \in A} \paren {x + \map F w} = x + \bigcup_{w \mathop \in A} \map F w$

It suffices to prove that $\ds \bigcup_{w \mathop \in A} \map F w$ is a limit ordinal.

Let $w = x^+$.

Then $\map F w = 1$, and Union of Ordinals is Least Upper Bound.

Thus:

$\ds \bigcup_{w \mathop \in A} \map F w \ne \O$


\(\ds z\) \(\in\) \(\ds \bigcup_{w \mathop \in A} \map F w\)
\(\ds \leadsto \ \ \) \(\ds \exists w \in A: \, \) \(\ds z\) \(<\) \(\ds \map F w\) Definition of Union of Family
\(\ds \leadsto \ \ \) \(\ds \exists w \in A: \, \) \(\ds z^+\) \(<\) \(\ds \map F {w^+}\)
\(\ds \leadsto \ \ \) \(\ds z^+\) \(\in\) \(\ds \bigcup_{w \mathop \in A} \map F w\)

Thus:

$\ds \bigcup_{w \mathop \in A} \map F w \ne z^+$

Therefore $\ds \bigcup_{w \mathop \in A} \map F w$ must be a limit ordinal.


To prove uniqueness, assume $x + z = y$.

Then by Ordinal Addition is Left Cancellable:

$\ds x + z = x + \bigcup_{w \mathop \in A} \map F w \implies z = \bigcup_{w \mathop \in A} \map F w$

$\blacksquare$


Also see


Sources