I found this pdf while searching on automated theorem provers:


It says:

"Proof by rote algorithm

Non-proof courses in mathematics generally teach algorithms to do calculations. It would be nice if there was an algorithm to find proofs of theorems. No such luck. There are algorithms to look for proofs of theorems, but it is a theorem (!) that no algorithm can find a proof of every provable theorem. You deserve to see plenty of examples of proof strategies, but you will also need creative thinking."

What exactly is the theorem it is referring to? Where can I learn deep about it? Thanks

  • 1
    $\begingroup$ Actually, there is an algorithm to find a proof of every provable theorem. It is not very efficient. $\endgroup$
    – bof
    Commented Nov 14, 2014 at 6:39
  • $\begingroup$ @bof OK, that's obviously not what the OP's instructor meant, and mentioning it may lead to confusion. $\endgroup$ Commented Nov 14, 2014 at 6:41
  • $\begingroup$ Distorted versions of undecidability results are common. $\endgroup$ Commented Nov 14, 2014 at 6:43
  • $\begingroup$ That's what it means to say that the set of (provable) theorems, and the set of proofs, are recursively enumerable sets. Likewise the set of non-proofs is recursively enumerable. The hitch is that the set of unprovable statements is not recursively enumerable. $\endgroup$
    – bof
    Commented Nov 14, 2014 at 6:46
  • $\begingroup$ Well, OK, yes, the instructor should say there's no algorithm to find a proof of every true theorem. But this objection relies on the technical definition of "provable," no? $\endgroup$ Commented Nov 14, 2014 at 6:58

2 Answers 2


This is essentially Gödel's first incompleteness theorem. To learn deeply about it is liable to be a long journey-better to start small. There are many references on the Wikipedia article, and a particularly famous book partly on the subject which is beautiful, moderately rigorous, basically accurate, but not overwhelmingly technical is Gödel, Escher, Bach: an Eternal Golden Braid by Douglas Hofstadter. The more technical route would be to begin studying proof theory, which I have never done, so I will forebear from offering references.


Start with a set $S$ that is your axioma as a set of theorems.

Construct a new set of theorems $U$ as:

  • for each pair of theorems in $S$ as $s_1$ and $s_2$ (or however many your logic's rules of inference demands)
  • for each rule of inference $I$ in your logic
  • let $T = I(s_1, s_2)$ and add $T$ to $U$

then $U$ is all the the theorems that can be inferred in $1$ "step" from $S$. Add $U$ to $S$, and repeat. This is a simple breadth first search of logic. This defines what theorems are provable and is completely constructive.

If you use this procedure to search for a theorem that is provable or disprovable, then obviously it will terminate. If you use it to search for a theorem that is undecidable (neither provable nor disprovable) then it will not terminate.

So that raises two questions: (1) Do such undecidable theorems exist and (2) If they exist, can we just run another algorithm and determine if a theorem is undecidable?

The answer to (1) is "sort of". If a logic's set of axioms is consistent and nontrivial, then the "Godel Sentence" gives and example of a theorem which must be undecidable; so in that case the answer to (1) is "yes".

The answer to (2) is that if such an algorithm existed, the algorithm itself could be used as an axiom to (in a fairly contrived way) to assign "true" and "false" to undecidable theorems and add those assignments to the axioma while maintaining the consistency of the axioma. Such an algorithm would allow you to construct a complete and consistent logic, which would contradict (1) and the demonstrable existence of the Godel Sentence.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .