# How does undecidability of 'theoremhood' imply that human ingenuity is necessary in mathematics?

In Robert Stoll's "Set Theory and Logic", there is the following passage on effectiveness of theorems (p. 375) :

Mathematical logicians have shown that for many interesting axiomatic theories the notion of theorem is not effective. We emphasize that this means the nonexistence of effective procedures for "theoremhood" has been proved for some theories and not merely the nondiscovery to date of effective procedures. It follows that human inventiveness and ingenuity is necessary in mathematics.

This seems to imply that human inventiveness/ingenuity can accomplish something which can not be accomplished by a machine, due to the impossibility of an effective procedure for deciding "theoremhood".

However, if for a certain theory, a human could decide whether any given sentence is a theorem, then he/she should be able to provide a formal demonstration of that claim (otherwise the claim would have little value). Such a demonstration could take two forms :

1. If the sentence is a theorem, the demonstration would simply be its proof. But if such proof exists, a machine can easily accomplish the same, simply by recursively enumerating all possible proofs of the theory.

2. If the sentence is in fact not a theorem, the demonstration would have to be expressed as a proof $P_M$ in some metalanguage - with supposedly a richer set of axioms, if formalized, than the subject theory at hand - which would allow it to show that no proof $P_S$ in the subject theory exists for the theorem. But by the same argument as in 1, if this metalanguage and its axioms are formalized, a machine can find $P_M$ by enumerating all the possible proofs in this richer language.

So, in all cases a machine accomplishes whatever a human is able to accomplish. What then is the advantage of human inventiveness/ingenuity?

-
The advantages would seem to be obvious. They are saying that no "algorithms" for producing proofs exist in some theories - in other words, there is no "brute-force" alternative to human reason and creativity. In practice, this has proved to be painfully true. For instance, read about ( arxiv.org/abs/1309.4501 )Timothy Gowers' problem solver. Written by two of the most brilliant people in the world, and... well... let's just say that it can't do much. –  NotNotLogical Apr 24 '14 at 1:19
@NotNotLogical: When you say "two of the most brilliant people in the world", what is your definition of "brilliant"? Is it "mathematician" or "academic" or is it wide enough to include sufficiently many people outside the circles of academia and mathematics? –  Asaf Karagila Apr 24 '14 at 1:23
@AsafKaragila Um... I guess I didn't have anything specific in mind. I was just pointing out that even prominent mathematicians can't get theorem provers to do much that is interesting... –  NotNotLogical Apr 24 '14 at 1:27
I think that it is a dangerous task to extrapolate philosophical conclusion from mathematical results. Take G's 2nd Incompl.Th: the original proof is half page long; an "informal" formalization of it (see Hilbert & Bernays or Toutlakis' book) needs about 100 pages. G's was "human inventiveness and ingenuity". "But if such proof exists, a machine can easily accomplish the same, simply by recursively enumerating all possible proofs of the theory." I do not know, but there exist a theorem-builder able to "produce" f-o arithmetical theorems? If so, have it already produced G's theorems? –  Mauro ALLEGRANZA Apr 26 '14 at 10:27

But humans live in the physical world. We are bound by time and resources that ideal Turing machines don't. Well, not quite exactly, but almost.

Even if you can recursively enumerate all the proofs, if you cannot effectively decide whether or not something is a theorem, then you will have to live forever in order to be sure that it is not a theorem. Since you can never tell whether or not the next proof is the proof you seek.

On the other hand, if a theory is decidable, then it is true we might not live to see the computation finish in finding our proof, but there is a proof that it will definitely stop at some point to tell us whether or not the sentence is a theorem or not. This means that if we manage to keep the machine running sufficiently long we will be certain whether or not we found a theorem or not; whereas in the undecidable case we will just have to live forever before we find out.

Human ingenuity is an oracle, sort of anyway, that allows us to transcend that issue of bounded time, and find a proof anyway. But since we have no guarantee that a recursive enumeration will find this proof within our lifetime, the Sun's remaining billions of years, or even the time remaining until the decay of the last proton in the universe, this method is not feasible for us.

Perhaps in the future we will tap to the Infinity Gems and the Power Cosmic and this will allow us to run infinite calculations immediately. In that case, you're right. If you can recursively enumerate all the proofs, then you can use a machine (and these awesome new powers of humankind) to find out whether or not something is a theorem or not a theorem.

I wouldn't place a large amount of money on that happening, not within our lifetime, anyway.

-
It should be noted that Feynman had a finite algorithm for solving any problem; but that algorithm is only recursive in the presence of the human ingenuity oracle. –  Asaf Karagila Apr 24 '14 at 1:20
The passage I quoted almost seemed to imply that if there was an effective procedure for deciding theorems, human ingenuity wouldn't be needed - which is obviously not the case since that 'effective procedure' could take trillions of years for all we know, whereas a human might take a couple of minutes. So I assumed it was talking purely theoretically - and so my question was whether there are any theoretical advantages of human inventiveness over machines, ignoring any practical resource and time bounds (lifespan, etc.). –  Tim Apr 24 '14 at 5:23
And given that idealization, for the case where something is not a theorem, if no machine can prove that claim, then neither can any human! Because any formalized demonstration that a human comes up with, can itself be gotten by a recursive enumeration by some machine. –  Tim Apr 24 '14 at 5:24

To put it simply, no matter how many techniques you know, there will always be some theorem that will require a new technique to be able to solve it. Machines cannot come up with the new technique, otherwise following the machine itself would be a universal procedure that finds a proof for all provable theorems. But we know that there is no such procedure (if we want to be able to prove theorems involving arithmetic) because it can be used to solve the Halting Problem. Therefore only non-mechanical entities can possibly be able to prove arbitrary theorems involving arithmetic. Note that there are algorithms to prove theorems in restricted formal systems that are unable to express the standard arithmetic.

-