Timeline for Is Kolmogorov complexity (KC) relevant for proof theory? [closed]
Current License: CC BY-SA 3.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 25, 2014 at 13:31 | comment | added | usul | E.g. consider a theorem of the form "For all $x$ there exists $y$". A constructive proof actually produces a $y$ from any given $x$, i.e. is an algorithm. If this algorithm runs in polynomial time, then surely the theorem is very simple. If it can produce a certificate that it has produced a valid $y$, and this certificate may be checked in polynomial time, then surely the theorem is not too complicated. (For a concrete example, a proof of Brouwer might construct a fixpoint. I can probably not do so in polynomial time, but the fact that my fixpoint is correct can be checked in polytime.) | |
| Jan 25, 2014 at 13:14 | comment | added | usul | I think a better measure for proof theory would actually be time and space complexity, in the computational sense. In the KC sense, a description of just $k$ bits can produce a $BB(k)$-length string (busy beaver function). So perhaps there is "order", but it is very hard to work with. On the other hand, if you can make a time-complexity statement, this may be a much more reasonable measure of regularity or simplicity. | |
| Jan 25, 2014 at 11:58 | review | Reopen votes | |||
| Jan 26, 2014 at 2:44 | |||||
| Jan 25, 2014 at 11:51 | history | edited | Armando Matos | CC BY-SA 3.0 |
added 156 characters in body; edited title
|
| Jan 25, 2014 at 11:38 | history | edited | Armando Matos | CC BY-SA 3.0 |
added 156 characters in body; edited title
|
| Jan 25, 2014 at 10:48 | comment | added | Sh.M1972 | why are you sure that such a TM exists? | |
| Jan 25, 2014 at 0:17 | history | closed |
Ricardo Andrade Noah Schweber Stefan Kohl♦ Andrey Rekalo Qiaochu Yuan |
Needs details or clarity | |
| Jan 24, 2014 at 19:50 | answer | added | Sam Nead | timeline score: 2 | |
| Jan 24, 2014 at 19:31 | comment | added | Sam Nead | Would you say that the digits of $\pi$ are "very regular, structured, and compressible"? After all, the first $n$ digits of $\pi$ have Kolmogorov complexity at most $\log(n) + c$. I guess they compress pretty well, but they don't look regular to me... Perhaps what makes your thesis unsatisfying is that you don't measure the other resources required to run the program that finds the proof. | |
| Jan 24, 2014 at 18:37 | comment | added | Noah Schweber | What exactly is the question here? (Also, Henry's comment is spot-on.) | |
| Jan 24, 2014 at 16:18 | review | Close votes | |||
| Jan 25, 2014 at 0:22 | |||||
| Jan 24, 2014 at 13:55 | comment | added | Henry Cohn | This is why people don't use Kolmogorov complexity to measure proof length: it's not very meaningful to compress a proof of the classification of finite simple groups all the way down to essentially saying "it's the shortest proof of the classification of finite simple groups". I wouldn't interpret Kolmogorov complexity as "bits of inspiration", though, since almost all these bits are just stating the theorem and describing the formal proof system. All you need is one bit of inspiration: if you know there is a proof, then you can definitely find it by brute force if you search long enough. | |
| Jan 24, 2014 at 13:24 | comment | added | Emil Jeřábek | The technical part is correct, but I disagree with the interpretation. The fact that a proof can be (in principle) found by exhaustive search does not make it in any way regular or structured. | |
| Jan 24, 2014 at 13:22 | comment | added | Joel David Hamkins | Very interesting observation! | |
| Jan 24, 2014 at 12:50 | history | asked | Armando Matos | CC BY-SA 3.0 |