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?
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.Sign up to join this community
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.