Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

The Completeness Theorem (in one of its equivalent forms) says that every consistent first-order theory has a model, linking syntax and semantics. It doesn't tell you any thing about how you would go about justifying that a theory is consistent.

People hoped that some logical system capable of formalizing real mathematics would be able to justify its own consistency. Godel's Incompleteness Theorem (and stronger, related results) imply that any system capable of formalizing real mathematics (or even a very weak subset of it) can not justify its own consistency, requiring an appeal to a stronger system. Obviously, that raises the obvious question of why that stronger system is consistent. There are constructive proofs (due to Godel himself, Gentzen, and others) of the consistency of Peano Arithmetic, but by the Incompleteness Theorem they must all be non-finitary in some fashion, no matter how slight.

However, there are some limits to this understanding of Godel's Incompleteness Theorem. There are theories that are strong enough to prove (and perhaps more importantly, state) their own consistency but not strong enough to formalize diagonalization. If PA is consistent, then there is a theory that can state and prove its own consistency as well as the consistency of PA. The trick is that provability can be formalized on the basis that subtraction and division are total functions, whereas diagonalization requires addition and multiplication to be total functions. These theories can prove that subtraction and division are total functions, but not addition and multiplication.



Consider applying for YC's Fall 2026 batch! Applications are open till July 27.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: