The use-mention distinction and category theory

The use-mention distinction and category theory

[Baruch Garcia]

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?

Any suggestion, insight, clarification would be appreciated.

Many Thanks!
Baruch


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The use-mention distinction and category theory

[Patrik Eklund]

Dear Baruch,

I am nothing but clumsy about such analytics, but let me try to
understand 'distinction' and 'analogue'. I would say that category might
help in being the metalanguage for logic that needs to build upon types.

Is natural language logical? Many might say yes, and also saying natural
language is even more so, but also logical.
Is natural language typed? I would say not at all, and I would even say
anti-typed, because natural language really needs to allow extreme
overlapping of types. This to me makes natural language alogical, or at
least a-mathematical_logical.

What makes
Boston (as a city)
Boston
in
Boston is populous?
And what do we mean by populous?
And what is
is
in
Boston is populous?

Can you see the missing character above? It's obviously the carriage
return, which helps to avoid parenthesis.
If we write all that on one line, it becomes the following:

What makes Boston (as a city) Boston in Boston is populous? And what do
we mean by populous? And what is is in Boston is populous?

I might try to use characters like
' " _ |
around words in that one line thing, but the more I use them, the more I
have to explain them. Peano said something like "we usually put
characters one by one side by side" about mathematical expressions, and
Church distinguished between formal and informal symbols, but we haven't
really been able to deal with these constraints properly within
mathematics, I would say. That two-dimensional thing about Boston
somehow avoids using extra characters.

Logically, is Boston and expression or just the name for an expression?
Boston could be a variable or a variable name. Then you can substitute
expressions as required. On the other hand, is Boston a statement or the
name for a statement? In that case substitutions can not be applied
similarly. If we say Boston is populous, Boston appears more like an
expression. There are semantic values than can be attached to Boston.
But if we say Who wants to go to Boston, we might assume Boston is
described by a set of statements which we use in argumentation. So there
you may have one use-mention distinction, namely, that use is closer to
expressions and substitutions, and in category we say it's closer to
being modelled by monads. Kleisli categories for monads are closer to
syntax and substitutions, whereas Eilenberg-Moore cagegories to monads
are closer to meaning and semantics. Statements representing mentioning,
however, lend themselves to be constructed by functors, not necessarily
extendable to monads. This is an important distinction in logic, not
well understood, in particular in first-order logic.

A bit far fetched it is, but I could say use use is monadic and mention
is simply functorial. However, my fellow category theoreticians might
see all these category and philosophy remarks as crap. They probably
are, but I feel there is also a distinction between categorically
philosophical and philosophically categorical, so it's crap on both of
these.

To me this dimensionality feeling above shows something similar that
happens in category theory about composition of natural transformations.
There is the ordinary composition, and there is the so called
star-composition. The Interchange Law for these compositions can be
written on one line, but is better understand when visualized in two
dimensions. Indeed, we sometimes call these compositions vertical and
horizontal, and refer to Godement's Cinq r??gles de calcul fonctoriel in
1958 and Ehresmann's work related to star compositions in 1960. Note in
the two-dimensionality above how lines are adjacent and that adjacency
makes sense, and also how each line makes sense in itself. So you can
read and verify going right and down basically in any order, so that by
the time you come to last question mark, your understanding of the whole
is not dependent on he order by which your eyes scan through that verse.

Take Shakespeare's "All the world's a stage". We wouldn't like to see
that on one line. Indeed, Shakespeare seems to use more than just
linebreaks. "At first, the infant," is something like that. It is also
interesting to see how he moves from age to age, mostly using "then",
sometimes at the end of the line, sometimes at the beginning, but going
into the sixth age he uses "shifts", before going into the societally
very expensive "last scene of all".

Is second childishness and mere oblivion,
Sans teeth, sans eyes, sans taste, sans everything.

What is second childishness? What is mere oblivion? I guess it's not
important because it might just be everything, something very hard to
model in logic and mathematics, and a nuisance in category theory as
well, I can assure you. Important is that it is, isn't it?

By the way, to me its fascinating to see how forearm fractures start to
increase after the fifth stage, and the number of hip fractures is
larger than the number of forearm fractures after the shift to the sans
everything age. You wouldn't believe it but national falls prevention
activity in Sweden builds largely upon this age transition modelling by
Shakespeare. This to me is one of the strongest proofs that category
theory can be applied in health care.

All the best,

Patrik



On 2017-09-03 22:19, 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?
>
> Any suggestion, insight, clarification would be appreciated.
>
> Many Thanks!
> Baruch
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: The use-mention distinction and category theory

[Mike Stay]

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

Re: The use-mention distinction and category theory

[Gershom B]

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

Re: The use-mention distinction and category theory

[Baruch Garcia]

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