an outline of "intuitive mathematics"? This question is related to the third answer in this post. 
There seems to be a difference between the intuitive idea of a thing (such as a function) and "models" of that thing in mathematics (such as the way we view functions as being a kind of set of ordered pairs). Another instance of this is the natural numbers and the set-theoretic construction of the natural numbers. If our set theory does not have an axiom of infinity which allows us to define $\mathbb{N}$, then are we disallowed the use of induction? Or is induction something "we just believe" independent of any model? A concrete question that comes to mind is: if there was no axiom of infinity, could we prove the statement "If $X_1,\dots,X_n$ are sets, then there exists a set $\{X_1,\dots,X_n\}$"? (this is a statement that I believe requires induction and the axiom of infinity). Could "$X_1,\dots,X_n$" even be stated without the formal notion of $\mathbb{N}$?
My questions are this: 
1) Do the formal models, such as set theory, actually justify "intuitive mathematics"? My feeling is that they don't. I take the numbers $0,1,2,\dots$ and induction for granted (conceptually prior to set theory).
2) If not, then why is the formality of set theory often used as justification for "intuitive mathematics"? For example, you might see authors explaining induction by mentioning the inductive set, which is kind of irrelevant if induction is something we just take for granted.
3) Are there textbooks or documents which attempt to outline what constitutes "intuitive mathematics" without appealing to models or the formality of set theory?
I guess I'm interested in understanding "what comes first". What should we all take for granted? What is the metatheory (is this the right word?)?
 A: There is no way to "prove" or "justify" one's intuition. What you can do, is view properties that you would expect something to have, and check to see that the "set theoretic" construction agrees with them (with proof.) Similarly, I think that you can take a construction that you find "intuitive" and prove that it is equivalent to a more "formal," or "different" approach." In some sense, you could make your intuition precise, and frame it in mathematical terms, and then prove its equivalence to a more formal definition.
I think that this is a good example.
Alternatively, one might feel that the one of the three constructions of $\mathbb{R}$ are intuitive, and prove them equivalent to the other two:


*

*The completion of all Cauchy sequences in $\mathbb{Q}$.

*Construction by Dedekind Cuts

*Define $\mathbb{R}$ to be an Ordered Field with the Least Upper Bound Property.
Poincare has some nice views on intuition/logic in mathematics: Poincare on intuition.
Here is a brief quotation:  
And then," say the philosophers, "it still remains to show that the object which corresponds to this definition is indeed the same made known to you by intuition; or else that some real and concrete object whose conformity with your intuitive idea you believe you immediately recognize corresponds to your new definition. Only then could you affirm that it has the property in question. You have only displaced the difficulty."
That is not exactly so; the difficulty has not been displaced, it has been divided. The proposition to be established was in reality composed of two different truths, at first not distinguished. The first was a mathematical truth, and it is now rigorously established. The second was an experimental verity. Experience alone can teach us that some real and concrete object corresponds or does not correspond to some abstract definition. This second verity is not mathematically demonstrated, but neither can it be, no more than can the empirical laws of the physical and natural sciences. It would be unreasonable to ask more."
Perhaps you would also be interested in intuitionsim, as developed by Brouwer.
A: "Intuitive maths" isn't a model in and of its own, it is a convenient abstraction over formal models which are essentially meaningless outside said field.
1) Not "intuition", which isn't well-defined, but intuitive maths is often simply thought of as an abstraction, which is valid.
2) Because it allows justifying some intuition. Essentially, it is used to "convince" the reader.
3) Most text books on Axiomatic Set Theory or Foundations of mathematics will introduce various concepts ("abstractions") allowing for a more intuitive mind model.
If we want to look away from set theory, type theory is perhaps closer to intuition, and might be worth reading about.
A: To answer your question "Do formal models justify intuitive mathematics?" I would answer that it is just the opposite: intuitive mathematics justify the formal models.  In physics it is rather clear that the bottom line is the physical phenomena and the theories physicists develop are ultimately justified only to the extent they seem to fit with the former.  In the 1950s after a fruitful career both in mathematics and in physics, Hermann Weyl came to what to him was a startling conclusion that in mathematics things are ultimately very similar: our formal theories are merely bold idealisations rather than having a life of their own.  Not all mathematicians subscribe to this view; an opinion popular among some set theorists and also mathematicians is that there is something called an "Intended Interpretation" that is the "foundation" of our mathematics; for more on this see this thread.
A: Induction still works in the absence of the axiom of infinity. 
Without AxInf, you still have $0 = \emptyset, 1 = \{0\}$, $2 = \{0, 1\}$, etc.
For a set $X$, if we define the the successor of $X$ to be $X \cup \{X\}$, then every set has a successor. In short, we have a collection whose members are exactly $0, 1, 2, 3, \dots$ This collection is not a set, but we can still do induction. The collection of natural numbers is still well-ordered, and they satisfy the Peano axioms.
See Andrés E. Caicedo's answer to this question. What are the consequences if Axiom of Infinity is negated?. In particular, "ZFC with infinity replaced by its negation is biinterpretable with PA, Peano Arithmetic." 
A: "If our set theory does not have an axiom of infinity which allows us to define N, then are we disallowed the use of induction?"
Sometimes, the inductive step of an inductive proof can get defined something like the following: 
For any n, if P(n) holds, then P(S(n)) holds, where S(n) indicates the successor of n in the sequence.
Suppose that you can do induction with a finite set validly, such as a sequence A.  Then you could show that by supposing P(n) you can deduce that P(S(n)) holds.  But, A has a last member, and thus P(S(n)) has no meaning when n is the last member of A.  Consequently, we can't validly show that for any, if P(n) holds, then P(S(n)).
That said though, I suppose you might reformulate the principle of mathematical induction as something like:
For any n, if S(n) exists, then if P(n) holds, then P(S(n)) holds.
"Or is induction something "we just believe" independent of any model?"
I won't proclaim to speak for others beliefs here.  But, I don't believe in induction if say talking about the set of fuzzy numbers, or the set of interval numbers.  So, no, I don't believe it independent of any model.
"A concrete question that comes to mind is: if there was no axiom of infinity, could we prove the statement "If X1,…,Xn are sets, then there exists a set {X1,…,Xn}"
Consider a n-ary operation that for any sequence of sets it takes all of the members of that sequence to {X1, ..., Xn}.  So long as such an n-ary operation exists, there thus exists a set {X1, ..., Xn}.
