8
$\begingroup$

I am just learning about formal systems and mathematical logic. It seems to me that it could be relatively easy to generate all the possible theorems that flow from a particular formal system (set of axioms, rules of inference, formal language). Formal system seems to me to be almost equivalent to the game of chess. You have some initial conditions (= axioms) like in the game of chess and you have some strict rules which allows you to derive new truths from those axioms. Why is it than so difficult to derive all the possible theorems (in chess I would say scenarios) from such a formal systems?

For example in a propositional logic, which is just a particular type of a formal system, it seems to be relatively easy to produce all the possible conclusions that flow from a particular set of premises by using some particular rules of inference.

Why is it than nowadays impossible to derive all the theorems from every formal system?

Please note that I'm just a beginner in formal systems.

|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ If the axioms are a recursively enumerable set, then we can generate automatically theorems. Butt their number is infinite: thus "to derive all" of them requires an infinite ampunt of time. $\endgroup$ – Mauro ALLEGRANZA Aug 26 '19 at 9:04
  • 1
    $\begingroup$ There are really two major problems. The first one, obviously, is time -- you could run your computer for a very long time and the number of actually-useful things it might stumble into proving would be very few. The other problem is that in some formal systems there might actually be uncountably many possible constructions, and so it would be literally impossible to iterate through them all. Automated theorem proving is an active field of research, though, and new developments are being made in this area all the time. $\endgroup$ – Jack Crawford Aug 26 '19 at 9:05
  • 7
    $\begingroup$ Start with the much simpler problem of chess (only twenty possibilities for the first move and no game is longer than 6000 moves) so that we know once and for all if it is a win for white .. $\endgroup$ – Hagen von Eitzen Aug 26 '19 at 9:08
  • 1
    $\begingroup$ So if I understand it properly, it is relatively easy to make a computer to derive theorems. The problem is that there is usually so much of the possible theorems that it would take ages for a computer to derive all the theorems. Am I saying it right? $\endgroup$ – TKN Aug 26 '19 at 9:08
  • 2
    $\begingroup$ There is a combinatorial explosion of possibilities. The number of possible ways to combine axioms together quickly becomes astronomical. We can't explore all possible chess games either. Chess engines do not work purely by brute force. Rather, they use heuristics or machine learning techniques to estimate the strengths of various positions, and explore only a tiny subset of the space of all possible games resulting from a given position. $\endgroup$ – littleO Aug 26 '19 at 9:10
2
$\begingroup$

Automated theorem proving is an area of research. Checking all proofs of length (counting symbols) $\le n$ takes exponential time. (A complication: if the theory has an axiom schema, in finite time we cannot explicitly generate all elements of each theorem schema as separate results.) The usual goal is not to find all theorems that thus result, but to check whether an interesting question can be settled in a proof of length $\le n$.

But this is an NP-complete problem, so is unlikely to have a polynomial solution, and the obvious way to solve it runs in exponential time too. Therefore, modern research looks into trying to prove efficiently, i.e. to search the space of proofs in a way that would hopefully find proofs in a manner more similar to human thought than the brute-force approach. ATP isn't necessarily still in its infancy, but it has a long way to go.

|cite|improve this answer
$\endgroup$
2
$\begingroup$

As was pointed out in the comments, for nice formal systems, you can in principle derive "all" theorems (in the sense that any theorem will come up in a finite amount of time) with a naïve algorithm.

There are a few problems with this approach :

  • The naïve algorithm is very (very very....) inefficient : you have to go through all proof trees of length $\leq n$; and there is an explosion of possibilities.

  • All in all you have infinitely many theorems so you will never get done : you will never have a finished list of theorems (in particular any given theorem can appear very very late, later than the survival of humans, which makes for a poor algorithm for practical purposes)

  • I think the most important point : the naïve algorithm cannot make a difference between theorems; any two theorems look alike to it. But us humans are interested in very specific theorems, and the amount of theorems we're interested in is probably ridiculous when compared to all theorems. That is, the naïve algorithm spits out tons of theorems of the form "$Q\implies (P\implies Q)$" for tons of already complex formulas $P,Q$, whereas we're not interested in them. And even more complex theorems we'd have to first decypher them in order to see if they're interesting : imagine the computer spits out a $160000$ character long theorem, written out in fully formalized form [note that usually our theorems can be short because we use abbreviations, abuse of notations, etc. that we understand among ourselves]; and you have to understand it to see if it's of any interest !

All these make a naïve approach such as "I have axioms and rules of inference so I can just use these to derive all theorems" untractable and most likely uninteresting. That's why there has to be a lot of work when trying to use computers to help us with proofs, to come up with clever solutions to the issues mentioned above.

Automated theorem proving, proof-assistants and related fields have come a long way, but still have a long way to go.

|cite|improve this answer
$\endgroup$

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.