You can always enumerate all theorems (i.e. all provable sentences of formal logic) by systematically applying rules of inference to axioms and previously obtai

You can always enumerate all theorems (i.e. all provable sentences of formal logic) by systematically applying rules of inference to axioms and previously obtained theorems. You only need axioms to be recursively enumerable. Though most theorems obtained this way are going to be dull tautologies like "every even number is even"; the hard part here is finding out which theorems are interesting. And it's prohibitively expensive computationally; in fact, it needs infinite memory to store all the previously obtained sentences.