Algorithm to find a proof of every provable theorem.

Question

I found this pdf while searching on automated theorem provers:

https://www.math.ucdavis.edu/~greg/145/notproof.pdf

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

Answer 1

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.

Answer 2

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.