Homotopy Type Theory an axiomatization of the real numbers > history (Rev #1)

Idea

An axiomatization of the real numbers very similar to Tarski’s axiomatization of the real numbers, in that it only uses a strict order $\lt$, addition $+$, and one $1$ to define the real numbers.

Definition

Strict order axioms: $\lt$

• For all terms $a:\mathbb{R}$, $a \lt a$ is false.

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, $c:\mathbb{R}$, $a \lt c$ implies $a \lt b$ or $b \lt c$

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, not $a \lt b$ and not $b \lt a$ implies $a = b$.

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, $a \lt b$ implies not $b \lt a$

Denseness and Dedekind completeness axioms: open intervals, lower bounded open intervals, and upper bounded open intervals can be defined in any strictly ordered set

• For all terms $a:\mathbb{R}$ and $b:\mathbb{R}$, the open interval $(a,b)$ is inhabited.

• For all terms $a:\mathbb{R}$, the lower bounded open interval $(a,\infty)$ is inhabited.

• For all terms $a:\mathbb{R}$, the upper bounded open interval $(-\infty,a)$ is inhabited.

• For all terms $a:\mathbb{R}$ and $b:\mathbb{R}$, $a \lt b$ if and only if $(b,\infty)$ is a subinterval of $(a,\infty)$

• For all terms $a:\mathbb{R}$ and $b:\mathbb{R}$, $b \lt a$ if and only if $(-\infty,b)$ is a subinterval of $(-\infty,a)$

• For all terms $a:\mathbb{R}$ and $b:\mathbb{R}$, if $a \lt b$, then $F$ is a subinterval of the union of $(a, \infty)$ and $(-\infty, b)$

• For all terms $a:\mathbb{R}$ and $b:\mathbb{R}$, the intersection of $(a,\infty)$ and $(-\infty,b)$ is a subinterval of $(a,b)$

Addition axioms: $+$

• For all terms $a:\mathbb{R}$ and $b:\mathbb{R}$, $a + b = b + a$

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, and $c:\mathbb{R}$, $a + (b + c) = (a + b) + c$

• For all terms $a:\mathbb{R}$ and $b:\mathbb{R}$, there exists a term $c:\mathbb{R}$ such that $a + b + c = a$

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, and $c:\mathbb{R}$, $a \lt a + b$ and $a \lt a + c$ implies $a \lt a + b + c$

Archimedean property:

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, and $c:\mathbb{R}$, $a \lt a + b$ and $a \lt a + c$ implies that there exists a natural number $n:\mathbb{N}$ such that $b \lt n c$, where $n c$ is the additive $n$-th power (n-fold addition)

One axioms: $1$

• $1 \lt 1 + 1$