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?