# “Internal” versus “external” definitions of functions: equivalent foundations for mathematics?

This is a generalization of the question given at Definition of Function.

I think it fairly clear that the Bourbaki and the ordered pair definition of functions are equivalent. A deeper question is whether or not the conception of functions as arrows-as in category theory without specification-is equivalent.

Let me be a little more specific what I mean. Currently,there are roughly 2 kinds of foundations proposed for mathematics: "internal" and "external".

An internal foundation for mathematics is one based on a primitive building block from which the functions are ultimately constructed explicitly from the building blocks. Examples are,of course,set theories-particularly Zermelo-Frankel set theory-where sets are defined as abstract collections that satisfy a finite number of axioms (union,extensionality,etc).

We then define ordered pairs explicitly from sets (to be precise,the set of ordered pairs ={{x},{x,y}} of elements is a subset of the power set of the power set of the union of sets where the elements {x} and {x,y} are taken). A function is then defined as a subset of this set where no 2 different ordered pairs have the same first member.

An extensionalist foundation-such as Paul Taylor and to a lesser extent, William Lawvere,have proposed-takes the FUNCTIONS to be the primitive elements as arrows that are specified in some manner. There are then 2 ways sets can be obtained from functions: 1) the sets can simply be defined as the domain and ranges of maps without specifying thier composition explicitly. I think this is what Taylor does,more or less-but I had a lot of difficulty understanding exactly what he's proposing since most of it is couched in heavy logical language. 2) A primitive function-called the membership function-is proposed which assigns single elements to collections and they are built up as the ranges of collections of membership maps. The rest of set-theoretic constructions are built up in a similar manner using specialized functions. This is what William Lawvere and Robert Rosebraugh do in thier fascinating book,Sets For Mathematics.

The extensionalist approach,of course,is favored by those who want to replace set theoretic models with categorical ones for mathematics. In some respects,it is simpler-arrows are easier to deal with then axiomatic sets. It also allows us to sidestep the sticky cardinality issues that come up in category theory,when dealing with collections that are too large to be sets,that started all this debating in the first place. Unfortunately,what makes set theory difficult is also what gives it it's tremendous power as a foundation for mathematics: It allows us to develop all objects in mathematics explicitly and unambiguously.There's absolutely no doubt 2 sets are equal in axiomatic set theory since in principle,you can see that they indeed have the same elements.

Personally,I favor a foundation that allows us to do both.Thinking we need to jettison one for the other is tantamount to saying we can't accept quantum theory without rejecting general relativity.

My question: Can these 2 conceptions of function-internal and external-be shown to be logically equivalent?Of course,the question's probably not that simple-you'd probably need to specify which "theory" you're talking about-for example,Taylor or Lawvere/Rosebaugh's.

So would they be equivelent in:

a) Paul Taylor's vrs. classical ZFC models? b) Lawvere/Rosebaugh's vrs. classical ZFC models?

It seems to me the model proposed in Lawvere/Rosebaugh should be equivalent since the membership function more or less is the same as the membership relation in axiomatic set theory. In Taylor's though-it's not so clear.

-
MO is not your blog. – Harry Gindi Jul 5 '10 at 7:49
Why is this question CW? – Qiaochu Yuan Jul 5 '10 at 10:15
Some of what you claim here as background is, at the very least, debatable. Categorical foundations certainly don't let us sidestep issues of cardinality/size, but on the other hand, they do (many logicians would argue) let us develop mathematics quite as "explicitly and unambiguously" as traditional set theory does. The difference is not so much one of content or expressive power (most foundational theories on either side are equivalent to something on the other side), but rather of language and emphasis. – Peter LeFanu Lumsdaine Jul 5 '10 at 11:31
@Qiaochu: Because it's Not a real question™. – Harry Gindi Jul 5 '10 at 13:15
@Harry Firstly,you're not the hall monitor,here,Harry.If the moderators agree with you,they'll shut it down.Secondly-it's a very general question and I was told those kinds of questions are appropriate for community wiki.I'm trying to follow the house rules here. – The Mathemagician Jul 5 '10 at 18:16

The first answer to your question is "yes". In a topos, say, morphisms are in bijective correspondence with functional relations. More precisely, given objects $A$ and $B$, there is an isomorphism between the exponential $B^A$ and the object $FunRel(A,B)$ of functional relations between $A$ and $B$. In the internal language of the topos $FunRel(A,B)$ is described as (where $\exists!$ means "exists exactly one") $$FunRel(A,B) = \lbrace F \in \mathcal{P}(A \times B) \mid \forall x \in A \exists! y \in B . \; \langle x, y \rangle \in F \rbrace.$$ You will of course recognize this as the usual set-theoretic definition of a function as a collection of ordered pairs. The crucial bit of logic that is needed for the bijection is the principle of unique choice, which says that for every $R \subseteq A \times B$, $$(\forall x \in A \exists! y \in B . \; \langle x, y \rangle \in R) \implies \exists f \in B^A \forall x \in A . \langle x, f(x) \rangle \in R.$$

This brings me to the second answer to your question, which is "no". Typically, the definitions of functions which do not rely on set theory and first-order logic are more widely applicable that the usual set-theoretic one. Two examples come to mind:

1. the notion of morphism can be interpreted in any category, as you already mentioned,
2. the definition of function as an element of a function type $\tau \to \sigma$ in a (simply typed) $\lambda$-calculus allows us to interpret functions as programs, see for example primitive recursive functionals. These do not in general satisfy the law of extensionality $(\forall x : \tau .\; f(x) = g(x)) \implies f = g$.

Students of mathematics are sometimes told that in the old days people were confused about the notion of function, that they equated functions with symbolic expressions (like students still do), or with Taylor expansions (not the same Taylor). The students walk away with the impression that those silly 17th, 18th and 19th century mathematicians lived in great confusion, thinking that all functions can be computed and they all have series expansions, and that we all have to thank 20th century set theory for setting us straight. But that's a rather narrow view of the world. There are very good reasons why in certain contexts we should think of functions as something other than bags of dust. Sometimes function are symbolic expressions (called "programs" nowadays), and sometimes they are Taylor expansions (in synthetic differential geometry). To paraphrase a Taylor, in such situations it is better to axiomatize the algebra of functions directly than to glue them together from dust found in some bags.

-
Dear Andrej, why should we consider morphisms in SDG when we can just call them morphisms? Just because they're morphisms in a topos doesn't mean that we need to consider them when we're defining functions. Should natural transformations of presheaves on any category also be comsidered functions? – Harry Gindi Jul 5 '10 at 15:37
@Harry: The point of mentioning SDG was that in a model of SDG every real function has a Taylor expansion (inside a model of SDG there is no distinction between "morphism" and "function"). Thus it is not so crazy to believe that all functions have Taylor expansions, you just have to be careful what else you believe. This way we can rehabilitate some old arguments in geometry and analysis which were done "imprecisely" from the viewpoint of modern mathematics. Regarding natural transformations between presheaves: in the internal language of the presheaf topos these are functions. – Andrej Bauer Jul 5 '10 at 16:03
Is there any real reason to do SDG inside of its internal logic as opposed to dealing with the topos as a Grothendieck topos? – Harry Gindi Jul 5 '10 at 16:40
@Andrew: the primitive conception of function is probably that of an exponential in a category. It just talks about two things: that there is an evaluation map, and that given a function of two variables we can fix the value of one variable to obtain a function of the remaining variable. It is easy to argue that such a characterization is no more mysterious or magical than the one in terms of functional relations. I suppose it really is a question of getting used to new ways of thinking about familiar objects. – Andrej Bauer Jul 6 '10 at 6:57
@Harry: yes, definitely, it's a lot of fun to work inside a model of SDG where you can do crazy things like divide a circle into infinitely thin isosceles triangles and compute with nilpotent infinitesimals as if you were a physicist – Andrej Bauer Jul 6 '10 at 6:59

Von Neumann proposed a foundation for mathematics in which "function" was a primitive notion. A set is a special kind of function. (Perhaps a function taking only values 0 and 1, I no longer remember the details. Of course 0 and 1 are themselves certain functions.) But in short order more conventional mathematicians re-cast this into an equivalent system with sets as primitive. But to do that, "proper classes" had to be allowed, as well as sets. http://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory

-
I'm well aware of Von Neumann's proposed model and I'm glad you brought it up.The history of the modern concept of function is fascinating,but I was afraid it would get too far off point for MO to digress into it. – The Mathemagician Jul 5 '10 at 18:18