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.
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).
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 .
Let be given by . Then by the uniqueness condition of the Kock-Lawvere axiom, we have that .
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:
4. If for all , , then .
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.