From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9362 Path: news.gmane.org!.POSTED!not-for-mail From: Baruch Garcia Newsgroups: gmane.science.mathematics.categories Subject: Re: The use-mention distinction and category theory Date: Tue, 26 Sep 2017 14:17:38 -0500 Message-ID: References: Reply-To: Baruch Garcia NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" X-Trace: blaine.gmane.org 1506558100 18320 195.159.176.226 (28 Sep 2017 00:21:40 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Thu, 28 Sep 2017 00:21:40 +0000 (UTC) Cc: Mike Stay , categories To: Gershom B Original-X-From: majordomo@mlist.mta.ca Thu Sep 28 02:21:35 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 1dxMZy-0003dn-0O for gsmc-categories@m.gmane.org; Thu, 28 Sep 2017 02:21:26 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:45920) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1dxMar-0001NA-Dq; Wed, 27 Sep 2017 21:22:21 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1dxMZ1-0003eD-LM for categories-list@mlist.mta.ca; Wed, 27 Sep 2017 21:20:27 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9362 Archived-At: Thanks, Gershom. While Lawvere correctly points out that some try to misuse Godel's theorem, I disagree with his *philosophical *perspective of the equivalence of Cantor's diagonal argument and Godel's diagonal lemma. The former does not employ the use-mention distinction while the latter does. This is what gives rise to the "paradoxical" nature of Godel's theorem. Please read Quine's "The Ways of Paradox" for more. Regardless, Lawvere's approach to Godel and Tarski provides an important bridge between computer science and category theory. Best, BG On Tue, Sep 26, 2017 at 12:00 PM, Gershom B wrote: > 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/ ]