Finding out whether a proposition variable $A$, its negation ${\sim}A$ or neither can be deduced from an infinite set of premises $\mathcal T$ (i.e. respectively $\mathcal T \vdash A$, $\mathcal T \vdash {\sim}A$, or $\left( \mathcal T \nvdash A \ \text{and}\ \mathcal T \nvdash {\sim}A \right)$) is not in general computable, because the possibility of the "neither" case implies that the process may not terminate.
Yet, it does seem that $\{\, A \mathop{|} \mathcal T \vdash {\sim}A \,\}$ is a legitimate set, even if membership of an arbitrary $A$ is undecidable.
The following consideration inclines me to think my hesitation to use such a set in a constructive proof is unwarranted:
- The property $\mathcal T \vdash {\sim}x$ is provably undecidable, therefore is is well-defined; and so is therefore the subset of the universe of discourse that exhibits this property.
Somehow, I suspect that decidability/computability and well-definedness belong to different domains. But I don't know how to articulate this precisely. Is there some foundation principle I can refer to?