[Solved]: Why is automated theorem proving impossible?

Problem Detail: 

As far I know, in general case there is no Turing machine which could get any theorem on its input and produce its proof on its output.

Why is it so?

Asked By : peterh

Answered By : Jake

We have to be carful here. I think you mean that a program given a formula could not, in general, produce a proof of it or its negation. I can write a program that, given a theorem, will produce it's proof as long as the set of proofs is recursively enumerable. This is not possible in general because of Godel's incompleteness theorem (well that was the first case we knew of). If everything that was true could be proved then we could write a program that enumerated all the proofs until it found the proof of the formula or its negation. However this is not the case as the incompleteness theorem points out. While Godel was the first to prove this was the case the halting problem gives us a nice simple proof that some things are not provable.

The argument goes like this:

Say you have a sound and complete logic for proving the termination of computer programs. The rules of the logic make the proofs recursively enumerable as well. If the logic wasn't sound we wouldn't have to worry about proving anything because false things are already provable; everything falls apart. If it wasn't complete (generally the case) then there would be a true thing that wasn't provable and thus neither you nor the computer could ever prove it. If The proofs were not recursively enumerable then there would be a proof that the program couldn't check to be valid or even reach and thus it couldn't prove the corresponding formula. Now consider the following program:

Given a program called pgrm foreach p in set of proofs //remember, proofs are recursively enumerable   if p is a proof that pgrm halts     output that pgrm halts   if p is a proof that pgrm loops     output that pgrm loops 

This program would solve the halting program however so one of our 3 assumptions must be wrong. In practice we work with what we think are sound systems of logic and we work with recursively enumerable sets of proofs as well.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/41982