Re: Predicativity in Categories

[Steve Vickers <s.j.vickers@cs.bham.ac.uk>]

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/ ]