Today at lunch, I brought up this issue with my colleagues, and to my surprise, Jeff E.'s argument that the problem is decidable did not convince them (here's a closely related post on mathoverflow). A problem statement that is easier to explain (is P = NP?) is also decidable: either yes or no, and so one of the two TMs that always output those answers decides the problem. Formally, we can decide the set $S :=\{|\{P, NP\}|\}$: either the machine that outputs $1$ only for input $1$ and otherwise $0$ decides it, or the machine that does so for input $2$.One of them boiled it down to basically this objection: if that's how weak the criterion of decidability is - which implies that every question which we can formalize as a language that we can show to be finite is decidable - then we should formalize a criterion that doesn't render any problem with finitely many possible answers that's formalizable in this way decidable. While the following is possibly a stronger criterion, I suggested that maybe this could be made precise by requiring that decidability should depend on being able to show a TM, basically proposing an intuitionist view of the matter (which I don't incline towards - nor do any of my colleagues, all of them accept the law of excluded middle).Have people formalized and possibly studied a constructive theory of decidability?
Constructive version of decidability?
computability;undecidability
I think the question you are trying to ask is is computability theory constructive?. And this is an interesting question, as you may see by this discussion on the Foundations of Mathematics mailing list.Unsurprisingly, it has been considered, since a lot of recursion theory was developed by people with constructive sensibilities and vice versa. See e.g. Besson's book and the venerable Introduction to Metamathematics. It's pretty clear that the first couple of chapters of recursion theory survive moving to a constructive setting with minimal changes: e.g. the s-n-m theorem, Rice's theorem or the Kleene recursion theorems survive unchanged.After the first chapters though, things get a bit tougher. In particular, the higher levels of the arithmetic hierarchy are usually defined by a notion of truth. In particular, widely used theorems such as the Low Basis Theorem seem to be explicitly non-constructive.Perhaps a more pragmatic response, though, is that these paradoxically computable languages are simply an idiosyncrasy, that can (and have!) been studied at great length, like non-measurable sets of reals, but that once the initial surprise has been overcome, one can move on to more interesting things.