3 ms·

>> "...random points in theorem-space..." Question: Given an arbitrary powerful computer, is the nature of mathematics such that in principle we could exhaust

by avn2109 11y ago

>> "...random points in theorem-space..." Question: Given an arbitrary powerful computer, is the nature of mathematics such that in principle we could exhaust the points in theorem space by brute force? E.g. is there in principle a finite amount of math?

andreyf 11y ago
The theorem space is infinite. The theorem space that is learnable in a single human lifetime is probably finite, but we are not anywhere near having explored it.
chei0aiV 11y ago
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.
noamyoungerm 11y ago
This is the type of question that quickly runs into problems wrt incompleteness, but there are a few key points that show that there are infinitely many theorems For any given statement P and any given theorem T, P OR T is a theorem, meaning you can generate infinitely many theorems from one. More worryingly, there are infinitely many theorems that are true but impossible to prove. From Gödel's first incompleteness theorem, we know at least one such theorem must exist. Any theorem of the form Unprovable AND TRUE can be proved only if you can prove the unprovable theorem. From a more general perspective, it's worth remembering that theorems can always be described as a finitely-long string of symbols in some formal logic system, and so running out of theorems to try and prove is like running out of strings.
- grkvlt 11y ago
  Since each theorem has a Gödel-number, there must be a function f(x) -> {0,1} where, when x is the number of an 'interesting' theorem, f(x) is 1, and otherwise it is 0. So, we just need to find this function (or rather, its Gödel number) and then we can iteratively feed all the integers to it, translating the interesting ones back into theorems. This job is made much easier by the fact that the proof of this 'interestingness' theorem has a Gödel-number of its own; call it F. And, proving that something is interesting is obviously also interesting. So, just find the situation where: f(F) = 1 and we're done! I'll collect my Fields medal later, thanks.
  - JadeNB 11y ago
    Your condition `f(F) = 1` doesn't seem to do anything to distinguish your meta-theorem `F` from any other interesting theorem.
  - digama 11y ago
    You just defined a subset of the natural numbers, and asserted it has a Godel number. Sorry, there are uncountably many subsets of natural numbers and countably many Godel numbers, so there is no guarantee that this is possible. More subtly, you can consider many "natural" classes of functions, such as computable functions, recursively enumerable functions, etc. and for each such enumeration there will be a "natural" function that escapes the class. Functions to do with definability or (in this case) 'interestingness' are especially susceptible to this. See also "Tarski's theorem on the undefinability of truth".

by avn2109 11y ago

andreyf 11y ago

The theorem space is infinite. The theorem space that is learnable in a single human lifetime is probably finite, but we are not anywhere near having explored it.

chei0aiV 11y ago

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.

noamyoungerm 11y ago

This is the type of question that quickly runs into problems wrt incompleteness, but there are a few key points that show that there are infinitely many theorems For any given statement P and any given theorem T, P OR T is a theorem, meaning you can generate infinitely many theorems from one. More worryingly, there are infinitely many theorems that are true but impossible to prove. From Gödel's first incompleteness theorem, we know at least one such theorem must exist. Any theorem of the form Unprovable AND TRUE can be proved only if you can prove the unprovable theorem. From a more general perspective, it's worth remembering that theorems can always be described as a finitely-long string of symbols in some formal logic system, and so running out of theorems to try and prove is like running out of strings.

grkvlt 11y ago
Since each theorem has a Gödel-number, there must be a function f(x) -> {0,1} where, when x is the number of an 'interesting' theorem, f(x) is 1, and otherwise it is 0. So, we just need to find this function (or rather, its Gödel number) and then we can iteratively feed all the integers to it, translating the interesting ones back into theorems. This job is made much easier by the fact that the proof of this 'interestingness' theorem has a Gödel-number of its own; call it F. And, proving that something is interesting is obviously also interesting. So, just find the situation where: f(F) = 1 and we're done! I'll collect my Fields medal later, thanks.
- JadeNB 11y ago
  Your condition `f(F) = 1` doesn't seem to do anything to distinguish your meta-theorem `F` from any other interesting theorem.
- digama 11y ago
  You just defined a subset of the natural numbers, and asserted it has a Godel number. Sorry, there are uncountably many subsets of natural numbers and countably many Godel numbers, so there is no guarantee that this is possible. More subtly, you can consider many "natural" classes of functions, such as computable functions, recursively enumerable functions, etc. and for each such enumeration there will be a "natural" function that escapes the class. Functions to do with definability or (in this case) 'interestingness' are especially susceptible to this. See also "Tarski's theorem on the undefinability of truth".