From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9423 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 18:49:26 +0200 Message-ID: References: Reply-To: Patrik Eklund NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit X-Trace: blaine.gmane.org 1510357106 29794 195.159.176.226 (10 Nov 2017 23:38:26 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Fri, 10 Nov 2017 23:38:26 +0000 (UTC) Cc: categories@mta.ca To: Steve Vickers Original-X-From: majordomo@mlist.mta.ca Sat Nov 11 00:38:22 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 1eDIsQ-0007Xh-Cp for gsmc-categories@m.gmane.org; Sat, 11 Nov 2017 00:38:22 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:59691) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1eDItB-0005Fj-Ck; Fri, 10 Nov 2017 19:39:09 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1eDIrk-0000JV-BS for categories-list@mlist.mta.ca; Fri, 10 Nov 2017 19:37:40 -0400 In-Reply-To: <5A05AAB4.5020000@cs.bham.ac.uk> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9423 Archived-At: 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/ ]