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 1 to define the real numbers.
Definition
Strict order axioms: < \lt
For all terms a : ℝ a:\mathbb{R} , a < a a \lt a is false.
For all terms a : ℝ a:\mathbb{R} , b : ℝ b:\mathbb{R} , c : ℝ c:\mathbb{R} , a < c a \lt c implies a < b a \lt b or b < c b \lt c
For all terms a : ℝ a:\mathbb{R} , b : ℝ b:\mathbb{R} , not a < b a \lt b and not b < a b \lt a implies a = b a = b .
For all terms a : ℝ a:\mathbb{R} , b : ℝ b:\mathbb{R} , a < b a \lt b implies not b < a b \lt a
Denseness and Dedekind completeness axioms: open interval s, lower bounded open interval s, and upper bounded open interval s 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 < b a \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 < a b \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 < b a \lt b , then F F 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 + a a + b = b + a
For all terms a : ℝ a:\mathbb{R} , b : ℝ b:\mathbb{R} , and c : ℝ c:\mathbb{R} , a + ( b + c ) = ( a + b ) + c a + (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 = a a + b + c = a
For all terms a : ℝ a:\mathbb{R} , b : ℝ b:\mathbb{R} , and c : ℝ c:\mathbb{R} , a < a + b a \lt a + b and a < a + c a \lt a + c implies a < a + b + c a \lt a + b + c
Archimedean property:
For all terms a : ℝ a:\mathbb{R} , b : ℝ b:\mathbb{R} , and c : ℝ c:\mathbb{R} , a < a + b a \lt a + b and a < a + c a \lt a + c implies that there exists a natural number n : ℕ n:\mathbb{N} such that b < n c b \lt n c , where n c n c is the additive n n -th power (n-fold addition)
One axioms: 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 08:40:17 by
Anonymous? .
See the history of this page for a list of all contributions to it.