I think you’re right about practicality. Seems like nonstandard models of arithmetic suggest that there are things we cannot know about all natural numbers, because some of them (nearly all of them) are “too high to work with.” They are too high when all you can do with them is write proofs about them using induction.

There’s a sense in which the set of natural numbers is too big to be practically useful, but no smaller set makes sense when writing proofs. The set of numbers you can reach without using induction (say, by using a computer to check) isn’t well-defined.

And that has nothing to do with AI’s limitations.