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