Hello, In his 1974 paper Osius showed that there are enough transitive objects in the initial topos to define a naive set theory. He then goes on the assume his topoi are well-pointedness and produces a characterisation of the category of sets in terms familiar to set theorists. I'm wondering whether anyone has produced an axiomatic set theory from Osius' naive set theory which characterises the initial topos. -- Dr Elwood Wilkins e-mail: elwood@essex.ac.uk Senior Research Officer tel: (+44) (0)1206 872336 Department of Computer Science fax: (+44) (0)1206 872788 University of Essex, Colchester, Essex, UK
Elwood Wilkins reminds us that...
In his 1974 paper Osius showed that there are enough transitive objects in the initial topos to define a naive set theory. ...
Gerhard Osius's work was significant in 1974 as one of the ways in which it was shown that toposes do the same thing as set theory. In fact Osius's is, so far as I am aware, the only work that discusses *set* theory - Benabou, Joyal, Mitchell, Lawvere etc showed that toposes do the same thing as some form of *type* theory. Of course, it is the latter that mathematicians actually use when they claim to be using set theory as foundations, but set theory - epsilontics as Lawvere calls it - is of some interest in the study of very high powered induction. Peter Johnstone included a precis of Osius's paper in his book "Topos Theory" (Academic Press, 1977). Apart from that, I was unable to track down anything that built significantly on it. Indeed, Osius himself didn't seem very interested when I wrote to him about it (he now does statistics). The successor to this paper would therefore seem to be my "Intuitionistic Sets and Ordinals", J. Symbolic Logic, 61 (1996) 705--744 This develops, in a symbolic way, the notions of "transitive set" and "ordinal" in the sense of a carrier equipped with an extensional well founded relation. Several qualitatively different notions of ordinal arise intuitionistically. I also pick up on Osius's set theory and pose some questions that suggest ways of adapting it to Grothendieck toposes in general. What remains of considerable interest (once we have agreed that set theory is wrong, wrong, wrong) is Osius's categorical notion of recursion. The equation f(x) = r( { f(y) | y in [=element_of] x } ) he writes as the (3=1, not 2=2) commutative square P(f) { y | y in x } P(X) ---------> P(A) ^ ^ | | | | | | | | | | r | | | | | | - | f v x X -------------> A which we may of course generalise to a "homomorphism" from any P-coalgebra to any P-algebra, where indeed P may be any functor instead of the covariant powerset functor. The coalgebra admits recursion by definition if there is exactly one such "homomorphism" to any algebra whatever. The exercises in Chapter VI of my book "Practical Foundations of Mathematics" (Cambridge University Press, 1999) explore applications of the commutative square to recursive functional programs. http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/s6e.html Osius's 3+1 square is about RECURSION - defining functions or programs - but I have also considered INDUCTION - proving theorems - categorically. Again this is a property ("well foundedness") of coalgebras. See Section 6.3 http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/s63.html of the book, or my unfinished paper "Towards a Unified Treatment of Induction" (also known as "On the General Recursion Theorem") which you can get from my Hypatia page http://hypatia.dcs.qmw.ac.uk/author/TaylorP The final section of the book (s96.html) sketches the way in which this categorical notion of ordinal can be used to define transfinite iterates of a functor (for example, internally in a topos). I hope to use this to develop categorical notions of the Axiom of Replacement. Paul Taylor
Paul Taylor wrote:
Gerhard Osius's work was significant in 1974 as one of the ways in which it was shown that toposes do the same thing as set theory.
Osius showed that well-pointed topoi do essentially the same thing as set theory. I have yet to find any adequate analogy between what elementary topoi in general do and set theory. The problem being, as far as I can see, that classical set theory finds it very difficult to describe the rather more subtle behaviour occurring in the initial topos. Whence the standard set theoretic account of topos logic includes the assumption that bound variables denote, which make the semantics of elementary topoi almost identical to those of well-pointed ones (for instance every proper subtype of 1 is treated as though it is empty!).
In fact Osius's is, so far as I am aware, the only work that discusses *set* theory - Benabou, Joyal, Mitchell, Lawvere etc showed that toposes do the same thing as some form of *type* theory. Of course, it is the latter that mathematicians actually use when they claim to be using set theory as foundations ...
In practice this is true, but not if they're interested in actually studying the foundations of maths. My (set minded) colleagues point out (quite forcibly) that unless something is expressible in ZF (say) then they find it hard to accept, a view that appears to be widespread in the theoretical end of computer science. Now I have the practical problem of convincing people that what I do constructively is better than what they do with their "bound variables denote" assumptions, and an axiomatic set theory equivalent to the initial topos would make this much easier: they could go away contentedly believing that I'm really doing set theory (while I can be happy with the knowledge that they're doing typed theory). There are potential applications to category theory from producing a set theory. For instance one might speculate that this set theory could replace the rather cumbersome Freyd cover in the proof of the constructive properties of the initial topos. A host of other speculations can be formulated ... Elwood -- Dr Elwood Wilkins e-mail: elwood@essex.ac.uk Senior Research Officer tel: (+44) (0)1206 872336 Department of Computer Science fax: (+44) (0)1206 872788 University of Essex, Colchester, Essex, UK
Dear categoricians, Is there any formalization of process algebras in term of categories? I would be interested in giving an computational, multi-process semantics to certain graphs, and I thought it could be done in terms of a functor to a process category (if this concept exists...) Is there any literature about this? Thank you for your help, Matthieu Amiguet
----------
Da: matthieu amiguet <matthieu.amiguet@info.unine.ch> A: categories@mta.ca Oggetto: categories: process algebras Data: Gio, 20 apr 2000 14:49
Dear categoricians,
Is there any formalization of process algebras in term of categories? I would be interested in giving an computational, multi-process semantics to certain graphs, and I thought it could be done in terms of a functor to a process category (if this concept exists...) Is there any literature about this? Thank you for your help,
Matthieu Amiguet
We have a categorical formalization of process algebras in terms of enriched category theory. You can see for a general presentation: S.Kasangian, A.Labella "Observational trees as models for concurrency" Math. Struct. in Comp.Science (1999) vol.9 pp.687-718 Anna Labella
Another few papers which may be of interest are: "Constructing process categories" J.R,B. Cockett (me!) & D.A. Spooner TCS 177 (1997) 73-109 "Categories for syncrony and asynchrony" J.R,B. Cockett & D.A. Spooner Electronic Notes in Theoretical Computer Science I (1995) 495-520 These papers explore the "combinatorial" representation of processes using span categories. In particular they give an account of Abramsky's program to model processes (based on a CCS style presentation) using span categories. -robin
Is there any formalization of process algebras in term of categories? I would be interested in giving an computational, multi-process semantics to certain graphs, and I thought it could be done in terms of a functor to a process category (if this concept exists...) Is there any literature about this?
around 1995, i had two papers about "convenient categories for process calculus" and one about "categorical logic of concurrency and interaction". the simplest way to get them is probably on hypatia, or from my web page http://www.kestrel.edu/HTML/people/pavlovic/ i am not sure to which extent is this what you are looking for, but it is surely related. later samson abramsky and i figured how to deal with process categories much better, but most of it was never written up. an initial account was in our CTCS 97 paper (also available, i think, at the same sites.) -- dusko pavlovic
Is there any formalization of process algebras in term of categories? I would be interested in giving an computational, multi-process semantics to certain graphs, and I thought it could be done in terms of a functor to a process category (if this concept exists...) Is there any literature about this?
I have a CTCS99 paper ``On the semantics of message passing processes'' at http://theory.doc.ic.ac.uk/~le which may be relevant. As the title suggests, it looks at categorical semantics for a CSP-like language with assignment. It is related to the work mentioned by Robin and Dusko. Also, the conclusions of my thesis discusses representing process networks as diagrams in a category of processes. This might be related to your comment above. Lindsay
participants (7)
-
Anna Labella -
dusko＠dusko.org -
Lindsay Errington -
matthieu amiguet -
Paul Taylor -
Robin Cockett -
Wilkins E B