The real numbers, when constructed as Dedekind cuts over the rationals, form a field.

We shall often write the one-sided [dedekind_cut Dedekind cut] $~$(A, B)$~$ %%note:Recall: "one-sided" means that $~$A$~$ has no greatest element.%% as simply $~$\mathbf{A}$~$ (using bold face for Dedekind cuts); we can do this because if we already know $~$A$~$ then $~$B$~$ is completely determined. This will make our notation less messy.

The field structure, together with the [total_order total ordering] on it, is as follows (where we write $~$\mathbf{0}$~$ for the Dedekind cut $~$(\{ r \in \mathbb{Q} \mid r < 0\}, \{ r \in \mathbb{Q} \mid r \geq 0 \})$~$):

• $~$(A, B) + (C, D) = (A+C, B+D)$~$
• $~$\mathbf{A} \leq \mathbf{C}$~$ if and only if everything in $~$A$~$ lies in $~$C$~$.
• Multiplication is somewhat complicated.
• If $~$\mathbf{0} \leq \mathbf{A}$~$, then $~$\mathbf{A} \times \mathbf{C} = \{ a c \mid a \in A, a > 0, c \in C \}$~$. [todo: we've missed out the complement in this notation, and can't put set-builder sets in boldface]
• If $~$\mathbf{A} < \mathbf{0}$~$ and $~$\mathbf{0} \leq \mathbf{C}$~$, then $~$\mathbf{A} \times \mathbf{C} = \{ a c \mid a \in A, c \in C, c > 0 \}$~$.
• If $~$\mathbf{A} < \mathbf{0}$~$ and $~$\mathbf{C} < \mathbf{0}$~$, then $~$\mathbf{A} \times \mathbf{C} = \{\} $~$ [todo: write down the form of the set]

where $~$(A, B)$~$ is a one-sided [dedekind_cut Dedekind cut] (so that $~$A$~$ has no greatest element).

(Here, the "set sum" $~$A+C$~$ is defined as "everything that can be made by adding one thing from $~$A$~$ to one thing from $~$C$~$": namely, $~$\{ a+c \mid a \in A, c \in C \}$~$ in Set builder notation; and $~$A \times C$~$ is similarly $~$\{ a \times c \mid a \in A, c \in C \}$~$.)

Proof

Well-definedness

We need to show firstly that these operations do in fact produce [dedekind_cut Dedekind cuts].

Addition

Firstly, we need everything in $~$A+C$~$ to be less than everything in $~$B+D$~$. This is true: if $~$a+c \in A+C$~$, and $~$b+d \in B+D$~$, then since $~$a < b$~$ and $~$c < d$~$, we have $~$a+c < b+d$~$.

Next, we need $~$A+C$~$ and $~$B+D$~$ together to contain all the rationals. This is true: [todo: this, it's quite boring]

Finally, we need $~$(A+C, B+D)$~$ to be one-sided: that is, $~$A+C$~$ needs to have no top element, or equivalently, if $~$a+c \in A+C$~$ then we can find a bigger $~$a' + c'$~$ in $~$A+C$~$. This is also true: if $~$a+c$~$ is an element of $~$A+C$~$, then we can find an element $~$a'$~$ of $~$A$~$ which is bigger than $~$a$~$, and an element $~$c'$~$ of $~$C$~$ which is bigger than $~$C$~$ (since both $~$A$~$ and $~$C$~$ have no top elements, because the respective Dedekind cuts are one-sided); then $~$a' + c'$~$ is in $~$A+C$~$ and is bigger than $~$a+c$~$.

Multiplication

[todo: this section]

Ordering

[todo: this section]

Additive commutative group structure

[todo: identity, associativity, inverse, commutativity]

Ring structure

[todo: multiplicative identity, associativity, distributivity]

Field structure

[todo: inverses]

Ordering on the field

[todo: a <= b implies a+c <= b+c, and 0 <= a, 0 <= b implies 0 <= ab]