Predicativity in Categories

Predicativity in Categories

[Sergey Goncharov]

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

Re: Predicativity in Categories

[Steve Vickers]

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

Re: Predicativity in Categories

[Sergey Goncharov]

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

Re: Predicativity in Categories

[Thomas Streicher]

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