V_V comments on PSA: Eugine_Nier evading ban? - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (68)
The halting property is semi-decidable: if a program halts, then you can always trivially prove that it halts, you just need run it. If a program does not halt, then sometimes you can prove that it doesn't halt, and sometimes you can't prove anything.
For any programming language, there exist a length such that you can compute the halting property for all programs shorter than that. At length L_max, there will be program Bad_0, which:
You can never prove that any string S has Kolmogorov complexity K if K > L_max, as it would imply that you proved that Bad_0 doesn't halt, or at least doesn't emit any symbol which is not a prefix of S.
Since there are only finitely many strings with complexity up to L_max, we can only compute Kolmogorov complexity, for finitely many strings.
If the language is Turing-complete I don't think this is possible. If you think that an arbitrary string S has complexity K, how can you prove that there exist no program shorter than K that computes S?
[retracted]