Re: How analogous are categorial and material set theories?
Is Category Theory a Theory? I think not. At least not in a logical sense. Is Logic a Theory. Of course not. Logic is a construction that embraces ways of creating logical theories. Can we describe Category in Logic? No, we cannot. Can we describe Logic in Category. Yes we can. Topos, and all that, even if I regret we are happy about quantifiers being adjoint functors to the contra powerfunctor. Logic should be a bit more than just that, shouldn't it? --- Can we describe Logic over Category? Yes we can. This is less recognized. This is the lative construction of logic from signatures, through terms, to sentences, and so on, as Goguen (Institutions) and Meseguer (Entailment Systems) did, without being explicit about signatures. This is Category Theory as a construction embracing ways of creating logics. We must be explicit about the starting point, the underlying signature. Just think about it, we potentially have the object of types in a monoidal category! It's just around the corner. Let's go get it, and the world will never be the same! --- Discussions under FOM now related to distinctions between first, second and third order logic is really bizarre, or boring to say the least. Much of what they try to say could be said more clearly if they would understand to use category theory as a construction site to build what they try to build. Hilbert was not a bad person, if you ask me. --- Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Patrik, The theory of categories is a first order theory, so what exactly are you denying here? Steve.
On 7 Dec 2017, at 18:58, peklund@cs.umu.se wrote:
Is Category Theory a Theory? I think not. At least not in a logical sense.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
I prefer to think of what Steve presumably has in mind here as an equational theory where composition is 2-ary where 2 is not 1+1 but rather o--->o. One difference between equational logic and first order logic is that only the former has well-defined homomorphisms (not sure if Gerald Sacks would have agreed).?? Just as group theory (in Steve's sense) has homomorphisms, so does category theory in that sense have functors. I'm not sure how one argues that CT has natural transformations however.?? They seem to enter as part of the metatheory, which as usually presented seems to be pretty set theoretic in its outlook. How do NT's look in an HOTT account of CT? The language of the Big Bang Theory is pretty family-oriented, except for equality which seems somewhat controversial.?? But I digress. Vaughan On 12/07/17 10:49 PM, Steve Vickers wrote:
Dear Patrik,
The theory of categories is a first order theory, so what exactly are you denying here?
Steve.
On 7 Dec 2017, at 18:58, peklund@cs.umu.se wrote:
Is Category Theory a Theory? I think not. At least not in a logical sense.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Natural Transformations are homomorphisms of Functors. Working in a dependently-typed setting, this becomes very clear. You don't even need to go to HoTT to see this. By this I mean that if you work 'syntactically', and figure out what it means for a presentation of a theory X to have homomorphisms, then the presentation of Functors qua theory has a natural (ha!) notion of homomorphism, which turns out to be Natural Transformations 'on the nose'. Jacques On 2017-12-08 20:15 , Vaughan Pratt wrote:
I prefer to think of what Steve presumably has in mind here as an equational theory where composition is 2-ary where 2 is not 1+1 but rather o--->o.
One difference between equational logic and first order logic is that only the former has well-defined homomorphisms (not sure if Gerald Sacks would have agreed).?? Just as group theory (in Steve's sense) has homomorphisms, so does category theory in that sense have functors.
I'm not sure how one argues that CT has natural transformations however.?? They seem to enter as part of the metatheory, which as usually presented seems to be pretty set theoretic in its outlook. How do NT's look in an HOTT account of CT?
The language of the Big Bang Theory is pretty family-oriented, except for equality which seems somewhat controversial.?? But I digress.
Vaughan
On 12/07/17 10:49 PM, Steve Vickers wrote:
Dear Patrik,
The theory of categories is a first order theory, so what exactly are you denying here?
Steve.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On Fri, Dec 8, 2017 at 5:15 PM, Vaughan Pratt <pratt@cs.stanford.edu> wrote:
I'm not sure how one argues that CT has natural transformations however.?? They seem to enter as part of the metatheory, which as usually presented seems to be pretty set theoretic in its outlook. How do NT's look in an HOTT account of CT?
I'm not sure what you mean by "metatheory" here. You can define categories, functors, and natural transformations inside HoTT in roughly the same way that you can inside set theory. If you're thinking of a "synthetic" theory of categories analogous to how HoTT is a synthetic theory of (higher) groupoids, then that's not a very well developed idea and there are various competing proposals (I'm most familiar with https://arxiv.org/abs/1705.07442); but in all of them that I know of natural transformations also arise "naturally", generally as a sort of "directed homotopy" using a "directed equality type" analogous to the undirected equality type of ordinary HoTT.
The language of the Big Bang Theory is pretty family-oriented, except for equality which seems somewhat controversial.?? But I digress.
Vaughan
On 12/07/17 10:49 PM, Steve Vickers wrote:
Dear Patrik,
The theory of categories is a first order theory, so what exactly are you denying here?
Steve.
On 7 Dec 2017, at 18:58, peklund@cs.umu.se wrote:
Is Category Theory a Theory? I think not. At least not in a logical sense.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear All, Thanks once again for the responses---I appreciate it! @Cory. Thanks! This was helpful to see that the two perspectives respond to different `needs' within mathematics, and that for many applications the algebraic perspective suffices. I did just want to pick up on the point about large cardinals. I suspect that those sorts of `arithmetical definability' characterisations will only work for cardinals you can characterise from below (i.e. by stating that there's a fixed point for some sort of describability property) and thus are likely to be consistent with V=L. However, there are really interesting categorial characterisations of *very* strong large cardinals, some of them dating back to the 1960s (see Brooke-Taylor and Bagaria, `On Colimits and Elementary Embeddings'). But I'm not really on top of this material, so don't have a feel for how the proof works yet (other than that the embeddability in the category-theoretic setting somehow transfers to the existence of large cardinal embeddings in set theory). @Mike. Thanks for the points about the meta-theory---all clear to me now. Similarly for ordinals. I was talking about the etale space. My claim wasn't meant to be that it *couldn't* be done structurally, just that sometimes the set-theoretic perspective is useful for seeing what's going on in a particular construction (but maybe this is just a holdover of how I first came across sheaves---then there was a lot of quotienting in material set theory). You're right of course about the large cardinals (as I mentioned to Cory). This strikes me as very interesting stuff that I'm just not on top of yet. The example of L is also super-nice...thanks! I will have a think about this. @Patrik: I'm also unsure how category theory is not a `theory'. Obviously were interested in many and varied categories but the core axiomatisation of what a category is is still first-order. Similarly in material set theory, even though ZFC is the `core' set theory (for many people anyway) we still consider lots of different theories. So I don't see how the phrase `is category theory a theory? I think not.' wouldn't apply mutatis mutandis to material set theory. I *do* think however there's an important philosophical difference: Set theory aims at an intended interpretation (the cumulative hierarchy), whereas category theory doesn't (the whole *point* of it is to apply across diverse contexts). But maybe things are more subtle than I realise [plus I'm maybe straying into off-list philosophical territory with this claim]. Best Wishes, Neil On 8 December 2017 at 06:49, Steve Vickers <s.j.vickers@cs.bham.ac.uk> wrote:
Dear Patrik,
The theory of categories is a first order theory, so what exactly are you denying here?
Steve.
On 7 Dec 2017, at 18:58, peklund@cs.umu.se wrote:
Is Category Theory a Theory? I think not. At least not in a logical sense.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
-- Dr. Neil Barton Postdoctoral Research Fellow Kurt Gödel Research Center for Mathematical Logic University of Vienna [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Quotients, of course, also make perfect sense structurally. You can even define the quotient by an equivalence relation as its set of equivalence classes; this involves only "local" membership (elements of a set belonging to subsets of that set) so it makes sense in ETCS etc. On Fri, Dec 8, 2017 at 5:20 PM, Neil Barton <bartonna@gmail.com> wrote:
Dear All,
Thanks once again for the responses---I appreciate it!
@Cory. Thanks! This was helpful to see that the two perspectives respond to different `needs' within mathematics, and that for many applications the algebraic perspective suffices.
I did just want to pick up on the point about large cardinals. I suspect that those sorts of `arithmetical definability' characterisations will only work for cardinals you can characterise from below (i.e. by stating that there's a fixed point for some sort of describability property) and thus are likely to be consistent with V=L. However, there are really interesting categorial characterisations of *very* strong large cardinals, some of them dating back to the 1960s (see Brooke-Taylor and Bagaria, `On Colimits and Elementary Embeddings'). But I'm not really on top of this material, so don't have a feel for how the proof works yet (other than that the embeddability in the category-theoretic setting somehow transfers to the existence of large cardinal embeddings in set theory).
@Mike. Thanks for the points about the meta-theory---all clear to me now. Similarly for ordinals.
I was talking about the etale space. My claim wasn't meant to be that it *couldn't* be done structurally, just that sometimes the set-theoretic perspective is useful for seeing what's going on in a particular construction (but maybe this is just a holdover of how I first came across sheaves---then there was a lot of quotienting in material set theory).
You're right of course about the large cardinals (as I mentioned to Cory). This strikes me as very interesting stuff that I'm just not on top of yet. The example of L is also super-nice...thanks! I will have a think about this.
@Patrik: I'm also unsure how category theory is not a `theory'. Obviously were interested in many and varied categories but the core axiomatisation of what a category is is still first-order. Similarly in material set theory, even though ZFC is the `core' set theory (for many people anyway) we still consider lots of different theories. So I don't see how the phrase `is category theory a theory? I think not.' wouldn't apply mutatis mutandis to material set theory.
I *do* think however there's an important philosophical difference: Set theory aims at an intended interpretation (the cumulative hierarchy), whereas category theory doesn't (the whole *point* of it is to apply across diverse contexts). But maybe things are more subtle than I realise [plus I'm maybe straying into off-list philosophical territory with this claim].
Best Wishes,
Neil
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (6)
-
Jacques Carette -
Michael Shulman -
Neil Barton -
Patrik Eklund -
Steve Vickers -
Vaughan Pratt