An abelian group is a pointed set with a binary operation called subtraction such that
for all ,
for all ,
for all and ,
for all , , and ,
Halving groups
A halving group is an abelian group G with a function called halving or dividing by two such that for all , .
Totally ordered halving groups
An abelian group is a totally ordered abelian group if it comes with a function such that
for all elements ,
for all elements and ,
for all elements , , and ,
for all elements and , implies that for all elements ,
for all elements and , or
Strictly ordered pointed halving groups
A totally ordered commutative ring is a strictly ordered pointed abelian group if it comes with an element and a type family such that
for all elements and , is a proposition
for all elements , is false
for all elements , , and , if , then or
for all elements and , if is false and is false, then
for all elements and , if , then is false.
for all elements and , if and , then
…
Archimedean ordered pointed halving groups
A strictly ordered pointed halving group is an Archimedean ordered pointed halving group if for all elements and , if , then there merely exists a dyadic rational number such that and .
Sequentially Cauchy complete Archimedean ordered pointed halving groups
Let be an Archimedean ordered pointed halving group and let
be the positive elements in . is sequentially Cauchy complete if every Cauchy sequence in converges: