From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9360 Path: news.gmane.org!.POSTED!not-for-mail From: Gershom B Newsgroups: gmane.science.mathematics.categories Subject: Re: The use-mention distinction and category theory Date: Tue, 26 Sep 2017 13:00:47 -0400 Message-ID: References: Reply-To: Gershom B NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" X-Trace: blaine.gmane.org 1506520192 21352 195.159.176.226 (27 Sep 2017 13:49:52 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Wed, 27 Sep 2017 13:49:52 +0000 (UTC) Cc: Baruch Garcia , categories To: Mike Stay Original-X-From: majordomo@mlist.mta.ca Wed Sep 27 15:49:41 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 1dxCiZ-0004px-Rb for gsmc-categories@m.gmane.org; Wed, 27 Sep 2017 15:49:39 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:45709) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1dxCjg-0005vo-Q5; Wed, 27 Sep 2017 10:50:48 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1dxChq-0001Nj-Ly for categories-list@mlist.mta.ca; Wed, 27 Sep 2017 10:48:54 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9360 Archived-At: I would suggest that one approach to the use-mention distinction is given in topos theory, or more generally in categorical logic, when we can talk about the "internal logic" of a category, and discuss objects of categories from both the internal and external standpoints. A common case of this arises in Mike's message when he discusses the internal hom. Godel, Halting, etc. all can be seen as statements based on a particular structure surrounding the internal hom as in [1]. [1] https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem Cheers, Gershom On Tue, Sep 5, 2017 at 1:36 PM, Mike Stay wrote: > On Sun, Sep 3, 2017 at 1:19 PM, Baruch Garcia wrote: >> Hello, >> >> I was wondering if someone of the categories list could answer this >> question: >> >> In Godel's/Tarski's theorem and the Halting problem, the use-mention >> distinction (e.g. Boston is populous, but "Boston" is disyllabic) is >> essential. Is there an analog to the use-mention distinction in category >> theory or is the use-mention distinction just its own principle independent >> of category theory? > > There's something like a distinction between use and mention in a > symmetric monoidal closed category. Given a morphism f:X -> Y, > there's the "name" of the function curry(f):I -> X -o Y, where I is > the monoidal unit and -o is the internal hom. The evaluation morphism > takes a value g of type X -o Y and a value x of type X and returns > uncurry(g)(x). > > > -- > 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/ ]