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 <gershomb@gmail.com> 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 <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/ ]