Eugine_Nier comments on Proofs, Implications, and Models - Less Wrong

58 Post author: Eliezer_Yudkowsky 30 October 2012 01:02PM

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

Comments (209)

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

Comment author: bryjnar 29 October 2012 12:03:35PM *  5 points [-]

Note that this notion of 'completeness' is not the one used in Gödel's incompleteness theorems.

Um, yes it is, I think. The incompleteness theorems tell you that there are statements that are true (semantically valid) but unprovable, and hence they provide a counterexample to "If X |=Y then X |- Y", i.e. the proof system is not complete.

EDIT: To all respondents: sorry, I was unclear. Yes, I do realise that FOL is complete, but the same notion of completeness generalises to different proof systems. The incompleteness theorems show that the proof system for Peano arithmetic is incomplete, in precisely this way

Comment author: Eugine_Nier 29 October 2012 08:27:48PM 4 points [-]

The simplest way to explain the difference, is that Gödel's completeness theorem applies to first order logic, whereas Gödel's incompleteness theorem applies to second order logic.

Comment author: bryjnar 29 October 2012 11:16:53PM 2 points [-]

Right.