"Internal" versus "external" definitions of functions: equivalent foundations for mathematics? - MathOverflow

"Internal" versus "external" definitions of functions: equivalent foundations for mathematics?

2010-07-05T07:13:31Z

This is a generalization of the question given at http://mathoverflow.net/questions/30381/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.

Answer by Andrej Bauer for "Internal" versus "external" definitions of functions: equivalent foundations for mathematics?

2010-07-05T09:11:43Z

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:

the notion of morphism can be interpreted in any category, as you already mentioned,
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.

Answer by Gerald Edgar for "Internal" versus "external" definitions of functions: equivalent foundations for mathematics?

2010-07-05T11:54:32Z

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