red75 comments on AI cooperation in practice - Less Wrong

26 Post author: cousin_it 30 July 2010 04:21PM

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

Comments (157)

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

Comment author: Vladimir_Nesov 31 July 2010 10:37:40AM 2 points [-]

You don't specify the implementation of "proves(code, maxsteps)".

Nothing depends on the details of proof verifier, since it completely covers all proofs up to some length, a set of proofs which is completely defined by the logical language. The arguments of proves(-,-) determine its value (and it's even a primitive recursive function).

Comment author: red75 31 July 2010 04:31:16PM -1 points [-]

Enumeration order of proofs is not specified, so we can construct pathological prover, that reorders proofs such that all proofs of "main()==1" require more steps than maxsteps.

Comment author: Vladimir_Nesov 31 July 2010 04:32:55PM *  4 points [-]

You can't influence the length of a proof by placing it at a different position in some list of proofs. Parameter 'maxsteps' specifies the maximum length (or Gödel number) of the proofs that get checked, not the maximum number of steps performed by the proof checker algorithm.

Comment author: red75 31 July 2010 04:38:23PM 2 points [-]

Ouch. maxsteps means maxprooflenght. My inattention, sorry.