For any two sets $\alpha$ and $\beta$, let $\alpha+\beta = \{\alpha', \alpha+\beta'\}$ and $\alpha\cdot\beta = {\alpha\cdot\beta'+\alpha'}$, where $\alpha'$ and $\beta'$ are variables taking as values all elements of $\alpha$ and $\beta$ respectively. These operatons are well-defined by induction for all well-founded sets. Then the following statements all have "one-line" inductive proofs (for all sets $\alpha$, $\beta$, and $\gamma$):
- $\alpha+0=0+\alpha=\alpha$
- $\alpha\cdot 0=0\cdot\alpha=0$
- $\alpha\cdot 1=1\cdot\alpha=\alpha$
- $\alpha+(\beta+\gamma)=(\alpha+\beta)+\gamma$
- $\alpha\cdot(\beta+\gamma) = \alpha\cdot\beta + \alpha\cdot\gamma$
- $\alpha\cdot\beta\gamma=\alpha\beta\cdot\gamma,$
where $0 = \varnothing$ and $1 = \{0\}$. In each case the induction hypothesis is that the identity holds whenever we replace one of $\alpha$, $\beta$, or $\gamma$ by $\alpha'$, $\beta'$, or $\gamma'$ (note that this is vacuously true when the set being replaced is empty). For example, the proof that addition is associative is as follows:
$$ \alpha+(\beta+\gamma) = \{\alpha'+(\beta+\gamma), \alpha+(\beta+\gamma)' \} = \\ \{\alpha'+(\beta+\gamma), \alpha+(\beta'+\gamma), \alpha+(\beta+\gamma') \} = \\ \{(\alpha'+\beta)+\gamma, (\alpha+\beta')+\gamma, (\alpha+\beta)+\gamma' \} = \\ \{(\alpha+\beta)'+\gamma, (\alpha+\beta)+\gamma' \} = (\alpha+\beta)+\gamma.$$
It's also possible to prove that the sum or product of two ordinals is always an ordinal, and in fact $+$ and $\cdot$, when restricted to ordinals, are equivalent to the usual definition of the ordinal sum and product. Yet I've never seen ordinal arithmetic defined in this way! So my question is, is this definition well-known? And if so, why is it so seldom used?