Many mathematicians, from Archimedes to Leibniz to Euler and beyond, made use of infinitesimals in their arguments. These were later replaced rigorously with limits, but many people still find it useful to think and derive with infinitesimals.
Unfortunately, in most informal setups the existence of infinitesimals is technically contradictory, so it can be difficult to grasp the means by which one fruitfully manipulates them. It would be useful to have an axiomatic framework with the following properties:
1. It is consistent.
2. The system acts as a good “intuition pump” for the real world. In particular, this entails that if you prove something in the system, then while it won’t necessarily be true in the real world, there should be a high probability that it’s morally true in the real world, i.e., with some extra assumptions it becomes true. It should also ideally entail that many of the proofs of Archimedes, et al., involving infinitesimals can be formulated as is (or close to “as is”).
“Smooth infinitesimal analysis” is one attempt to satisfy these conditions.
(This is a blogified version of the first part of an article I wrote here.)
Axioms and Logic
Consider the following axioms:
Axiom 1. is a set, 0 and 1 are elements of
and
and
are binary operations on
. The structure
is a commutative ring with unit.
Furthermore, we have that , but I don’t want to call
a field for a reason I’ll discuss in a moment.
Axiom 2. There is a transitive irreflexive relation on
. It satisfies
, and for all
,
, and
, we have
and (
and
.
It also satisfies , but I don’t want to call
total, for a reason I’ll discuss in a moment.
Axiom 3. For all there is a unique
such that
.
Axiom 4 [Kock-Lawvere Axiom]. Let . Then for all functions
from
to
, and all
, there is a unique
such that
.
After reading the Kock-Lawvere Axiom you are probably quite puzzled. In the first place, we can easily prove that : Let
. For a proof by contradiction, assume that
, then there is a
and if
equalled 0, we would have
.
For an alternate proof that : Again assume that
for a contradiction. Then
or
. In the first case,
, so
(since
is irreflexive). In the second case, we have
by adding
to both sides, and again
.
Now, if , then for any
, and any function
from
to
, we have
for all
. This contradicts the uniqueness of
. Therefore, the axioms presented so far are contradictory.
However, we have the following surprising fact.
Fact. There is a form of set theory (called a local set theory, or topos logic) which has its underlying logic restricted (to a logic called intuitionistic logic) under which Axioms 1 through 4 (and also the axioms to be presented later in this paper) taken together are consistent
Definition. Smooth Infinitesimal Analysis (SIA) is the system whose axioms are those sentences marked as Axioms in this paper and whose logic is that alluded to in the above fact.
References for this theorem are [Moerdijk-Reyes] and [Kock]. References for topos logic specifically are [Bell1] and [MacLane-Moerdijk].
Essentially, intuitionistic logic disallows proof by contradiction (which was used in both proofs that above) and its equivalent brother, the law of the excluded middle, which says that for any proposition
,
holds.
I won’t formally define intuitionistic logic or topos logic here as it would take too much space and there’s no real way to understand it except by seeing examples anyway. If you avoid proofs by contradiction and proofs using the law of the excluded middle (which usually come up in ways like: “Let . Then either
or
.”), you will be okay.
But before we go further we might ask, “what does this logic have to do with the real world anyway?” Possibly nothing, but recall that our goals above do not require that we work with “real” objects; just that we have a consistent system which will act as a good “intuition pump” about the real world. We are guaranteed that the system is consistent by a theorem; for the second condition each person will have to judge for themselves.
To conclude this section, it should now be clear why I didn’t want to call a field and
a total order:
Even though we have invertible), we can’t conclude from that that
invertible)), because the proof of the latter from the former uses the law of the excluded middle. Calling
a field would unduly give the impression that the latter is true.
For the rest of this blog entry I will generally work within SIA (except, obviously, when I announce new axioms or make remarks about SIA).
Single-Variable Calculus
An Important Lemma
This lemma is easy to prove, but because it is used over and over again, I’ll isolate it here:
Lemma [Microcancellation] Let . If for all
we have
, then
.
Proof.
Let be given by
. Then by the uniqueness condition of the Kock-Lawvere axiom, we have that
.
Basic Rules
Let be a function from
to
, and let
. We may define a function
from
to
as follows: for all
, let
. Then the Kock-Lawvere axiom tells us that there is a unique
so that
for all
. Thus, we have that for all functions
from
to
and all
, there is a unique
so that
for all
. We define
to be this
.
We thus have the following fundamental fact:
Proposition [Fundamental Fact about Derivatives]
For all , all
, and all
,
and furthermore, is the unique real number with that property.
Proposition Let ,
,
. Then:
1.
2.
3.
4. If for all ,
, then
.
5. .
Proof
I’ll prove 3 and 5 and leave the rest as exercises.
To prove 3: Let and
. Let
. Then
which, multiplying out and using , is equal to
On the other hand, we know that , so
Since was an arbitrary element of
, we may use microcancellation, and we obtain
.
To prove 5: Let and
. Then
Now, is in
(since
), so
As before, this gives us that is the derivative of
.
In order to do integration, let’s add the following axiom:
Axiom 5 For all there is a unique
such that
and
. We write
as
.
We can now derive the rules of integration in the usual way by inverting the rules of differentiation.
Deriving formulas for Arclength, etc.
I’d now like to derive the formula for the arclength of the graph of a function (say, from
to
). Because “arclength” isn’t formally defined, the strategy I’ll take is to make some reasonable assumptions that any notion of arclength should satisfy and work with them.
For this problem, and other problems which use geometric reasoning, it’s important to note that the Kock-Lawvere axiom can be stated in the following form:
Proposition [Microstraightness] If is any curve,
, and
, then the portion of the curve from
to
is straight.
Let be any function, and let
be the arclength of the graph of
from 0 to
. (That is,
is the function which we would like to determine.)
Let and
be arbitrary and consider
. It should be the length of the segment of
from
to
, as in the following figure.
Because of microstraightness, we know that the part of the graph of from
to
is a straight line. Furthermore, it is the hypotenuse of a right triangle with legs
and
. The length of
is
.
To determine the length of : Note that the height of
is
, so the height of
is
. On the other hand, the height of
is
, so the length of
is
.
The hypotenuse of a right triangle with legs of length 1 and is
. By scaling down, we see that the length of
is
.
So, we know that should be
. On the other hand,
. By microcancellation, we have that
. Since
, we have
Several other formulas can be derived using precisely the same technique. For example, suppose we want to know the surface area of revolution of . Furthermore, suppose we know that the surface area of a frustum of a cone with radii
and
and slant height
as in the figure below is
. (See below to eliminate this assumption.)
Then, let be the surface area of revolution of
from
to
about the
-axis. As before, consider
where
is arbitrary. This should be the surface area of the frustum obtained by rotating
about the
-axis. The slant height is the length of
, which we determined earlier was
. The two radii are
and
. Therefore,
which, multiplying out, becomes . As before,
is also equal to
, so
In a precisely analogous way, one may derive the formula for the volume of the solid of revolution of about the
-axis, the formula for the arclength of a curve
given in polar form, and show that the (signed) area under the curve
from
to
is
.
Above we assumed that we knew the surface area of a frustum of a cone. Finally, as an exercise, eliminate this assumption by deriving the formula for the surface area of a cone (from which the formula for the surface area of a frustum follows by an argument with similar triangles) as follows:
Fix a cone of slant height
and radius
. The cone
can be considered to be the graph of a function
from
to
revolved a full
radians around the
-axis.
Let be the area of the surface formed by revolving the graph of
from
to
only
radians around the
-axis.
Using a method similar to that above, determine that . This gives the surface area as
.
The Equation of a Catenary
In the above section, essentially the same method was used again and again to solve different problems. As an example of a different way to apply SIA in single-variable calculus, in this section I’ll outline how the equation of a catenary may be derived in it. The full derivation is in [Bell2].)
To do this, we’ll need the existence of functions ,
,
in
satisfying
,
,
,
and
. We get this from the following set of axioms.
Axiom (Scheme) 6. For every function
(in the real world), we assume we have a function
(in SIA). Furthermore, for any true identity constructed out of such functions, composition, and partial differentiation operators, we may take the corresponding statement in SIA to be an axiom. (“True” means true for the corresponding functions between cartesian products of
in the real world.)
(We can actually go further. For every manifold
in the real world, we may assume that there is a set
in SIA, and for every
function
we may assume that there is a function
in SIA, and we may assume that these functions satisfy all identities true of them in the real world. But I will not use these extra axioms in this article.)
Suppose that we have a flexible rope of constant weight per unit length suspended from two points
and
(see the figure below). We would like to find the function
such that the graph of
is the curve that the rope makes. (We will actually disregard the points
and
and consider
to be defined on all of
.)
Let be the tension in the rope at the point
. (Recall that the tension at a point in a rope in equilibrium is defined as follows: That point in the rope is being pulled by both sides of the rope with some force. Since the rope is in equilibrium, the magnitude of the two forces must be equal. The tension is that common magnitude.)
Let be the angle that the tangent to
makes with the positive
-axis. (That is,
is defined so that
). We suppose that we have chosen the origin so that
.
Let be the arclength of
from 0 to
.
Let and
be arbitrary. Consider the segment of the rope from
to
. This segment is in equilibrium under three forces:
1. A force of magnitude with direction
.
2. A force of magnitude with direction
.
3. A force of magnitude with direction
.
By resolving these forces horizontally and using microcancellation, one can show that the horizontal component of the tension (that is, ) is constant. Call the constant tension
.
By resolving these forces vertically and using microcancellation and the fact that , one can show that the vertical component of the tension (that is
) is
.
Finally, by combining the results of the previous two paragraphs and using the fact that and
, one can show that
satisfies the differential equation
, where
.
Solving differential equations symbolically is the same in SIA as it is classically, since no infinitesimals or limits are involved. In this case, the answer turns out to be
if we add the initial condition to our previously assumed initial condition
.
I’ll include a post on multivariable calculus later.
I don’t understand a word/character/symbol but it looks great!
I recently became very interested in smooth infinitesimal analysis, and found your article a useful guide when trying to understand some of the earlier works (Kock, Reyes-Moerdijk, etc.).
However, there is something that bothers me about this setup, and I wonder if you have any ideas on it. Specifically, the problem is Axiom 5. This axiomatizes the fundamental theorem of calculus! Is there no way to define an area function using infinitesimals, then show that its derivative is the original function?
I think the idea of taking as an axiom “every curve is made up of infinitesimally small line segments” a beautiful concept, but it seems to me to be giving up too much to also have to axiomatize the existence of an anti-derivative.
Do you know of any way to not have to take this as an axiom?
Hi Geoff,
I’m glad you liked the article and find the subject interesting!
Axiom 5 doesn’t really axiomatize the fundamental theorem of calculus, since all Axiom 5 says is that antiderivatives of functions exist. The fundamental theorem of calculus says something more: it says that not only do antiderivatives of (suitable) functions
exist, but that furthermore the function
giving the (signed) area under the graph of
from
to
is a specific example of an antiderivative. (Also, that all other antiderivatives are equal to
plus some constant.)
The notation is confusing though, because in Axiom 5, I said that antiderivatives of functions exist, and furthermore I denoted the antiderivative of
which takes the value
on input
by
. This could be confusing, because normally
is defined as a Riemann sum, which is the classical formalization of the “area” concept, and so with that notation, the statement that the derivative of
is
is indeed the fundamental theorem of calculus. But with the notation I used in this article, it’s just a definition.
As an aside, you can prove a version of the fundamental theorem of calculus in smooth infinitesimal analysis, in much the same way that you can find the area of a cone.
If you want to not take the existence of antiderivatives as an axiom, you might want to take a look at Bell’s book “A Primer on Smooth Infinitesimal Analysis,” which does a lot of stuff without that axiom, but in its place he assumes that if
and
then
.
Ah, of course you’re right. I think I was confused by the notation. Thanks for the quick reply.
I guess my next question would be: how does one define the “area under a curve” function? I assume we would like to do it without limits.
Now that I look over the above again, I notice that there’s something similar with the arc length function: you mention that it’s not formally defined, so instead work with what reasonable properties it should have. But there has to be some nice way to formally define these notions; perhaps I just need to get Bell’s book.
As a side note, I’m amazed by how much more elegant some of the proofs with smooth infinitesimal analysis are than with regular calculus. In particular, the proofs of the product and chain rules are so much nicer than their usual counterparts.
I definitely agree that the proofs in smooth infinitesimal analysis are much nicer than in classical calculus; that’s the main reason why I like it.
You define the “area under a curve” function in a similar way to arclength as follows: You show that, given
, there is a unique function
(to be interpreted as the area under the curve
from
to
such that: for all
,
and, if
is linear on
, then
is the appropriate value (i.e., the formula for the area of a trapezoid:
. You can then prove that there is a unique function
with these properties, and it’s
.
The way area is dealt with in smooth infinitesimal analysis (i.e., isolate some conditions that an area function must have, then prove there is a unique function satisfying those conditions) is not so different from what is done in the classical case. The problem is that it’s done over again for each problem type: that is, you use it once to determine the area of a cone, then once again to prove the fundamental theorem of calculus, etc.
If I understand your question right, you’re wondering if you can do it once and for all. That is, can you prove that there is a unique function assigning to subsets of, say,
an element of
satisfying the appropriate conditions. I don’t know, but I would guess that the answer is “no.” I would have to think some more about that (and probably learn some more first!). If you have any thoughts, let me know.
Can these notions be extended to the calculus of variations?
Robert, I wouldn’t call myself an expert, but yes: the fact that smooth infinitesimal analysis is modeled in a topos means “smooth spaces” include function spaces, where the calculus of variations naturally lives. For instance, one has a smooth space of smooth paths between two points of a manifold, and it is an easy proposition that tangent vectors in that smooth space are equivalent to vector fields along a chosen path. One can go on to perform analysis on smooth functionals on such function spaces within this setting in a very intuitive fashion.
Have you seen Keisler text book
Elementary Calculus: An Infinitesimal Approach
1976, 1986 available on line free at
http://www.math.wisc.edu/~keisler/calc.html