Lambda the Ultimate

Most mathematicians consider the language of set theory (as the foundation of math) simpler and more intuitive than that of lambda calculus (or the related category theory). In other words, there does not appear to be a compelling reson for switching to the competing product. Obviously, LC and CT can be useful in their appropriate areas.

You hit the nail on the head. Axiomatic set theory is foundational to all of mathematics. Mathematicians would rather have something that is simple and intuitive to reason about that can form the foundation of mathematics. Since the lambda calculus is about functions and functions are not very intuitive*, the lambda calculus doesn't make a very good foundation for the rest of mathematics. Sets and predicates can generally be understood at an intuitive level**, without having to resort to the use of other ideas from mathematics (integers, for example). The idea of a set is intuitive, because we see them all around us every day. I can see a collection of coins on my desk. I can identify with the idea of “the set of coins on my desk.” If I take some of those coins and place them in a bowl, I understand, at a very intuitive level, the idea that there is a set of coins on my desk, a set of coins in the bowl, and yet all of these coins belong to the set of coins in the room. I don't have to resort to other ideas from mathematics to understand this. The same can be said of predicates. I understand, at an intuitive level, the idea of truth and falsehood. I understand that the statement “coin x is in the bowl” may be true or may be false, depending upon what coin, x is. I can also use that statement (predicate) to build up the set of all coins in the bowl.

EDIT: Oh and I forgot. You might (the original poster) be interested in reading a book on ZF set theory. Since ZF has been around awhile, you don't need some fancy new book. An older book from Dover would do just fine. (I have no relation whatsoever with Dover, and that link doesn't give me any sort of points with Dover, if I had any such thing with them. If you don't trust me go ahead and do a Google search and get there that way). You can find some books on more classical subjects (mathematics for example) for a very reasonable price (usually less than $15), so you don't have to feel like your throwing away a lot of money just to buy a book to learn about something you may not find interesting in the end anyway. Of course there is lots of good information out there on the web too, but some people prefer to have a dead tree copy.

* By intuitive, I mean, it is hard to imagine a mathematical function without resorting to the use of other concepts from mathematics, specifically, sets.

** One of the main issues we face when dealing with foundations is that we eventually reach a point where we have to stop defining things and just accept a term as “intuitive” (otherwise we end up with circular definitions). This is uncomfortable for mathematicians (especially those who are interested in foundations), because they like to give very precise definitions for everything around them.

Since the lambda calculus is about functions and functions are not very intuitive*, the lambda calculus doesn't make a very good foundation for the rest of mathematics.

You probably know this, but it deserves to be stated anyway. Alonzo Church's purpose in inventing the lambda calculus was exactly that.

(Why it didn't take off is he was using the untyped lambda calculus and it had exactly Russel's paradox (namely the quite appropriate term, Y not). Hence his work on the simply typed lambda calculus.)

Whats amazing is that the Lambda Calculus was such a brilliant development. Even though Church failed (for the most part) in his origonal goal, his work ended up not only being useful in proving the Entscheidungsproblem, but highly influential for Computer Science in general. In many ways Church is not as recognized as he should be, (How many undergraduates in computer science even know who Alonzo Church is as compaired to Alan Turing?) but alas, "them's the breaks", right?

Naively, predicate (or formula) defines a set. That's called the "unrestricted comprehension" axiom. It should be obvious that a predicate (as a predicate logic language expression) is not the same as the set (thing) it defines/describes. Also, the comprehension axiom has to be restricted in order to avoid the Russell paradox.

I understand that a language expression is different from the thing it denotes, if that is what you mean, but it is not obvious to me what the need is for a difference between predicates and sets, hence my post. A restricted comprehension is to an unrestricted comprehension as a typed lambda abstraction is to an untyped lambda abstraction (see point 1 in the first post). Russell's paradoxical proposition becomes ((λ x . (¬ (x x))) (λ x . (¬ (x x)))) in the alternative notation (note the similarity with the Ω combinator), and this term cannot typed, hence the paradox.

Most mathematicians consider the language of set theory (as the foundation of math) simpler and more intuitive than that of lambda calculus (or the related category theory). In other words, there does not appear to be a compelling reson for switching to the competing product. Obviously, LC and CT can be useful in their appropriate areas.

Appeals to `intuitiveness' are not convincing to me at all. The conventional definions lead to problems, among which are an ambiguity in the meaning of (f x) (is it the function f applied to x or the ordered pair x occuring in f?), a nonsensical meaning of ∋ (see point 2), and a redundancy regarding predicates and sets.

I do not consider Lambda Calculus a `competing product', but Set Theory a special case of Lambda Calculus. Perhaps I was insuffciently clear about this.

Mathematicians are used to understanging higher-order logic as a fragment of set theory, and so have historically seen no reason to use type-theoretic rather than set-theoretic foundations. However, ZFC and the Calculus of Inductive Constructions (used in Coq) can each encode the other, and are essentially equivalent. See Benjamin Werner's paper "Sets in Types, Types in Sets".

As a result, which take to prefer is a matter of taste. My own preference is for the type-theoretic approach, because I think it mechanizes much more smoothly, and I think that machine-checkable proof is the wave of the future.

For example, peer reviewers were unable to verify Hales's claimed proof of the Kepler conjecture, and so he's started the Flyspeck Project to redo the proof in HOL, so that he can produce a machine-checkable proof object. Since verifying a proof checker is relatively straightforward, the human verification burden is greatly simplified.

I understand that a language expression is different from the thing it denotes, if that is what you mean, but it is not obvious to me what the need is for a difference between predicates and sets, hence my post.

If you do not care about what your predicates mean (interpretation) and are only interested in symbol manipulation, then yes you do not need sets.

A restricted comprehension is to an unrestricted comprehension as a typed lambda abstraction is to an untyped lambda abstraction

It's unclear what that supposed to mean. Assuming, you want to say that typed LC disallows lambda terms expressing Russell's paradox then, yes, at the expence of simply typed LC not being Turing complete. However, illative lambda calculus based on untyped LC avoids the paradox without need for typing.

1. Lambda abstractions are similar to set comprehensions. Compare {x | M} to (L x . M) (or {x:A | M}) to (? x:A . M)).

That does not make any obvious sense. How can a list comprehension {x | M} be equivalent to a lambda abstraction ? Please elaborate.

and this term cannot typed, hence the paradox

If this term cannot be typed in [typed lambda calculus], then there is no paradox because the term is syntactically incorrect.

Appeals to `intuitiveness' are not convincing to me at all.

That's strange position to assume, but so be it.

The conventional definions lead to problems, among which are an ambiguity in the meaning of (f x) (is it the function f applied to x or the ordered pair x occuring in f?)

What conventional definition do you have in mind ?

a nonsensical meaning of E (see point 2)

Point 2 does not make any obvious sense (for starters, what is predication syntax). Could you elaborate on the nonsensical meaning of the membership 'operator' which is normally called the 'membership predicate' in the set theory ?

I do not consider Lambda Calculus a `competing product', but Set Theory a special case of Lambda Calculus.

How would you go about expressing, for example, real analysis in lambda calculus ? Besides, what specific variety of lambda calculus as a foundation of math do you have in mind ? Clearly, you cannot use the original untyped LC because of the paradox. What then ?

If you do not care about what your predicates mean (interpretation) and are only interested in symbol manipulation, then yes you do not need sets.

Even if you are interested in interpretation, I still do not understand the reason for a distinction between predicates and sets.

How can a list comprehension {x | M} be equivalent to a lambda abstraction ? Please elaborate.

(λ x . M) is the characteristic function of {x | M} and behaves in exactly the same way. Did you read the original post?

The conventional definions lead to problems, among which are an ambiguity in the meaning of (f x) (is it the function f applied to x or the ordered pair x occuring in f?)

What conventional definition do you have in mind ?

E.g., defining a function as a binary relation relating x to (f x), and defining ∋ as a binary relation between sets.

a nonsensical meaning of ∋ (see point 2)

Point 2 does not make any obvious sense (for starters, what is predication syntax). Could you elaborate on the nonsensical meaning of the membership 'operator' which is normally called the 'membership predicate' in the set theory ?

Predication syntax is the juxtaposition of a predicate symbol with a subject, "(P s)", which behaves identically to function application.

Defining set membership using a set membership relation is as nonsensical as defining function application using a function application function: if (f x) is really (a f x), then (a f x) is (a a f x), and that is (a a a f x), etc. The correct way is to treat set membership and function application as (the same) special operator (∋ / @), usually ommited for brevity.

How would you go about expressing, for example, real analysis in lambda calculus ? Besides, what specific variety of lambda calculus as a foundation of math do you have in mind ? Clearly, you cannot use the original untyped LC because of the paradox. What then ?

In the same way as you would in set theory, only transcribing the syntax in the way suggested by the original post. I do not know enough about foundations to answer your second question.

Even if you are interested in interpretation, I still do not understand the reason for a distinction between predicates and sets.

Without interpretation, predicate logic formulas are a meaningless game of symbols.

With interpretation and your belief that predicates and sets are indistinguishable, how would you handle situations like that:

o the same predicate holds true in one set theory and not in another, e.g. Exists(R)(R = {x is not a member of x };
o two predicates define the same set;
o a set is defined without any predicates.

(λ x . M) is the characteristic function of {x | M} and behaves in exactly the same way. Did you read the original post?

To make any sense of that, please define in terms of functions:

o the characteristic function;
o the set;
o set equality.

defining a function as a binary relation relating x to (f x),

What's the problem with defining a function as a relation [with some additional properties] ?

and defining ∋ as a binary relation between sets.

Assuming you mean set membership, no one defines it "as a binary relation between sets".

"(P s)", which behaves identically to function application.

"which behaves identically to function application" does not make any obvious sense. Please elaborate.

Defining set inclusion using a set inclusion relation.

No one defines "set inclusion using a set inclusion relation". Loosely, for any sets A and B where B is a member of A, there exists set C whose elements are members of B and some predicate P holds, C = { (B is a member of A) and P }. Such C is called a subset of B.

The correct way is to treat set inclusion and function application as (the same) special operator (∋ / @), usually ommited for brevity.

In order to make sense of that, please define 'special operator'.

I do not know enough about foundations to answer your second question.

If you do not know enough about foundations, how can you claim *anything* you've claimed ?

In order to make sense of that, please define 'special operator'.

Sebastian is referring to the common practice of using a syntactic operator (@, in this case), to represent function application. In other words, instead of writing f x, we might write f @ x or even @(f, x). His point is that it is nonsensical to think of this syntax as itself an instance of function application, since it results in a recursive use of the "function application operator". Instead we might wish to think of @ as a "special operator", purely syntactic, or perhaps as a meta-function. (It's interesting to note that some language systems actually implement function application by applying the function and its arguments to a meta-functional definition of "apply". I believe PLT Scheme does this, and provides a hook to allow this function to be redefined.)

I'm not willing to argue in favor of Sebastian's claim that set inclusion and function application should be regarded as the same, but I hope this at least helps clarify his point. I think his notion of "special operator" does make sense.

I think his notion of "special operator" does make sense.

Right, it may in a narrow sense, but what has it got to do with the 'foundational' stuff he wrote about sets, LC, 'inclusion' etc. ?

With interpretation and your belief that predicates and sets are indistinguishable, how would you handle situations like that:

o the same predicate holds true in one set theory and not in another, e.g. Exists(R)(R = {x is not a member of x };

(You probably meant proposition instead of predicate). This is not really related to the discussion: the proposition would simply be true in one `function theory' and not in another.

o two predicates define the same set;
o a set is defined without any predicates.

If predicates and sets are the same thing then these situations are meaningless or cannot occur.

To make any sense of that, please define in terms of functions:
o the characteristic function;
o the set;

The set and the characteristic function are then the same, so again it is unclear what you mean.

o set equality.

As I wrote, you can simply transcribe any definition, so the definition of set equality might become: If A and B both have type C → Bool then (= A B) is defined by (∀ x : C . (↔ (A x) (B x))). (But one might question the utility of an equality specifically for sets.)

What's the problem with defining a function as a relation [with some additional properties] ?

I have already explained this in my previous posts (look for "ambiguity").

Assuming you mean set membership, no one defines [∋] "as a binary relation between sets".

Yes, I should have written "membership" and have now corrected the terminology. And no, set membership is conventionally seen as a relation between two sets.

"(P s)", which behaves identically to function application.

"which behaves identically to function application" does not make any obvious sense. Please elaborate.

I have already explained the similarity between (P s) and (f x) in my first post (points 2--4), and I am not going to repeat things because there really is nothing more to it, and you are evidently not reading what I write.

No one defines "set inclusion using a set inclusion relation".

This is off topic, but: "is a subset of" is not a relation according to you?

In order to make sense of that, please define 'special operator'.

A special operator is a part of the concrete syntax of a term used to distinguish what kind of primitive form it is. Other examples of special operators are λ itself, the pair constructor ⟨,⟩ and whatever other primitives the language has. I think it is correct to think of ∋ as a special operator (identical to @), not as a relation.

If you do not know enough about foundations, how can you claim *anything* you've claimed ?

Well, because what I have claimed (in the original post) is true, for starters, and secondly because one does not immediately need to propose an entire alternative foundation for mathematics (if such a thing is even possible) down to every jot and tittle, merely to point out that there is a similarity between function application and set membership, and between function abstraction and set comprehension, to suggest these things might be identified (functions being the more general concept).

(You probably meant proposition instead of predicate). This is not really related to the discussion: the proposition would simply be true in one `function theory' and not in another.

The predicate is (x is not a member of x) which has an interpretation in one set theory but not in another.

If predicates and sets are the same thing then these situations are meaningless

{ x|(x e N) and (x gt 6) and (x lt 8) }
{ x|(x e N) and (x*x = 49) }

... are the same set defined by two different predicates (N is a set of natural numbers).

The set and the characteristic function are then the same, so again it is unclear what you mean

Cool, please define the characteristic function.

As I wrote, you can simply transcribe any definition, so the definition of set equality might become: If A and B both have type C → Bool then (= A B) is defined by (∀ x : C . (↔ (A x) (B x))). (But one might question the utility of an equality specifically for sets.)

What's a type ? You did not define it. How do you interpret "for all" if you do not have the notion of collection ? "For all" what ?

I have already explained this in my previous posts (look for "ambiguity").

You did not, you mere stated it without any supporting evidence.

set membership is conventionally seen as a relation between two sets.

It is not. Do you have any supporting evidence for such bizarre claim ?

I have already explained the similarity between (P s) and (f x) in my first post (points 2--4), and I am not going to repeat things because there really is nothing more to it, and you are evidently not reading what I write.

Ok, if you cannot explain what kind of similarity you mean, let's skip it.

This is off topic, but: "is a subset of" is not a relation according to you?

Sure, it is, but it is not *defined* as such.

I think it is correct to think of ∋ as a special operator (identical to @), not as a relation.

No, it is not because ∋ is neither.

[...] are the same set defined by two different predicates (N is a set of natural numbers).

I would say that the predicate formulas are the different, but the predicates (properties) they express are the same. But how would you explain/describe the difference between predicates and sets?

The set and the characteristic function are then the same [...]

Cool, please define the characteristic function.

Define what characteristic function in terms of what and why? The characteristic function corresponding to any set {x ∈ A | M} is (λ x : A . M).

What's a type ? You did not define it. How do you interpret "for all" if you do not have the notion of collection ? "For all" what ?

You can have a notion of a collection perfectly well, and this notion is again a function to Booleans. (Types are not necessarily seen as sets though.)

You did not, you mere stated it without any supporting evidence.

I you want to think that then fine, but I see this discussion is going nowhere so this will be my last reply.

set membership is conventionally seen as a relation between two sets.

It is not. Do you have any supporting evidence for such bizarre claim ?

Are you intentionally being daft? Here are some quotes from a random sample from the library: "∈ refers to a relation between two sets" (The Theory of Sets and Transfinite Arithmetic, Alexander Abian), "The primitive notions of set theory are "set" and the relation "is and element of" (Set Theory, Kuratowski & Mostowski), "∈ [is] a binary relation [...] called the element or membership relation" (Set Theory For Mathematicians, Rubin). One can find plenty more.

Ok, if you cannot explain what kind of similarity you mean, let's skip it.

I explained it in the first post, but if that is your explanation for your lack of desire or ability to read my posts then so be it.

["is a subset of"] is not *defined* as [a relation].
[...]
∋ is neither [a special operator nor a relation].

Alright, what are they according to you?

I would say that the predicate formulas are the different, but the predicates (properties) they express are the same

What is 'the predicate property' ? What does it mean to 'express predicate property' ?

But how would you explain/describe the difference between predicates and sets?

A predicate can be interpreted as a set in some model. The predicate (x e I) & ( mod(x,2) = 0), a meaningless string of characters without interpretation, is interpreted as a set of even integers in the default model.

Define what characteristic function in terms of what and why? The characteristic function corresponding to any set {x ∈ A | M} is (λ x : A . M).

Obviously in terms of functions and their applications.

You can have a notion of a collection perfectly well

If you have 'a notion of a collection perfectly well', what's the point of using 'function' as a building block ? It's either cheating or at least unnecessarily redundant since one can easily construct a function from a collection, but apparently not vice versa (at least *you* did not show how).

What set would the function Lx.xyz would correspond to ? What function would correspond to the predicate (x e I) & (x > 0) ?

"you merely stated it without any supporting evidence"

I you want to think that then fine, but I see this discussion is going nowhere so this will be my last reply

In a sense, that's a perfectly fine reply to a request of providng any supporting evince to you argument that a function is somehow defined ambiguously.

Are you intentionally being daft? Here are some quotes from a random sample from the library: "∈ refers to a relation between two sets" (The Theory of Sets and Transfinite Arithmetic, Alexander Abian), "The primitive notions of set theory are "set" and the relation "is and element of" (Set Theory, Kuratowski & Mostowski), "∈ [is] a binary relation [...] called the element or membership relation" (Set Theory For Mathematicians, Rubin). One can find plenty more.

The first description (that you used in your previous message) is obviously incorrect because it excludes elements that are not sets from being elements of a set (which is truly bizarre). You misunderstood the other two quotes: is_a member is interpreted as a relation allright, but it's not *defined* as such, it cannot be defined at all since it's a primitive notion. Similarly, in your favourite function theory, you would not define 'application' and 'function', but use those as primitives.

Alright, what are they according to you? [subset and set membership]
As I wrote before :
"
Loosely, for any sets A and B where B is a member of A, there exists set C whose elements are members of B and some predicate P holds, C = { (B is a member of A) and P }. Such C is called a subset of B.
"

Set membership is a two argument predicate in the first-order logic. It is *interpreted* as a relation between an element and a set in some model of set theory after the notion of relation itself is defined.

Disclaimer: I am not a mathematician. I only have undergraduate (Bacholors) degrees, so take the following with a grain of salt.

The first description (that you used in your previous message) is obviously incorrect because it excludes elements that are not sets from being elements of a set (which is truly bizarre).

I'm not so sure about that, at least in ZF. As I understand it, ZF (which is very formal) basically assumes, as intuitive, two ideas:

1. A set is an aggregate of elements.
2. If a particular element a member the aggregate, we say it is an element of the set.

Note that we don't really say what those elements are, but since ZF hasn't really assumed or proven (or even speculated the existence of) anything except for the set (specifically the empty set, from the axiom schema of specification), it is not unreasonable to assume that everything in ZF is a set. In fact ZF builds from this simple base (just the set and set membership) along with axioms describing sets and their behavior, the Natural numbers, along with other concepts fundamental to the rest of mathematics, which then means, all of mathematics can be build up from these simple ideas. (Do you have a warm fuzzy feeling inside yet?).

Now, the question in my mind isn't concerning the possibility of building up a foundation for mathematics from another idea (for example the Lambda Calculus), for I am convinced that it certainly is possible---and all you would have to do is show that it is possible to build up the equivalent of ZF and you could get the rest for free. The question in my mind is: are the base objects of these other systems (LC, CT, whatnot) intuitive enough to form the foundation? The whole point of foundations (as I see it) is to demonstrate that all of mathematical knowledge can be build from simple, intuitive ideas. Is the basis of LC, the function, intuitive enough to be understood without resorting to the use of something else, like sets, for example? I'm not convinced. I can easily grasp the concept of a set, and set membership without having to define function or relation. I'm not so sure I can imagine the idea of a relation without imagining sets. Note: this may be cultural, i.e. I may be biased because whenever I learned about relations and functions in school, they were defined in terms of sets.

To get back to the original question: Mathematicians make distinctions between sets, predicates, and their characteristic functions because they are different (equating them would introduce circular definitions into mathematics) and because it makes set theory much more simple. Since set theory is mostly about foundations, mathematicians are interested in having a very simple, intuitive (read visual, because the human mind is really good at visual processing) base from which to build of a foundation.

"
The first description (that you used in your previous message) is obviously incorrect because it excludes elements that are not sets from being elements of a set (which is truly bizarre).
"

I'm not so sure about that, at least in ZF. As I understand it, ZF (which is very formal) basically assumes, as intuitive, two ideas

You are quite right with respect to ZF. Its universe consists only of sets. However, the blanket general statement that 'e' refers to relationship between sets is still strange because it would preclude us from talking about things like 'a set of apples' or 'a set of whatever which is not a collection' in contexts other than that of ZF.

Also, there are alternative axiomatizations that admit elements that are not sets which are called 'urelements'. E.g. Russell's typed set theory has sets consisting only of urelements, then sets of sets consisting only of urelements, then sets of sets of sets consisting only of urelements, and so on. The Kripke-Platek set theory also has urelements.

[...]
The question in my mind is: are the base objects of these other systems (LC, CT, whatnot) intuitive enough to form the foundation? The whole point of foundations (as I see it) is to demonstrate that all of mathematical knowledge can be build from simple, intuitive ideas.
[...]

I agree with the rest of what you've written.

You cans define integers in LC as Church numerals.

...natural numbers but a construction of the set of natural numbers. I'd like to see what such a thing would look like in the proposed framework. In ZF I know not only how to construct individual naturals but also how to construct the set of all of them. (You show how to build the set inductively and the axiom of infinity says that such a scheme is a valid way to define a set.)

One can get two possible answers:

1. since the notion of set is absent from LC, the question is meaningless. That would contradict "...Set Theory [is] a special case of Lambda Calculus";

2. One has to import the language of set theory into LC in order even to be able to talk about sets. That would also contradict the OP's assertion since LC is presumably self-sufficient as a foundation of math and does not need any additional vocabulary.

I hope the OP might be able to clarify how a set in general and the set of integers in particular can be defined in LC.

...with its characteristic function so I was hoping to see such a characteristic function.

I'd then like to see how the axioms of set theory can be derived from those of lambda calculus.

And it may be that I'm asking for a lot. But as the OP seems to be offering a complete working replacement for ZFC I think these are reasonable things to ask for.

I think this discussion is going off the rails a little bit...

As far as defining a characteristic function for the set of natural numbers, we could first construct the Church numerals and boolean values, and we could then define a function which, when applied to a Church numeral returns T, and returns F otherwise. I don't immediately see how to write such a function, but I'm willing to believe that it's possible, and I'm not willing to spend a lot of time on it.

The general idea of using lambda calculus as a foundational formalism for mathematics is "neither dead nor ended" (see discussion beginning on page 12), although I think current attempts look a lot different from the scheme presented in the original post, as Marc and Neel hint at in their comments. This paper by Klaus Grue looks quite interesting, although I haven't found time to read it yet. A recent discussion on Martin-Löf Type Theory might also be helpful.

(As an aside, I'm not sure I'm willing to admit that sets are more intuitive than functions, either. I recall some research indicating that the cognitive (or was it cultural?) development of the natural numbers may be based on isomorphisms between physical objects more than abstract notions of counting that we take for granted. However, I can't seem to find anything related to this, so I'm certainly not willing to make any definite claims. But I would say that "groups of things" and "mappings between things" both seem very intuitive, while the mathematical notions of set and function both seem very abstract and rarefied.)

OK, let's assume that a set is defined as a function:

"A set is function such that ..."

Could you provide such, more or less formal, definition ? Also, how would you define set equality based on the above definition ?

Re. integers. It's quite easy to define the set of integers using set theory basic concepts. Yet, you find it non-obvious how to do the same in the "function theory".

The general idea of using lambda calculus as a foundational formalism for mathematics is "neither dead nor ended" (see discussion beginning on page 12), although I think current attempts look a lot different from the scheme presented in the original post, as Marc and Neel hint at in their comments.

I am not saying that using building math foundations with the function as a basic block is impossible, it's just unclear what advantages if any such approach would offer in comparison to the traditional set theory.

E.g. in "Lambda calculus as a foundation of mathematics" you've referenced, Grue has to add the following basic notions to that of the function:

o a non-function which is used to represent truth
o another element which is neither a function or the non-function but is used to represent somewhat mysterious "infinite looping".
o Adding this non-function non-non-function element violates 'tertium non datur'.

Compare this quite involved collection of the 'basic' notions with the set theory primitives, 'set' and 'membership'.

As I wrote earlier, apparently, the intuitive notion of the set as a collection of objects is accessible virtually to everyone. You can explain to a 5-year old what a set is by relying on analogies like a deck of cards or a pack of wolves. How would you explain what a function is to a person who never heard of the word no matter how old he is ? What would you say the intuitive basis for the function is?

I'm not sure I'm willing to admit that sets are more intuitive than functions, either.

And yet, you cannot give a definition of the set of integers (which is in itself a pretty basic notion) that would rely on a presumably more intuitive notion of 'function'.

Grue summarises succinctly at the start of his paper:

"lambda-terms have shown very useful for expressing semantics in computer science, but there has been no natural choice of a theory of reasoning about these lambda-terms".

No surprise then that mathemticians generally don't use lambda calculus.

Later on he deals specifically with the OP's question:
"It is tempting...to represent classes by their characteristic functions. This approach has not succeeded."

He does not say why this representation has not succeeded and does not provide references about this either. (Or does he refer to the first sentence you quoted?)

You can explain to a 5-year old what a set is by relying on analogies like a deck of cards or a pack of wolves. How would you explain what a function is to a person who never heard of the word no matter how old he is ? What would you say the intuitive basis for the function is?

Since when is the opinion of five-year olds decisive for foundational issues? `Intuitiveness' should never be be the criterium for deciding mathematical questions. Jerry Bona once joked that mathematicians consider the Axiom of Choice to be intuitively true, the Well Ordering Principle intuitively false, and are unclear about Zorn's Lemma (even though they are logically equivalent).

Formalisms have to rely on some intuiton, how can it be otherwise ? Saying that a 5-yer-old can understand what a set merely emphasizes how simple the original intuitive idea is.

But you did not comment on what kind intuition you can offer for the function. Could you do that ?

Simple. Functions have existed far, far longer than sets. Further the Set theoretic definition of function was not very palatable in the beginning as one tended to think of a function as a rule providing an output for a given input and not as just a table of input/output pairs. Often "function" implicitly (or explicitly) is used to mean smooth function (or nice is some other way).

Set theoretic definition of function was not very palatable in the beginning

What evidence can you offer to support that statement ?

think of a function as a rule providing an output for a given input

And how is this description different from the set theoretical one except being extremely informal ? How 'given input' is different from what is now called 'domain'/'set of input values' and 'output' from 'co-domain'/'set of output values' ? You have the same pairs but in the set theory they are defined more clearly than in your informal description.

If that's the intuitive function undrstanding, it's unclear how you can divorce it from the notion of collection/set and define collection/set in terms of functions.

You can't equate functions and their graphs, unless you have a Cantorian hierarchy of transfinite sets. The decision to do so is not a simple one, and it has highly nontrivial consequences, not the least of which is the existence of non-computable functions!

However, you can equate functions and effective procedures, so that a function is a finite recipe for transforming a value in the input domain to a value in the output. Then it turns out you don't need a Cantorian hierarchy: everything remains countable, because a recipe is a string, and there are only countably many of those. This is not a simple choice, either -- it leads you to constructive mathematics.

If you tell me that anything about the foundations of math is intuitive, I won't believe you. We face a lot of different choices, each one leading to deep, subtle and fascinating consequences, and possibly each is suited to illuminating a different kind of mathematical practice.

If you tell me that anything about the foundations of math is intuitive, I won't believe you.

It's an odd statement -- sets most certainly are, as is the notion of membership, as is cumulative hierarchy. That's all you need );

Saying, that one considers foundations unintuitive almost makes the whole body of math meaningless [in the sayer's mind].

What does all this have to do with programming languages, anyway?

But the points I wanted to make are:

• One person's intuitive is another's gobbledygook.
• Just because something appears to be intuitive at first glance does not mean it will remain intuitive when you start actually studying its details.

None of those things are intuitive.

Let's start with the notion of membership. Informally, we say an element x is a member of a set if we can look at the set's elements and find one that's equal to x. Easy, right?

Not at all! It's utterly unclear to me that this procedure works in general. Consider the case of a set with countably infinitely many elements -- can we really test membership? It would take an infinite amount of time to check whether an element is in it or not, and it seems like an abuse to say, "We can check membership, but it will take infinitely long to do so." Is this really a capability to check membership?

This objection also applies if you consider the possibility that the elements of a set might themselves be infinite objects. Comparing them for equality is questionable, for the same reasons as before, and so this means that the principle of cumulative hierarchy comes into question.

It's quite easy to define the set of integers using set theory basic concepts. Yet, you find it non-obvious how to do the same in the "function theory".

Given an initial member "0", the recursive closure of the function f n = n+1.

Also, how would you define set equality based on the above definition

Check out the standard approaches from category theory.

Given an initial member "0", the recursive closure of the function f n = n+1.

I think it won't do because 1) you did not define "recursive closure" as a set; 2) the expression is in untyped lambda calculus which is not suitable for foundations.

Check out the standard approaches from category theory

Could provide an example of the set definition as well as set equality defined in CT terms ?

Besides, we were talking about set equality in terms of functions, not in terms of CT.

Could provide an example of the set definition as well as set equality defined in CT terms ?

Try section 5 of this paper which outlines how to construct a local set theory using a topos. Note that I am not agreeing with the claims of the original post, merely noting that there do exist some reasonable theories to construct set theory using category theory.

Try section 5 of this paper which outlines how to construct a local set theory using a topos.

He talks about replacing the notion of set with that of type, introduces the language and types and then defines 'local set theory'.

The problem with using CT as foundations is that it requires quite a lot of 'primitive' baggage in order to just get started:

E.g. notion of topos presupposes understanding of the notion of category
which in its turn relies on the notions of collection and function. None of these is simple or intuitive with the exception of collection.

Also, in its expositions, CT eventually returns to the notions of collection (collection of arrows, objects, classes, etc). So if we are already dealing with collections as primitives, why bother and talk about topoi, functors and such if the collection/set language is quite adequate for foundational purposes ?

Of course, there is no denying that the language of CT is quite useful in its appropriate areas.

CT is subservient to at least some level of set theory - you do need some concept of collection. I think the aim with CT as a foundation is that it requires far less in the way of set theory to proceed: you can use a very simple theory that carries concepts of collections and don't require the extra machinery of classical set theory.

As to how intuitive the notion of "function" is - I think there's room for debate there, certainly with regard to arrows as defined in category theory (as opposed to classical functions). It's really just a conception of relationship between two objects (the domain and codomain) with the axioms that the relations be composable, and that composition be associative. A classical definition of function, on the other hand, is more of a higher level concept.

Finally, I tend to see any foundation that can be shown to provie equivalent constructions as merely a matter of convenience. Perhaps that's the mathematician in me coming out, but I really don't believe there's a "correct" or "better" description or expression - merely a particular one that suits the task at hand. As you say Category theory has it's uses, and foundations explained in terms of CT can provide a good framework from which to look at some problems. At the same time a set theoretic foundation has already proven to provide a good language and framework with which to discuss things. I don't see either as being "inferior", merely different and both useful.

I suspect we probably agree

We mostly do.

I think the aim with CT as a foundation is that it requires far less in the way of set theory to proceed: you can use a very simple theory that carries concepts of collections and don't require the extra machinery of classical set theory

Right, but it does require much more involved conceptions *in addition* to the 'plainer' set. None of those notions is very intuitive and in my opinion cannot be understood without substantial previous mathematical experience to lean on(as opposed to the classical set theory). However, I readily admit that I may be missing something in the CT-qua-foundations approach.

Try Conceptual Mathematics by Lawvere. It's a math text targetted at high school level (or lower), yet works in terms of category theory. It doesn't provide a Category theoretic foundation for math, but is interested in introducing fundamental concepts of category theory (like arrows) as fairly natural and intuitive concepts. I agree that arrows are a more complex notion than set membership, but they are, in many ways, simpler and more natural than classical conceptions of functions, and not that hard to work with even with very limited mathematical experience.

In many ways how "hard" a concept is to understand is, in a large part, related to how well acquainted you are with it. Negative numbers were, at one time, an extremely complex and hard to grasp notion. Few people find them so now due to increased exposure to them. Likewise I think many CT notions are relatively natural but due to lack of exposure they seem more complex than they perhaps actually are.

Thank you, I'll take a look. I derive my understanding of CT as foundations from the Saunders McLane book.

Not disagreeing with you, but from sheer curiosity, could you give an intuitive reference for the formal notions of 'function' and 'arrow', and why the latter is simpler that the former ? I am interested mainly from the teaching point of view. Clearly, one cannot rely on collections or sets, or things like 'a function is like mapping between two things' because it would be essentially falling back on the notion of collections/sets.

The biggest difference between classically defined functions and arrows in CT is that a function requires some notion of the internal structure of its domain and codomain - that is, in fact, what it is: a pairing of elements from the domain with elements from the codomain. An arrow, on the other hand is simply pointer, or relationship, from one object to another. All we require of arrows is that we can (when it makes sense) compose them, and that that composition is associative (which is a very natural condition really). This sort of thinking arises naturally if you wish to study objects by considering how they relate to things around them, with arrows being those relationships. It is possible to arrive at this notion without having to go through a construction of a classical function considering internal structure of an object.

One of my tutors from my student days years ago was involved in an ongoing 'feud' with Saunders Mac Lane over the relative merits of the set theoretical view of things and the categorical view. I recommend section 10 of his paper "The Strength of Mac Lane Set Theory" here: http://www.dpmms.cam.ac.uk/~ardm/ . There is also "What is Mac Lane Missing?" which was also replied to by Saunders Mac Lane. Unfortunately the latter seems only to exist in printed form.

I recommend section 10 of his paper "The Strength of Mac Lane Set Theory"

An interesting read, sigfpe, but I would like to draw your attention to a particular passage:

Indeed I would view with suspicion any claim by anybody to have an account of the whole of mathematics, because I believe that mathematics flows from at least two distinct intuitions, and that the balance between these intuitions will be different in different mathematicians.

I expressed a similar sentiment at the beginning of the thread

I don't think that ANYONE on the CT "side" here has expressed anything incompatible with this sentiment. The "side" you seem to have supported earlier in this thread, on the contrary, is the one that can't conceive of anything mathematical going on that isn't set theoretic.

I think PL enthusiasts have enough of our own pointless, petty feuds (you know what topic I mean...) without importing some from the mathematical community. ;-)

My side is only the side that says that it's highly non-trivial to build a foundation for mathematics built on identifying sets with their characteristic functions. I think this is a perfectly good answer to the question "can somebody tell me why mathematicians keep making a distinction between sets, predicates and their indicator functions".

My complaint is not that someone wants to relegate sets to second class citizenship, but that the scheme they propose for doing it is problematic. As the Grue paper mentioned above points out (though I haven't read the whole thing, I'm going on trust here) - you can happily found a large chunk of mathematics in lambda calculus (plus a few additions) by using a different scheme to encode sets. I'm all for using whatever scheme you want to do mathematics, as long as it generates useful and interesting results and isn't plagued with contradictions.

For those who might be interested, though not all too relevant, I ran across this paper recently with the following pointed abstract:

If a category B with Yoneda embedding Y : B → CAT(B^op,set) has an adjoint string, U -| V -| W -| X -| Y, then B is equivalent to set.

1) you did not define "recursive closure" as a set

My point is exactly to show that you don't need the notion of set to define the natural numbers: you can take the notion of function as a primitive and define them that way.

2) the expression is in untyped lambda calculus which is not suitable for foundations

I wasn't using LC: I was offering a simple, self-contained way to enumerate the natural numbers without recourse to set theory using only the notion of a function.

As Neel said, foundations of mathematics are deep waters with plenty of undertow. To assume that only one approach, i.e. set theory, is adequate is likely to result in drowning in them.

My point is exactly to show that you don't need the notion of set to define the natural numbers: you can take the notion of function as a primitive and define them that way.

I regret to say but you showed no such thing.

I wasn't using LC: I was offering a simple, self-contained way to enumerate the natural numbers without recourse to set theory using only the notion of a function.

If you were not using LC, then the phrase

Given an initial member "0", the recursive closure of the function f n = n+1.

... is meaningless. In order to make sense of it, you need to define:

o a number
o '0'
o '+'
o 'recursive closure' in terms of 'function'

I'm familiar with the notion of recursive closusre as applied to a set. Take the set {0} and then form the union of f{0}, ff{0}} and so on. How do I do this with indicator functions? Given the indicator function for a set A, and a function f, how do I write the indicator function of the recursive closure of A with respect to f?

And how do I write the indicator function of the set {0} to get the ball rolling? Nobody is letting drop even the slightest clue. As a mathematician I'm pretty familiar with set theory. On the other hand my knowledge of computer science and lambda calculus is pretty scanty. Can't someone actually construct one of these functions for me from first principles?

Given the indicator function for a set A

You cannot have the indicator function for a set because 'set' simply is not in your basic vocabulary. In an exposition I am familiar with, a set *is*/defined as an [indicator] function. Then set membership is defined and subsequently the treatment pretends that it deals with ordinary sets and set membership. There is of course a bunch of axioms as well.

When I say "the indicator function of a set A" I mean the function in this proposed new system that behaves like the set A in the old system.

If someone says there is some kind of functional recursive closure corresponding to the set-theoretical one I'd like to see it. I'd like to see any of the functions I've asked for actually.

If someone says there is some kind of functional recursive closure corresponding to the set-theoretical one I'd like to see it. I'd like to see any of the functions I've asked for actually.

I am curious too ;)

In an exposition I am familiar with, a set *is*/defined as an [indicator] function.

What exposition would that be?

Unfortunately, I do not remember the reference, but it was an exposition of some alternative (to ZF) set theory which was restated in terms of functions (up to defining 'set' and 'set membership' and re-using the earlier stated set-theoretical stuff).

Take the set {0} and then form the union of f{0}, ff{0}} and so on. How do I do this with indicator functions?

I get the feeling that you are using the formal notion of "set" and the informal notion of "collection of things" (in this case the natural numbers) interchangeably.

You can generate the natural numbers with these axioms:

1) 0 is a natural number
2) there is a function f such that if n is a natural number f n is a natural number

These aren't the axioms of set theory and they don't refer to sets, though implicitly the natural numbers form a collection of objects.

There are other ways of defining the natural numbers without sets (e.g. there is a standard on in CT); I'm not sure why this strikes anyone as a shocking idea.

I get the feeling that you are using the formal notion of "set" and the informal notion of "collection of things" (in this case the natural numbers) interchangeably.

Your feeling is wrong. The above is a loose exposition of the standard set-theoretical construction of integers satisfying ZF axioms.

You can generate the natural numbers with these axioms:

1) 0 is a natural number
2) there is a function f such that if n is a natural number f n is a natural number

Those are *not* natural numbers. Let f(n) = 0. You 'natural numbers' consist of one element '0'.

There are other ways of defining the natural numbers without sets (e.g. there is a standard on in CT);

What specific "standard [of defining natural numbers] in CT" are you referring to ?

Your feeling is wrong. The above is a loose exposition of the standard set-theoretical construction of integers satisfying ZF axioms.

Yes, I may have studied some Set Theory myself. However, the whole point of this discussion is to define mathematical concepts, such as natural numbers, WITHOUT relying on the definitions or axioms of Set Theory.

This can be done, it has been done, it can be done several ways. This doesn't diminish Set Theory; it enriches mathematics.

Those are *not* natural numbers. Let f(n) = 0. You 'natural numbers' consist of one element '0'.

If you read the definition more carefully you will see that the proposed axiomatic system asserts that 0 is a "natural number" (the mathematical concept being defined), and by the second axiom therefore so is f0 and ff0 and fff0, etc. Just as ω "is" the natural numbers because it contains one element that can be mapped uniquely to every natural number, so too the infinite chain of applications in this simple system maps one nesting level of application to each natural number.

This is exactly analagous to the Set Theory example, just without relying on the set-theoretic axioms.

What specific "standard [of defining natural numbers] in CT" are you referring to ?

See Wikipedia for a simple introduction.

The OP claimed that sets could be replaced by their indicator functions. I asked for how this could be done for the integers. You proceeded to say something about constructing the integers that is essentially an application of the Axiom of Infinity from ZF and made no suggestion of what the indicator function might look like. Am I correct in interpreting this as meaning that you don't know what such an indicator function would look like?

Why is everyone avoiding the issue?

Apparently, it's not so easy as proponents of function-based foundations would like us to believe. ('us' is an impersonal pronoun here);

Do you think so? ;-)

"Apparently, it's not so easy as proponents of function-based foundations would like us to believe. ('us' is an impersonal pronoun here)"

It's rather trivial to axiomatize set theory with function application as primitive instead of membership. This is how von Neumann originally presented the system of set theory that is now known, in a form based on classes and membership rather than functions, as von Neumann-Bernays-Gödel set theory.

In von Neumann's system you have two kinds of functions: those that can be arguments to functions and those that can't. This corresponds to the more familiar distinction between sets and proper classes. There are two special primitive objects A and B, and a collection X is identified with its characteristic function f(a) = A if a \in X and f(a) = B if a not \in X. It is also postulated that a function can be an argument to another function if and only if there is no bijection between those a for which the function yields A and the collection of all functions that can be arguments, which in set theoretic terms means that a class is a set just in case it's not equipollent to the set theoretic universe V. In addition, we need the axiom of infinity and power set, the rest of usual set theoretic axioms - including global choice - follow from the "limitation of size" axiom, and a bunch of axioms for general function existence carefully crafted so that for formula with all bound variables restricted to functions which can be arguments there is a function yielding A for exactly those functions which can be arguments of which the formula holds.

I rather doubt the original poster had anything like von Neumann's system in mind, though.

It's rather trivial to axiomatize set theory with function application as primitive instead of membership. This is how von Neumann originally presented the system of set theory

Right, but he himself said that it was rather a technicality. The characteristic function is just a euphemism for membership:

Define: A set is function C such that for all x f(x) = A or f(x) = B.

The question is what are "all x" if not elements (or function-encoded elements) of some collection ?

Right, but he himself said that it was rather a technicality.

Indeed.

The characteristic function is just a euphemism for membership:

Define: A set is function C such that for all x f(x) = A or f(x) = B.

Sure, but this argument cuts both ways, and we can with equal justification say that membership is just euphemism for application yielding A. Functions as conceived in von Neumann's system and sets as usually conceived are trivially mutually interpretable.

The question is what are "all x" if not elements (or function-encoded elements) of some collection ?

This I don't follow at all.

membership is just euphemism for application yielding A

What intuitive picture should one lean one when one talk about application ? Application of what to *what* ? (supposing one needs to be introduced to math with 'application' as a primitive notion).

The question is what are "all x" if not elements (or function-encoded elements) of some collection ?

This I don't follow at all.

What is the thing the characteristic function is applied to ?

Application of functions to other functions, obviously, just as in the set theoretic picture we have membership of sets in other sets. The characteristic function is thus applied to other functions, namely those functions that can be arguments.

However, the whole point of this discussion is to define mathematical concepts, such as natural numbers, WITHOUT relying on the definitions or axioms of Set Theory.

This can be done, it has been done, it can be done several ways.

And yet, you are unable to provide such definition [of the natural numbers], but just keep on saying that there is one.

If you read the definition more carefully you will see that the proposed axiomatic system asserts that 0 is a "natural number" (the mathematical concept being defined), and by the second axiom therefore so is f0 and ff0 and fff0, etc.

Your 'axiomatic' system states that
1. 0 is a natural number
2. there exist a function, f(n), such that if n is a natural number f(n) is a natural number too.

Now, let's choose f(n) = 0. Clearly, such function trivially satisfies (2). It's easy to see that f(0) = 0, f(f(0))=0, and so on. So your system consists of a single element '0' which is obviously not what is understood as natural numbers. It's odd that you do not see that and yet insist on talking about CT as foundations.

See Wikipedia for a simple introduction [to natural numbers defined in CT]

What specific simple introduction do you have in mind ?

A "natural number object" in a category is an object N, and a pair of arrows z : 1 -> N and s : N -> N such that for all q : 1 -> A and f : A -> A, there exists an arrow u : N -> A with the property that u o z = q and u o s = f o u. (Read the 'o' as function composition.)

If you work through a few examples, you'll be able to see that this is equivalent to having zero and successor, and an induction principle.

A "natural number object" in a category is an object N, and a pair of arrows z : 1 -> N and s : N -> N such that for all q : 1 -> A and f : A -> A, there exists an arrow u : N -> A with the property that u o z = q and u o s = f o u.

If you mean Lawvere's natural numbers, then before constructing N, he has to :
o define terminal and initial objects (1, 0);
o explain what it means for a diagram to commute and define (co)products, (co)equalizers via specific diagrams;
o introduce eight axioms asserting:
o terminal/initial object existence
o exponentiation existence requiring the notion of adjoint functor
o existence of a distinguished object N with its own commuting diagram
o axiom of choice
o three axioms mimicking Peano axioms
o prove recursion theorem

All this heavy machinery is no comparison with the five Peano postulates which look almost trivial in comparison.

What's also disturbing is that instead of just two basic notions (set and membership), he has to introduce as undefined :

o mappings (arrows)
o domain and co-domain
o composition

Further, he says that the intuition for mapping is as follows: "mapping f consists of three parts a set S, a set S' and a rule which assigns to every element of S exactly one element of S'". Sounds quite set-theoretical.

The axioms of category theory (obviously), the existence of a terminal object, and the existence of an N, s, and z satisfying neelk's definition (with perhaps a "unique" thrown in) is all that is necessary to say that a category has an NNO.

As for Lawvere, I'm not sure what you are citing but most applications and formulations of category theory are not trying to be foundational. They readily use sets.

I'd really like to know what you are reading or what the context you are reading is w.r.t that last quote. Most introductions to category theory make it quite clear that arrows, "mappings", are not necessarily functions (though functions are a familiar example). Nor are the objects sets. An arrow between A and B which are just arbitrary elements of Ob(C) is just an element of Hom(A,B). For example, given a poset (P,<=) you can make a category C by having Ob(C)=P and for each a and b in P Hom(a,b) is a singleton set if a<=b and empty otherwise. In this example, a and b are not (necessarily) sets and an arrow between can't be a "mapping" as you suggest.

"
and the existence of an N, s, and z satisfying neelk's definition (with perhaps a "unique" thrown in) is all that is necessary to say that a category has an NNO.
"

According to Lawvere and Mac Lane, you need much more in order to prove that Peano's axioms hold for N (see the reference). Do you have a reference to an alternative presentation ? How do you prove the recursion theorem (required to prove that N satisfies Peano's axioms) with neelk's kind of N ?

Also, what do you mean by "with perhaps a "unique" thrown in" ? Anyway, a reference (other than Lawvere's) would be much appreciated.

"
I'd really like to know what you are reading or what the context you are reading is w.r.t that last quote.
"

http://138.73.27.39/tac/reprints/articles/11/tr11.pdf

"
but most applications and formulations of category theory are not trying to be foundational. They readily use sets.
"

Offering alternative foundations was what this thread originated with. The OP suggested functions, and the discussion quickly progressed/degenerated ? to CT as foundations. As to Mac Lane and Lawvere, both of them suggested CT qua foundations at one time or another (see the reference).

"
can't be a "mapping" as you suggest
"

Not me but Lawvere (see the reference), besides it depends on how you define 'mapping'.

In any case, my point was that for simple stuff like systems satisfying Peano axioms using CT machinery does not seems not very elegant or reasonable unless one aspire to use CT foundationally.

Lawvere carefully says ETCS “provides a foundation for mathematics . . . in the sense that much of number theory, elementary analysis, and algebra can apparently be developed within it.” This aspect relies entirely on the elementary axioms. But he did not claim that such formal adequacy makes ETCS a formalist or logicist starting point for mathematics, as if there was no mathematics before it. He says that ETCS condenses and systematizes knowledge we already have of “the category of sets and mappings. . . denoted by S” (pp. 1-2).

So a) this paper is about formalizing the category of Sets, it is no wonder that the arrows are sound suspiciously like Set mappings! This is why I asked for either the paper or the context, in this context arrows are mappings. This paper is not an introduction to category theory. With regards to your other reply, you could embed the elements into sets and have functions between them ([editted a bit crazy before] make the set of lower sets {a | a said and nor is that necessary. Even formalizing category theory using sets there's no reason to attempt to map arrows to functions; it makes fine sense (almost) algebraically. What you are doing is like trying to fit multiplication of a group, say, into composition of functions. You can, but that is irrelevant; there's no reason to identify elements of a group with sets and multiplication with composition.

As for the NNO, as I said what neelk listed (and the things his (the) defintion clearly assumes) is what is necessary to say that a category has an NNO. This is true... by definition. (With regards to the "unique" simply replace "exists an arrow" with "exists an unique arrow" and that is what I was referring to. These axioms work for all categories and have no irrelevant structure, i.e. having a member of the number 3 is not what one thinks of as part of the structure of numbers. If I say that Set has an NNO, then the NNO will be (up to unique bijection) the natural numbers. Another quote from the paper you read:

Paul Benacerraf made the question prominent for philosophers one year after (Lawvere 1964). The two were no doubt independent since philosophers would not look in the PNAS for this kind of thing. Benacerraf argued that numbers, for example, cannot be sets since numbers should have no properties except arithmetic relations. The set theory familiar to him was ZF, where the elements of sets are sets in turn, and have properties other than arithmetic. So he concluded that numbers cannot be sets and the natural number structure cannot be a set.

Further, reading the paper myself, I still have no idea how you get the ideas that you have. The third axiom is exactly that this "Set" category has an NNO (just as neelk defined it plus the "unique"). It immediately proves primitive recursion (much as you would with a foldNat function which is essentially what the axiom assumes). The whole paper isn't about defining the NNO, for example, the Axiom of Choice is completely irrelevant to it. The Peano Axioms do not axiomatize sets, yet you seem to want to compare an axiomatization of Sets somewhat detached from Set theory to an axiomatization of natural numbers assuming set theory, by your logic I could say that you too have to have the Axiom of Choice beyond Peano's Axioms to define natural numbers (if you were simply working in ZFC). Most of the other things you list are explanation or are irrelevant to defining natural numbers. He does not need to spell out what a terminal object is (or a coequalizer, etc.) he does this because this is more than just a listing of axioms.

So a) this paper is about formalizing the category of Sets, it is no wonder that the arrows are sound suspiciously like Set mappings!

If the article is about formalizing sets in terms of categories, why does it rely on the set intuitions ? What's the point of such theory if it imports sets intuitions ? Instead, it should have said something like "we have arrows and domains and codomains and sets are just another name for domains/codomains". Apparently, the problem is that there is no comparable intuition for arrows and when category theorists talk about "codomains/domains" they use the euphemism "collection".

It's interesting that McLarty, whom you've quoted, carefully avoids talking about CT as foundations. Both Lawvere and Mac Lane had foundational hopes w.r.t CT in late 60s as did McLarty in late 90s although the latter was talking about importing natural numbers in toto from the set theory (which again raises the question what's the point ?).

The third axiom is exactly that this "Set" category has an NNO (just as neelk defined it plus the "unique"). It immediately proves primitive recursion.

That does not make any obvious sense. How NNO can "prove primitive recursion" ? NNO is just an object in some category with a bunch of arrows. How can an object prove anything ?

(much as you would with a foldNat function which is essentially what the axiom assumes).

It does not make any sense either: 1. CT has no notion of foldNat; 2. axioms in general, and the NNO one in particular, do not "assume" anything, they *are* [theory-specific] assumptions.

by your logic I could say that you too have to have the Axiom of Choice beyond Peano's Axioms to define natural numbers (if you were simply working in ZFC).

No, you could not because you have not.

As to "neelk's NNO":

A "natural number object" in a category is an object N, and a pair of arrows z : 1 -> N and s : N -> N such that for all q : 1 -> A and f : A -> A, there exists an arrow u : N -> A with the property that u o z = q and u o s = f o u.

1. Assume there is a singleton category Single(N) with N as its single object and the identity arrow as its single arrow.
2. Prove N is NNO: obvious
3. Does it represent the totality of natural numbers ? No.

Since you are clearly not reading what I'm writing (proof, the very first thing in the big blue blockquote answers both of your first questions), I will return the favor.

Missed this first time:

For example, given a poset (P,<=) you can make a category C by having Ob(C)=P and for each a and b in P Hom(a,b) is a singleton set if a<=b and empty otherwise. In this example, a and b are not (necessarily) sets and an arrow between can't be a "mapping" [....]

Why not ? It's trivial to imagine a class of functions with singleton sets 'constructed' from the elements of the original P as domains and codomains: { {(x,y)} | x e P, y e P, x <= y }. How is it different from arrows ?

You don't need set-theoretic intutions. Think of the objects as types, and the morphisms as total functional programs between those types. NNOs in this case would be the type of natural numbers, the zero constructor, the successor constructor, and the fold function. Roughly, think of the following ML program:

datatype nat = zero | succ of nat

fun iter z s zero = z
  | iter z s (succ n) = s (iter z s n)

(The analogy is imprecise because ML has side-effects; in a purely functional language it would be completely precise, and nat would be an NNO in the syntactic model formed from the language.)

It should be clear that such an intuition is non-set-theoretic, because there's no room in it for the powerset axiom or consequently the cumulative hierarchy -- the number of programs of type nat -> nat is still firmly countable, unlike the number of set-theoretic functions from the set of nats to the set of nats.

I am not talking about set-theoretical intuitions. I am just saying that your 'NNO' presentation is too simplistic. I briefly listed what axiomatic base (in addition to CT axioms) you need in order to build the structure and gave the reference where Lawvere devotes several pages to describing how to do just that, including the recursion theorem proof based on which he proves that the 0:1->N, s:N->N structure indeed satisfies Peano's axioms. Among the axioms he needs to prove the fact, is the Axiom of Choice which is pretty impressive.

In order to construct natural numbers in set theory without the Axiom of Choice, you need five lines.

To do as much as Lawvere did, you need to take the Peano axioms, and then show that the von Neumann encoding of the naturals baked into ZFC via the axiom of infinity satisfies them. Next, you need to show that every set which satisfies the Peano axioms is in bijective correspondence with the von Neumann set. It's only after all this that we can do proofs about the integers without having to commit to a particular encoding of them.

All this work is essentially the proof of the existence of an natural number object in the category of sets and functions.

1. Define: 0 is {};
2. Define: S(x) = x U {x};
E.g. 1= 0 U {0} = {0}, 2 = 1 U {1} = {0,1}, etc.
3. Define an S-closed set SC if 0 e SC and forall(x e SC)(S(x) e SC);
4. Define a natural number as an element of such set;
5. Prove that a set of naturals exists: by Infinity SC exists and by Separation omega = {x e SC| x is a natural number} exists.
6. Prove (omega, 0, S) satisfies Peano.
P1 (0 is a natural): by definition 0 is in every S-closed set.
P2 (S(n) is a natural) : assume n is in omega so n is in every S-closed set so S(n) is in S-every closed set so S(n) is also in omega.
P4 (0 is not a successor): since a successor is a non-empty set, 0 is not a successor.
P5 (induction): Obvious.

P3: (S(n) = (S(m) ==> n = m) requires about half a page but just as easy.

Compare the set-theoretic simple natural numbers encoding to the baroque Lawvere 'N' object and see how much stuff he needs in order to prove that his N satisfies Peano. His using the Axiom of Choice is especially interesting.

Next, we need to show that all sets satisfying the Peano axioms are isomorphic to the the von Neumann naturals. This is important because mathematicians must be free to change the encoding of the natural numbers to suit their proofs, and still have the results apply in general -- data abstraction is as valuable to mathematicians as it is to computer programmers.

To do this, we're going to have to define the isomorphism functions by recursion, which means we have to prove the recursion theorem to justify that definition. And the axiom of choice shows up very naturally here, because it's what you use to show that every set is well-ordered.

Everything Lawvere is doing is all perfectly natural and well-motivated from a set-theoretic perspective; it's just said in a weird way. The benefit of the categorical approach is that it works equally naturally for non-set-theoretic cases, too.

This then more than doubles the benefit, because you can use it to investigate what constructions in ZFC really mean constructively by looking at the functors between the category of sets and functions, and between the syntactic category of the lambda calculus (for example).

1. Assume (L, l0, ls) and (M, m0, ms) are two Peano systems.
2. Define ln = ls(ls(....(l0))) 3. Prove ln is different from l0,...,ln-1. Trivial by induction;
4. Prove L ={ln|n element of omega}. By contradiction (if not, contradicts P5);
5. The same can be proved w.r.t (M,m0,ms) and the sequence mn which is the required isomorphism between ln and mn.

To do this, we're going to have to define the isomorphism functions by recursion, which means we have to prove the recursion theorem to justify that definition. And the axiom of choice shows up very naturally here, because it's what you use to show that every set is well-ordered.

That does not make sense, the AC is not required to prove that.

That does not make sense, the AC is not required to prove that.

Uh? The well-ordering theorem ("every set has a well-ordering") is equivalent in strength to AC, yes. This is a member of the pantheon of theorems (along with Zorn's lemma, Hausdorff's maximality principle, Noether's theorem on finite generation, Tychonoff's theorem on products of compact spaces, etc) that are taught to beginning mathematicians as being equivalent to AC in ZF.

Uh? The well-ordering theorem ("every set has a well-ordering") is equivalent in strength to AC, yes. This is a member of the pantheon of theorems (along with Zorn's lemma, Hausdorff's maximality principle, Noether's theorem on finite generation, Tychonoff's theorem on products of compact spaces, etc) that are taught to beginning mathematicians as being equivalent to AC in ZF.

"The beginning mathematician" should know that the principle of mathematical induction is an *axiom*.

Proofs by MI have got nothing to do with AC. One can prove the principle of MI assuming AC, but no such assumption is needed for MI proofs.

"The beginning mathematician" should know that the principle of mathematical induction is an *axiom*.

No kidding? *rolls eyes*

The last sentence of Neel's paragraph that you responded to stated that proving the existence of a well-ordering for every set requires AC. So excuse me for assuming that's what you were disagreeing with...

One can prove that natural numbers are well-ordered by induction. To prove that *any* set can be well-ordered, one needs AC.

Since pure haskell is sugared lazy LC, you could define recursive closure like:

rclosure f z = (f z : rclosure f (f z))

And sets could be encoded as normalized lists, using a normalize function that removes duplicates and a is_equal function that says is two elements are equals.

Or I missing something?

I have an object in this Haskell universe. I'll call it x. How do I reason about whether or not x is in this list? What tools does the proposed alternative system have to offer that would allow me to deduce whether x is in the list?

What happens when I want to construct the set of real numbers?

And how does this respond to the original suggestion that sets be identified with their indicator functions?

I have an object in this Haskell universe. I'll call it x. How do I reason about whether or not x is in this list? What tools does the proposed alternative system have to offer that would allow me to deduce whether x is in the list?

This is why I need a function is_equal. I think it would work when you have only natural numbers.

What happens when I want to construct the set of real numbers?

You are right, it does not work for real numbers because they are uncontable infinite, is_equal never finish. Are real number set allowed in intuitionist set theory?)

And how does this respond to the original suggestion that sets be identified with their indicator functions?

Nothing. I was only thinking about how to represent the recursive closure of a set using only functions.

i'm absolutely not an expert on this, but logic associated with computing, functions, etc tends to be constructivist (at least traditionally, i believe), which doesn't include the axiom of infinity. so it may be that the best you can do is show how to construct (for example) more natural numbers than any specified number.

...and define the set containing just the number 1. As a Church numeral, 1 is the identitify function. So we need to define a function which when applied to the identity function returns true but returns false for every other argument. How do we construct such a function using the basic ingredients of lambda calculus? Once we've done this we can move on to other kinds of set.

tends to be constructivist (at least traditionally, i believe), which doesn't include the axiom of infinity

Normally its the axiom of choice that is not considered constructivist.
The axiom of infinity has a well-defined procedure for being constructed, it just would take infinite time. ;-)

This is a problem for computation, but not for mathematics.

Constructivists or maybe just Intuitionists originally did not like the Axiom of Infinity, but it has since been considered constructive.

i thought the justification for not including the law of the excluded middle was that an infinite number of tests could not be made to verify exclusion. if the axiom of infinity is included, that then imples the law of excluded middle, and it's kind of hard to see any difference between intuitionist and classical logic.

i know that there have been extensions in the field of computer science to handle continuations which have involved extensing intuitionist logic in this way. but if intuititionist logic is more than just something computer scientists use to go from types to programs and back again then i'm not sure it's fair to say that (current) intuitionist logic itself includes those extensions.

but as i said, i'm just learning this and would be glad to be corrected by a reference that taught me more.

[edit: in particular, and something that i am currently interested in, i don't see how intuitionistic logic would remain safe from godel's attack. one motivation for such an approach (which, i understand, has been used to provide a basis for most of modern maths, including measure theory) is that it provides a basis that is safe from the questions raised by godel (which requires the axiom of inifinity).]

[totally rewritten]
Bah, here's a link to a PDF titled "History of Constructivism in the 20th Century".

just seen this reply. thanks very much for that - looks really useful. cheers.

Normally its the axiom of choice that is not considered constructivist.

And for good reasons! The axiom of choice together with extensionality implies the law of the excluded middle.

[Someone needs to close an italics. Drupal should close all unclosed HTML tags at the end of a post. (I'm suggesting this, not saying that it does this.]

You may want to look at, for example, The Seven Virtues of Simple Type Theory (PDF,compressed PS)

There are more interesting looking papers, related and unrelated, here.

[The following is on edit]

Another link one may want to look at is Classical Type Theory (look down the page).

Anyway, I think much of the confusion in this thread comes from a variety of sources. Mainly the lambda calculus is used in a variety of ways w.r.t. foundations and set theory.

To start with, we can reduce naive set theory to (and maybe eta conversion too):
a in { x | P(x) } <-> P(a)
Clearly replacing this with
(λx.P(x)) a <-β-> P(a)
is just a notational variation. Naive set theory has it's problems, but applying the restrictions to it to avoid the known problems can equally be applied to this notational variation. To get the "characteristic function" defining the natural numbers simply translate the Axiom of Infinity. Obviously, from this perspective, it is trivial.

There is also type theory. Type theory is a different approach and as mentioned in the above "Classical Type Theory" there are different trade-offs, one of which is that Set Theory is rather untyped and this results in trade-offs akin to the ones between statically and dynamically typed languages. In Type Theory, as shown in the first paper I mentioned, you would have a natural number type with axioms that would characterize it as the natural numbers. We can identify a set with a characteristic function in this case, but, as in category theory, the result would be "a set of A's" and not just "a set".

A further confusion in this respect is that by lambda calculus, or the type theory, that we mean simply the good 'ole computable functions (or some subset) that we deal with or (less strongly but more subtly) that we mean some intuitionistic type theory. Neither is necessary. For example, essentially by adding equality we can get a classical and non-constructive (let alone computable) type theory. So, as I suspect some think, it is not like all math is being reduced to computable functions and programming.

You're right to say that mathematicians generally don't care about foundational issues. But they care a lot about the language they use. For example: most mathematicians use the language of set theory all the time. But most probably can't actually list the axioms of ZF.

The OP was proposing identifying a set with its indicator function. This is more than a new foundation, it presumably would change the notation that working mathematicians use. I think you'll find mathematicians care very strongly about that.

In the end the OP is trying to claim that these things are somehow equivalent. Mathematics has a way of dealing with equivalent descriptions of the same structure: you simply use whatever expression or representation of the structure is most convenient for making clear the concepts you wish to describe. Where it is of use category theory and characteristic functions are used, and where set theoretic language provides more clarity it gets used. Trying to mandate some "correct" representation or manner of expression is as pointless as trying to mandate a "correct" way of representing groups. The OP asks

can somebody tell me why mathematicians keep making a distinction between sets, predicates and their indicator functions (other than historcial reasons)? Why not simply equate sets, predicates and their characteristic functions?

The answer is "because it is convenient to do so". Mathematicians use whatever language is convenient for the task, and as it happens distinguishing sets from sharacteristic functions provides a manner of expression that is often useful. They are all equivalent in the end, so what counts is how easy it is to express or represent what it is you want to say in the language of choice.

While it doesn't cover everything you're asking for, Ian Stewart's Concepts of Modern Mathematics is an excellent and very readable popular introduction to things like set theory, relations and functions, abstract algebra, graph theory, and topology. Not a truly rigorous treatment, but it will give you a feel for what's going on and why it's important. Plus it's a Dover book, so the price is very reasonable :-)

I have been thinking about trying to write exactly such a book - something that qualifies as a pop culture book but manages to bring together a lot of modern mathematics which has come a surprisingly long way in the last 100 years.

I see that Concepts of Modern Mathematics has already been mentioned. It's a great book (though I'm not sure it qualifies as a pop-culture book - it is, at the very least, very accessible). Other great reads to get you introduced are "Introduction to Mathematical Philosophy" by Bertrand Russell - it's old, but it will give you a solid grounding in bootstrapping mathematics, why sets matter, and why some questions are not as easy as you would think. Not to mention that Russell is a great writer. There's also "Sets for Mathematics" by Lawvere and Rosebrugh which is an easy going (though definitely no pop-culture, more of textbook-that-assumes-no-prior-knowledge-of-anything) introduction to Category theory. It certainly makes clear why sets and maps are important, and is one of those deceptive books where everything seems very easy and trivial and then suddenly you've found you're out in deep waters proving deep results with the same ease as the trivial ones.

If you want a true pop-culture book to warp your mind with interesting mathematics try "Flatterland" by Ian Stewart. Easy-going and suitable for anyone, it does a fine job of contorting your brain while pelting you with an endless array bad puns and jokes.

Thanks Leland and Allan for great book recommeedations.

Leland, you mentioned that you might write a book about modern mathematics of the last 100 years. I hope you look at Moshe Vardi's On the Unusual Effectiveness of Logic in Computer Science. A while ago I found a great video of his lecture. He talks about Aristotle and connects him to Church, Codd and others. It is very informative, suprisingly funny and best of all, provides a context for many ideas (and the people who discovered them). Unfortunately google is failing me right now.

I think my interest in only the last 100 years or so is that in practice it has seen, really, several minor revolutions in mathematics, right down to the very core of what we think mathematics is. Much of this has been going on deep within the realms of philosophy of math and pure math, and these very different views of mathematics haven't really filtered out into wider popular culture yet. Read a popular math book like say "Mathematics for the Million" from 1937 and you'll have something a lot of modern pure mathematicians would just shake their head at. "Mathematics is the language of quantity"? Even Russell's "Introduction to Mathematical Philosophy" is, in many ways, very much showing its age. That may not sound especially significant - new ideas often come to replace old ones. What you have to remember is that, while mathematics itself progressed impressively, philosophy of mathematics changed very little from what Plato and Aristotle had to say up until the 19th century. In many ways there has been as much or more change in the last 100 years than there was in the first 2000 years since Aristotle.

absolutely. i just finished reading "Great Ideas of Modern Mathematics" published in 1959 and many areas were still a mess, even then. brief review (self link).

But in response to your question in the first point about geometric inteperatation of complex multiplication: in Clifford/geometric algebra, there are things called bivectors, which in 2D are isomorphic to the imaginary numbers in a very trivial way. They represent 2D directed areas. The combination (via sum, actually) of a real (0 blade, in the lingo) and a bivector (2-blade) forms a rotor, which are isomorphic to the complex numbers in a trivial way. They may represent rotations. Rotations are composed by multiplication, and applied by left multiplying a half-rotation and then right multiplying that half-rotation's conjugate (in 2D, this is identical to just left multiplying by the full, rotation, but not so in higher dimensions). This extends to N dimensions trivially. In 3D, the rotors are isomorphic to quaternions.

thanks (you reply by clicking on "comment on this post" at the bottom of the page, editing the mail address to remove anti-spam stuff, and sending an email; the email will appear as a comment - obviously i need to clarify that in the interface!).

Just a quick update, I saw the books mentioned in the title (two volume set) and am impressed with what they cover. They are by no means "pop-culture," actually they are not at all easy to understand for some trying to self-study. However, it is good to see that such books exist. There is a website for the book which covers much of the material.

Following are the table of contents:
Volume I:
Fundamentals-Concepts and Logic
Axiomatic Set Theory
Boolean Set Algebra
Functions and Relations
Ordinal and Natural Numbers
Recursion Theorem and universal Properties
Natural Arithmetic
Infinities
The Classical Number Domains Z,Q,R, and C
Categories of Graphs
Construction of Graphs
Some Special Graphs
Planarity
Monoids, Groups, Rings and Fields
Primes
Formal Propositional Logic
Formal Predicate Logic
Languages, Grammars, and Automata
Categories of Matrixes
Modules and Vector Spaces
Linear Dependence, Bases, and Dimension
Algorithms in Linear Algebra
Linear Geometry
Eigenvalues, the Vector Product, and Quaternions

Volume II
Limits and Topology
Differentiability
Inverse and Iimplicit Functions
Integration
The Fundamental Theorem of Calculus and Fubini's Theorem
Vector Fields
Fixpoints
Main Theorem of ODEs
Categories
Splines
Fourier Theory
Wavelets
Fractals
Neural Networks
Probability Theory
Lamda Calculus

Equal is perhaps a bad term, because it implies that the objets are somehow "the same thing" in some objective sense. Isomorphic is a better description. What we really mean is that, as far as all the things we are considering are concerned, the objects are indistinguishable.

In CT we understand an object by its relationships, via arrows, to other objects. If we have arrows f:A->B and g:B->A with f.g=id_B and g.f=id_A then any relationship we construct relating A to other objects (in other words anything we can say of A), can be, by composing suitably with f and g, converted into an identical relationship between B amd the other objects. That is, using f and g we find that anything we can say about A we can also say about B and vice versa. In this sense, within the catgeory, we cannot distinguish between A and B - there is nothing we can say about either A or B to tell them apart.

A and B may be, in practice, "different objects" but the category only sees relationships via arrows. For example perhaps A is integers under addition modulo 5, and B is rotations of a pentagon: different objects but within the category of groups (which only sees the structure and is not concerned with what the objects "actually are") they are indistinguishable.

Equal is perhaps a bad term, because it implies that the objets are somehow "the same thing" in some objective sense.

And this is a problem how?

Equality is a crucial concept when doing category theory. In your attempt to discuss isomorphism you said f.g=id_B which presupposes a notion of equality.

Consider the category with two objects, A and B, and four arrows, two arrows f,g:A->B. From your description you make it seem like the two arrows are indistinguishable because they can be composed in exactly the same way as each other. But of course they can be distinguished - the very definition of category rests on a notion of equality and the category with f=g is not isomorphic to the one with f/=g.

Equality and isomorphism are different concepts that need to be distinguished (as I was embarassingly reminded of during the viva for my own PhD). Category theorists have found themselves in ugly pickles when they've used equality when they meant isomorphism, or vice versa. See John Baez's "Tale of n-categories" starting here for how examples of how important different concepts arise from switching between equality, natural isomorphism and isomorphism. (Baez is a bit informal and sloppy in places but he fully understands the importance of the distinction.)

Equal is perhaps a bad term, because it implies that the objets are somehow "the same thing" in some objective sense. Isomorphic is a better description. What we really mean is that, as far as all the things we are considering are concerned, the objects are indistinguishable.

In CT we understand an object by its relationships, via arrows, to other objects. If we have arrows f:A→B and g:B→A with f.g=id_B and g.f=id_A then any relationship we construct relating A to other objects (in other words anything we can say of A), can be, by composing suitably with f and g, converted into an identical relationship between B amd the other objects.

That works for objects, but what does it mean to have two equal arrows? Is that a primitive notion, or can it be further explained?

You are missing one more subtle equality implicit in the definition of category. How do you determine two arrows are composable? That said the equality is basically part of the data of a category. In fact the answer to your question is also there too. f . g = h just when (.) maps f and g to h.

I do not think the arrow equality concept is interpretable outside the SET category. One might regard it as a purely syntactic notion, I think. So saying that some diagram "commute", A o B = C o D, just vaguely says that A o B 'does the same thing' as C o D, but without a concrete structure (such as SET) it's impossible to say what the thing ( o B) or (C o D) 'do' is.

More knowledgeable will surely correct me ;)

A monadic logic is one in which predicate symbols take at most one argument -- that is, you can write P(x) but not Q(x,y). The reason that monadic second order logic is interesting is because it's one of the most powerful decidable logics known.

The title of the above cited paper is: MONA: Monadic Second-Order Logic in Practice. It has nothing to do with monads! This is what happens when you skip class.

The point that monadic logic is not related to monads is something I completely missed! Perhaps it is because I haven't taken any classes lately.

I made the same mistake, and was corrected during a presentation. :)