On 2/18/2013 9:27 PM, Shmuel (Seymour J.) Metz wrote: > In <hd-dnfiTht7VboLMnZ2dnUVZ_r6dnZ2d@giganews.com>, on 02/16/2013 > at 02:59 PM, fom <fomJUNK@nyms.net> said: > >> In the logical construction of the real numbers system >> using Dedekind cuts, one must fix a choice as to which >> kind of rational cut will be taken as canonical. > > It's more convenient to do so, but it's not actually necessary.
The construction establishes the identity of the cuts in relation ' to the ordering on the rationals from which those cuts are derived. In a full construction, that order is inherited from the naturals through several levels of definition.
Because different disciplines do different parts of the construction, this is not consistent in the literature. Generally, since the Dedekind cut construction would be presented in an analysis course, the order will reflect "initial segments". This is actually the reverse of an ordering carried up from the naturals.
> >>> In general , machines can't decide the equality or inequality of real >>> numbers ,or infinite strings in general ,without the 0.(9) = 1 >>> equivalence of real numbers. > > Programs capable of proving theorems have been available for decades. > >> So, in the hierarchy of logical definition, one obtains the real >> numbers from Dedekind cuts relative to a logical identity >> relation. Then, a definition of least upper bound and greatest >> lower bound for that system may be defined. Then, provided that >> the nature of relations used in the metrization lemma are >> satisfiable, one uses the function constructed in that proof to >> put a metric on the system of Dedekind cuts. > > It's the other way around; one needs the Reals to define a metric, and > once one has the Reals the standard metric is a trivial construction, > the details of which don't depend on whether one used Axioms, Cauchy > sequences of rational or Dedekind cuts of rationals. >
You seem to be thinking in terms of the Cantorian fundamental sequences. I never really thought there was a difference until I was very carefully tracing how one would take the logical
and attach a metric constraint on it.
For a metric, one has
x=y <-> d(x,y)=0
But logic does not begin with a metric in its assertions. To accomplish what I am talking about, one needs the weakened
x=y -> d(x,y)=0
which forces one to look at pseudometrics. The topological theory in which this happens is that of uniform spaces. These are derived from generalization of the uniform properties of the reals, but, one can speak of a uniform topology with respect to a system of binary relations that satisfy certain constraints, among which is containing the diagonal as a subset. These relations need not be obtained through numerical means.
In Kelley, the proof of what suffices to formulate a pseudometric for a system of relations utilizes the least upper bound property in an essential way. So, in that sense the Dedekind cuts are logically prior.
And, you are correct in your assertion. Whatever comes out of the metrization is not usable. It merely binds a system together in relation to a distance. One would immediately establish the usual metric by other means.