Number Trichotomy and Constructive Math I've been reading up on constructive math. Something that comes up is trichotomy: For all real numbers $x$, $x > 0$, $x < 0$, or $x = 0$.  In constructive math, you cannot prove this since you need to be able to prove which is true. Examples of numbers that cause problems are always based on unknown theorems. For example, we have a sequence $a_n$ such that the $n$th number is $0$ or $1$ based on whether the $2n$ is the sum of two primes (Goldbach's Conjecture). Then we use these $a_n$ combined with a series to define a number. The complaint a constructionist has is that, since Golbach's Conjecture is unproven, we can't prove whether the constructed number satisfies one of the three conditions in the trichotomy.
These examples never have much impact on me since we might someday have a proof of Goldbach's Conjecture, and thus know which of the trichotomy the number satisfies. I have probably seen about four or five numbers constructed this way. My question is: Why don't people use a known undecidable proposition (like the Continuum Hypothesis) to construct these numbers? Then it is rock solid that we will never know if the number is less than $0$, greater than $0$, or equal to $0$. Is it somehow invalid to use an undecidable proposition?
 A: You are mixing together different notions of decidability. The relevant notion of decidability here is defined as follows: $P$ is decidable iff $P \lor \neg P$ holds. The Continuum Hypothesis, along with every other proposition, is decidable in this sense classically. Of course, for $\text{CH}\lor\neg\text{CH}$, we know that it holds, but we don't know which case holds. The constructive interpretation of $\lor$, however, requires us to actually know which case it is.
(Extensional) equality of two given sequences of bits, i.e. functions $\mathbb{N}\to\mathbf{2}$, is a $\Pi_1$ statement as is the Goldbach conjecture. This means if either is false, we can algorithmically find a counter-example in finite time.
Note what's happening in the Goldbach conjecture case. We aren't saying "if Goldbach conjecture is true then $x$ else $y$", we are making a statement that given the constructive decidability of equality on reals (or, technically, functions $\mathbb{N}\to\mathbb{2}$ from which we can make real numbers) we get constructive decidability of the Goldbach conjecture as a special case. This sort of example is called a weak counterexample. The idea isn't so much "ha, we don't know if Goldbach's conjecture is true, so we can't decide equality of real numbers". Instead, it's that decidability of real number equality "solves" the problem for free.  The point is that decidability of real number equality "solves" all $\Pi_1$ problems for free; we can stick any $\Pi_1$ problem in for Goldbach's conjecture instead. We can formulate this more definitively.
Let $T$ be a Turing machine and define $a(T)_n$ as $1$ if $T$ is in a halting state after $n$ steps, and $0$ otherwise.  The function from (encodings of descriptions of) Turing machines to sequences of bits is completely constructively/algorithmically definable. (You can make a Turing machine to do it.) We can make a real number via $r_T = \sum_{n=0}^\infty a(T)_n/2^n$. This mapping is also constructively definable given a suitably constructive notion of reals. (Alternatively, we could just talk about equality of $\mathbb{N}\to\mathbf{2}$ functions.) Decidability of $r_T = 0$ is decidability of whether $T$ halts. Decidability of equality for the reals generally implies decidability of the halting problem. Since we can make a Turing machine that enumerates all the theorems of ZFC and halts when it finds a particular one, decidability of real number equality can now show for any statement in the formal theory of ZFC whether it's provable, refutable, or independent. You will not be surprised to hear that this is related to omniscience principles.
