- The Church-Turing theorem: No algorithm can be constructed to check, in a finite number of steps, whether a given formula in first-order logic is or is not provable in that system.
- Godel’s first incompleteness theorem (1931): Anything worth calling a formal system—so-called recursively axiomatizable—will have sentences in the language of the system that are not provable.
- Godel’s second incompleteness theorem: TBD
A system is considered consistent if it does not prove falsehoods. Conversely, an inconsistent system can prove any statement.