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?

  • 1
    $\begingroup$ 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. $\endgroup$ – user142299 Apr 24 '14 at 1:19
  • $\begingroup$ @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? $\endgroup$ – Asaf Karagila Apr 24 '14 at 1:23
  • 3
    $\begingroup$ @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... $\endgroup$ – user142299 Apr 24 '14 at 1:27
  • 1
    $\begingroup$ 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? $\endgroup$ – Mauro ALLEGRANZA Apr 26 '14 at 10:27

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...


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.

  • 1
    $\begingroup$ 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. $\endgroup$ – Asaf Karagila Apr 24 '14 at 1:20
  • $\begingroup$ 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.). $\endgroup$ – Tim Apr 24 '14 at 5:23
  • $\begingroup$ 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. $\endgroup$ – Tim Apr 24 '14 at 5:24

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.

  • $\begingroup$ Your first sentence is absurd; the statement the asker quoted is merely referring to undecidable theories such as Th(N). Since no program can enumerate all and only true arithmetical sentences, when we find some sentence that is independent of our current foundational system (if our foundational system is consistent) we can choose to take it as an extra axiom without being able to prove it if we believe it to be true. If you are unfamiliar with the incompleteness theorems, learn them instead of posting false claims and downvoting better answers. $\endgroup$ – user21820 Oct 3 at 18:07
  • $\begingroup$ @user21820 I apologize for downvoting in annoyance. I regretted it after reading the answers more carefully, but the site won't let me retract my vote. I know what the incompleteness results say. The idea that they have any bearing on the potential for automation of what human mathematicians actually do has never been defensible. There will always be people who will defend it, just like there will always be people who will defend anything, but the arguments don't make sense and never have. A million pages have been written about this as you probably know. $\endgroup$ – benrg Oct 3 at 18:22
  • $\begingroup$ Yes, I know very well the pitfalls of attempting to infer much about the human mind from the incompleteness theorems, and that is why I was quite careful with what I said, especially my specification of "standard arithmetic" (as in "standard model of PA"). I of course won't claim that humans have some oracular ability to prove true arithmetical sentences, and it comes down to belief. However, that too is what sets mathematicians apart from a single well-defined formal system; they prove what they like and not just what the axioms they previously chose allow them to. Whether it's true or not. $\endgroup$ – user21820 Oct 4 at 3:24
  • $\begingroup$ That said, I can see possible misinterpretations of my original post (more than 4 years ago), so I have edited it to make clear what humans do. How do you find it now? After the edit, you can change your vote if you like. $\endgroup$ – user21820 Oct 4 at 3:39
  • 1
    $\begingroup$ I'm confused. You were annoyed by the quote in the question, so you've decided to downvote the two answers? $\endgroup$ – Asaf Karagila Oct 4 at 7:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.