Comment by wat10000

"This is a perfect valid axiom. And it does rule out the nonstandard shit"

But the other commenter said:

"Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up with a formal definition of natural numbers that includes the actual natural numbers but will also include other number systems that contain mathematical objects that are infinitely big and hence are not actual natural numbers."

Is there some subtlety that allows both of these statements to be true, or is this just a contradiction? Was the other commenter implicitly assuming "unless you involve second-order logic"?