We should be able to make the bounds smaller… Let a be small (in comparison to n), and let P be the proof of length n that “T can’t prove a falsehood in f(n) symbols” is true.
Then define R as above, except it searches through all proofs beginning with P, of length n+a. Then T can completely simulate the execution of R in slightly over (n+a)exp(a) symbols. Then the same reasoning would establish that we only need to take f(n) >> (n+a)exp(a) in order for the reasoning to work.
Not sure how large a should be. It might be a constant, but more likely it grows logarithmically with n (as it probably has to include the definition of n itself). Which would mean f(n) >> n^2.
If this argument works, we might be able to get even better bounds restrictions—maybe we restrict R to look at proofs starting with P, which then include the definition of n somewhere after. Or maybe R just looks at a single proof—the actual proof that R printing anything is impossible? That would reduce to f(n) >> n.
Or maybe R just looks at a single proof—the actual proof that R printing anything is impossible?
Yeah, if you want to make the bounds smaller, something like that might be the way to go. Paul Christiano described an explicit Loebian construction along these lines in an email on Apr 1, maybe you could repurpose that? I’m tired right now, so I guess I’ll stick with the overkill bound :-)
We should be able to make the bounds smaller… Let a be small (in comparison to n), and let P be the proof of length n that “T can’t prove a falsehood in f(n) symbols” is true.
Then define R as above, except it searches through all proofs beginning with P, of length n+a. Then T can completely simulate the execution of R in slightly over (n+a)exp(a) symbols. Then the same reasoning would establish that we only need to take f(n) >> (n+a)exp(a) in order for the reasoning to work.
Not sure how large a should be. It might be a constant, but more likely it grows logarithmically with n (as it probably has to include the definition of n itself). Which would mean f(n) >> n^2.
If this argument works, we might be able to get even better bounds restrictions—maybe we restrict R to look at proofs starting with P, which then include the definition of n somewhere after. Or maybe R just looks at a single proof—the actual proof that R printing anything is impossible? That would reduce to f(n) >> n.
Yeah, if you want to make the bounds smaller, something like that might be the way to go. Paul Christiano described an explicit Loebian construction along these lines in an email on Apr 1, maybe you could repurpose that? I’m tired right now, so I guess I’ll stick with the overkill bound :-)