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 treated syntactically or semantically. But there is a huge difference between terms in analysis and the corresponding semantic theorems.

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.