twanvl comments on Loebian cooperation, version 2 - Less Wrong

13 Post author: cousin_it 31 May 2012 06:41PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (25)

Comments (25)

You are viewing a single comment's thread. Show more comments above.

Comment author: twanvl 01 June 2012 12:21:39AM *  6 points [-]

Some comments:

The length of that proof grows with the number of symbols needed to represent the number N within program A

  1. Program A needs F(N), not on N itself. So it either needs to represent F in addition to N, or just F(N). Since F is computable and therefore has a finite program, you can just include the whole thing.

  2. It is not at all evident that the length of the proof grows linearly or even polynomially with the length of the program A. This depends on the theory T, it might have a very inefficient way of denoting proofs.

Perhaps it would be easier to switch the roles of N and F(N), so you get

2) The formal theory T can prove the following statement in F(N) symbols or less: “For any program B, if the formal theory T can prove that A(B)=B(A) in N symbols or less, then A(B)=C”.

I am not sure if the corresponding variant of the bounded Löb's theorem holds, though.

the formal theory T can prove the following statement in 2*N symbols or less: "..."

The formal theory will need some additional symbols to tie everything together, so the total proof would need 2*N+K symbols, where hopefully K doesn't depend on N. This is ignoring point 2 above.

Comment author: cousin_it 01 June 2012 06:27:58AM *  1 point [-]

Twan, thanks for the detailed comments!

Program A needs F(N), not on N itself. So it either needs to represent F in addition to N, or just F(N). Since F is computable and therefore has a finite program, you can just include the whole thing.

Yes, the intended interpretation is that A represents F too, as do all statements that mention F. That's why in the bounded Lob's theorem the function L is stated to be computable.

It is not at all evident that the length of the proof grows linearly or even polynomially with the length of the program A. This depends on the theory T, it might have a very inefficient way of denoting proofs.

That's true. I guess I'll have to include that as an explicit assumption somehow.

I am not sure if the corresponding variant of the bounded Löb's theorem holds, though.

I think it doesn't hold. Actually it's a nice exercise for everyone to try coming up with alternate formulations of the bounded Lob's theorem, like switching around N and L(N), and see if they can be made to work. It's surprisingly tricky.

The formal theory will need some additional symbols to tie everything together, so the total proof would need 2*N+K symbols, where hopefully K doesn't depend on N.

That's true. Maybe it's easier and more general to just say the length of the total proof is a computable function of N, that way everything seems to work fine.

Powered by Reddit Powered by Reddit