metamath / metamath-book

Source of metamath book
Creative Commons Zero v1.0 Universal
45 stars 18 forks source link

State inconsistency limitation more precisely #229

Open david-a-wheeler opened 3 years ago

david-a-wheeler commented 3 years ago

The book says:

Goedel's incompleteness theorem showed that it is impossible to achieve absolute rigor in standard mathematics because. If mathematics is consistent, we will never know it, but must rely on faith. If mathematics is inconsistent, the best we can hope for is that some clever future mathematician will discover the inconsistency.

What Goedel proved is more subtle. As noted by Norman Megill, "A proof of consistency of PA is possible within a system stronger than PA such as ZFC, but Godel showed it's not possible within PA itself unless PA is inconsistent. If you are interested, see http://timothychow.net/consistent.pdf ".

We were trying to make things simple, but in this case I think we could be more precise without making it impossible to understand.

benjub commented 2 years ago

I think the current wording in Section 1.1.6 of the book (which is not exactly what you quote above: a chunk might have been lost in a copy-paste) can stay as is. It is indeed informal, but that whole part of the book is an informal exposition anyway, so I think this does not justify modifying posthumously Norm's words. Maybe one can add a footnote:

(free from contradiction).\footnote{
G\¨odel's second incompleteness theorem actually states that every recursively
axiomatizable formal system containing some basic arithmetic (for instance,
Robinson or Peano arithmetic) cannot prove its own consistency unless it is
inconsistent.}

(many of these terms require a precise definition, but this is not the purpose of this book).