Re: The use-mention distinction and category theory

[Baruch Garcia <baruchgarcia@gmail.com>]

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