Let's construct a theory of analysis of real numbers in the following manner:
I first define the superstructure over the reals as follows:
Let S(0) = R.
Then, let S(n+1) = S(n) U P(S(n))
That is, at each step I add in all subsets of what I've seen so far, so S(1) consists of the real numbers and all sets containing just real numbers, S(2) consists of the real numbers, and all sets containing just real numbers or sets of real numbers, et cetera.
Then I let S be the union of all of the S(n).
Inuitively, S simply consists of all the sets we would ever need to use when doing real analysis.
Now, I'll define a theory of real analysis as follows:
To define the language, we will take the usual symbols of first-order logic, whatever variable symbols we like, and each element of S gets its own constant symbol, and we will also use the symbol \in for the set membership operation. Furthermore, we will only allow bound quantifiers. IOW, we can say things like \forall A \in B: P(A), but we cannot say \forall A: P(A).
The axioms of the theory will simply be every true statement one can make in the above language.
Now, we can do all sorts of ugly logic tricks to this, but this is the easiest way to explain it:
Consider the collection of statements:
0 < x
x < 1
x < 1/2
x < 1/4
x < 1/8
x < 1/16
...
As it turns out, in the above theory, you cannot prove that there does not exist an x satisfying all of these inequalities. (To prove that there is no x requires we take an external viewpoint) (In generally, first-order logic is only capable of talking about fintely many statements... there's the compactness theorem that says if any finite subset of statements is internally consistent, then the entire infinite collection of statements is internally consistent)
So, this means that there must be some model of the above theory in which all of the axioms of the above theory are true, and this collection of statements is true! If we use this model, then we have (externally) proven that this model contains an infinitessimal number. (There's a cool theorem that says any consistent collection of statements has a model)
There are lots of ways to go about actually "constructing" such a model, and you can get many inequivalent models. The sets of numbers in these models that corresponds to the reals are called hyperreals, but often one particular canonical construction is used, and its hyperrals are called the hyperreals.
