Let IR be the field of real numbers, we define order on IR by the relation "less than" or " < ", such that, &forall. ~a, ~b, ~c, &in. &reals.:
Write _ ~a =< ~b _ ("less than or equal to") _ if ~a < ~b or ~a = ~b
also, write _ ~a > ~b _ ("greater than") _ <=> ~b < ~a
and _ ~a >= ~b _ ("greater than or equal to ") _ if ~a > ~b or ~a = ~b
We can deduce the following:
&naturals. &subset. &reals., IN = {1, 2, 3,...} the set of Natural Numbers or Positive Integers.
Axiom: A non-empty set of positive integers has a least member. i.e:
~S &subseteq. &naturals. , _ ~S != &empty. , _ then &exist. ~x &in. ~S such that _ ~x =< ~y , _ &forall. ~y &in. ~S
Note that ~x is unique (for ~S) for suppose ~x, ~x' least members, then ~x =< ~x' and ~x' =< ~x, so ~x = ~x'
There is no integer between 0 and 1.
Proof:
For any ~a &in. &reals. , _ 0 =< 1 , _ then _ 0 =< ~a^2 =< ~a =< 1.
If ~S = \{~n &in. &naturals. | ~n < 1 \} != &empty. , _ then ~S has a smallest member, _ ~m say , _ 0 < ~m < 1 _ => _ 0 =< ~m^2 =< ~m =< 1, _ => _ ~m^2 &in. ~S , _ Contradiction.
~S &subseteq. &naturals. , _ if _ 1 &in. ~S , _ and _ ~n &in. ~S => ~n + 1 &in. ~S , _ then ~S = &naturals.
Proof:
Suppose ~S != &naturals. , _ then if ~X = &naturals. #\ ~S, _ ~X != &empty., and &therefore. has a least member, ~m say, ~m != 1. So ~m - 1 &in. &naturals., but ~m - 1 &nin. ~X, so ~m - 1 &in. ~S => (~m - 1) + 1 &in. ~S by inductive hypothesis. So ~m &in. ~S. Contradiction.
For any ~x, ~y &in. &reals. , _ where _ ~x > 0, ~y > 0, _ &exist. ~n &in. &naturals. such that _ ~n~x > ~y.
Corollaries:
Proof: (of ii.)
Define the absolute value of ~x &in. &reals. as
| ~x | = ~x , _ if _ ~x >= 0
| ~x | = -~x , _ if _ ~x < 0
We have: | ~x | >= 0, _ &forall. ~x &in. &reals., _ and _ | -~x | = | ~x | .
Define the usual metric on IR : _ ~x, ~y &in. &reals. , _ d(~x, ~y) = | ~x - ~y |
we have:
Q &subset. &reals. _ - _ the set of rational numbers. _ ~q &in. Q _ => _ ~q = ~a/~b ; _ ~a, ~b &in. &integers.
There are rational numbers arbitrarily close to any real number.
i.e. _ for _ ~y &in. &reals. , _ given _ &epsilon. > 0 , _ &exist. _ ~p/~q &in. Q _ such that _ | ~y - ~p/~q | < &epsilon.
Proof:
&sqrt.2 &nin. Q
Proof:
Suppose _ (~p/~q)^2 = 2, _ and _ ~p/~q _ is in lowest terms. _ ~p^2 = 2~q^2 _ => _ ~p^2 is even , _ ~p = 2~r _ say, _ then _ (2~r)^2 = 2~q^2 , _ or _ 2~r^2 = ~q^2 _ => _ ~q^2 is even , _ so both ~p and ~q are even _ => _ ~p/~q is not in lowest terms. _ Contradiction.