The standard role of intuitive numbers in the foundations of mathematics 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?
 A: 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.
A: I will start by saying that I don't think there is exactly a "standard opinion" for all of these questions so I will give you what I have gathered from my logic professor and my readings.
I think it is important to understand that we assume ZFC axioms in order to do logic. Thus we already have definitions of finite when we start to define our first order logic. Likewise we can prove, from ZFC, that induction works on formulas works. I think this should hopefully clear up question 1 and 2.
For issue 3 I would like to note that the only reason that we have non-standard models is that the Peano axioms (specifically induction) are not fully expressible in the language of first order logic. Our best attempt at a first order formulation of the axioms is what has non-standard models.
For question three we have a similar situation to one and two. We are working within set theory when we do logic so the set of Von Neumann natural numbers does exist and is a very real model.
While I have addressed the issues regarding logic the question of whether there is a "standard intuitive notion of natural number" remains open. There is really no way for mathematicians to say for sure that they all have the same notion of natural number.
That being said, I think that almost every mathematician believes we share the same notion  of $\mathbb{N}$ (Likewise for reals and rationals and other things). This belief is mostly due to the fact that, as far as I know, there are not any properties of natural numbers that people disagree on.
This is not to say that there is an intuitive notion for all mathematical objects. When it comes to sets, some people still do not think that they have the choice property. Thus there are multiple intuitive notions of set.
Edit: Judging from the comments I need to give concrete evidence of the use of ZFC in logic proofs. The only one that I can think of off the top of my head is in my advisor’s paper on Dedekind-finite sets http://www.math.lsa.umich.edu/~ablass/ddiv.pdf Proposition 2.1 is a proposition about permutation models which explicitly uses the axiom of choice.
A: This question, besides intriguing, has been a waste of comments, answers and bounties.
Now that it's all over, allow me to throw in my 2 cents worth and enlighten a few more
issues, in an attempt to address the OP's issues and questions (again, second attempt), though with a twist.
The title alone is problematic already. Does there indeed exist a
standard role of intuitive numbers in the foundations of mathematics ?
If the answer would have been yes, then certainly there would have been sort of
consensus by several experts at the MSE forum here. But all of the comments and answers
indicate that there is no such role . Therefore let's cut the title in two pieces,
in order to get two more amenable questions:

the standard role of numbers in the foundations of mathematics
the role of intuitive numbers in the foundations of mathematics

The first version of the title, most probably, would have given rise to the Peano axioms,
or the von Neumann construction; all very standard. But the second version of the title
gives rise tot a non-standard answer, though not an "opinion of a very personal kind" either, which is my next point.

Intuitive natural numbers are defined as the very first thing in
Intuitionism . Quoted from this reference: The existence of the natural numbers is given
by the first act of intuitionism, that is by the perception of the movement
of time [ ... ]. Therefore intuitionism seems to be fine in its a priori
conception-without-axioms of the naturals, which hence may be truly called
intuitive numbers . However, the lack of the excluded third rule in intuionism
seems to be a major hurdle for the OP and is judged as nonsense by the major part of
mathematicians nowadays, as said below. Indeed: intuitionism is not standard. But I think
it does no harm if someone takes notice of the very first principles of intuitionism
- and eventually forget about the rest. (Inasmuch as reading the first few pages from
"Das Kapital" doesn't make someone a communist!) In a nutshell, we are left then with
intuitionism-without-the-trouble ("pink" intuitionism) / sort of naive constructivism
as uttered by Leopold Kronecker :
Die ganzen Zahlen hat der liebe Gott gemacht, alles andere ist Menschenwerk (rendered in English as: God made natural numbers; all else is the work of man).
So these must be the OP's intuitive numbers. I can't think of anything better.
A: For the first question, it depends on the context. When talking about strict foundations, finite would usually mean finite in the intuitive sense. This is rather important in this context – firstly it allows us to avoid (or postpone) ontological and intuitive pitfalls related to infinity, and secondly it allows us to encode everything using some Gödel numbering.
For second question, I believe Peano arithmetic is generally accepted, and sufficient for the proof of most basic foundational facts.
For the third question, I don't think there is much controversy about what a natural number is. A natural number is an object which can be obtained by adding $1$ to itself some finite number of times (though “finite” may be controversial). If the set of all natural numbers exists, it is certainly a model of any interesting theory of arithmetic: they are all approximations of what the natural numbers are like.
The last question is covered in the previous one, I think.
