Non-constructive proofs of decidability? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-20T03:16:48Z http://mathoverflow.net/feeds/question/14918 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/14918/non-constructive-proofs-of-decidability Non-constructive proofs of decidability? Hans Stricker 2010-02-10T17:12:21Z 2011-02-03T17:22:58Z <p>Are there examples of sets of natural numbers that are proven to be decidable but by non-constructive proofs only?</p> http://mathoverflow.net/questions/14918/non-constructive-proofs-of-decidability/14920#14920 Answer by Hans Stricker for Non-constructive proofs of decidability? Hans Stricker 2010-02-10T17:23:35Z 2010-02-10T17:23:35Z <p><a href="http://suppes-corpus.stanford.edu/techreports/IMSSS%5F182.pdf" rel="nofollow">FIVE NOTES ON THE APPLICATION OF PROOF THEORY TO COMPUTER SCIENCE</a> 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."</p> http://mathoverflow.net/questions/14918/non-constructive-proofs-of-decidability/14930#14930 Answer by Gerhard Paseman for Non-constructive proofs of decidability? Gerhard Paseman 2010-02-10T18:32:42Z 2010-02-10T18:32:42Z <p>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 great-grandchildren 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.</p> <p>Alternatively, any finite set which is arrived at by nonconstructive means (E.g. encodings of counterexamples to Frankl's union-closed families conjecture, where the presumed proof that there are only finitely many is nonconstructive) should count as an example.</p> <p>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.</p> <p>Gerhard "Ask Me About System Design" Paseman, 2010.02.10</p> http://mathoverflow.net/questions/14918/non-constructive-proofs-of-decidability/31097#31097 Answer by Matthew Wampler-Doty for Non-constructive proofs of decidability? Matthew Wampler-Doty 2010-07-08T18:24:19Z 2010-07-08T18:24:19Z <p>There are lots of theories in model theory that can be proven to be decidable, in a non-constructive manner, by showing that a first order theory exhibits <a href="http://en.wikipedia.org/wiki/Morley%2527s_categoricity_theorem" rel="nofollow">categoricity</a>. One example that comes to mind the the theory of countable densely ordered fields (via Cantor's non-constructive proof that they are all isomorphic).</p> <p>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 non-constructive, then the decidability of the corresponding set of Gödel will also be non-constructive.</p> http://mathoverflow.net/questions/14918/non-constructive-proofs-of-decidability/31111#31111 Answer by Joel David Hamkins for Non-constructive proofs of decidability? Joel David Hamkins 2010-07-08T20:24:55Z 2010-07-08T20:40:03Z <p>When I teach computability, I usually use the following example to illustrate the point. </p> <p>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? </p> <p>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.</p> <p>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. </p> <p>So we have proved that $f$ is computable in effect by providing an infinite list of programs and proving that <em>one</em> 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.</p> http://mathoverflow.net/questions/14918/non-constructive-proofs-of-decidability/54217#54217 Answer by Emil Jeřábek for Non-constructive proofs of decidability? Emil Jeřábek 2011-02-03T17:22:58Z 2011-02-03T17:22:58Z <p>The <a href="http://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem" rel="nofollow">Robertson–Seymour theorem</a> implies that every minor-closed 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 non-constructive.</p>