Are there examples of sets of natural numbers that are proven to be decidable but by nonconstructive proofs only?
When I teach computability, I usually use the following example to illustrate the point.
Let $f(n)=1$, if there are $n$ consecutive $1$s somewhere in the decimal expansion of $\pi$, and $f(n)=0$ otherwise. Is this a computable function?
Some students might try naively to compute it like this: on input $n$, start to enumerate the digits of $\pi$, and look for $n$ consecutive $1$s. If found, then output $1$. But then they realize: what if on a particular input, you have searched for 10 years, and still not found the instance? You don't seem justified in outputting $0$ quite yet, since perhaps you might find the consecutive $1$s by searching a bit more.
Nevertheless, we can prove that the function is computable as follows. Either there are arbitrarily long strings of $1$ in $\pi$ or there is a longest string of $1$s of some length $N$. In the former case, the function $f$ is the constant $1$ function, which is definitely computable. In the latter case, $f$ is the function with value $1$ for all input $n\lt N$ and value $0$ for $n\geq N$, which for any fixed $N$ is also a computable function.
So we have proved that $f$ is computable in effect by providing an infinite list of programs and proving that one of them computes $f$, but we don't know which one exactly. Indeed, I believe it is an open question of number theory which case is the right one. In this sense, this example has a resemblence to Gerhard's examples.

2$\begingroup$ There is a difference between "we do not know" and "there is no constructive proof". $\endgroup$ – Andrej Bauer Sep 24 '13 at 8:03

2$\begingroup$ Andrej, I agree with that. I had intended only to give an example where we have a proof of decidability, but we have no constructive proof, using the naturalmathematicallanguage meaning of this word, rather than the meaning arising in constructive logic. This is a softer interpretation of the question, but an interpretation that I believe the OP had intended. But you are right, to give an example where we can prove there is no constructive proof is another matter. $\endgroup$ – Joel David Hamkins Sep 26 '13 at 3:26

1$\begingroup$ I would expect that we can easily produce these latter kind of examples by design. For example, define a set using the excluded middle, in such a way that in classical logic, we can prove it is trivial and decidable, but for which because of the excluded middle there would be no constructive proof. $\endgroup$ – Joel David Hamkins Sep 26 '13 at 3:27

$\begingroup$ For example, fix an instance $p\vee\neg p$ of excluded middle that is not constructively provable, and let $A$ be the set of even numbers, in case $p$ holds and otherwise $A$ is the set of odd numbers. Classically, we can easily prove $A$ is decidable by splitting into cases depending on whether $p$ holds. But there can be no constructive proof of this, since it would have to settle $p\vee\neg p$. (But is this the kind of example that the OP is seeking?) $\endgroup$ – Joel David Hamkins Sep 26 '13 at 3:46

3$\begingroup$ For each program $p$, let $A_p$ be the set of programs that halt before $p$, if $p$ does halt, and otherwise nothing. Each $A_p$ is decidable, but there is no constructive proof. $\endgroup$ – Joel David Hamkins Sep 26 '13 at 11:11
The Robertson–Seymour theorem implies that every minorclosed family $F$ of finite graphs is decidable in time $O(n^3)$. However, it does not provide an explicit algorithm until one supplies an explicit finite list of forbidden minors that characterize $F$; the proof that such a list always exists is nonconstructive.
There is the standard example involving Fermat's Last Theorem, except that we now have a good idea what the set is. So let's replace it with "the smallest positive integer n which is a multiple of 4 and for which no Hadamard matrix of order n exists, or 1 if Hadamard matrices of all possible orders exist." This defines a singleton set, which is decidable. You could argue that in principle it is constructive, whereas I would argue that since we still don't know maximal determinants for small orders less than 100, you and your putative greatgrandchildren will not see a value for n, so you will have a hard time showing to me that a construction based on this definition exists, as there is no guarantee of termination of the construction.
Alternatively, any finite set which is arrived at by nonconstructive means (E.g. encodings of counterexamples to Frankl's unionclosed families conjecture, where the presumed proof that there are only finitely many is nonconstructive) should count as an example.
Better answers will arise once a good notion of nonconstructive has been specified. As to such a notion, I'll leave the philosophical wrangling to others.
Gerhard "Ask Me About System Design" Paseman, 2010.02.10

$\begingroup$ To whom it may concern: What was the reason for downvoting? $\endgroup$ – HansPeter Stricker Feb 11 '10 at 9:32

1$\begingroup$ I too would like to know. It would help to know what about the answer detracts from knowledge surrounding the answer. $\endgroup$ – Gerhard Paseman Feb 15 '10 at 6:50
Assume your set $A\subseteq\mathbb{N}$ is decidable, that is, $\forall_n (n\in A\vee n\not\in A)$. Markov's Principle ensures that your set is computable. As it is computable, it can be described by a $\Pi_2^0$Formula, and this is provable in Peano Arithmetic. Therefore, using the FriedmanTranslation, you'll find a constructive proof of its decidability from Heyting Arithmetic.
So much for the sets with decidability provable from Peano Arithmetic. There are of course things like Goodstein's Theorem, on which this Theorem might not be applicable. In this case, you have to specify which stronger constructive System you want. But probably, similar theorems also hold then.


$\begingroup$ IIRC, there is a similar theorem for set theory and $\Sigma_3$formulas. $\endgroup$ – Kaveh Apr 11 '16 at 23:13
Indeed, there exists some mathematical theorems with nonconstructive proofs which cannot have any constructive proof (now and ever). Here is an example:
Definition. Let $\boldsymbol\varphi_1,\boldsymbol\varphi_2,\boldsymbol\varphi_3,\cdots$ be a list of all unary partial computable functions (from $\mathbb{N}$ to $\mathbb{N}$). Denote the ChaitinKolmogorov Complexity by $\mathcal{C}$ which is defined by $\mathcal{C}(n)=\min \{e\mid\boldsymbol\varphi_e(0)\!\downarrow = n\}$.
Let us note that $\mathcal{C}$ is a total function ($\mathcal{C}:\mathbb{N}\rightarrow\mathbb{N}$).
The following theorem has a nonconstructive proof:
Theorem 1. For every natural $n$ there exists some $m$ such that $\mathcal{C}(m)\!>\!n$. That is $\forall y \exists x \mathcal{C}(x)\!>\!y$.
Proof: For each $i\leqslant n$ put $\alpha_i=\boldsymbol\varphi_i(0)$ if the value exists, i.e., $\boldsymbol\varphi_i(0)\!\downarrow$; otherwise let $\alpha_i=0$. Take $m$ to be any natural number greater than all $\alpha_i$'s. $\texttt{QED}$
As a matter of fact, the above theorem cannot have any constructive proof:
Theorem 2. There exists no computable function $f$ such that for every natural $n$ one has $\mathcal{C}\big(f(n)\big)\!>\!n$.
Proof: If there were such a computable (and total) $f$ then by Kleene's Recursion (aka Fixedpoint) Theorem there would exist some $\mathbf{e}$ such that $\boldsymbol\varphi_{\mathbf{e}}(0)=f(\mathbf{e})$. For this $\mathbf{e}$ then we would have $\mathcal{C}\big(f(\mathbf{e})\big)\leqslant\mathbf{e}$ contradicting the assumption of $\forall n: \mathcal{C}\big(f(n)\big)\!>\!n$. $\texttt{QED}$
Now, we have an example of a decidable set whose decidability cannot be proven constructively:
Let $\mathfrak{B}=\{n\in\mathbb{N}\mid \exists m: \mathcal{C}(m)>n\}$. We know that $\mathfrak{B}$ is decidable just because $\mathfrak{B}=\mathbb{N}$. But if anyone (now or in future) can have any constructive proof of its decidability, s/he should be able to compute the characteristic function $\chi_{\mathfrak{B}}$ of $\mathfrak{B}$ (defined by $\chi_{\mathfrak{B}}(x)=0$ if $x\not\in\mathfrak{B}$ and $\chi_{\mathfrak{B}}(x)=1$ if $x\in\mathfrak{B}$). That would amount to showing that $\chi_{\mathfrak{B}}=\mathbf{1}$ the constant function $1$. Thus any constructive proof of the decidability of $\mathfrak{B}$ would show (constructively) that $\mathfrak{B}=\mathbb{N}$ and thus would provide a computable function $f$ such that $\forall n\!\in\!\mathbb{N}: \mathcal{C}\big(f(n)\big)\!>\!n$; contradicting Theorem 2.
So, I believe, $\mathfrak{B}$ is a decidable set such that no proof of its decidability can be constructive.
FIVE NOTES ON THE APPLICATION OF PROOF THEORY TO COMPUTER SCIENCE by Georg Kreisel, p. 32. Kreisel notes, that his set "is recursive by (the mere fact of) decidability and recursive enumerability of the theorems of any formal system. There is no apparent way of refining [this] brutal definition."
There are lots of theories in model theory that can be proven to be decidable, in a nonconstructive manner, by showing that a first order theory exhibits categoricity. One example that comes to mind the the theory of countable densely ordered fields (via Cantor's nonconstructive proof that they are all isomorphic).
If one considers a decidable theory in stated in a a countable language, one can obtain a decidable set of numbers it corresponds to using Gödel numbering; ie, $\{\ \overline{\phi} \ \ T \vdash \phi\}$. If the proof that the theory was nonconstructive, then the decidability of the corresponding set of Gödel will also be nonconstructive.

1$\begingroup$ Can you point me to this proof of Cantor's, or describe the idea. It feels to me like this could be made constructive. $\endgroup$ – Andrej Bauer Sep 24 '13 at 8:01

$\begingroup$ Any ordered field has characteristic $0$, and so the ordering is dense (because $(a+b)/2$ is between $a$ and $b$). But there are lots of nonisomorphic, countable ordered fields (for example, the rationals and a countable elementary submodel of the reals). $\endgroup$ – Andreas Blass Sep 26 '13 at 14:28

2$\begingroup$ I disagree with the last sentence of this answer. A nonconstructive proof does not preclude the possibility of another, constructive proof. $\endgroup$ – Andreas Blass Sep 26 '13 at 14:30