From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9041 Path: news.gmane.org!.POSTED!not-for-mail From: Steve Vickers Newsgroups: gmane.science.mathematics.categories Subject: Re: Predicativity in Categories Date: Wed, 30 Nov 2016 11:01:18 +0000 Message-ID: References: Reply-To: Steve Vickers NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 (1.0) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: quoted-printable X-Trace: blaine.gmane.org 1480530257 1700 195.159.176.226 (30 Nov 2016 18:24:17 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Wed, 30 Nov 2016 18:24:17 +0000 (UTC) Cc: categories@mta.ca To: Sergey Goncharov Original-X-From: majordomo@mlist.mta.ca Wed Nov 30 19:24:13 2016 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.7.28]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1cC9YC-0007ke-QL for gsmc-categories@m.gmane.org; Wed, 30 Nov 2016 19:24:12 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:44969) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1cC9XS-0001Uu-VT; Wed, 30 Nov 2016 14:23:26 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1cC9XU-0001yk-0D for categories-list@mlist.mta.ca; Wed, 30 Nov 2016 14:23:28 -0400 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9041 Archived-At: Dear Sergey, For myself, I'm not exactly sure I understand the original notion of predica= tivity, but I have a rule of thumb that seems to work and satisfy predicativ= e mathematicians. I've frequently claimed that parts of my work are predicat= ive, and no one has complained so far. In topos theory, as you point out, the subobject classifier and powersets in= dicate impredicativity. My rule of thumb is that "geometric" reasoning, preserved (up to isomorphism= ) by the inverse image parts of geometric morphisms, is safely within the pr= edicative fragment. (Note that even exponentials, function sets, are not geo= metric, so geometric reasoning is quite restricted.) The subobject classifier and powersets are not geometric. On the other hand, the free semilattices, along with free algebras (for cart= esian theories) in general, are geometric, and they classify Kuratowski fini= te subobjects. My rule of thumb predicts that Kuratowski finite powersets ar= e predicative, and there seems to be general agreement with that. My current work on arithmetic universes seeks a setting for pure geometric r= easoning, without the non-geometric parts that exist in toposes, and indepen= dent of base topos so long as it has an nno. Best wishes, Steve Vickers. > On 27 Nov 2016, at 18:53, Sergey Goncharov wrote= : >=20 > Dear Community, >=20 > I am recently racking my brains in trying to understand what > (im-)predicativity means from a categorical perspective, but failing > short, hence calling for you help. >=20 > Certain constructive principle are easy to accommodate (and understand!) > within category theory, e.g. the axiom of choice (all epis are split), > excluded middle (every mono is a coproduct summand), however this does > not seem to be the case with the notion of predicativity. >=20 > The rough intuition says that impredicative definitions attempt to > define things topdown: first by introducing a class, and then defining > elements of this class by their characteristic properties -- arguably, a > controversial idea, if you strive for foundations. >=20 > That intuition is sort of helpful to deal with extreme cases, e.g. to > accept that toposes are impredicative, and Martin-L??f type theory is > predicative, but it does not seem to give a complete answer. >=20 > The discussion and the papers I found on the web rather seem to reflect > the set-theoretic tradition in categorical terms, than to explain the > issue intrinsically. >=20 > Let me clarify. >=20 > We agree that toposes are impredicative (or, at least not compatible > with predicative approach) because they include subobject classifiers, > and those arguably classify to much, for according to Bishop, we have no > idea a priory, what an arbitrary subset of given set is like. >=20 > On the other hand, classifying *something* can be OK, e.g. in extensive > categories we can classify summands: 2 =3D 1 + 1 is a summand classifier, > and extensive categories are certainly not considered to be > impredicative, for every pretopos is extensive. >=20 > Now, there is a spectrum of classes of monomorphisms that could be > classified, depending on a category. I could e.g. try to classify > r.e-subsets in an effective topos. How can I know, if it is still OK or > not OK from a predicative perspective? (I realize that if we reject > impredicativity in foundations, we probably just can not construct any > example of a topos, including the effective one, but suppose, I still > can make sense of this idea of classifying r.e.-subsets somehow without > constructing a topos). >=20 > Sorry, if that all sounded jumbled, but maybe you can understand my > concerns. >=20 > I presume that a complete answer just does not exist, and would be a > subject to an open research, but I would be happy to understand at least > informally what sort of justification is used to claim that one category > is predicative (or predicative-friendly) and another one is not. >=20 > Looking forward to your answers. >=20 > Sergey >=20 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]