Why is it impossible nowadays for a computer to derive all the possible theorems that flow from a particular formal system?

Question

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.

Answer 1

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, unless such schema elements are explicitly written in a non-schema format, with whatever length 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.

Answer 2

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.