We can define a notion of complexity for any given integer as being the size of the smallest program that returns that integer. Obviously, I'm being imprecise here, but it should hopefully be clear that it is possible to get the details right and the precise nature of those details aren't going to be relevant for what follows.
Now suppose we have a program that can find the complexity of a given integer. Then, we can write the following program:
for (i = 0; ; i++) {
if (complexity(i) > 2*K) {
return i;
}
}
(where K is the size of this program). Now we have a contradiction: we've constructed a program of size K that computes an integer i, but the smallest program that can do so is of size 2*K. This means that one of our assumptions is wrong, and the only one that can be wrong is that we could write a program that computes complexity.
As a result, we have some integer that has a complexity--it's still well-defined (at least if you have the axiom of choice, but I'm not sure if that axiom is necessary)--but we can't necessarily prove that any integer has a given complexity.
Any statement that can be made from the Peano axioms that is provable in ZFC is provable in ZF without C. So the axiom of choice should be irrelevant.
However we can write a program that does a brute force search through all proofs from ZF looking for the complexity of i. As you just showed, this program will not establish the complexity of all integers.
But how does it fail? It fails because there are programs which do not halt, that it can't prove don't halt, which if they halted COULD return i.
And therefore the complexity cannot be determined from ZF.
The prevailing philosophy of mathematics says it is well-defined. But there are alternate (entirely consistent!) philosophies under which complexity is not well-defined at all.
I feel like I'm missing something here - wouldn't the shortest program that returns the integer i just be "return i"? The length of that seems pretty easy to compute.
We can define a notion of complexity for any given integer as being the size of the smallest program that returns that integer. Obviously, I'm being imprecise here, but it should hopefully be clear that it is possible to get the details right and the precise nature of those details aren't going to be relevant for what follows.
Now suppose we have a program that can find the complexity of a given integer. Then, we can write the following program:
(where K is the size of this program). Now we have a contradiction: we've constructed a program of size K that computes an integer i, but the smallest program that can do so is of size 2*K. This means that one of our assumptions is wrong, and the only one that can be wrong is that we could write a program that computes complexity.As a result, we have some integer that has a complexity--it's still well-defined (at least if you have the axiom of choice, but I'm not sure if that axiom is necessary)--but we can't necessarily prove that any integer has a given complexity.