From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9461 Path: news.gmane.org!.POSTED!not-for-mail From: Patrik Eklund Newsgroups: gmane.science.mathematics.categories Subject: Re: How analogous are categorial and material set theories? Date: Thu, 07 Dec 2017 20:58:24 +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 1512675589 24835 195.159.176.226 (7 Dec 2017 19:39:49 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Thu, 7 Dec 2017 19:39:49 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Thu Dec 07 20:39:45 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 1eN21I-0006KD-S3 for gsmc-categories@m.gmane.org; Thu, 07 Dec 2017 20:39:45 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:40366) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1eN222-0005wf-1d; Thu, 07 Dec 2017 15:40:30 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1eN20Y-0007hh-N4 for categories-list@mlist.mta.ca; Thu, 07 Dec 2017 15:38:58 -0400 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9461 Archived-At: Is Category Theory a Theory? I think not. At least not in a logical sense. Is Logic a Theory. Of course not. Logic is a construction that embraces ways of creating logical theories. Can we describe Category in Logic? No, we cannot. Can we describe Logic in Category. Yes we can. Topos, and all that, even if I regret we are happy about quantifiers being adjoint functors to the contra powerfunctor. Logic should be a bit more than just that, shouldn't it? --- Can we describe Logic over Category? Yes we can. This is less recognized. This is the lative construction of logic from signatures, through terms, to sentences, and so on, as Goguen (Institutions) and Meseguer (Entailment Systems) did, without being explicit about signatures. This is Category Theory as a construction embracing ways of creating logics. We must be explicit about the starting point, the underlying signature. Just think about it, we potentially have the object of types in a monoidal category! It's just around the corner. Let's go get it, and the world will never be the same! --- Discussions under FOM now related to distinctions between first, second and third order logic is really bizarre, or boring to say the least. Much of what they try to say could be said more clearly if they would understand to use category theory as a construction site to build what they try to build. Hilbert was not a bad person, if you ask me. --- Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]