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 11 to define the real numbers.

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

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:a:\mathbb{R} and b:b:\mathbb{R}, the open interval (a,b)(a,b) is inhabited.

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

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

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

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

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

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

Addition axioms: ++

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

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

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

  • 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 a<a+b+ca \lt a + b + c

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

References

  • Alfred, Tarski (24 March 1994), Introduction to Logic and to the Methodology of Deductive Sciences, Oxford University Press, ISBN 978-0-19-504472-0

Revision on April 22, 2022 at 04:40:17 by Anonymous?. See the history of this page for a list of all contributions to it.