2 clarify

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).

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.

1

# Extensional theorems mostly used intensionally

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).