Re: The internal language of the category of categories



My particular context is a mixture of understanding a programming
language with an intutionistic logic, and the definition of something
I call "reasoning structures" of which I am saying that "toposes" are
a part. Furthermore, I am interested in infusing into our notions of
linguistics with the idea that formal languages with intiutionistic
logics will support the vital aspect of metaphor in language. Also, I
am interested in using a category of reasoning structures as a model
for social systems while enforcing the idea of translations between
reasoning structures, ie structure preserving maps in the category of
reasoning structures. I am looking for a good model of the impact of
the internet on civilization in the absence of empire.
So there, that's my context. Looking at web sites as objects in a
category and links as morphisms in that category makes clear that the
category of graphs, thus the category of categories is the best place
to understand the functionality of the internet. If we have the
internal language for the category of categories, then we have the
progamming language for the essential functinality of the internet.
As for why I am so interested in the intuitionistic side, it is the
translatability of reasoning that will be so vitally important in the
future.
Below is a posting of mine which addresses a particular view I have
on the subject. I wrote it before I had learned the adjoint functor
theorem. I sent this piece to Jim Lambek and he sent back a letter on
"putting one's finger on "the" category of SETS".

http://groups.google.com/group/sci.math/browse_thread/thread/e13b2cd54af1d992/58abd129fec38a6c#58abd129fec38a6c

I would phrase my problems with the set theoretic construction this
way "it heavily overburdens the theory of categories to the point
where the most important aspects get missed." It takes an entire
textbook in category theory to get to the adjoint functor theorem.
This is a failing of the current presentation of this theory and I put
the blame squarely on the set theoretic construction. In remedy to
this problem I would propose an alternate presentation of the theory
of categories starting with the adjoint functor theorem. OF course, I
am coming at this from the perspective of applied math, since I am a
scientist by training.
I looked at Lambek's book. In fact, I met with him last year. I
also tried talking about these things with John Bell, but both of
these guys are way, way beyond me. Also, I have a mixed background in
terms of my motivation in studying these subjects, so going into great
detail in terms of the means of calcuating these things doesn't appeal
to me enough (my bad).
I apologize for going way off topic here, but I am pleased to hear
each of your inputs. There are numerous questions I have on the
subject of the theory of categories and not all are as pedantic as the
one I posed earlier.
Thank you both for your responses.

Ben




On Jan 15, 4:07 pm, "Michal Przybylek" <m...@xxxxxxxxxxxx> wrote:
"Ben" <BenSpr...@xxxxxxxxx> wrote:
I believe, or want to believe the following statement, but I have no
way to calculate it

"The internal language of the category of categories has an
intuitionistic logic."
"The internal language of any strongly compact closed categories has
an intuitionistic logic."

Is this true?

I'm afraid, without any context this means nothing.

Perhaps the first statement refers to the internal language of a cartesian
closed category (which is alway intuitionistic). But I don't think CAT's
internal language is really interesting :-)

Also, can anyone give me some help on understanding
how to pinpoint the "internal language of a category"

Try "Introduction to Higher-order Categorical Logic" (J. Lambek, PJ. Scott).

mp
.

Relevant Pages

  • Re: The Promise of Forth
    ... but that can simply reflect the difficulty with language. ... And when your language includes internal contradictions, ... But when you find contradictions in your ... But there are nonstandard logics that can accommodate this just as there are non-Euclidean geometries. ...
    (comp.lang.forth)
  • Re: The Promise of Forth
    ... logical contraditions, it's sloppy. ... but that can simply reflect the difficulty with language. ... But our common culture still holds logic in a superstitious regard it manifestly doesn't deserve. ... (there are many "logics" these days, just as there are many "geometries") ...
    (comp.lang.forth)
  • Re: Rules of deduction.
    ... derived from words in spoken language, eg. if, not, all, some. ... The rules of inference in symbolic logic are derived from methods ... it is very interesting to see how quantification differs ... modern logics. ...
    (talk.origins)
  • WoLLIC2007 - Call for Participation
    ... 14th Workshop on Logic, Language, Information and Computation ... the Interest Group in Pure and Applied Logics ... It is likely that a few other international publishers will also take ... Marcelo da Silva Correa (U Fed Fluminense) ...
    (comp.specification.z)
  • Re: Godels incompleteness theorem vs Churchs/Turings work
    ... about to be incomplete, there must necessarily be ... a theory whose language consists of the propositional ... FOL is a logic. ... are THEORIES not NOT logics. ...
    (sci.logic)