6 ms·
No system is powerful enough to prove all of the facts about natural numbers, right?
by gepoch 6y ago
No system is powerful enough to prove all of the facts about natural numbers, right?
- Tainnor 6y agoI think that this is correct and a consequence of Gödel's incompleteness theorems, although my knowledge about this is quite sketchy. What I was referring to more (and should have clarified better) was that there are models of arithmetic that can characterise the natural numbers uniquely (up to isomorphism) - translated to type theory, it is possible in languages like Coq and Lean to fully define what a natural number is without including any extra objects - even if you won't be able to prove all theorems about them. Notably, though, first order theories are not sufficient to define the natural numbers, for every set of first-order axioms about the natural numbers, there are "non-standard models" that can look quite weird. You need second-order logic or something equivalent in power to prevent that (the difficult axiom here is the axiom of induction which needs to be able to quantify over predicates).