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?
$\begingroup$
$\endgroup$
7
-
1$\begingroup$ Could you be more specific? A theorem in which kind of logical system? $\endgroup$– André Souza LemosCommented Apr 30, 2015 at 1:09
-
$\begingroup$ @AndréSouzaLemos As I know, in any "enough complex" logical system, but the perfect formulation is probably over my skills. $\endgroup$– peterhCommented Apr 30, 2015 at 1:20
-
2$\begingroup$ Automated theorem proving is possible in specific cases though. Coq allows for the construction of programs that are guaranteed to meet their specification. Google about C compilers and JavaScript compilers written in Coq. $\endgroup$– RobCommented Apr 30, 2015 at 1:25
-
$\begingroup$ Ok, but why do you want this question answered? $\endgroup$– André Souza LemosCommented Apr 30, 2015 at 1:26
-
1$\begingroup$ What happens is that the answer to this question, as it is, is encyclopedic. I suggest that you devote some time to study the problem, and then come up with a smaller question, one that can be answered in a more productive way, for you, and for others. $\endgroup$– André Souza LemosCommented Apr 30, 2015 at 1:41
|
Show 2 more comments
1 Answer
$\begingroup$
$\endgroup$
2
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.
-
$\begingroup$ I like this presentation which I find quite pedagogical. However, Gödel's incompleteness theorem has a minimal requirement that the theory must be able to express elementary arithmetic. Is'nt that even less than having a logic for Turing Machines? So, is this in some sense a weaker proof, not covering as much as Gödel's proof? $\endgroup$– babouCommented Apr 30, 2015 at 11:12
-
$\begingroup$ Correct. It's just nice and a near full treatment fits on a post. $\endgroup$– JakeCommented Apr 30, 2015 at 14:33