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