[denotational]

> BB(764) is an integer (!) that I know is uncomputable

I meant BB(748) apparently.

To elaborate on this point a bit, I specifically mean uncomputable in ZFC. There may be other foundations in which it is computable, but we can just find another n for which BB(n) is uncomputable in that framework since BB is an uncomputable function.

[thaumasiotes]

Your method for deciding whether two rationals are or aren't equal relies on having representations of those rationals. If you don't have those, it doesn't matter that there's an efficient test of equality when you do.

But you're arguing that equality of Dedekind reals is undecidable based on a problem that occurs when you define a particular "Dedekind real" only by reference to some property that it has. If you had a representation of the values as Dedekind reals, it would be trivial to determine whether they were or weren't equal. You're holding them to a different standard than you're using for the integers and rationals. Why?

Let's decide a question about the integers. Is BB(800) equal to BB(801)?

It sure seems like it isn't. How sure are you?