I have a beginner's question about constructive mathematics.
Let $X$ denote a set in the constructive universe. Then a subset $A$ of $X$ is said to be decideable iff $X$ is the union of $A$ and it's complement. Of course, when it comes to the natural numbers, there's also a notion of decidability in computer science; a subset of $\mathbb{N}$ is said to be decideable iff the corresponding predicate on $\mathbb{N}$ is a computable function.
Question. Are these the same notion, and if not, what is the relationship between them?
The two concepts are closely related, but first we need to look at how to read the definitions. To avoid using "decidable" to mean two things, let's say that a set $X \subseteq U$ is complement-decidable if every element of $U$ is in $X$ or in $X^c$ - that is, every element is in $X$ or is not in $X$. We already know what it means for the set $X$ to be decidable in the sense of computability - it means the set is a computable set, that is, there is an algorithm to determine for an arbitrary $z$ whether $z \in X$.
To compare complement-decidability with computability more easily, let's also take $U = \mathbb{N}$. So now we have that a set $X \subseteq \mathbb{N}$ is complement-decidable if, for all $z \in \mathbb{N}$, either $z \in X$ or $z \not \in X$. And the definition of $X$ being computable is the standard one using Turing machines. For more general $U$, we would need more general concepts of computability.
If we read the definition of "complement-decidable" classically, we get nothing, because just the law of the excluded middle says that every subset of $\mathbb{N}$ is complement-decidable. We already know that not every subset of $\mathbb{N}$ is computable. So this is not a productive way to read things. To understand constructive mathematics we need to read formulas in the way that a constructive mathematician would read them.
If we read the definition of "complement-decidable" constructively, we start to see a resemblance with computability. Constructively, according to the BHK interpretation, if we can assert that $z \in X \lor z \not \in X$ then we are able to determine, somehow, whether $z$ is in $X$ or not. Asserting that $X$ is complement-decidable, according to the BHK interpretation, means having some process by which we can determine, given $z \in \mathbb{N}$, whether $z$ is in $X$.
So, reading things constructively, if we know (constructively) that a set $X \subseteq \mathbb{N}$ is computable, we also know it is complement-decidable, because we can use the Turing machine algorithm to make the appropriate determination for each $z\in\mathbb{N}$. Of course, we need a constructive proof that the algorithm really does decide membership for the set in question.
For the converse, the problem is whether the process we use to see that a set is complement-decidable actually corresponds to a formal algorithm that could be programmed into a Turing machine. Not all varieties of constructive mathematics are willing to explicitly limit the decision processes available to the mathematician to just computable processes. If a particular constructive mathematicians is not willing to make that restriction, then she may not be willing to accept that every complement-decidable subset of $\mathbb{N}$ is computable.
However, the method of realizability comes in when we starting looking at formal systems. From one perspective, the general purpose of realizability is to extract programs - computation algorithms - from formalized constructive proofs. Of course, a constructive mathematician may not be willing to limit her methods to any particular formal system. A resistance to formalization is one of the common characteristics of constructive mathematicians including Bishop and Brouwer. Nevertheless, suppose we do look at just provability in a fixed formal constructive theory.
For many constructive formal systems, such as Heyting Arithmetic, there are formal constructive proofs showing that every formula that is provable in the system is realizable by a Turing machine algorithm. In particular, in a constructive system that is amenable to these realizability methods, we can show that if the system proves a set $X \subseteq \mathbb{N}$ is complement-decidable, then the set $X$ is in fact computable. Some systems with that property include Heyting arithmetic and its extensions to constructive second-order arithmetic, some of which are comparable to Bishop's system of constructive mathematics.
We could also ask: if we know from outside a formal system that every function that is provably total in the system is computable, could we add the (classically false) axiom to the system which explicitly says that every total function is computable? This is analogous to adding an axiom saying that every complement-decidable subset of $\mathbb{N}$ is computable, once we know that every every set that is provably complement-decidable is computable. But in the literature it is usually stated in terms of functions rather than sets.
This line of thinking leads to something called Church's thesis (CT) in constructive mathematics, which is related to but not identical with the Church-Turing thesis in computability theory. Although the constructive CT is classically false, it is consistent with many constructive formal systems, including Heyting Arithmetic.
One way to understand this is that, if a constructive system can prove $(\forall z)(\exists !y)R(z,y)$, then by the BHK interpretation there should already be a process to determine $y$ from $z$, and so explicitly assuming that there is such a process does not necessarily add much strength to the system. The case of complement-decidability follows by taking $R(z,y) \equiv [y = 0 \leftrightarrow z \in X]$.