From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9445 Path: news.gmane.org!.POSTED!not-for-mail From: Michael Shulman Newsgroups: gmane.science.mathematics.categories Subject: Re: How analogous are categorial and material set theories? Date: Mon, 27 Nov 2017 04:10:04 -0800 Message-ID: References: Reply-To: Michael Shulman NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Trace: blaine.gmane.org 1511830205 28476 195.159.176.226 (28 Nov 2017 00:50:05 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Tue, 28 Nov 2017 00:50:05 +0000 (UTC) Cc: categories To: Neil Barton Original-X-From: majordomo@mlist.mta.ca Tue Nov 28 01:50:00 2017 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp2.mta.ca ([198.164.44.40]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1eJU60-0006m0-76 for gsmc-categories@m.gmane.org; Tue, 28 Nov 2017 01:49:56 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:36757) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1eJU6X-0001ZQ-JN; Mon, 27 Nov 2017 20:50:29 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1eJU54-0008JW-Vg for categories-list@mlist.mta.ca; Mon, 27 Nov 2017 20:48:58 -0400 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9445 Archived-At: Sorry, forgot to include original citations: the comparison of ZFC to ETCS goes back to Osius, Cole, and Mitchell in the 1970s, while various replacement axioms for ETCS have been formulated by Lawvere, Cole, Osius, and McLarty. On Mon, Nov 27, 2017 at 4:06 AM, Michael Shulman wro= te: > In general, I don't think ETCS has any more trouble building models or > comparing cardinality than ZFC does. A model in the abstract sense of > model theory doesn't use any of the "internal" membership-structure of > a ZFC-set; it is a purely structural entity: a set equipped with > certain functions and relations. So I don't see why any > model-theoretic theorem would be any harder to formalize in ETCS than > in ZFC. > > To translate statements from ZFC to ETCS that *do* involve internal > membership-structure, like distinguishing between {{}} and > {\beth_\omega}, one has to make that structure explicit by talking > about sets equipped with certain well-founded relations. There are > various ways to recover a model of a ZFC-like set theory inside ETCS: > rigid trees, accessible well-pointed graphs, etc. If one only wants > to talk about ordinal numbers, which is much more common, then one > doesn't need all that machinery; one can just talk about well-ordered > sets (up to isomorphism, like any other kind of structured set). > > ETCS is weaker than ZFC in that it doesn't include an analogue of the > axiom of replacement, which is needed for things like defining the > aleph function in generality. However, there are various ways to add > a replacement axiom to it, generally stated as a sort of "stack" > condition. This in particular allows defining families of sets by > recursion over well-founded relations, so that you can recurse over > any ordinal to get an aleph function on that ordinal, and then play > games with the analogue of proper classes to get "one aleph function" > if you like. > > Some of these issues are discussed in my preprint > https://arxiv.org/abs/1004.3802 . > > On Fri, Nov 24, 2017 at 2:36 PM, Neil Barton wrote: >> Dear All, >> >> I'm very interested in how categorial and material set theories >> interact, and in particular the advantages of each. >> >> It's well-known that categorial viewpoints are good for isolating >> schematic structural relationships. We can look at sets through this >> lens, by considering a categorial set theory like ETCS (possibly >> augmented, e.g. with replacement). A remark one sometimes finds is >> that once you have defined membership via arrows from terminal >> objects, you could use ETCS for all the purposes to which ZFC is >> normally put. >> >> My question is the following: >> >> (Q) To what extent can you ``do almost the same work'' with a >> categorial set theory like ETCS vs. a material set theory like ZFC? >> >> Just to give a bit more detail concerning what I'm thinking of: >> Something material set theory is reasonably good at is building models >> (say to analyse relative consistency), or comparing cardinality. >> However, there's no denying that for representing abstract >> relationships the language is somewhat clunky, since the same abstract >> schematic type can be multiply instantiated by structures with very >> different set-theoretic properties. So, to what extent can a >> categorial set theory like ETCS supply the good bits of the fineness >> of grain associated with material set theories, whilst modding out the >> `noise'? >> >> For example, the following are easily stated in material set theory: >> >> 1. \aleph_17 is an accessible cardinal. >> >> In material set theory, it's easy to define the aleph function and >> then state that the 17th position in this function can be reached by >> iterating powerset and replacement. But I wouldn't even know how to >> talk about specific sets of different cardinalities categorially. I >> suppose you could say something in terms of isomorphism between >> subobjects, and then exponentials, but it's quite unclear to me how >> the specifcs would go. Is that an easily claim to state (and prove) in >> ETCS? >> >> 2. How would you state that {{}} and {\beth_\omega} are very different >> objects? Set-theoretically, these look very different (just consider >> their transitive closures, for instance). But category-theoretically >> they should look the same---since they are both singletons they are >> isomorphic. So is this a case where their different set-theoretic >> propeties are considered just `noise', or where ETCS just wouldn't see >> a relationship, or where ETCS can in fact see some of these properties >> (and I'm just missing something)? >> >> 3. How would ETCS deal with model theory and cardinality ascriptions? >> (This links to a question asked earlier on this mailing list >> concerning syntactic theories in category theory, and whether from the >> categorial viewpoint we should be taking notice of them at all.) For >> instance, it's an interesting theorem (for characterising structure) >> that a first-order theory categorical in one uncountable power is >> categorical in every uncountable power (Morley's Theorem). But I have >> no idea how one might formalise this in something like ETCS---I know >> of Makkai and Reyes textbook (which I am currently reading) on >> categorial logic (where theories are represented by categories and >> models by functors), but I don't see how you could get >> categoricity-in-power claims out of the set up there. Can this be >> done? >> >> Any help and/or discussion would be greatly appreciated! >> >> Best Wishes, >> >> Neil >> >> -- >> Dr. Neil Barton >> Postdoctoral Research Fellow >> Kurt G=C3=B6del Research Center for Mathematical Logic >> University of Vienna >> Web: https://neilbarton.net/ >> >> >> [For admin and other information see: http://www.mta.ca/~cat-dist/ ] [For admin and other information see: http://www.mta.ca/~cat-dist/ ]