Extensional theorems mostly used intensionally

Question

Some theorems are stated and proved extensionally, but in practice are almost always used intensionally. Let me give an example to make this clear -- integration by parts: $$ \int_a^b f(x)g'(x)ds = \left[f(x)g(x)\right]_a^b - \int_a^b f'(x)g(x) dx$$ for two continuously differentiable functions $f$ and $g$. In practice, this is seldom ever applied to functions but rather to expressions denoting functions. Much more importantly, it is almost always applied by 'pattern matching' on a product term. But note that integration is usually described formally as an operation on functions (i.e. extensional objects), but then in first-year calculus the students are taught to master a series of rewrite rules (i.e. operations on intensional objects).

Logicians [Leibniz, Frege, Russell, Wittgenstein, Quine, Carnap to name a few] have worried a lot about this. Linguists [Montague comes to mind], and physicists [A. Bressan] have worried about this too.

I have two questions:

1. What other examples have you run into of such mixing of extension and intension?
2. Why is this dichotomy not more widely taught / appreciated?

In the case of algebra (more precisely, equational theories), the answer to #2 is very simple: because this dichotomy does not matter at all, because we have well-behaved adjunctions between the extensional and intensional theories [in fact, we often have isomorphisms]. For example, there is no essential difference between polynomials (over fields of characteristic 0) treated syntactically or semantically. But there is a huge difference between terms in analysis and the corresponding semantic theorems.

Answer 1

It seems to me that the mathematical equivalent of the intensional vs. extensional distinction in philosophy would be the distinction between "formal" vs. "functional" objects: formal power series vs. convergent power series, formal integration by parts (with no regard for checking the validity of the operation in a real analysis sense) vs. rigorous integration by parts, formal polynomials vs. functions which happen to be represented by a polynomial, etc. If so, I would say that the formal vs. functional distinction is usually dealt with in more advanced classes, though usually not at the first-year undergraduate level.

For instance, in algebra, the concept of an indeterminate variable (and its distinction from the set-theoretic notion of a variable in a fixed domain) tends to be sufficient for keeping the two concepts distinct in most situations involving set-theoretic functions and the formal expressions giving rise to those functions. In particular, polynomials can be formal by living in some polynomial ring $R[x]$ generated by an indeterminate $x$, rather than having to be set-theoretic functions on some domain. Algebraic geometry also takes particular care in distinguishing an ideal of polynomials from the set-theoretic locus that that ideal cuts out over a given field, or more generally by distinguishing a scheme from a variety.

Similarly, real analysis, with all its cautionary counterexamples as to how various formal operations (e.g. exchanging limits or sums) can lead to disaster if the appropriate functional hypotheses are not verified, also tends to be pretty good about distinguishing a formal computation from a functional one; often the former is used as an initial heuristic motivation only, with the latter then being brought in for the rigorous proof. Although certainly mistakes have been made by treating a formal computation as if it were functionally valid...

Related to this is the ubiquitous "abuse of notation" in which a package of objects, structures, and forms is referred to via its most prominent component (i.e. by synecdoche). Thus, for instance, one often sees a polynomial function $P: {\bf R} \to {\bf R}$ being used to simultaneously represent both the polynomial function and the formal polynomial that represents it, or vice versa (e.g. "the polynomial $x^2$" to refer to the function $x \mapsto x^2$). Another common instance of this is when dealing with spaces (sets with additional structure); one often abuses notation by using the set itself to denote the space, e.g. a group might be denoted by its set $G$ of elements, rather than by the tuple $(G, e, \cdot, ()^{-1})$ of group structures, or a set-theoretic function by just the mapping $f$, rather than than the triplet $(f,X,Y)$ that includes the domain and codomain of that mapping. Such abuses are technically illegal using the strictest interpretations of mathematical notation, but they save a lot of space and, when used correctly, allow readers to focus on the actual content of an argument rather than on its formalism. Still, it is useful and important to point these abuses out explicitly from time to time...

Answer 2

An example of (1) comes from the proof theory of arithmetic, and the way we view proofs of universal statements about the natural numbers. Gentzen's original consistency proof took an intensional view, reasoning explicitly about eigenvariables and induction. Schütte later gave a much simpler consistency proof based on an extensional view, where mathematical induction was eliminated in favor of the so-called "$\omega$-rule", an infinitary inference rule which asserts $\forall x.A(x)$ given proofs of $A(n)$ for all $n\in \mathbb N$.

Buchholz has connected the two approaches, showing how Gentzen's result can be reconstructed by translation into Schütte's sequent calculus, essentially by reading off the infinite extension of finite, intensionally-defined proofs. (He calls this viewing finite derivations as "notations for infinitary derivations".) There is certainly a much stronger asymmetry here, because once you take an extensional view of primitive recursive functions over the natural numbers, you can't go back to a (finite) symbolic view.

Answer 3

A recent question about combinatorial interpretations, namely to find an interpretation for the identity

$$\sum_{k=0}^m 2^{-2k} \binom{2k}{k} \binom{2m-k}{m}=4^{-m} \binom{4m+1}{2m}$$

gives another full class of such issues. This equation is much more than a tautology when interpreted intensionally as being about combinatorics: a combinatorial interpretation involves give a natural class $C_l$ of objects for the left-hand-side and $C_r$ for the right-hand side and a bijection between these classes. Furthermore, and this is where things get really interesting (with respect to my original question), such classes $C_l$ and $C_r$ would be considered 'natural' if by using the usual rules of combinatorial counting, we would naturally get that the number of objects of $C_l$ of size $m$ is the left-hand side expression (similarly for $C_r$ and the rhs). The point is that these counting expressions would be derived structurally from the combinatorial classes. This is a much more interesting interplay between 3 extensional objects (a counting function and 2 combinatorial classes) and 2 intensional ones (different-but-equal formulas representing the counting function).

Answer 4

Georges Gonthier and François Garillot are doing interesting things with phantom types and unification in Coq to allow one to write, for example, directv (V + W) to mean the proposition that $V \oplus W$ is a direct sum.

I haven't fully grasped how it works yet, but let me give you a simplified explanation of what I think is going on. What is happening is that directv X is really notation for directv_def _ (Phantom _ X).

Phantom is a constructor of a very trivial inductive type

Inductive phantom (A:Type) (a:A) : Type := Phantom : phantom A a

The function Phantom is a polymorphic constructor of type forall (A:Type)(a:A), phantom A a. The purpose of Phantom is to lift values to the type level so that type inference can operate on these values.

directv_def doesn't even use the (Phantom _ X) argument (because it contains no data). The only purpose of this argument is to drive the type inference engine to fill in the first argument. directv_def has type forall (VW : addv_expr) (_ : phantom _ (Vadd VW)), Prop. addv_expr is a record type.

Record addv_expr := build_addv_expr {
 V1 : VectorSpace; 
 V2 : VectorSpace;
 Vadd : VectorSpace }

The definition of directv_def is

directv_def (VW : addv_expr) _ := dim (V1 VW) + dim (V2 VW) = dim (Vadd VW)

The final ingredient is that fun V1 V2 => (build_addv_expr V1 V2 (V1 + V2)) is declared as a Canoncial Structure.

So what does Coq read when you write directv (V + W)? Well it parses this as notation for

directv_def _ (Phantom _ (V + W))

The first parameter to Phantom is the type of (V + W) so we can quickly fill that in to get

directv_def _ (Phantom VectorSpace (V + W))

Phantom VectorSpace (V + W) has type phantom VectorSpace (V + W), but directv_def is expecting something of type phantom _ (Vadd _) so it tries to unify (V + W) with (Vadd _). Because Vadd is a record projection, Coq tries to look up in its list of canonical structures to see if there are any declared whose Vadd field is of the form (V + W). It says, "ahha! there is! I can use build_addv_expr V W (V + W)" (notice the intensional behaviour of canonical inference here). So Coq successfully unifies (V + W) with (Vadd (build_addv_expr V W (V + W)), and this forces the first parameter of directv_def:

directv_def (build_addv_expr V W (V + W)) (Phantom VectorSpace (V + W))

And that is it for type inference. Later on this expression might be used, so it will start normalizing:

dim (V1 (build_addv_expr V W (V + W))) + dim (V2 (build_addv_expr V W (V + W))) = dim (Vadd (build_addv_expr V W (V + W))) 

and then to

dim V + dim W = dim (V + W)

If you try to write something else like directv 0 then the canonical structure inference will fail and you will get a (probably obtuse) type error.

---

This has been as simplified example. In reality, directv is much more complicated and allows one to write directv (\sum_(0 <= i < n) V i) to mean $\bigoplus_{i=0}^n V_i$ is a direct sum and accepts things like directv 0 to mean a trivial direct sum.

Matita allows you to write unification hints directly without the necessarily building canonical structures. I suspect doing this sort of intentional inference would be easier in such a system.

Answer 5

Is there a formal definition of the intension/extension distinction, or even of "intension" and "extension" as separate terms?

In the examples discussed here, the difference is simply that there is a richer type of object A, carrying its own set of allowed operations and relations, that maps (maybe in partially-defined way) to a coarser type of object B. The coarser thing B could be, as in the examples posted, a "forgetting of structure" or "de-categorification" or "numerical evaluation" of A. Some of the allowed operations on A's will not work perfectly or unambiguously on B's per se due to the loss of structure. For example, replacing $(x-1)/(x-1)$ by $1$ is correct for (intensional, formal) rational functions but requires additional input (a domain) to be defined unambiguously for (extensional, numerical) rational functions. The possibly missing additional structure can be seen as a reinstatement of the information lost when passing from A to B, or rigidification data needed to disambiguate the operations on B.

From this point of view, intension seems to be just a specification of context A, and an extensional interpretation of such a context is a specification of a map from A to some other, usually less structured, context B. Is there more to this distinction as it appears in the philosophy or computer science literature?

Answer 6

After reading some of the answers, I don't think there exists such a difference.

Let me explain myself. Take Edgar's comment: we don't say $1$ converges, but we do say $\sum_{n=1}^\infty 2^{-n}$ converges. Strictly speaking, $1$ does not converge, we can't talk about the convergence of a number. It becomes a meaningful statement when we understand $1$ as a constant sequence. It could be said that $\sum_{n=1}^\infty 2^{-n}$ is not defined properly either, but we've accepted that an infinite sum as a limit.

I think the same problem occurs here. After all, maths is all about formal objects. Once one starts to omit some of the details (probably for simplicity), for example, not specifying whether a polynomial should be thought of as an element of a ring, or as a function, mistakes might occur. I disagree with Tao in this subject: there are no semantic or functional interpretations of an object (or at least, there are no unique such interpretations). A polynomial can't be interpreted as a function. It is defined to be as an element of $K[x]$. If we want to talk about a polynomial function, then we must state the domain, the codomain and construct the transformation from the variable to the polynomial interpreted by replacement of the variable. But then we are no longer talking about a polynomial.

Applied to Carette's example, one can think that before applying the theorem as a rewrite rule, we first have to define the function we identify by the expression, replace the expression by the function, and then apply the theorem to the function. And that's what we are doing (or should be doing), but for simplicity we omit these steps. It would be the same as if we instantiated $aa^{-1}=1$ as $00^{-1}=1$. We can't forget the requirements for the application of the rule.

Answer 7

I'm not sure I understand the question, but doesn't this always happen? For example, if I'm going to state and prove the product rule, I'm going to write:

Proposition. $(fg)' = f'g+fg'$

And that's what I'll prove. However, in practice I will probably use

$$\frac{\partial}{\partial x}(\tau \sigma) = \left(\frac{\partial}{\partial x}\tau\right)\sigma+\tau \left(\frac{\partial}{\partial x}\sigma\right)$$

where $\tau$ and $\sigma$ are terms of type $\mathbb{R}$, and $\frac{\partial}{\partial x}$ is to be understood as the metafunction of metatype $\mathrm{Terms} \rightarrow \mathrm{Terms}$ given by $\tau \mapsto (\lambda x.\tau)'(x)$.

So I guess what I'm saying is that any time higher-order functions appear, we can expect theorems to be stated and proved "extensionally" but then used "intensionally." A good foundation should have inbuilt support for this kind of thing, in my opinion, since it is so completely widespread.

To answer question (2), "why is this dichotomy not more widely taught / appreciated", I think its because words like "formal expression" and "metafunction" are not widely taught and/or appreciated outside of logic circles. As computer-formalized mathematics becomes more widespread, this will surely change. By the way, if someone were to write a textbook called "explicit mathematics" based on the premise that we should make all these kinds of little nuances explicit, I would surely buy it, hint hint, nudge nudge :)