Re: The use-mention distinction and category theory

[Gershom B <gershomb@gmail.com>]

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 <metaweta@gmail.com> wrote:
> On Sun, Sep 3, 2017 at 1:19 PM, Baruch Garcia <baruchgarcia@gmail.com> 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/ ]