3 ms·
Would 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
by johncolanduoni 8y ago
Would 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.