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.
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.