You don't define it. You list things that you want to be true of it. The Peano Axioms are examples. But no matter how long your list gets, it can always get lo

You don't define it. You list things that you want to be true of it. The Peano Axioms are examples. But no matter how long your list gets, it can always get longer. For example we can ask whether a particular polynomial has integer roots. See https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC#Number_theory https://en.wikipedia.org/wiki/List_of_statements_independent.... (It doesn't, but you can't prove that in ZFC.) Even so, there is always an, "...and so on." You never finish, because finite does not actually have a finite definition. Second order logic gets around it because you can say something that simultaneously implies all the things that you want to say about "finite" in one go. Such as, "All possible functions from itself to itself that are onto are also one-to-one." A first order model need not capture the full intent of this statement, because it does not contain all possible functions. As we can see when we look at a model from within other models. But when I look at what the second order idea of "all possible functions" actually means, I think we're just begging the question of what it means to be finite. The way that I think about it is that some things are finite. Some things are infinite. And some things on the boundary are not yet determined. But then again, I do have Constructivist sympathies. And this is not a point of view that most mathematicians are very sympathetic towards.