From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9421 Path: news.gmane.org!.POSTED!not-for-mail From: Patrik Eklund Newsgroups: gmane.science.mathematics.categories Subject: Re: How can we have a categorical definition of "theory" Date: Fri, 10 Nov 2017 06:56:59 +0200 Message-ID: Reply-To: Patrik Eklund NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit X-Trace: blaine.gmane.org 1510356871 22958 195.159.176.226 (10 Nov 2017 23:34:31 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Fri, 10 Nov 2017 23:34:31 +0000 (UTC) Cc: categories@mta.ca To: David Yetter Original-X-From: majordomo@mlist.mta.ca Sat Nov 11 00:34:27 2017 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp2.mta.ca ([198.164.44.40]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1eDIoc-0005jW-Nt for gsmc-categories@m.gmane.org; Sat, 11 Nov 2017 00:34:26 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:59675) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1eDIpQ-0004mQ-Sz; Fri, 10 Nov 2017 19:35:16 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1eDInz-0000Dr-U9 for categories-list@mlist.mta.ca; Fri, 10 Nov 2017 19:33:47 -0400 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9421 Archived-At: 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 > 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 > 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 > www.mta.ca > Web page for the category theory mailing list. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]