Infinite mathematics as non-standard finite mathematics? I have in mind something like the following:

Start with some suitable version of "finite" mathematics. Some possibilities might be maybe ZFC with a suitable anti-infinity axiom, the topos $\mathbf{FinSet}$, Peano arithmetic, Turing machines... something whose objects are suitably "finite".
Then, posit the existence of both a standard and a non-standard model.
Now, in this setting, where we have access both to a standard model and a non-standard extension, use the non-standard objects as proxies for infinite objects (e.g. maybe some sort of set theory that has a set of natural numbers), and develop ordinary mathematics this way.

Has anybody worked on such a thing? Does anyone know of references of it being done? Or suggestions that it can't work out?
(P.S. I wasn't sure how to tag this....)

Edit: After more thought and reviewing the answers thus far, I think I can state an example of the sort of thing i was imagining. Define a first-order theory with two types $T_1$ and $T_2$, two binary relation symbols $\in_1, \in_2$ (one for each sort), and a map $\tau : T_1 \to T_2$ satisfying:


*

*$(T_1, \in_1)$ satisfies the axioms of finite set theory

*$(T_2, \in_2)$ satisfies the axioms of finite set theory

*$\tau$ is injective

*$\tau$ is not surjective

*$\tau$ satisfies an axiom schema that says it's an elementary embedding


and the question is to what extent we can develop infinite set theory in this theory.
 A: You might want to look into the work of Vopenka and his collaborators on what they call alternative set theory.  The formal theory looks a bit strange, since it allows proper classes to be subclasses of sets, but one interpretation of the theory is that the sets are the internal sets of a nonstandard model of finite-set-theory while the classes are arbitrary (not necessarily internal) subsets.  There's a small book, "Mathematics in the Alternative Set Theory," by Vopenka, that should serve as a good introduction to the subject.
A: Update: I looked a bit more into it.  It seems that IST is still a system of ZFC, and therefore infinite.  So this isn't what you are looking for.
I'm not positive, but I think this is similar to Nelson's internal set theory.  There is an AMS Bulletin article (Internal set theory: A new approach to nonstandard analysis) on it that I have been meaning to read.  Again, I haven't read it so I am not certain.
While you wanted all of mathematics, Nelson also has a treatment of probability theory (Radically Elementary Probability Theory), which I believe works by starting with finite probability theory and gets infinite probability theory through nonstandard models.  (Again, this is on my to-read list, so I am not certain.)
A: For another route to the phenomenon, consider the following theorem of Ressayre, which has always both fascinated and mystified me. Indeed, I find the conclusion a bit alarming and perhaps even bizarre, precisely because it seems to be a too-strong fulfillment of your requested phenomenon.
Theorem. If ${\cal M}=\langle M,\hat\in\rangle$ is a nonstandard model of finite set theory, such as the natural model arising from a nonstandard model of PA, and if $T$ is any consistent computably axiomatizable extension of ZF, such as ZFC or ZFC+$\exists$ supercompact cardinal, then there is a submodel $N\subset M$ such that ${\cal N}=\langle N,\hat\in\rangle$ is a model of $T$. 
That is, even though $\cal M$ is a model of finite set theory, it has a substructure realizing the infinitary theory of ZFC or much more. In this way, the theorem fulfills your request, since we are enabled to find within the nonstandard finite part of the model a fully accurate copy of the infinitary set theory. The amazing thing, to me, is that we can do so in such a flexible way so as to realize large cardinals or any other consistent set theory.
Ali Enayat explains some of the details in his answer to Mirco Mannucci's question Set theory inside arithmetics via the Ackerman yoga, citing J. P. Ressayre, Introduction aux modèles récursivement saturés, Séminaire Général de Logique 1983–1984 (Paris, 1983–1984), 53–72, Publ. Math. Univ. Paris VII, 27, Univ. Paris VII, Paris, 1986. 

Update (11/20/2012). 
My paper Every countable model of set theory embeds into its own constructible universe contains the following strengthening of Ressayre's theorem:
Theorem. If ${\cal M}$ is any nonstandard model of PA, then every countable model of set theory is isomorphic to a submodel of $\langle\text{HF}^{\cal M},{\in}^{\cal M}\rangle$. Indeed, this structure is universal for all countable acyclic binary relations. 
Here, $\text{HF}$ refers to the natural model of finite set theory defined inside $\cal M$, the hereditary finite sets as coded in $\cal M$. The relation $\in^{\cal M}$ is the Ackerman relation, so that $n\in^{\cal M} m$ just in case the $n$ th bit in the binary expansion of $m$ is $1$.
This theorem eliminates the role of the theory $T$ in Ressayre's theorem, for not only do we get merely at least one model of $T$ as a submodel of $\cal M$, but indeed every countable model of $T$ arises as a submodel. 
The point now---and the reason I look upon this as relevant for your question---is that any given countable model of ZFC, even one satisfying a very strong theory, can be found as a submodel of any given nonstandard  model of the strictly finitary theory $\text{ZFC}^{\neg\infty}$, which thinks every set is finite. So this is exactly a situation where we have an entire universe of infinite mathematics arising precisely as a form of nonstandard finite mathematics.
A: The standard system of a first-order model of Peano Arithmetic works in this way.
The standard model $\mathbb{N}$ is an initial segment of every nonstandard model $\mathcal{M}$. Pick a nonstandard element $w$ of $\mathcal{M}$. The binary expansion of numbers in $\mathcal{M}$ below $2^w$ define nonstandard binary strings of length $w$. For each such $x$, there corresponds a subset $X$ of $\mathbb{N}$ where a standard number $n$ belongs to $X$ if and only if the $n$-th bit of $x$ is $1$. The collection of all these sets $X$ is called the standard system $\mathrm{SSy}(\mathcal{M})$ of $\mathcal{M}$. This standard system is always a Scott set, so it can be used to form a standard model of second-order arithmetic where the weak König lemma is true. The structure of the first-order model $\mathcal{M}$ dictates a lot of the properties of this second-order model.
Similar constructions can be done in different contexts, but this is surely the most common one.
