4 ms·
The axioms of the higher order theory of the natural numbers are not countable and consequently not computationally enumerable. For example, there are uncounta
by carlehewitt 8y ago
The axioms of the higher order theory of the natural numbers are not countable and consequently not computationally enumerable. For example, there are uncountable many instances of the higher order induction axiom. Consequently, there are axioms that are not expressible as the abstractions of finite strings, just as there are real numbers that are not expressible as the abstractions of finite strings.
But proof checking is still computationally decidable by a provably total higher order procedure. See the following: https://hal.archives-ouvertes.fr/hal-01566393 https://hal.archives-ouvertes.fr/hal-01566393
- johncolanduoni 8y agoWould you mind explaining how the system avoids proofs being a recursive set implying the axioms are recursive? I'm afraid I don't understand how you can invoke axioms that are not expressible via finite strings in a proof that is expressible in such a manner.
- carlehewitt 8y agoInstances of the induction axiom are uncountable for the higher order theory of the natural numbers, which obviously means that they cannot be enumerated using the natural numbers. However, it is very easy to use the induction axiom in proofs that are expressible using finite strings. Please see the article above published in HAL Archives.