- 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 theory is considered consistent if it does not prove falsehoods; for example, a theory is classically consistent if there is not a proof of a contradiction in classical logic from its axioms. Conversely, an inconsistent theory can prove any statement.