2

If one looks at the directed graph of all theorems proved, let there be a vertex between statement A and B directional if A implies B, ideally it will connect results across different fields. Is there any existing system, by computer or not, dedicated in looking into how existing proved theorems imply some otherwise not proved statements? Can one get access to it?

user61606
  • 27
  • 1
    I don't have an answer to your question, but I can tell you that given a theorem, the problem of finding a proof to it is NP-complete. You might be interested in this podcast: http://www.multimedia.ethz.ch/speakers/pauli/2012/?doi=10.3930/ETHZ/AV-eee0b1ea-b95d-4eb8-abba-1ba21d818da3&autostart=false (I was at that conference, it was quite interesting and the speaker is really good) and this paper: http://www.math.ias.edu/~avi/PUBLICATIONS/MYPAPERS/GMW91/GMW91.pdf – Daniel Robert-Nicoud Feb 15 '13 at 22:42
  • Assuming a base theory of, say, ZFC, every theorem of ZFC implies every other theorem of ZFC. Do you want to use a weaker base theory (which would make your question the sort of thing studied in reverse mathematics) or do you want edges only for proofs of "A implies B" that are "simpler" in some sense that the simplest proof of B from scratch? – Trevor Wilson Feb 15 '13 at 23:58

1 Answers1

1

In an unsatisfying sense, there already exists software for automatically deducing consequences of existing theorems. Several automated theorem provers exist (see the list at Wikipedia), and I've used them in research from time to time.

But there is a catch: the vast majority of theorems are uninteresting. Running this software blindly will simply result in a gigantic list of uninteresting theorems.

Let me illustrate: When studying groups, Prover9 consistently gets bogged down in deducing a zillion theorems equivalent to the cancellation law or some other well-known identity. Here's one random example (where * denotes the binary operation, e denotes the identity and ' denotes $^{-1}$):

x * (y' * (z * u')) != e | w * (u * (z' * (y * x'))) = w.

which says $$\forall w \forall u \forall x \forall y \forall z \quad\quad xy^{-1}zu^{-1}=\mathrm{id} \implies wuz^{-1}yx^{-1}=w.$$ A human would recognize this as a consequence of the group identity $(xy)^{-1}=y^{-1}x^{-1}$ and regard it as uninteresting.

Automated theorem provers are also more-or-less stuck with first-order logic (at least, for the time being), which is an enormous limitation.

However I'd like to note that they can be useful too, particularly if you want to prove millions of micro-theorems, which would be too tedious to do by hand.

Douglas S. Stones
  • 21,079