Vladimir_Nesov 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:14:29AM *  5 points [-]

Checking a proof in a recursively axiomatizable theory for correctness is decidable. The post topic programs only check proofs up to some length in, say, Peano arithmetic, which is recursively axiomatizable. Tarski's undefinability theorem is about complete theories of arithmetic.