I claim Dedekind cuts should be defined in a less hardcoded manner. Galaxy brain meme:
An irrational number is something that can sneak into (Q,<), such as sqrt(2)=”the number which is greater than all rational numbers whose square is less than 2″. So infinity is not a real number because there is no greatest rational number, and epsilon is not a real number because there is no smallest rational number greater than zero.
An irrational number is a one-element elementary extension of (Q,<). (Of course, the proper definition would waive the constraint that the new element be original, instead of treating rationals and irrationals separately.)
The real numbers are the colimit of the finite elementary extensions of (Q,<).
I claim Cauchy sequences should be defined in a less hardcoded manner, too: A sequence is Cauchy (e.g. in (Q,Euclidean distance)) iff it converges in some (wlog one-element) extension of the space.
Not sure this works constructively. x < y or x = y or x > y is valid for the constructive rationals, but taboo for the constructive reals. Wouldn’t this make it taboo for the real order to be an elementary extension of the rational order? Not familiar with constructive model theory so not entirely sure.
It seems that a real number defined this way will have some perhaps-infinite list of rationals it’s less than and one it’s greater than. You might want to add a constraint that the maximum of the list of numbers it’s above gets arbitrarily close to the minimum of the list of numbers it’s below (as Tailcalled suggested).
With respect to Cauchy sequences, the issue is how to specify convergence; the epsilon/N definition is one way to do this and, constructively, gives a way of computing epsilon-good approximations.
With just that you could get upper bounds for the real. You could get some lower bounds by showing all rationals in the enumeration are greater than some rational, but this isn’t always possible to do, so maybe your type includes things that aren’t real numbers with provable lower bounds.
If you require both then we’re back at the situation where, if there’s a constructive proof that the enumerations min/max to the same value, you can get a Cauchy real out of this, and perhaps these are equivalent.
They are. To get enumerations of rationals above and below out of an effective Cauchy sequence, once the Cauchy sequence outputs a rational q such that everything afterwards can only differ by at most ε, you start enumerating rationals below q−ε as below the real and rationals above q+ε as above the real. If the Cauchy sequence converges to r, and you have a rational q<r, then once the Cauchy sequence gets to the point where everything after is gauranteed to differ by at most r−q2, you can enumerate q as less than r.
Chaitin’s constant, right. I should have taken my own advice and said “an enumeration of all properties of our number that can be written in the first-order logic (Q,<)”.
This means that, in particular, if your real happens to be rational, you can produce the fact that it is equal to some particular rational number. Neither Cauchy reals nor Dedekind reals have this property.
Sure! Fortunately, while you can use this to prove any rational real innocent of being irrational, you can’t use this to prove any irrational real guilty of being irrational, since every first-order formula can only check against finitely many constants.
Something that I think it unsatisfying about this is that the rationals aren’t previleged as a countable dense subset of the reals; it just happens to be a convenient one. The completions of the diadic rationals, the rationals, and the algebraic real numbers are all the same. But if you require that an element of the completion, if equal to an element of the countable set being completed, must eventually certify this equality, then the completions of the diadic rationals, rationals, and algebraic reals are all constructively inequivalent.
Hmmmm. What if I said “an enumeration of the first-order theory of (union(Q,{our number}),<)”? Then any number can claim to be equal to one of the constants.
If you want to transfer definitions into another context (constructive, in this case), you should treat such concrete, intuitive properties as theorems, not axioms, because the abstract formulation will generalize further. (remark: “close” is about distances, not order.)
If constructivism adds a degree of freedom in the definition of convergence, I’d try to use it to rescue the theorem that the Dedekindorder and Cauchydistance structures on ℚ agree about the completion. Potential rewards include survival of the theory built on top and evidence about the ideal definition of convergence. (I bet it’s not epsilon/N, because why would a natural property of maps from ℕ to ℚ introduce the variable of type ℚ before the variable of type ℕ?)
I claim Dedekind cuts should be defined in a less hardcoded manner. Galaxy brain meme:
An irrational number is something that can sneak into (Q,<), such as sqrt(2)=”the number which is greater than all rational numbers whose square is less than 2″. So infinity is not a real number because there is no greatest rational number, and epsilon is not a real number because there is no smallest rational number greater than zero.
An irrational number is a one-element elementary extension of (Q,<). (Of course, the proper definition would waive the constraint that the new element be original, instead of treating rationals and irrationals separately.)
The real numbers are the colimit of the finite elementary extensions of (Q,<).
I claim Cauchy sequences should be defined in a less hardcoded manner, too: A sequence is Cauchy (e.g. in (Q,Euclidean distance)) iff it converges in some (wlog one-element) extension of the space.
Not sure this works constructively. x < y or x = y or x > y is valid for the constructive rationals, but taboo for the constructive reals. Wouldn’t this make it taboo for the real order to be an elementary extension of the rational order? Not familiar with constructive model theory so not entirely sure.
It seems that a real number defined this way will have some perhaps-infinite list of rationals it’s less than and one it’s greater than. You might want to add a constraint that the maximum of the list of numbers it’s above gets arbitrarily close to the minimum of the list of numbers it’s below (as Tailcalled suggested).
With respect to Cauchy sequences, the issue is how to specify convergence; the epsilon/N definition is one way to do this and, constructively, gives a way of computing epsilon-good approximations.
Oh, I misunderstood the point of your first paragraph. What if we require an enumeration of all rationals our number is greater than?
With just that you could get upper bounds for the real. You could get some lower bounds by showing all rationals in the enumeration are greater than some rational, but this isn’t always possible to do, so maybe your type includes things that aren’t real numbers with provable lower bounds.
If you require both then we’re back at the situation where, if there’s a constructive proof that the enumerations min/max to the same value, you can get a Cauchy real out of this, and perhaps these are equivalent.
They are. To get enumerations of rationals above and below out of an effective Cauchy sequence, once the Cauchy sequence outputs a rational q such that everything afterwards can only differ by at most ε, you start enumerating rationals below q−ε as below the real and rationals above q+ε as above the real. If the Cauchy sequence converges to r, and you have a rational q<r, then once the Cauchy sequence gets to the point where everything after is gauranteed to differ by at most r−q2, you can enumerate q as less than r.
Chaitin’s constant, right. I should have taken my own advice and said “an enumeration of all properties of our number that can be written in the first-order logic (Q,<)”.
This means that, in particular, if your real happens to be rational, you can produce the fact that it is equal to some particular rational number. Neither Cauchy reals nor Dedekind reals have this property.
Sure! Fortunately, while you can use this to prove any rational real innocent of being irrational, you can’t use this to prove any irrational real guilty of being irrational, since every first-order formula can only check against finitely many constants.
Something that I think it unsatisfying about this is that the rationals aren’t previleged as a countable dense subset of the reals; it just happens to be a convenient one. The completions of the diadic rationals, the rationals, and the algebraic real numbers are all the same. But if you require that an element of the completion, if equal to an element of the countable set being completed, must eventually certify this equality, then the completions of the diadic rationals, rationals, and algebraic reals are all constructively inequivalent.
Hmmmm. What if I said “an enumeration of the first-order theory of (union(Q,{our number}),<)”? Then any number can claim to be equal to one of the constants.
If you want to transfer definitions into another context (constructive, in this case), you should treat such concrete, intuitive properties as theorems, not axioms, because the abstract formulation will generalize further. (remark: “close” is about distances, not order.)
If constructivism adds a degree of freedom in the definition of convergence, I’d try to use it to rescue the theorem that the
Dedekindorder andCauchydistance structures on ℚ agree about the completion. Potential rewards include survival of the theory built on top and evidence about the ideal definition of convergence. (I bet it’s not epsilon/N, because why would a natural property of maps from ℕ to ℚ introduce the variable of type ℚ before the variable of type ℕ?)