equality is always undecidable until you see the light of intuition. consider the rational number whose numerator is 0 if $theorem is true, and 1 if it is false, and whose denominator is 1.
Okay, theorem=generalized-continuum hypothesis. If you use exotic axioms to give that a definite result, the go eat a Gödel.
We define computable numbers to be Turing machines, lambda reduction processes, or whatever your favorite model of computation happens to be. If you don't like this kind of definition, then we need to talk philosophy of computation.
To decide equality, we let your machines clunk along until they both produce a result, which we then compare (using another machine). Hello Mr. Halting Problem. Specific programs are fine, but comparing against arbitrary classes of program is the bugger. This is why discontinuous functions cannot exist in a hardline computable analysis theory.
But there are numbers in constructivism for which it is unknown whether they are zero. Some of which must remain unknown, if mathematics is consistent. This is a rather important and weird edge case.
We define computable numbers to be Turing machines, lambda reduction processes, or whatever your favorite model of computation happens to be. If you don't like this kind of definition, then we need to talk philosophy of computation.
To decide equality, we let your machines clunk along until they both produce a result, which we then compare (using another machine). Hello Mr. Halting Problem. Specific programs are fine, but comparing against arbitrary classes of program is the bugger. This is why discontinuous functions cannot exist in a hardline computable analysis theory.