# General Associative Law for Ordinal Sum

Jump to navigation
Jump to search

## Theorem

Let $x$ be a finite ordinal.

Let $\left\langle{a_i}\right\rangle$ be a sequence of ordinals.

Then:

- $\displaystyle \sum_{i \mathop = 1}^{x + 1} a_i = a_1 + \sum_{i \mathop = 1}^x a_{i + 1}$

## Proof 1

The proof shall proceed by induction on $x$.

### Basis for the Induction

If $x = 0$, then:

\(\displaystyle \sum_{i \mathop = 1}^{0 + 1} a_i\) | \(=\) | \(\displaystyle \sum_{i \mathop = 1}^0 a_i + a_1\) | definition of ordinal sum | ||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle a_1\) | by Ordinal Addition by Zero | ||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle a_1 + \sum_{i \mathop = 1}^0 a_i\) | by Ordinal Addition by Zero |

This proves the basis for the induction.

$\Box$

### Induction Step

Suppose that:

- $\displaystyle \sum_{i \mathop = 1}^{x + 1} a_i = a_1 + \sum_{i \mathop = 1}^x a_{i + 1}$

Then:

\(\displaystyle \sum_{i \mathop = 1}^{x + 2} a_i\) | \(=\) | \(\displaystyle \sum_{i \mathop = 1}^{x + 1} a_i + a_{i + 2}\) | Definition of Ordinal Sum | ||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle \left({a_1 + \sum_{i \mathop = 1}^x a_{i + 1} }\right) + a_{i + 2}\) | by Inductive Hypothesis | ||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle a_1 + \left({\sum_{i \mathop = 1}^x a_{i + 1} + a_{i + 2} }\right)\) | Ordinal Addition is Associative | ||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle a_1 + \sum_{i \mathop = 1}^{x + 1} a_{i + 1}\) | Definition of Ordinal Sum |

This proves the induction step.

$\blacksquare$

## Proof 2

From Ordinal Addition is Associative we have that:

- $\forall a, b, c \in \operatorname{On}: a + \left({b + c}\right) = \left({a + b}\right) + c$

The result follows directly from the General Associativity Theorem.

$\blacksquare$