timtyler 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: cousin_it 31 July 2010 08:53:08AM *  2 points [-]

The proof checker checks proofs within some formal theory. The Godel sentence for the checker is certainly true and provable by us, given the consistency of that formal theory. (If the theory were inconsistent, the checker would be able to prove any sentence.) But this doesn't work as a proof within the theory! The theory cannot believe its own consistency (Godel's second incompleteness theorem), so the checker cannot assume it when checking proofs. So your argument doesn't actually give an example of a valid proof rejected by the checker.

Comment author: timtyler 31 July 2010 11:24:36AM *  0 points [-]

Let's say we are trying to prove statements within ZFC.

"ZFC can never prove this statement to be true"

...is one thing and...

"This proof checker can never prove this statement to be true"

...is another.

Neither can be proved by the specified proof checker - but the second statement can be proved by another, better proof checker - still working within ZFC - so it can be seen that it is true.

Comment author: Jonathan_Graehl 01 August 2010 07:49:29AM 2 points [-]

"proved by a proof checker" - huh?

Comment author: timtyler 01 August 2010 08:44:40AM -1 points [-]

"Asserted", "approved" - whatever.