* Predicativity in Categories @ 2016-11-27 18:53 Sergey Goncharov 2016-11-30 11:01 ` Steve Vickers 2016-12-01 14:55 ` Thomas Streicher 0 siblings, 2 replies; 4+ messages in thread From: Sergey Goncharov @ 2016-11-27 18:53 UTC (permalink / raw) To: categories Dear Community, 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. 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. 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. 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. 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. Let me clarify. 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. On the other hand, classifying *something* can be OK, e.g. in extensive categories we can classify summands: 2 = 1 + 1 is a summand classifier, and extensive categories are certainly not considered to be impredicative, for every pretopos is extensive. 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). Sorry, if that all sounded jumbled, but maybe you can understand my concerns. 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. Looking forward to your answers. Sergey [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Predicativity in Categories 2016-11-27 18:53 Predicativity in Categories Sergey Goncharov @ 2016-11-30 11:01 ` Steve Vickers 2016-12-01 16:05 ` Sergey Goncharov 2016-12-01 14:55 ` Thomas Streicher 1 sibling, 1 reply; 4+ messages in thread From: Steve Vickers @ 2016-11-30 11:01 UTC (permalink / raw) To: Sergey Goncharov; +Cc: categories Dear Sergey, For myself, I'm not exactly sure I understand the original notion of predicativity, but I have a rule of thumb that seems to work and satisfy predicative mathematicians. I've frequently claimed that parts of my work are predicative, and no one has complained so far. In topos theory, as you point out, the subobject classifier and powersets indicate 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 predicative fragment. (Note that even exponentials, function sets, are not geometric, 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 cartesian theories) in general, are geometric, and they classify Kuratowski finite subobjects. My rule of thumb predicts that Kuratowski finite powersets are predicative, and there seems to be general agreement with that. My current work on arithmetic universes seeks a setting for pure geometric reasoning, without the non-geometric parts that exist in toposes, and independent of base topos so long as it has an nno. Best wishes, Steve Vickers. > On 27 Nov 2016, at 18:53, Sergey Goncharov <sergey.goncharov@fau.de> wrote: > > Dear Community, > > 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. > > 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. > > 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. > > 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. > > 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. > > Let me clarify. > > 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. > > On the other hand, classifying *something* can be OK, e.g. in extensive > categories we can classify summands: 2 = 1 + 1 is a summand classifier, > and extensive categories are certainly not considered to be > impredicative, for every pretopos is extensive. > > 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). > > Sorry, if that all sounded jumbled, but maybe you can understand my > concerns. > > 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. > > Looking forward to your answers. > > Sergey > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Predicativity in Categories 2016-11-30 11:01 ` Steve Vickers @ 2016-12-01 16:05 ` Sergey Goncharov 0 siblings, 0 replies; 4+ messages in thread From: Sergey Goncharov @ 2016-12-01 16:05 UTC (permalink / raw) To: Steve Vickers; +Cc: categories Dear Steve, thank you for your answer! Indeed, I was seeking for feedback in this style. Like you said, with the restrictions you adopt you are on a safe side, but those exclude function spaces, which are allowed in Martin-L?f TT, and the latter is commonly called predicative. I realize though that you have additional motivation for geometric logic (as a logic of observable properties, at least this is my current intuition, which I also picked up from your book) and that happens to be predicative. The reason I believe that one can potentially make sense of predicativity in categories is because I learned recently from the paper "Modular correspondence between dependent type theories and categories including pretopoi and topoi" by Maria Maietti that various classes of categories are uniformly described by their internal language written is the style of extensional dependent type theory. By incrementally extending the language one obtains narrower and narrower classes of categories ending up at toposes. Hence, I thought that there might be a way to formally classify such extensions as predicative or impredicative. Best regards, Sergey On 30/11/16 12:01, Steve Vickers wrote: > Dear Sergey, > > For myself, I'm not exactly sure I understand the original notion of > predicativity, but I have a rule of thumb that seems to work and > satisfy predicative mathematicians. I've frequently claimed that > parts of my work are predicative, and no one has complained so far. > > In topos theory, as you point out, the subobject classifier and > powersets indicate 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 predicative fragment. (Note that even exponentials, > function sets, are not geometric, 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 cartesian theories) in general, are geometric, and they classify > Kuratowski finite subobjects. My rule of thumb predicts that > Kuratowski finite powersets are predicative, and there seems to be > general agreement with that. > > My current work on arithmetic universes seeks a setting for pure > geometric reasoning, without the non-geometric parts that exist in > toposes, and independent of base topos so long as it has an nno. > > Best wishes, > > Steve Vickers. > >> On 27 Nov 2016, at 18:53, Sergey Goncharov >> <sergey.goncharov@fau.de> wrote: >> >> Dear Community, >> >> 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. >> ... >> Looking forward to your answers. >> >> Sergey >> [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Predicativity in Categories 2016-11-27 18:53 Predicativity in Categories Sergey Goncharov 2016-11-30 11:01 ` Steve Vickers @ 2016-12-01 14:55 ` Thomas Streicher 1 sibling, 0 replies; 4+ messages in thread From: Thomas Streicher @ 2016-12-01 14:55 UTC (permalink / raw) To: Sergey Goncharov; +Cc: categories Categorical Logic is such a versatile tool that it allows to give an account uf both impredicative and predicatives systems. A topos is a categorical account to higher order logic and thus impredicative. A logos (Freyd) gives an account of intuit. first order logic and thus is "predicative". A locally cartesian closed category (after splitting) is a model of Martin-Loef type theory. That is predicative. Both predicative and impredicative universes can be defined categorically within lcc's. This was done is the second half of the 1980s by many people (including myself). Whether category theory itself is "impredicative" however is an ill-posed question in my eyes. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2016-12-01 16:05 UTC | newest] Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2016-11-27 18:53 Predicativity in Categories Sergey Goncharov 2016-11-30 11:01 ` Steve Vickers 2016-12-01 16:05 ` Sergey Goncharov 2016-12-01 14:55 ` Thomas Streicher
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).