2
$\begingroup$

Lets assume the proof of a conjecture, for example, the famous Goldbach conjecture. Is it possible to try to prove or disprove such a conjecture by devising a Turing machine that accepts if the proof is possible. So, for Turing machine M,

If, the conjecture is provable, accept, else reject.

So, in essence, we don't try to find a proof of the conjecture, but, try to find whether its provable, something like zero-knowledge proofs.

Additional Details: I felt the way most of these conjectures go, is they say: For all n, C holds true. So, in essence, even if it can be shown that C holds up to some n, but, it hasn't been able to be derived for all n. And, this seems to bear a striking similarity to the Halting problem. So, I felt a mapping must be worthwhile to study/research.

$\endgroup$
  • 1
    $\begingroup$ A) It's not clear to me if achieving this goal would help anyway... (is proving that $P$ is provable as hard as proving $P$?). B) My own instinct is the TM approach is very unlikely to help, because we know that in general reasoning about TMs/halting/accepting/rejecting is hard. So you need to encode a lot of the structure of your problem into the algorithm somehow (compare to a universal prover that searches for the proof/disproof of any given theorem...we can show nothing about this). C) Perhaps a good question is "Are there any known cases of this technique working?" $\endgroup$ – usul Feb 16 '14 at 8:13
  • 2
    $\begingroup$ to me this is highly worthwhile/meaningful research & actually have done exactly this re collatz conjecture, but there is no immediate chance of success because even small TMs can barely be analyzed by existing "technology"... it would have to be seen as a very longterm research program; there are other very longterm type programs in CS eg "geometric complexity theory". but it requires an inspiring leader to trigger those types of efforts... would like to answer your question with refs but am gonna hold off until there are votes, which suspect will very likely not materialize =( $\endgroup$ – vzn Feb 16 '14 at 15:39
  • 1
    $\begingroup$ hi user1951547, "progress" is extremely limited in this area due to it being a very hard unified/crosscutting theory/challenge spanning both deep TCS/math. closest line of research is prob on busy beavers with some modest results so far & [continuing] work in that area. am planning on writing a blog on it with the collected refs & scattered se questions on subj/line of research also. after you earn 20pt rep somewhere on se can Theoretical Computer Science Chat about it further. $\endgroup$ – vzn Feb 16 '14 at 17:53
  • 1
    $\begingroup$ @vzn Straw man is where you misrepresent a point in order to attack it. I was disagreeing with your "many great examples of this from theoretical math/TCS & in many ways this phenomenon lies at the heart of progress": hyperbole all yours, no need for me to exaggerate or misrepresent you. Most progress isn't from "bridge theorems", and the big results don't originate on SE. I'm not claiming it's off topic, it's just you seemed to feel the question is on the brink of some great discovery, but I really didn't get that impression, and was pointing out that suchlike are usually hard fought for. $\endgroup$ – AndrewC Feb 17 '14 at 19:21
  • 3
    $\begingroup$ It may be worth OP's time to read this post by Terry Tao: plus.google.com/114134834346472219368/posts/cy6KB8TKMkA. Posing a problem in a new language is only useful if it opens a new perspective on the structure of the problem and/or gives access to powerful tools. TMs are general enough to "reduce" almost any statement to a statement about whether a particular TM halts. But I don't see how that is a useful reduction in either of the two senses above. $\endgroup$ – Sasho Nikolov Feb 18 '14 at 5:18
6
$\begingroup$

First, you don't need to turn them into Turing machines, it is essentially the same as running a proof search algorithm. The logical complexity of the formula (which in the cases you have in mind are $\Pi^0_1$) has no effect on this, searching for proofs in any effective theory (like ZFC, for proof to make sense you have to fix a theory) can be done in a straight forward manner, the set of provable statements for any effective theory is $\Sigma^0_1$ and therefore computable enumerable. But there are no reasons to do that, you don't gain anything a priori just by adding one extra unnecessary layer of coding, it has no benefit (AFAIK).

Also don't confuse proof search with a direct reduction from the truth of a $\Pi^0_1$ statement to the halting problem (which exists as not halting is $\Pi^0_1$-complete).

Second, consider the much simpler case of propositional tautologies in place of first-order statements like GC. (propositional tautologies is a coNP set also known as $\Pi^B_1$). The state of art proof search algorithms (i.e. SAT solvers) are exponentially inefficient in finding proofs of very simple finitary mathematical statements like the pigeon-hole principle tautologies. You can run a first-order proof search program to look for a ZFC proof of GC but I haven't seen any interesting mathematical statement being discovered/proven by unguided brute-force search of proofs. So there is no example of this being useful. (For human-guided use of computer in proving mathematical theorems we have the four colors theorem.)

Third, if you use a proof search algorithm you will only know if there is a proof, if there isn't any you will not know and the algorithm will continue forever without halting. In other words, you can't write a program like the one you have stated in the question (which is why I commented that this is more suitable for CS Q&A site since this is very basic mistake in computability theory).

See also my answers to similar questions on math and CS.

$\endgroup$
  • $\begingroup$ following se popular convention: in busy beaver research, which admittedly started out more as a "toy" type problem as in its whimsical naming, but which has significantly advanced over many years, there are many TMs that have been proven to be nonhalting, but for which these proofs have never been converted to any other proof systems in the literature. it is certainly true that equivalent proofs could be constructed in other proof systems. also, sometimes misc problems are solved via "bridge thms" etc $\endgroup$ – vzn Feb 19 '14 at 16:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.