Here will be presented a draft of mathematical formalization (as an axiomatic theory) of the concepts of quantity (as used throughout physics) and real numbers and justification of their main properties.

I consider this as a quite needed work, usually neglected, with
the habit of mathematicians to ignore the concept of quantity and
focus instead on formalizing the system of real numbers, in a
rather complicated way; and the absence of interest or inspiration
by physics teachers to bring any mathematical rigor in their
courses.

Still some claims here will be admitted without proof, as the full
proofs would be a bit too difficult for the main purpose of this
text which is to introduce the mathematical language for physics.

(abelian = commutative)

We start with the concept of *ordered abelian group*, that
is a set G with :

Structures:

- a constant (0)
- a binary operation (+)
- a negation function (-)
- a subset (or unary relation of positivity)
*G*_{+}⊂*G*called the*positive cone*of*G*(the set of positive elements of G).

Axioms:

- (
*G*, 0,+,-) is a commutative group: - ∀
*x*∈*G*,*x*+0=*x* - ∀
*x*∈*G*,*x*+(-*x*)=0 - ∀
*x*,*y*∈*G*,*x*+*y*=*y*+*x*

- ∀
*x*,*y*,*z*∈*G*, (*x*+*y*)+*z*=*x*+(*y*+*z*) *G*_{+}is a sub-monoid of G:- 0∈
*G*_{+} - ∀
*x*,*y*∈*G*_{+},*x*+*y*∈*G*_{+} - ∀
*x*∈*G*_{+}, (-*x*)∈*G*_{+}⇒*x*=0

We define the subtraction *x*−*y* = *x*+(-*y*)
so that *z* = *x*−*y* ⇔ *x* = *y*+*z*.

We also define the product *nx* for *x*∈*G* and
*n*∈ℕ, as equal to (*x*+...+*x*) (*n* times),
also equal to the image of *n* by the unique morphism of
monoid from ℕ to *G* that maps 1 to *x*.

An element *x*∈*G* is called *negative* if its
opposite is positive: *x*∈*G*_{-} ⇔ -*x*∈*G*_{+}.
Thus the last condition says that an element cannot be both
positive and negative, unless it is 0.

The preorder relation defined by an action of such a *G* on
a set *E* (by ∀*x*,*y*∈*E*, *x*≤*y*
⇔∃*g* ∈*G*_{+} G, *g*+*x*=*y*)
is then a order if every element of *E* belongs to the
trajectory of a free element.

Thus it also defines an order relation on *G*, as *G*
acts on itself by + and fits this condition.

It can be expressed as

∀*x*,*y*∈*E*, *x*≤*y* ⇔ *y*−*x* ∈*G*_{+}*.*

Now we introduce the more specific concept of *totally ordered
abelian group*, by strengthening the last condition: every
element is either positive or negative, while only 0 is both:

- ∀
*x*∈*G*, (*x*∈*G*_{+}⇔*x*∈*G*_{-}) ⇒*x*=0.

Then, the order defined by an action of such a *G* is a
total order.

Denoting the set of strictly positive elements as *G*_{++}
= {*x*∈*G*_{+}|*x*≠0}=*G*\*G*_{-},
the strict order is

*x*<*y* ⇔ *x*≤*y*∧*x*≠*y*
⇔ *x*−*y* ∉*G*_{+}⇔ *y*−*x* ∈*G*_{++}*.*

(Note: it would also be possible to formalize totally ordered
abelian groups by means of the monoid *G*_{+} alone,
as any other element is negative so that it can represented by its
opposite in *G*_{+}. To ensure the same properties,
such a formalization would involve the operation of subtraction,
with some axioms. )

Further possible properties of this system can be considered:

A totally ordered abelian group is

*Archimedean*if ∀*x*,*y*∈*G*_{++}, ∃*n*∈ℕ,*y*≤*nx*.*Complete*if every nonempty subset of*G*_{+}has an infimum (see definition of infimum in the text on Galois connections)*Discrete*if it has a smallest strictly positive element (a unit 1∈*G*_{++}such that ∀*x*∈*G*_{++}, 1≤*x*) and is thus isomorphic with the set of integers; otherwise it is called*dense*.

Being complete implies being Archimedean, but the converse is not
true (for example the set of rational numbers is Archimedean but
not complete).

**Definition.** A *type of quantities* is a totally
ordered abelian group that is dense and complete.

**Definition.** The *set of real numbers* is a type of
quantities denoted ℝ, with another constant symbol 1∈ℝ_{++}
called the unit (thus, not the smallest element of ℝ_{++}).

This "definition" does not exactly specify the system ℝ, but it
essentially does so in the sense that for any 2 systems satisfying
this definition there exists a unique isomorphism between them.
This will come from the following theorem, whose proof (not
written were) actually involves a specifically constructed ℝ, but
finally works for any type of quantity with a choice of unit:

**Theorem.** For any totally ordered abelian group *G*
and any ∀*x*∈*G*_{++} such that (∀*y*∈*G*_{+},
∃*n*∈ℕ, *y*≤*nx*), there exists a unique morphism
("ratio by x") *r _{x}* ∈Mor(

(to be continued)

with axioms that require this to be a total order.

Back to homepage: set theory and
foundations