Sorry, replace "x < B" with "0 < x" above. On Tue, Jul 8, 2014 at 10:53 AM, Scott Fenton <sctfen@gmail.com> wrote:
OK, I can't find anything other than a mention of it being related to Eudoxus' definition of magnitude. From Euclid's Elements, that goes as follows (rephrased into modern notation):
If A, B, C, D are positive reals, then A/B = C/D iff:
forall n, m in NN : ( ( n*A < m*B iff n*C < m*D ) and ( n*A = m*B iff n*C = m*D ) and ( n*A > m*B iff n*C > m*D ) )
From total ordering, this can be simplified to:
forall n, m in NN : ( n*A < m*B iff n*C < m*D )
With cross-multiplying, setting B to 1, and renaming variables, we get this:
If A, B, C are positive reals, then A*B = C iff
forall n, m in NN: ( n*A < m iff n*C < m*B ) Since n, m are naturals, the multiplication there can be replaced by summation:
forall n, m in NN: ( sum(A,k,1,n) < m iff sum(C,k,1,n) < sum(B,k,1,m) )
We can generalize this to all real numbers as follows (I think):
Given A, B real, A*B is defined as follows:
If A or B is 0, then A*B = 0 Else, A*B is the unique real number "x" such that:
( (0 < A iff 0 < B) iff x < B ) and forall n, m in NN: ( sum(abs(A),k,1,n) < m iff sum(abs(x),k,1,n) < sum(abs(B),k,1,m) )
From a modified version of density, I'm pretty sure I can prove uniqueness of x. The problem now is to prove existence and the field properties. Anyone got any ideas? Remember, we've only got addition, limits, and comparison to work with.
-Scott