In my career I've been formed mostly in the formal side of mathematics, that is, standard set theory and every classical branch of mathematics that uses set theory.
However, I am not quite sure about the common "rules" that are accepted in meta-math and, more specifically, in the foundations of mathematics.
I have several questions, but all of them are related to the nature of intuitive natural numbers.
I will start from the formal side, to explain my point, but I am really interested in the intuitive and metamathematical issues.
From the formal point of view, we have a "set" of natural numbers, $\mathbb N$, which can be obtained for example by the Von Neumann construction:
$$0 = \emptyset$$ $$1 = \{0\}$$ $$2 = \{0,1\}$$
and so on.
The existence of a set containing all these "formalized" natural numbers comes with the development of set theory. To be concrete, I will talk about ZFC.
However, ZFC has to be sustained in the first order logic, and both are formally expressed in the "language" of first order logic, which consists of a collection of symbols $\mathcal L = \{\wedge,\vee, \forall,\exists, ...\}$, and rules to form formulas with that symbols.
FIRST ISSUE. It is common to see in the books of logic that the collection $\mathcal L$ of symbols of the language is "finite". Moreover, the word "set" is used (I am using "collection" in order to not merge things of different contexts). The meaning of "finite" in the metamath context cannot be referring to any notion of "finite set" of ZFC, because this would be circular (the problem is that, if I am "constructing" set theory from "nothing", and the notion of "finite set" comes later, after some theory is done, I cannot talk about "finiteness" in the "ZFC sense"). So:
FIRST QUESTION. In what sense is it understood that the collection of symbols $\mathcal L$ (intended to construct first order logic) is considered "finite"? In what sense is it understood that the length of a formula of first order logic is finite? Is it implied by a previously accepted notion of intuitive natural number? Please, I need to know the standard point of view, and not opinions of a very personal kind.
SECOUND ISSUE. When methamath theorems are demonstrated, sometimes some "properties" of natural numbers are used, as for example the induction on the number of symbols in a given logical formula. Again, these properties are referring to the intuitive natural numbers.
SECOUND QUESTION. How can I be sure about what properties of natural numbers can be accepted or not, in the metamath context? Is there some kind of consensus about what intuitive properties of natural numbers can be used?
THIRD ISSUE. If a formal first order theory contains the Peano axioms, then on the semantic side there are a lot of non-standard models... However I am even more intrigued by the "standard model", which is, again, the intuitive natural numbers.
THIRD QUESTION. Are they actually a "model"? In order to prove that, what properties of intuitive natural numbers are commonly accepted as "true"?
FINAL QUESTION. Does there exist an agreement about what the intuitive natural numbers are and which of their properties are accepted and used in metamaths?
The usual answer (or dodge, depending on yuor philosophical position) is to talk about the intended model (more precisely, intended interpretation) of the natural numbers. If such a thing exists (and many mathematicians do believe it exists, including the constructivist Errett Bishop), then one can interpret references to "finite" at the meta-level as referring to things equinumerable with individuals in the intended model. If you don't want to believe in an intended model then you also have to give up hope of an absolutely rigorous development of mathematics "from scratch". Whether or not you actually lose anything in the process again depends on your philosophical position. Kronecker, by the way, never expressed any opinion on the matter in writing. Whatever is reported in his name is hearsay based on Weber (who certainly made a mistake when he mentioned "whole numbers" rather than "natural numbers").
Juat out of curiosity, I looked up "intended interpretation" on wiki, and was led to the following comment:
Intended interpretations. Many formal languages are associated with a particular interpretation that is used to motivate them. For example, the first-order signature for set theory includes only one binary relation, ∈, which is intended to represent set membership, and the domain of discourse in a first-order theory of the natural numbers is intended to be the set of natural numbers. The intended interpretation is called the standard model (a term introduced by Abraham Robinson in 1960).[8]
Note the definite article, which I guess begs the question (namely, yours). Here the reference is to the paper
Roland Müller (2009). "The Notion of a Model". In Anthonie Meijers. Philosophy of technology and engineering sciences. Handbook of the Philosophy of Science 9. Elsevier. ISBN 978-0-444-51667-1
which you may find useful (though I hasten to admit that I never read it). If you gain some insights do let me know.
The book that the article is in can be found here.
For a related question see What are natural numbers? where you will also find an accepted answer containing a passionate defense of the intended interpretation without mentioning the term ("categorical" and all).
For a detailed discussion of the intended interpretation see this post.
George Reeb's position was that the naive counting numbers do not exhaust $\mathbb N$; see this post for a bit of a discussion and this article for more details.