Variable-centric logical foundation of calculus - MathOverflow

Variable-centric logical foundation of calculus

2011-12-24T15:23:22Z

Since calculus originated long before our modern function concept, much of our language of calculus still focuses on variables and their interrelationships rather than explicitly on functions. For example, in the assertion "If $y=x^2$ then $\frac{dy}{dx}=2x$," the functions $f$ and $f'$ remain unnamed while the variables $x$ and $y$ take center stage. We interpret this as notational finesse, but there seems to be an important philosophical difference between what we say and what we mean.

I have sometimes wondered: Is there an alternate logical foundation of Calculus in which variables, expressions, and equations are the central ideas, and functions per se are implicit?

Answer by Joel David Hamkins for Variable-centric logical foundation of calculus

2012-12-06T00:27:53Z

All the various computer algebra system approaches to calculus, which are increasingly prevalent and powerful, although imperfect, seem to me to be prime instances of the kind of foundations you mention. These systems, at least the kind I have in mind, are completely syntactic, working by necessity explicitly on the syntactic strings used to represent the various functions, that is, with the variables, expressions and equations as syntactic objects, rather than with the abstract mathematical objects that these strings represent for us. In particular, the systems have to deal with all kinds of issues such as free and bound variables and variable types and all sorts of irritating syntactic issues involving substitution and composition and whatnot, which we mathematicians usually prefer to glide smoothly past without pause. At bottom, however, the development of these computer algebra systems has required the developers in effect to formulate a syntactic foundation of exactly the kind you seek. The actual meaning of the expressions, the actual abstract mathematical objects, are merely implicit in the operation of the systems.

Answer by Andrej Bauer for Variable-centric logical foundation of calculus

2012-12-06T04:15:14Z

I would like to argue in the opposite direction. The 17th century notation that is still in use today is a syntactic hodgepodge which does great disservice to students and their teachers alike, despite claims of its usefulness (by people who never tried an alternative). It is partially responsible for the fact that the average mathematician in the street cannot coherently describe the notion of a bound variable, thinks there isn't much difference between $f$ and $f(x)$, and is willing to believe that $\frac{\partial L}{\partial \dot q}$ is a sensible notation.

Functions as mathematical objects (as opposed to symbolic expressions) are fundamental to differential calculus. Moreover, important concepts such as derivative, definite integral, differential operator, gradient, etc., are themselves functions of higher order (they take functions as arguments).

Let me mention two modern foundational explorations in analysis.

First there is Synthetic differential geometry (introductory reading material here and here) whose distinguishing features are that it calculates with nilpotent infinitesimals, and that arbitary function spaces can be formed at will (whereas in classical analysis forming a function space is always a Big Thing). This makes certain definitions very easy. For example, the tangent bundle of $M$ is simply the space of function $\Delta \to M$ where $\Delta = \lbrace x \in R \mid x^2 = 0\rbrace$ is the space of infinitesimals (of order 2). And it does not even matter what $M$ is here, the definition just makes sense, both intuitively and technically. The classical approach to analysis requires a whole edifice just so that the tangent bundle can be defined. It is too complicated for the average undergraduate.

A foundation for calculus which is most directly based on functions is the differential $\lambda$-calculus (introduction here). The $\lambda$-calculus is the theory of functions. For example, functional programming languages are based on it. The differential $\lambda$-calculus is an enrichment of $\lambda$-calculus with (abstract) differential operators.

So, while I am sure somebody has cooked up a foundation of calculus based on avoiding functions, the arrow of progress points in the opposite direction.

Answer by Todd Trimble for Variable-centric logical foundation of calculus

2012-12-07T01:54:25Z

In one of my comments over at the other thread (this other thread), I had mentioned some discussion at the $n$-Category Café about a differential $\lambda$-calculus (from the looks of it, different to the one alluded to in Andrej Bauer's answer, although I looked only briefly). I'll try to sketch out some of it here, as it seems relevant.

Categorical models of typed $\lambda$-calculus are cartesian closed categories, and the idea was to contemplate the universal (i.e., initial) cartesian closed category that comes equipped with

A commutative ring object $R$ (finite products suffice to describe what is meant by a commutative ring object),
A differentiation operator $D\colon R^R \to R^R$ (here $R^R$ is the "function space object" whose existence is given by cartesian closure; the elements of $R^R$ correspond to morphisms $R \to R$), satisfying all the formal expected properties of differentiation (product rule, chain rule, etc.).

This universal cartesian closed category can be constructed syntactically and could be called "the $\lambda$-theory of high school calculus"; I'll call it $\mathit{Diff}$. A model of this theory is by definition a cartesian closed category $C$ together with a functor $S\colon \mathit{Diff} \to C$ which preserves the cartesian closed structure up to isomorphism (meaning the canonical comparison maps $S(a \times b) \to S(a) \times S(b)$ and $S(a^b) \to S(a)^{S(b)}$ are required to be isomorphisms). If the receiving category $C$ consists of concrete structures and structure-preserving maps, then you could call such a model a "denotational semantics" of $\mathit{Diff}$.

Now, there exists no denotational semantics $S\colon \mathit{Diff} \to Set$ which takes the object $R$ to the reals $\mathbb{R}$ as commutative ring. In other words, there is no operator $D\colon \mathbb{R}^{\mathbb{R}} \to \mathbb{R}^{\mathbb{R}}$ that satisfies all the formal properties of differentiation. But, there are other toposes $C$ of interest besides $Set$ which do admit such a semantics, where one can arrange the commutative ring object $R$ in $C$ so that its elements $1 \to R$ correspond exactly to real numbers. There is some flexibility in what one can arrange general morphisms $R \to R$ to be -- certainly they won't correspond to all functions $\mathbb{R} \to \mathbb{R}$, but you can get various interesting subclasses of functions (for which the modeled differentiation operator $D$ coincides with the usual one). For example:

If $C$ is the topos of functors $CAlg_{fp} \to Set$ where $CAlg_{fp}$ is the category of finitely presented commutative $\mathbb{R}$-algebras, then $\hom(R, R) \cong \mathbb{R}[x]$ is the set of polynomial functions on $\mathbb{R}$.
If $C$ is the topos of functors $C^{\infty}Alg_{fp} \to Set$ where $C^{\infty}Alg_{fp}$ is the category of finitely presented $C^{\infty}$-algebras (see here for definitions), then $\hom(R, R)$ is isomorphic to the ring of $C^{\infty}$-functions $\mathbb{R} \to \mathbb{R}$.

There were various further ruminations on this, coming under the heading of "snowglobe models" as models "sitting inside $Set$ as a miniature universe", as discussed here.