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

Idea

I am going to define this in terms of Archimedean pointed halving groups…

Definition

Strict order axioms: <\lt

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

  • For all terms a:a:\mathbb{R}, b:b:\mathbb{R}, c:c:\mathbb{R}, a<ca \lt c implies a<ba \lt b or b<cb \lt c

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

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

Archimedean property:

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

One axioms: 11

  • 1<1+11 \lt 1 + 1

See also

Revision on June 15, 2022 at 18:28:09 by Anonymous?. See the history of this page for a list of all contributions to it.