6

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

Martin Sleziak
  • 53,687
user162208
  • 61
  • 1
    Actually, there is an algorithm to find a proof of every provable theorem. It is not very efficient. – bof Nov 14 '14 at 06:39
  • @bof OK, that's obviously not what the OP's instructor meant, and mentioning it may lead to confusion. – Kevin Carlson Nov 14 '14 at 06:41
  • Distorted versions of undecidability results are common. – André Nicolas Nov 14 '14 at 06:43
  • 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. – bof Nov 14 '14 at 06:46
  • 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? – Kevin Carlson Nov 14 '14 at 06:58
  • @KevinCarlson But that's sort of the point - this is a field where technical precision is essential to make sure that the things one's stating are actually correct. I'm frankly more than a little surprised to see this sloppiness, given the instructor (who has a generally excellent reputation). – Steven Stadnicki Nov 14 '14 at 08:08
  • There is no terminating algorithm to assign "true", "false", or "undeciable" to every possible theorem. However, it is trivial to construct a terminating algorithm that determines whether a decidable statement is provable or not. It's just not possible to algorithmically determine whether a statement is decidable. – DanielV Nov 14 '14 at 09:06
  • @StevenStadnicki but this is from the syllabus on a course on introduction to pros, not a course on logic. So I'd say "this field" in this case is not, in fact, proof theory, and that in a situation where "provable" will never be defined, there's little harm to be done by such phrasing. You will observe the instructor did not, in fact, "state" the theorem at all. – Kevin Carlson Nov 14 '14 at 16:47

2 Answers2

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.

Kevin Carlson
  • 52,457
  • 4
  • 59
  • 113
1

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.

DanielV
  • 23,556