Proof of Chain Rule using Nonstandard Analysis I am trying to make an introduction and make myself comfortable with the Nonstandard Analysis in order to gain intuition for derivatives and integration. I am trying to prove myself the famous Chain Rule for differentiation by using the principles of Nonstandard Analysis but I am stuck at somewhere and I am trying to understand where I am doing wrong.
Here is the procedure I am following.
We have two functions $x=f(t)$ and $y=g(x)$ hence $y=g(f(t))$ $f$ has derivative at $t$ and $g$ has derivative at $f(t)$.
As it is widely known, chain rule states that the derivate of $y$ with regards to $t$ is:
$\frac{dy}{dt} = g'(f(t))f'(t) = \frac{dy}{dx}\frac{dx}{dt}$
Now, I first write the slope equation of the $x=f(t)$ with regards to $t$:
$\frac{\Delta{x}}{\Delta{t}} = f'(t) + \epsilon$
Whre $\epsilon$ is an infitesimal. Now according to Increment Theorem, it is
$f(t + dt) - f(t) = \Delta{x} = f'(t)dt + \epsilon dt$ 
Where $dt = \Delta{t}$. So we can write the differential of x as $dx = f'(t)dt$.
Now I move to the $y=g(x)$ and apply the same methodology. The independent variable $t$ has increased by $dt$ which causes an infitesimal change $\Delta{x}$ in the dependent variable $x$, so the slope equation for $g(x) = g(f(t))$ at $x = f(t)$ is:
$\frac{\Delta{y}}{\Delta{x}} = g'(f(t)) + \delta$ 
Where $\delta$ is infinitesimal.
Applying Increment Theorem:
$g(f(t + dt)) - g(f(t)) = g(x + \Delta{x}) - g(x) = \Delta{y} = g'(f(t))\Delta{x} + \delta \Delta{x}$ 
Now I divide all sides of the above equation by $dt$ which is equal to $\Delta{t}$:
$\frac{\Delta{y}}{dt} = g'(f(t))\frac{\Delta{x}}{dt} + \delta \frac{\Delta{x}}{dt}$.
Taking the standard part of the above expression should yield the derivative we are looking for:
$st(\frac{\Delta{y}}{dt}) = st(g'(f(t))\frac{\Delta{x}}{dt}) + st(\delta \frac{\Delta{x}}{dt}) = g'(f(t))st(\frac{\Delta{x}}{dt}) + 0 = g'(f(t))f'(t)$
The line above actually completes the proof, but what I want is to express the equation in the form of $\frac{dy}{dx}\frac{dx}{dt}$ as well, since it is not a mere notation anymore in Nonstandard Analysis and all $dy, dx, dt$ have actual values attached to them. This where I run into a problem.
We know that it is $\frac{dx}{dt} = f'(t)$ already. But from the Increment theorem of $\Delta{y}$ it is $\Delta{y} = g'(f(t))\Delta{x} + \delta \Delta{x}$, so, the differential $dy$ is:
$dy = g'(f(t))\Delta{x}$ and $\frac{dy}{\Delta{x}}=g'(f(t))$.
Now I substitute both $g'(f(t))$ and $f'(t)$ with differential representations and it becomes:
$g'(f(t))f'(t) = \frac{dy}{\Delta{x}} \frac{dx}{dt}$
As you can see $\Delta{x}$ and $dx$ are different values and do not cancel each other out. So I cannot write the chain rule in the form of differentials. I think I am making a mistake in the procedure I am following but I cannot figure it out, so I turned here for help. What is incorrect here?
Thanks in advance.
 A: Instead of introducing $dx$ as $f'(x)dx$, I would work with $\Delta t$ and $\Delta x$ throughout.  This way one gets the relation $\frac{\Delta y}{\Delta t} = \frac{\Delta y}{\Delta x} \frac{\Delta x}{\Delta t}$.  Note that there is a technical point here that needs to be handled when $\Delta x$ vanishes (in which case one can't divide by it).  This is a relation among hyperreal quantities rather than real quantities, and is therefore not the chain rule yet.  It is only at this stage that I would apply the standard part function to the relation $\frac{\Delta y}{\Delta t} = \frac{\Delta y}{\Delta x} \frac{\Delta x}{\Delta t}$, so as to get the relation between the derivatives.
A: There's a much easier way to do this. You don't even need the increment theorem for it.
First, let's limit our focus to functions defined at the point $(0, 0)$. If we can prove the chain rule for $f_0$ and $g_0$ at $(0, 0)$, then we can prove it for any two functions $f$ and $g$ at any point $(t, y)$ by setting
$f_{0}=a\mapsto f\left(t+a\right)-f\left(t\right)$
and
$g_{0}=a\mapsto g\left(f\left(t\right)+a\right)-g\left(f\left(t\right)\right)$.
Second, let's think of functions as constrained sets of points. The antecedent of the chain rule postulates that there are two real numbers $\dot x, \dot y$, and a set of infinitessimal triples:
$\left(\Delta t, \Delta x, \Delta y\right)$
Constrained by:


*

*$\Delta t \neq 0$

*$\exists \epsilon_x\ \left(\Delta x = \left( \dot x+\epsilon_x \right)\Delta t\right)$

*$\exists \epsilon_y\ \left(\Delta y = \left( \dot y+\epsilon_y \right)\Delta x\right)$
(In other words: $\Delta y$ is approximately proportional to $\Delta x$, which in turn is approximately proportional to $\Delta t$. $\dot y$ and $\dot x$ are the respective proportionality constants.)
And the consequent claims that $\Delta t$ and $\Delta y$ are constrained by:
$\exists \epsilon_{xy}\ \left(\Delta y = \left( \dot x \dot y + \epsilon_{xy} \right)\Delta t\right)$
Assuming the antecedent, the consequent can be proven using substitution:
$\Delta y = \left(\dot y + \epsilon_y\right)\Delta x
= \left(\dot y + \epsilon_y\right)\left(\dot x + \epsilon_x\right)\Delta t
=
\left( \dot x\dot y + \epsilon_x\dot y + \epsilon_y\dot x + \epsilon_x \epsilon_y \right) \Delta t$
The existence of $\epsilon_{xy}$ is thus proven by constructing it as
$\epsilon_x\dot y + \epsilon_y\dot x + \epsilon_x \epsilon_y$.

Differentials don't really have a place in this. You don't need them. I think I see what you want them for: you want real numbers that characterize the relationships between $t$ and $x$; $x$ and $y$; $t$ and $y$. And you want to call these numbers $\frac{dx}{dt}$, $\frac{dy}{dx}$, $\frac{dy}{dt}$.
The thing is, there are already numbers for this purpose: $\dot x$, $\dot y$, $\dot x \dot y$. (aka $f^\prime(t)$, $g^\prime(f(t))$, $g^\prime(f(t))f^\prime(t)$.)
Furthermore, if $dt$, $dx$, $dy$ are just values, then
$\frac{dy}{dt}=\frac{dy}{dx}\frac{dx}{dt}$
is just a tautology. In order to express anything at all using that equation, you have to equivocate between $dy = \dot x \dot y dt$ and $dy = \dot y dx$, and you have to equivocate between $dx = \Delta x$ and $dx = \dot x dt$.
Differentials work when you only want to refer to one variable's dependence on one other variable.
