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/ ]