Lambda the Ultimate

Reading off the categorical definition and considering that the categories in question represent languages (or at least their semantics) should get you off to a good start. In practice there isn't a category-theoretic interpretation of monads, just a category-theoretic definition.

Categorically, a monad is the composition of two adjoint functors. If F -| U, then U o F is a monad. IIRC, they were invented to model substitution in finitary(?) equational theories. The fact that they are useful in modelling effects in functional programs came as something of a surprise.

Your best bet is to read Moggi's paper "Notions of Computation and Monads" -- you're probably better qualified to read it than I am. :)

This, I think, is exactly what I was looking for. Thanks : )

This introductory level paper was discussed on LtU recently.

Are those flaws part of the text?

(1) The text states:

"The repeated use of the word repetoire is already a hint that something big is being hidden. It would be downright embarrasing, for example, to have replaced the words 'repetoire' int he above description by 'set,' for besides the blatant circularity, we would worry, with Russell, about what arcane resrictions we would have to make about the universal quantifier, once that is thrown into the picture".

The author does not profer an axiom of comprehension, and explicitly sets aside notions of quantifiers, but is at pains (during the parts that I have read) to separate the concept of 'class' from the concept of 'set', so I do not understand how the theory he presents suffers from Russel's antimony.

(2) Does the "bare bones" set theory need an axiom of infinity, or rather, is such a discussion truly germaine to this text? The author reminds us that the set theory being used is not as important as the concepts of category theory on which he is concentrating, and on page 10 introduces the term "B.Y.O.S.T." (bring your own set theory).

(3) You already acknowledged.

-----

Being very much a beginner in category theory, I must say I've found the text, so far, to be a useful and easily absorbed contribution to a diffucult subject.

1.

How does merely using words 'class' and 'repertoire' prevents one from saying:

{X | X not in X} ?

The author does not profer an axiom of comprehension, and explicitly sets aside notions of quantifiers, but is at pains (during the parts that I have read) to separate the concept of 'class' from the concept of 'set', so I do not understand how the theory he presents suffers from Russel's antimony

So how can one say anything about sets without some axiom of comprehension ? If the axiom is implied, {x | P(x)}, then his sets surely suffer from the paradox.

Likewise, how can one say something about a set (or practically anything) without using the notion of the universal quantifier ?

2.

(2) Does the "bare bones" set theory need an axiom of infinity, or rather, is such a discussion truly germaine to this text?

Because if one does not assume some sort of axiom of infinity, one cannot prove that the natural number object even exists in his category. It makes the subsequent discussion unfounded.

The 'bare bone' set, as I said before, also admits arbitrary collections which leads to Russell's paradox. So, no, you cannot bring your any of own arbitrary sets, only some.

3. Right.

To me it seems that if you bring a bad set theory you only have to blame your self. i.e. B.Y.O.S.T. realy means bring a set theory that you think is good.

Because if one does not assume some sort of axiom of infinity, one cannot prove that the natural number object even exists in his category. It makes the subsequent discussion unfounded.

Where does one draw the line, "assuming" the axiom of infinity or assuming the existence of some appropriate set theory? Of course, one needs to explore these concepts, but the paper is about category theory, not ZF set theory.

Since the natural number structure in category theory is parasitic on one of Dedekind's theorems (recursive definition), the author should have explained how his 'bare' sets might have such structure. Without such explanation, the section does not make sense.

The article contains some dark hints that are hard to interpret:

"This, of course, has shock-value: it recruits the entire apparatus of propositional verification to its particular end. "

What's the above supposed to mean?

Is he not referring to the part of the definition which states "if P(n) is any proposition ... , then P(n) is true for all n in N". The definition relies on a notion of knowing what a proposition is and is not, and what a proposition means. The definition also quantifies over all propositions, which is kind of shocking, is it not?

Is he not referring to the part of the definition which states "if P(n) is any proposition ... , then P(n) is true for all n in N". The definition relies on a notion of knowing what a proposition is and is not, and what a proposition means. The definition also quantifies over all propositions, which is kind of shocking, is it no

The account is dubious for the following reasons:

1. It's a second order Peano postulates formulation (a strawman). There is no need to rely on second-order logic.

2. The induction principle can be reformulated in set terms without appealing to propositions and such:

P3: "If P is a subset of N, 1 is in P, and the implication (x in P ==> successor(x) in P) holds, then S = N".

Is it hard to understand ?

3. The induction principle is a *theorem* in the standard set theory. What's so shocking about it ?

I guess the whole thing is shocking (to me) because whichever way you look at it you have axiom schemes that are instantiated once for each proposition in your language (i.e. a scheme of infinitely many axioms) such as the axiom of separation and the axiom of replacement in ZF set theory. It took me a little while when I learned it to understand the difference between that and higher order logic.

The definition of natural numbers (P3) in the parent post cannot effectively be applied without the axiom of separation, which is where your proto-quantifying over all propositions comes back into it: The definition merely hides the fact that this is what is happening.

I think the author explicitly acknowledges that you ultimately need these devices, in the series of paragraphs culminating in:

When we gauge the differences in various mathematical viewpoints [...] for ultimately they may require exactly the same things, but also to pay attention to the order in which each piece of equipment is introduced [...]

I guess the whole thing is shocking (to me) because whichever way you look at it you have axiom schemes that are instantiated once for each proposition in your language (i.e. a scheme of infinitely many axioms) such as the axiom of separation and the axiom of replacement in ZF set theory.

I do not understand what you are saying at all.

In the first order Peano formulation, ZFC with its axioms is irrelevant.
In the second order formulation, one does not need the infinite induction axiom schema, naturally. In fact, induction is a theorem in ZF.

The (P3) definition you gave uses the term "if P is a subset of ...". How do you define the notion of subsets without ZF, or something like it? And in ZF, the mechanism of constructing subsets is the axiom (scheme) of separation which is a single sentence per proposition, i.e. infinitely many sentences.

So the (P3) definition harnesses the machinery of propositions.

How do you define the notion of subsets without ZF

The notion of subset is trivial and does not require ZF or anything like that. What actually is required is paradox avoidance caused by unrestricted comprehension. It can be achieved in many various ways. ZF is one example with its axiom of separation/subset/restricted comprehension schema, NBG is another example which admits a finite axiomatization.

And in ZF, the mechanism of constructing subsets is the axiom (scheme) of separation which is a single sentence per proposition, i.e. infinitely many sentences

Why is it a problem ?

So the (P3) definition harnesses the machinery of propositions

I do not understand that at all. P3 is a simple theorem in ZF or NBG.

It is not a problem that the axiom scheme of separation requires infinitely many axioms. The point however was to show that (P3) does indeed harness the notion of propositions, because you do not use (P3) over ZF as a lemma without also using separation to construct subsets.

I get your point about the author's original definition being (misleadingly) a second order formulation, because it was expressed in the manner "for all propositions P ...".

On the question of comprehension: Can you show me where the author suggested that unrestricted comprehension is on the cards? I do not see it.

I do not understand what you mean by:

The point however was to show that (P3) does indeed harness the notion of propositions,

What's "harness the notion of propositions" supposed to mean in simple words ?

because you do not use (P3) over ZF as a lemma without also using separation to construct subsets.

Once again, you do no use separation to "construct" anything, you use it to *exclude* the collections that would otherwise have led to Russell's paradox. Please clarify what exactly you've meant by your statement.

On the question of comprehension: Can you show me where the author suggested that unrestricted comprehension is on the cards? I do not see it

He did not say explicitely that his "bare sets" allow unrestricted comprehension, but unless such restriction is clearly stated, the default is to assume the naive set theory with unrestricted comprehension. After all, there are several ways to avoid the paradox: ZF, NBG, NF, etc. He sort of hinted that the collection of objects in his category of "bare sets" are not sets (still not good enough but so be it), but he did not impose any restriction on the objects/sets themselves.

I believe these quotes (elided in places) are explicit enough for the purposes of the text, is it not?

[ It we were to equate [class] with "set" ... ] we would worry, with
Russell, about what arcane restrictions we would have then to make regarding our universal quantifier, once that is thrown into the picture.

the standard word is class and the notion behind it deserves much
discussion; we will have some things to say about it in the next section.

In short by a class, we mean a collection of
objects, with some restrictions on which subcollections we, as mathematicians, can
deem sets and thereby operate on with the resources of our set theory.

1.

believe these quotes (elided in places) are explicit enough for the purposes of the text, is it not?

[ It we were to equate [class] with "set" ... ] we would worry, with
Russell, about what arcane restrictions we would have then to make regarding our universal quantifier, once that is thrown into the picture.

I do not understand the above. When can the universal quantifier be thrown *out* of the picture ?

In short by a class, we mean a collection of
objects, with some restrictions on which subcollections we, as mathematicians, can
deem sets and thereby operate on with the resources of our set theory.

First, what are those restrictions ? The author never quite explains what he means. His library analogy is muddled. In fact, a class *can* contain all the possible sets as its members -- that's exactly what his collection of objects in the category of sets does.

Secondly, and more importantly, he uses the notion of class when he talks about the collection of objects in his category, but not when he talks about the sets-as-objects (as I said before).

Thirdly, ZF for example, does not have the notion of class. So assuming he applies the notion of class to the objects as well(although there is no indications he does), would it mean that ZF is excluded as an underlying set theory for his objects ? What's his "bare bones" set theory is then ? Is it powerful enough to have a set of natural numbers ? Is it too naive to have paradoxes ?

First, what are those restrictions ? The author never quite explains what he means. His library analogy is muddled. In fact, a class *can* contain all the possible sets as its members -- that's exactly what his collection of objects in the category of sets does.

Muddled? I don't like the analogy but I don't see where it is muddled. Where does the author say a class cannot contain all the possible sets as its members?

he uses the notion of class when he talks about the collection of objects in his category, but not when he talks about the sets-as-objects (as I said before).

Can you explain this in more detail? I cannot understand your point.

Thirdly, ZF for example, does not have the notion of class. So assuming he applies the notion of class to the objects as well(although there is no indications he does), would it mean that ZF is excluded as an underlying set theory for his objects ? What's his "bare bones" set theory is then ? Is it powerful enough to have a set of natural numbers ? Is it too naive to have paradoxes ?

Isn't this a strawman since he doesn't attempt to construct categories in which the objects are classes?

What's his "bare bones" set theory is then ? Is it powerful enough to have a set of natural numbers ? Is it too naive to have paradoxes ?

On page 12 he uses the words "as we shall see, such an initial object exists given that the underlying bare bones set theory is not ridiculously impoverished".

Overall though, you seem to object to the pedagogic style.

Muddled? I don't like the analogy but I don't see where it is muddled. Where does the author say a class cannot contain all the possible sets as its members?

So what do you think is a class as explained by the 'library analogy' ?

Can you explain this in more detail? I cannot understand your point.

I've already said several times that he applies the notion of class to the collection of objects in his category of sets but not to the object themselves. What's not clear about that ?

Isn't this a strawman since he doesn't attempt to construct categories in which the objects are classes?

So *what* kind of objects are his sets ? ZF-sets, NBG-sets or some other sets ? He does not give a hint.

"as we shall see, such an initial object exists given that the underlying bare bones set theory is not ridiculously impoverished".

And what do you think that supposed to mean ? What is "not ridiculously impoverished" ?

Overall though, you seem to object to the pedagogic style

I just do not understand whole passages in the exposition, like the library analogy, "the position of the natural numbers as a discrete dynamical system, among all discrete dynamical systems." , the "it recruits the entire apparatus of propositional
verification to its particular end" piece, etc. Do you ?

What's that supposed to mean ? How can natural numbers be "a discrete dynamical system"

What's that supposed to mean ? How can natural numbers be "a discrete dynamical system"

Anyone with a hint of imagination can guess what he has in mind: the elements of N are the points of the dynamical system and the successor function is the time evolution operator.

the elements of N are the points of the dynamical system and the successor function is the time evolution operator

That does not make any obvious sense. What are "the points of the dynamical system" in the context of natural numbers as defined in ZF (or any other set theory) or in category theory ? What is "the time evolution operator" in the same context ?

That does not make any obvious sense. What are "the points of the dynamical system" in the context of natural numbers as defined in ZF (or any other set theory) or in category theory ? What is "the time evolution operator" in the same context ?

A discrete dynamical system (I should probably throw in another adjective such as "autonomous") is a pair (X,t) consisting of a set X and a map t : X -> X. We often think of X as a kind of space, its elements as points and t as a time evolution operator that defines the evolution of these points from one time-step to the next. The objects of Mazur's Peano category can then be thought of as base-pointed discrete dynamical systems.

I think this underlying definition is pretty clear from his remarks:

"This strategy of defining the Natural Numbers as “an” initial object in a category of (what amounts to) discrete dynamical systems, as we have just done, is revealing, I think; it isolates, as Peano himself had done, the fundamental role of mere succession in the formulation of the natural numbers."

A discrete dynamical system (I should probably throw in another adjective such as "autonomous") is a pair (X,t) consisting of a set X and a map t : X -> X. We often think of X as a kind of space, its elements as points and t as a time evolution operator that defines the evolution of these points from one time-step to the next. The objects of Mazur's Peano category can then be thought of as base-pointed discrete dynamical systems.

No kidding ? A discrete dynamic system is defined as a pair (X, t) where X is a topological space and t is a continuos function t:X->X. Then, the trajectory of point x in X is defined as the sequence (x, t(x), ..., tn(x)) where n in N and tn is the composition of 'n' applications of t. It just did not occur to me, probably due to lack of imagination, that the abstruse notion of DDS can be somehow revealing when applied to natural numbers. I honestly thought that the author had some other insightful idea in his mind.

Natural numbers would be a ludicrously trivial DDS instance, on par with a light switch being a DDS or virtually any thing being a DDS by taking t as the identity 'morphism', if it were not for a fatal cirularity in definition. The very word 'discrete' [in the given context] is meaningless without first having an idea what natural numbers are.

Further, forgetting the sloppiness for a moment (natural numbers clearly are not the initial object, rather the 'Peano triple' as an algebra is), how does such triple 'isolates the fundamental role of mere succession' any better, or even equally well, than the original Peano axioms do ? What's the point of making something simple and easily understandable be just the opposite ?

So *what* kind of objects are his sets ? ZF-sets, NBG-sets or some other sets ? He does not give a hint.

He says, somewhere, that it does not matter. His very point seems to be that the whole concept of categories is independent of (or, if you want, parametric in) the choice of a particular notion of set.

He says, somewhere, that it does not matter

But it does matter for his natural numbers exposition -- the 'bare' set theory should be powerful enough to contain them and not too powerful to avoid inconsistency. As soon as you specify what powerful enough actually means, you'll discover that natural numbers description as a category-of-sets structure is just a paraphrase of set theory treatment.

... and the author acknowledges almost exactly that ("is [...] a paraphrase") in the text. Again, pedagogic style.

and the author acknowledges almost exactly that ("is [...] a paraphrase") in the text.

I am not sure what exact words you are referring to. Besides, I do not know how he can possibly paraphrase something if the original phrasing was not provided.

The comments I refer to have already been quoted in one of the posts on this thread.

As you wish.

Once again, you do no use separation to "construct" anything, you use it to *exclude* the collections that would otherwise have led to Russell's paradox. Please clarify what exactly you've meant by your statement.

Sorry: Don't understand this at all.

(1) I am quite used to seeing terms like "we construct the subset { x in Blah | P(x) }", i.e. we use (an instance of) the axiom of separation to construct a set.

(2) How would you "use it to *exclude* the collections that would otherwise ...": what are these collections, and from what other things are you excluding them?

(1) I am quite used to seeing terms like "we construct the subset { x in Blah | P(x) }", i.e. we use (an instance of) the axiom of separation to construct a set.

So when you say "read-headed people", do you imagine a process whereby some force plucks read-heads and puts them into some sort of a container ("constructs a set"), rather then just imagining those folks as possessing some feature ('read-headednes') ? If so, I guess it's an OK intuition although unusual when one talks about ZF sets. It depends on whether you consider sets as existing 'out there' or rather as created anew every time you want to use them and destroyed when the interest in such sets is lost.

2) How would you "use it to *exclude* the collections that would otherwise ...": what are these collections, and from what other things are you excluding them?

OK, let me rephrase. In ZF, there are predicates that cannot define a set, such as R = {x | not( x in x)} that can be restated as R = { x in V | not (x in x)} where V is the universal set. Since it can be shown that thanks to AoS V does not exist, { x in V | not (x in x)} does not define a set in ZF.

In NBG, on the other hand R defines a collection called a proper class.

Please ignore this post

I assume you mean "red headed".

Nope, I meant exactly what I wrote.

you would (for instance) have previously established that "[all] people" is a set

That 'people' is a set in *any* set theory is an obvious fact by virtue of people being a finite collection.

It depends on whether you consider sets as existing 'out there' or rather as created anew every time you want to use them and destroyed when the interest in such sets is lost.
Sorry I dont understand this.

What's unclear about that ? One can consider sets as either existing in some Platonic universe or being formed 'constructively'. The latter viewpoint if pursued consistently leads to construstive mathematics with its gains and pains.

Here you would not using separation to show that R is not a set,

No true, first one shows that the universal set does not exist assuming AoS and not(x in x) so it follows that { x in V | not (x in x)} does not define a set. See Zermello's original proof for starters.

you would use a simple diagnonalisation argument, which requires reductio ad absurdum, and utilises purely logical inference.

That is not correct.

... rather it is one of the axioms of ZF that is used to include (or "construct") certain sets into the universe of sets.

OK, so given {{ x in V | not (x in x)} which is an instance of such AoS construction, you construct yourself right into the paradox because you did not *prove* that V = {x | x=x} does not exist in ZF, it's a 'legitimate' set definition. So what's good is your constructive reading of AoS ?

In ZF, R is an empty class due to well-foundedness, and since NBG is a conservative extension of ZF, it is an empty class in NBG too.

You are terribly confused.

1. The ZF language does not have a notion of class at all.

2. R is a proper class in NBG.

3. An empty class is a set, and R is clearly not a set. In fact, in NBG, R = V.

OK, so given {{ x in V | not (x in x)} which is an instance of such AoS construction, you construct yourself right into the paradox because you did not *prove* that V = {x | x=x} does not exist in ZF, it's a 'legitimate' set definition. So what's good is your constructive reading of AoS ?

No it is not an instance of such an AoS construction; You have not shown that V is a set (and never will). In AoS you certainly have to prove that the thing from which you are constructing a subset is a set; Where did I state otherwise?

Why do you say "... because you did not *prove* that .. does not exist"? The reason you enter a paradox is because you did not use the AoS, you used some other strawman.

You are terribly confused.

1. The ZF language does not have a notion of class at all.

2. R is a proper class in NBG.

3. An empty class is a set, and R is clearly not a set. In fact, in NBG, R = V

Agreed - I wasn't thinking, specifically:

2. I was thinking of R = { x in V | x in x }, which is empty.

1. I should have said "In ZF, R - as a proposition - is false" (if that had ever been the case to start with) rather than in "In ZF, R is an empty class", but you could easily have understood what I meant, there is plenty of this kind of shorthand notation around.

3. I agree, in NGB, R = V, and is a proper class.

The reason you enter a paradox is because you did not use the AoS

But I did. Assume: V is a set of everything. Sounds like a reasonable assumption, after all some set theories do have the universal set.

By separation:

R = {x in V | not(x in x) }

I did not prove that such set exists, however neither did you prove that such set does not exist so your theory is open to the paradox until you eliminate V. You just do not know whether V exists or not, there are other means to 'construct' sets in ZFC other than separation.

1. I should have said "In ZF, R - as a proposition - is false" (if that had ever been the case to start with) rather than in "In ZF, R is an empty class", but you could easily have understood what I meant, there is plenty of this kind of shorthand notation around.

No, I do not understand that at all. R is not a proposition but something that the Russell predicate defines, the predicate being 'not (x in x)'. So, given,

S = { {1,2}, {3,4}} and T = {x in S | not (x in x)}, one can easily (hopefully) see that S = T. So how did you arrive at the bizarre conclusion that T must be empty ? The collection would be empty if not (x in x) evaluated to false for every x, but, on the contrary it evaluates to true for every x in S.

So when you say "read-headed people", [ ... ]

I assume you mean "red-headed people". This is not prima facie an instance of separation until you have established that "[all] people" is a set. Why did you chose that example as a follow-up?

So to answer your question: I would have to start off assuming "readheaded people" is a class ("readheadedness"), until you proved to me that it was a set.

In my example, "Blah" is a set (I suppose I should have said that :-), previously constructed, and separation by P is used to construct a subset of it.

It depends on whether you consider sets as existing 'out there' or rather as created anew every time you want to use them and destroyed when the interest in such sets is lost.

I'm sorry I dont understand this analogy.

OK, let me rephrase. In ZF, there are predicates that cannot define a set, such as R = {x | not( x in x)} that can be restated as R = { x in V | not (x in x)} where V is the universal set. Since it can be shown that thanks to AoS V does not exist, { x in V | not (x in x)} does not define a set in ZF.

Agreed, but where are you using separation to exclude R from being a set? Rather, you use a bunch of logical inferences (reductio ad absurdum) to prove that R cannot be a set, in which I can see no ZF axioms being applied.

So the question remains, how do you (in a wide context) use separation to exclude things from being sets?

I repeat my earlier claim: Separation is used to construct subsets (OK it may crop up as part of some proof that some other class is proper, but that is purely incidental).

In NBG, on the other hand R defines a collection called a proper class.

Do not agree: Due to well-foundedness, R is empty in ZF, and since NBG is a conservative extension of ZF, it is empty in NBG too. Therefore it is the empty set, and not a proper class.

For something in that general direction you might consider what can be done with algebraic specification which seeks to generate requirements that define a model "up to isomorphism", and make use of category theory to allow for an essentially pluggable logic system via institutions. this article provides a good basic introduction.

Also see this article by the same authors for an informal introduction. They make a good point in section 5 which is that, one doesn't usually need models "up to isomorphism". What really matters is behavioural equivalence. For example, I could implement a list ADT using a tree datatype - as long as that implementation respects the list axioms then it doesn't matter that trees are not isomorphic to lists. I can still go ahead and substitute them into any context where lists were expected.

You can see echoes of this stuff all the way back, from Dijkstra's rather academic admonitions to not commit to choices you aren't forced to follow, to the very practical code-bumming advice of 60's assembly programmers and their ISA-level advice: "if you won't branch, don't test" -- both of these are pretty much equal to: "code, if you must, but only up to isomorphism".

A database and its log file are examples of isomorphic data structures, but with differing optimizations (reading the former requires no decisions, writing the latter requires no decisions -- redundancy and uniqueness can be duals). When your hashing is used for caching, it's a similar story, and again introducing redundancy means that we're only dealing with addresses up to isomorphism.

Over a network, there are numerous ways that a sequential stream can be sent as bags of packets, but we normally don't pay any attention, as long as they are all (up to isomorphism) the same as the original sequential stream. Ditto for a disk, which can be thought of as connecting a node and itself across time, rather than two distinct nodes across space.

Some laptops have decent migration tools, so that one can expect one's new laptop to behave the same as one's old one, up to isomorphism -- note that, in general, one doesn't wish for equality here; there would be very little point in upgrading to the same box.

etc. usw. (the trouble with abstract nonsense is that after a while, everything starts to look the same, only different...)