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

Question

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?

Answer 1

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.

Answer 2

To put it simply, no matter how many facts you know, there will always be some fact that will require a new assumption to be able to prove it. Machines cannot come up with the new axiom, otherwise following the machine itself would be a universal procedure that finds a proof for all facts. But we know that there is no such procedure (that proves only true arithmetical statements) because it can be used to solve the Halting Problem. Therefore only non-mechanical entities can possibly be able to prove arbitrary facts involving arithmetic. Note that there are algorithms to prove theorems in specific formal systems (such as PA or ZFC) that are unable to pin down the standard arithmetic (standard model of PA). To be precise, if the formal system interprets PA but does not prove $0=1$, then it also does not prove some true arithmetical sentence.

To be clear, this does not imply that humans can prove arbitrary facts about arithmetic. What humans do is that they rely on intuition (which may be wrong) to tell them whether or not to accept some new axiom that they are believe to be independent over their initial formal system. Just for example, if one believes their original system S to be (arithmetically) consistent (i.e. does not prove $0=1$), then one also believes Con(S) to be true, but one must also believe that S cannot prove Con(S). So what can one do? Accept Con(S) as true by faith...

Answer 3

The statement you quoted is absurd. What does he think is happening in the brain?

Mathematicians don't look at propositions like Goldbach's conjecture and say "by the power of Graymatter, I perceive this to be true" and then move on to the next one. What mathematicians do is prove theorems. Not a prescribed sequence of theorems, but whatever they can manage to prove, and whatever seems interesting.

We have no evidence to support the idea that the output of all human mathematicians so far is in any way superior to the output of a randomized search algorithm with a similar "interestingness" heuristic.

The fact that we, collectively as a species, have not managed to write a good enough heuristic yet is frankly embarrassing, given that our brains originated from a natural process that might be described as "iterated brute stupidity". I don't see our failure to understand our own brains as a sign of their marvelous superiority to algorithms, but as an example of our inability to grasp anything that has any level of actual complexity.

We have no reason to believe that any of our breakthroughs in M-theory would rise above the level of obvious trivialities to any alien beings that we may someday meet if we don't destroy ourselves. All we know is that it's the best we've managed to do so far.

I don't think that human beings are very good at mathematics, but we're good at hubris.