Some questions about different notions of "theory"

Some questions about different notions of "theory"

[Mike Stay]

1) Finitary monads correspond to Lawvere theories.  Is there a name
for those monads that correspond to toposes?

2) In topos theory is there any analogous result to Lawvere's theorem
that the opposite of the category of free finitely generated gadgets
is equivalent to the Lawvere theory of gadgets?  Something like "the
opposite of the category of fooable gadgets is equivalent to the topos
of gadgets"?

3) nLab says a sketch is a small category T equipped with subsets
(L,C) of its limit cones and colimit cocones.  A model of a sketch is
a Set-valued functor preserving the specified limits and colimits.  Is
preserving limits and colimits like a ring homomorphism?  Preserving
both limits and colimits sounds like it ought to involve profunctors,
but maybe I'm level slipping.

-- 
Mike Stay - metaweta@gmail.com
http://www.cs.auckland.ac.nz/~mike
http://reperiendi.wordpress.com


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Some questions about different notions of "theory"

[ptj]

1) I'm not sure what Mike means by `those monads that correspond to toposes'
since most toposes don't correspond to monads on anything. I did investigate
those toposes which are monadic over Set, or a power of Set, in my papers
`When is a variety a topos?', Algebra Universalis 21 (1985), 198--212, and
`Collapsed toposes and cartesian closed varieties', J. Algebra 129 (1990),
446--480.

2) A possible answer to this question is that the (2-)category of finitely
presented minimal toposes (and logical functors) is equivalent to the dual
of the free topos (on no generators), where a topos is said to be minimal
if it has no proper full logical subtoposes. This is a result of Peter
Freyd, but I don't know whether he ever published it.

Peter Johnstone

On Nov 7 2017, Mike Stay wrote:

>1) Finitary monads correspond to Lawvere theories.  Is there a name
>for those monads that correspond to toposes?
>
>2) In topos theory is there any analogous result to Lawvere's theorem
>that the opposite of the category of free finitely generated gadgets
>is equivalent to the Lawvere theory of gadgets?  Something like "the
>opposite of the category of fooable gadgets is equivalent to the topos
>of gadgets"?
>
>3) nLab says a sketch is a small category T equipped with subsets
>(L,C) of its limit cones and colimit cocones.  A model of a sketch is
>a Set-valued functor preserving the specified limits and colimits.  Is
>preserving limits and colimits like a ring homomorphism?  Preserving
>both limits and colimits sounds like it ought to involve profunctors,
>but maybe I'm level slipping.
>
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

How can we have a categorical definition of "theory" ...

[Patrik Eklund]

How can we have a categorical definition of 'theory', when we do not
have a categorical definition of 'sentence'?

Institutions (Goguen) and Entailment Systems (Meseguer) do have a
Sentence functor but their underlying category of signatures is
abstract, so without sort (over a category?) and operators (potentially
over another category?).

Many-valuedness and its (algebraic) foundations is looking into these
things.

Just wondering if anybody is thinking along these lines. Uwe at least, I
guess.

Cheers,

Patrik

PS Why many-valuedness? Well, for one thing, everything in and around
Google and Facebook is many-valued.



On 2017-11-08 01:57, ptj@maths.cam.ac.uk wrote:
> 1) I'm not sure what Mike means by `those monads that correspond to
> toposes'
> since most toposes don't correspond to monads on anything. I did
> investigate
> those toposes which are monadic over Set, or a power of Set, in my
> papers
> `When is a variety a topos?', Algebra Universalis 21 (1985), 198--212,
> and
> `Collapsed toposes and cartesian closed varieties', J. Algebra 129
> (1990),
> 446--480.
>
> 2) A possible answer to this question is that the (2-)category of
> finitely
> presented minimal toposes (and logical functors) is equivalent to the
> dual
> of the free topos (on no generators), where a topos is said to be
> minimal
> if it has no proper full logical subtoposes. This is a result of Peter
> Freyd, but I don't know whether he ever published it.
>
> Peter Johnstone
>
> On Nov 7 2017, Mike Stay wrote:
>
>> 1) Finitary monads correspond to Lawvere theories.  Is there a name
>> for those monads that correspond to toposes?
>>
>> 2) In topos theory is there any analogous result to Lawvere's theorem
>> that the opposite of the category of free finitely generated gadgets
>> is equivalent to the Lawvere theory of gadgets?  Something like "the
>> opposite of the category of fooable gadgets is equivalent to the topos
>> of gadgets"?
>>
>> 3) nLab says a sketch is a small category T equipped with subsets
>> (L,C) of its limit cones and colimit cocones.  A model of a sketch is
>> a Set-valued functor preserving the specified limits and colimits.  Is
>> preserving limits and colimits like a ring homomorphism?  Preserving
>> both limits and colimits sounds like it ought to involve profunctors,
>> but maybe I'm level slipping.
>>
>>
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How can we have a categorical definition of "theory"

[Steve Vickers]

Dear Patrik,

Categorical logic can interpret, but doesn't rigidly follow, the
standard logical path of signature, formula and sentence to reach theory
= signature + sentences.

I guess that's the path you had in mind that underlies your question,
and it is also the path that influenced Goguen and Meseguer.

Even where categorical logic interprets that standard path, it can move
away from the "Hilbert-style" idea that a sentence is a formula with no
free variables. Look in Elephant part C (?) and you'll see that the
sentences there are sequents in context.

But categorical logic goes further than ordinary logic in its attempt to
define 'theory'. Think of a category as loosely motivated by sets. The
set constructions that logic most directly accesses - as formulae - are
subsets of finite products (of carriers). It struggles to get to other
constructions that category theory accesses quite naturally. Hence
category theory can - and does - define 'theory' in ways that seem quite
unnatural to a logician, either presented (for instance by sketches) or
completed (as classifying categories, such as Lawvere theories).

Regards,

Steve.

On 09/11/2017 07:13, peklund@cs.umu.se wrote:
> How can we have a categorical definition of 'theory', when we do not
> have a categorical definition of 'sentence'?
>
> Institutions (Goguen) and Entailment Systems (Meseguer) do have a
> Sentence functor but their underlying category of signatures is
> abstract, so without sort (over a category?) and operators (potentially
> over another category?).
>
> Many-valuedness and its (algebraic) foundations is looking into these
> things.
>
> Just wondering if anybody is thinking along these lines. Uwe at least, I
> guess.
>
> Cheers,
>
> Patrik
>
> PS Why many-valuedness? Well, for one thing, everything in and around
> Google and Facebook is many-valued.
>



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Some questions about different notions of "theory"

[Andrée Ehresmann]

In answer to Mike:

"3) nLab says a sketch is a small category T equipped with subsets (L,C)
of its limit cones and colimit cocones. A model of a sketch is a
Set-valued functor preserving the specified limits and colimits. Is
preserving limits and colimits like a ring homomorphism? Preserving both
limits and colimits sounds like it ought to involve profunctors, but
maybe I'm level slipping." Sketches were introduced by Charles Ehresmann
in 1966 (and developed by us and our research students) in several
papers, among which I'll cite: (i) The main Charles' paper "ESQUISSES ET
TYPES DES STRUCTURES ALG??BRIQUES", Bul. Inst. Pol. Iasi, Tome XIV-1-2,
1968 (in French), reprinted in
http://ehres.pagesperso-orange.fr/C.E.WORKS_fichiers/Ehresmann_C.-Oeuvres_IV_1.pdf
on p. 19-32 (with several Comments in English I added on p. 329-332);
(ii) Our joint paper "Categories of sketched structures", Cahiers
Top.GDC XIII-2, 1972
http://www.numdam.org/article/CTGDC_1972__13_2_104_0.pdf I have been
surprised to see the definition given in nLab of a sketch as a category
with some limit-cones and co-limit-cones. For us, a 'sketch' is a
category S (or even a graph) with some distinguished cones and co-cones
(but not necessarily (co-)limit-cones). And in the above citation we
construct the 'prototype' of the sketch which is constructed by forcing
the (co-)cones to become (co-)limit-cones. Indeed, our idea was that a
sketch describes a 'smaller' presentation of a generalized algebraic
structure (for instance of categories themselves), and from it we
deduced its prototype and also its type (analogue of the theory for
Lawvere algebraic structures). The 'realisation' (or 'model') of a
sketch S in a category C is then a functor from S to C which transforms
the distinguished (co-)cones into (co-)limit-cones. There is no need of
profunctors here. Let us note that C is not required to admit all
(co-)limits, just the images of the distinguished (co-)cones must become
(co-)limit-cones. An initial 1959 example (at the basis of Charles'
definition) was the notion of a 'differentiable category' which is a
model of the sketch of categories into the category of differentiable
maps (which admits limits but only specific co-limits). Sincerely Andree



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Some questions about different notions of "theory"

[Michael Shulman]

On Thu, Nov 9, 2017 at 3:26 AM, Andrée Ehresmann
<andree.ehresmann@u-picardie.fr> wrote:
> I have been
> surprised to see the definition given in nLab of a sketch as a category
> with some limit-cones and co-limit-cones. For us, a 'sketch' is a
> category S (or even a graph) with some distinguished cones and co-cones
> (but not necessarily (co-)limit-cones).

Thanks for pointing this out.  I think this is an error on the nLab
page, or perhaps a sloppy phrasing that got misinterpreted by a later
editor; I'll fix it.  In the case when a sketch is a graph rather than
a category, it has to come equipped also with some distinguished
diagrams that are supposed to commute in its models, right?


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Some questions about different notions of "theory"

[Mike Stay]

On Tue, Nov 7, 2017 at 4:57 PM,  <ptj@maths.cam.ac.uk> wrote:
> 1) I'm not sure what Mike means by `those monads that correspond to toposes'
> since most toposes don't correspond to monads on anything.

I'm sorry, I meant "those monads that correspond to higher-order
theories", where a higher-order theory gets interpreted in a topos in
the same way that a Lawvere theory gets interpreted in a category with
finite products.
-- 
Mike Stay - metaweta@gmail.com
http://www.cs.auckland.ac.nz/~mike
http://reperiendi.wordpress.com


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Some questions about different notions of "theory"

[ptj]

Dear Mike,

Thanks for the clarification, but the same comment applies: most higher-
order theories don't correspond to anything as simply described as a monad
(just as most first-order theories don't, but only the very special class
of algebraic theories). For first-order theories (including infinitary
ones) you have the notion of sketch, but that (unlike a monad) is still
presentation-dependent (i.e. it varies according to which parts of the
structure you're modelling you regard as primitive); if you want something
that doesn't depend on the presentation, you need to go all the way to the
syntactic category, which essentially consists of `everything that has to
be present in a category containing a model of the theory under
consideration' (just as a Lawvere theory contains all the operations which
have to be present in a model of an algebraic theory). Syntactic categories
can also be constructed for higher-order theories, and they are in fact
toposes; but they tend to be insanely complicated (even the free topos,
which corresponds to the empty theory, has an incredibly rich structure).

Peter Johnstone

On Nov 9 2017, Mike Stay wrote:

>On Tue, Nov 7, 2017 at 4:57 PM,  <ptj@maths.cam.ac.uk> wrote:
>> 1) I'm not sure what Mike means by `those monads that correspond to
>> toposes' since most toposes don't correspond to monads on anything.
>
>I'm sorry, I meant "those monads that correspond to higher-order
>theories", where a higher-order theory gets interpreted in a topos in
>the same way that a Lawvere theory gets interpreted in a category with
>finite products.
>



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How can we have a categorical definition of "theory"

[Patrik Eklund]

Thanks, Steve.

On 2017-11-10 15:33, Steve Vickers wrote:
> Dear Patrik,
>
> Categorical logic can interpret, but doesn't rigidly follow, the
> standard logical path of signature, formula and sentence to reach
> theory
> = signature + sentences.

You could also more broadly write that equality as something like

Logic = Sign (giving terms) + Sen + |- + |= + Ax + Th + Inf

or in some alternative order, but clearly say that + is not commutative,
meaning "logic is latively constructed".

> I guess that's the path you had in mind that underlies your question,
> and it is also the path that influenced Goguen and Meseguer.

I did, but we should recall Sign in their model enters concretely only
in examples, not in the general model. We require to have in the general
model, so that we truly have a general substitution model.

> Even where categorical logic interprets that standard path, it can move
> away from the "Hilbert-style" idea that a sentence is a formula with no
> free variables. Look in Elephant part C (?) and you'll see that the
> sentences there are sequents in context.

We have to get rid of "free", because it's outside the categorical
machinery.

> But categorical logic goes further than ordinary logic in its attempt
> to
> define 'theory'.

I think it goes further away rather than further.

> Think of a category as loosely motivated by sets. The
> set constructions that logic most directly accesses - as formulae - are
> subsets of finite products (of carriers). It struggles to get to other
> constructions that category theory accesses quite naturally. Hence
> category theory can - and does - define 'theory' in ways that seem
> quite
> unnatural to a logician, either presented (for instance by sketches) or
> completed (as classifying categories, such as Lawvere theories).

I have difficulties with sets only. We can act over monoidal closed
categories.

Let me again underline that we are driven by concrete and real
applications of these logic constructions.

Categorical "logic" in a topos to me makes no practical sense at all.

Patrik


>
> Regards,
>
> Steve.
>
> On 09/11/2017 07:13, peklund@cs.umu.se wrote:
>> How can we have a categorical definition of 'theory', when we do not
>> have a categorical definition of 'sentence'?
>>
>> Institutions (Goguen) and Entailment Systems (Meseguer) do have a
>> Sentence functor but their underlying category of signatures is
>> abstract, so without sort (over a category?) and operators
>> (potentially
>> over another category?).
>>
>> Many-valuedness and its (algebraic) foundations is looking into these
>> things.
>>
>> Just wondering if anybody is thinking along these lines. Uwe at least,
>> I
>> guess.
>>
>> Cheers,
>>
>> Patrik
>>
>> PS Why many-valuedness? Well, for one thing, everything in and around
>> Google and Facebook is many-valued.
>>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How can we have a categorical definition of "theory"

[Steve Vickers]

Dear Patrik,

It's absolutely vital to Grothendieck's idea of toposes as generalized
spaces. It's essentially categorical logic that allows you to think of
toposes as spaces and geometric morphisms as continuous maps.

For an introduction, see my TACL talks

   http://www.cs.bham.ac.uk/~sjv/talks.php

particularly numbers 1-4 (the Olomouc tutorials).

Steve.

On 10/11/2017 16:49, peklund@cs.umu.se wrote:
> ...
>
> Categorical "logic" in a topos to me makes no practical sense at all.
>
> Patrik
>
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How can we have a categorical definition of "theory"

[Patrik Eklund]

Operads is just another name for signatures (sorts and operators).
Operads emphasize arity a bit more, which might invite operads and
signatures e.g. "over monoidal categories" to try out different paths,
but "over Set" they are the same.

Operads tend to "overlook" the distinction between constant and
variable, as seen e.g. in tree automata.

Anyway, terms (from signatures) have been formally constructed by means
of monads over monoidal categories, but sentence functors are rare.

In predicate calculus, the (informal!) quantifier symbols are
problematic, as they disable a functorial sentence construction. G??del
treats those symbols as formal since they are part of his numbering.
I've often said that self-referentiality is what makes incompleteness
theorems dubious, but treating quantifier symbols as formal ones and
disabling categorical constructions is probably the root of that
"G??del's success story".

The concept of 'theory' in universal algebra (Lawvere theories) and in
generalized logic (Goguen, Meseguer, and as we have generalized it to
fully embrace signatures) is related but not the same.

Let me indeed underline that when terms and sentences are categorically
constructed, they are not just "strings of symbols". Monoids are not
that universal.

Let me also restate that in our developments of these things (including
practical applications) we prefer to say that logic must be 'lative' in
the sense that terms are constructed in order to enable sentence
construction, and so on, and later in that "lative chain" comes
'theory', and many other things making 'logic' a categorical object. In
that category, still to be fully unravelled, morphisms are really
challenging and fascinating.

We feel there is a growing interest in such 'lative' approaches, and we
do invite the CT community to be more curious about such foundational
things.

Best,

Patrik



On 2017-11-10 03:55, David Yetter wrote:
> In what way is defining a theory dependent on defining a sentence?
>
>
> There are lots of categorical definitions of theories of various sorts:
>
>
> Operads, PROPs, Lawvere theories,..., even monads.
>
>
> One of the points of category theory, esp. higher category theory, has
>
> been to liberate mathematical thought from being bound to strings of
>
> symbols like terms and sentences.
>
>
> Best Thougths,
>
> David Yetter
>
> Professor of Mathematics
>
> Kansas State University
>
> ________________________________
> From: Patrik Eklund <peklund@cs.umu.se>
> Sent: Thursday, November 9, 2017 1:13 AM
> To: categories@mta.ca
> Subject: categories: How can we have a categorical definition of
> "theory" ...
>
> How can we have a categorical definition of 'theory', when we do not
> have a categorical definition of 'sentence'?
>
> Institutions (Goguen) and Entailment Systems (Meseguer) do have a
> Sentence functor but their underlying category of signatures is
> abstract, so without sort (over a category?) and operators (potentially
> over another category?).
>
> Many-valuedness and its (algebraic) foundations is looking into these
> things.
>
> Just wondering if anybody is thinking along these lines. Uwe at least,
> I
> guess.
>
> Cheers,
>
> Patrik
>
> PS Why many-valuedness? Well, for one thing, everything in and around
> Google and Facebook is many-valued.
>
>
>
> On 2017-11-08 01:57, ptj@maths.cam.ac.uk wrote:
>> 1) I'm not sure what Mike means by `those monads that correspond to
>> toposes'
>> since most toposes don't correspond to monads on anything. I did
>> investigate
>> those toposes which are monadic over Set, or a power of Set, in my
>> papers
>> `When is a variety a topos?', Algebra Universalis 21 (1985), 198--212,
>> and
>> `Collapsed toposes and cartesian closed varieties', J. Algebra 129
>> (1990),
>> 446--480.
>>
>> 2) A possible answer to this question is that the (2-)category of
>> finitely
>> presented minimal toposes (and logical functors) is equivalent to the
>> dual
>> of the free topos (on no generators), where a topos is said to be
>> minimal
>> if it has no proper full logical subtoposes. This is a result of Peter
>> Freyd, but I don't know whether he ever published it.
>>
>> Peter Johnstone
>>
>> On Nov 7 2017, Mike Stay wrote:
>>
>>> 1) Finitary monads correspond to Lawvere theories.  Is there a name
>>> for those monads that correspond to toposes?
>>>
>>> 2) In topos theory is there any analogous result to Lawvere's theorem
>>> that the opposite of the category of free finitely generated gadgets
>>> is equivalent to the Lawvere theory of gadgets?  Something like "the
>>> opposite of the category of fooable gadgets is equivalent to the
>>> topos
>>> of gadgets"?
>>>
>>> 3) nLab says a sketch is a small category T equipped with subsets
>>> (L,C) of its limit cones and colimit cocones.  A model of a sketch is
>>> a Set-valued functor preserving the specified limits and colimits.
>>> Is
>>> preserving limits and colimits like a ring homomorphism?  Preserving
>>> both limits and colimits sounds like it ought to involve profunctors,
>>> but maybe I'm level slipping.
>>>
>>>
>>
>>
>> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
> Categories Home Page - Mount Allison University |
> Homepage<http://www.mta.ca/~cat-dist/>
> www.mta.ca
> Web page for the category theory mailing list.
>
>
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
> Categories Home Page - Mount Allison University |
> Homepage<http://www.mta.ca/~cat-dist/>
> www.mta.ca
> Web page for the category theory mailing list.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How can we have a categorical definition of "theory"

[David Yetter]

In what way is defining a theory dependent on defining a sentence?

There are lots of categorical definitions of theories of various sorts:

Operads, PROPs, Lawvere theories,..., even monads.

One of the points of category theory, esp. higher category theory, has
been to liberate mathematical thought from being bound to strings of
symbols like terms and sentences.

Best Thougths,
David Yetter
Professor of Mathematics
  Kansas State University


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]