Not signed in (Sign In)

Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeApr 24th 2012
    • (edited Nov 3rd 2013)

    I was involved in some discussion about where the word “intensional” as in “intensional equality” comes from and how it really differs from “intenTional” and what the point is of having such a trap of terms.

    Somebody dug out Martin-Löf’s lecture notes “Intuitionistic type theory” from 1980 to check. Having it in front of me and so before I forget, I have now briefly made a note on some aspects at equality in the section Different kinds of equalits (below the first paragraph which was there before I arrived.)

    Anyway, on p. 31 Martin-Löf has

    intensional (sameness of meaning)

    I have to say that the difference between “sameness of meaning” and “sameness of intenTion”, if that really is the difference one wants to make, is at best subtle.

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 24th 2012

    I suppose there were two options from the participles of the Latin tendere, tensum or tentum. Two lines of term derived from intendere, but only one from extendere, hence no need for extention.

    One difference is that intensional applies to sentences, whereas intentional applies to mental states.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeApr 24th 2012

    I don’t understand; is the word “intentional” used in mathematics? What distinction are we drawing here?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2012
    • (edited Apr 25th 2012)

    What distinction are we drawing here?

    That is my question: why the funny word “intensional equality” if it comes down (according to the citations I gave) to pretty much coinciding with the standard English word “intentional” (“intended equality”) ?

    I witnessed these discussions that went like this:

    A: This is called intensional identity.

    B: Why?

    C: Because it reflects the intention of the terms.

    A: No! Crucially not. It is spelled differently!

    B: So what’s the difference?

    A: Er, ahm, well. It’s some important distinction in linguistics.

    B: Namely?

    A: Er, well. Hm.

    :-)

    • CommentRowNumber5.
    • CommentAuthorTom Leinster
    • CommentTimeApr 25th 2012

    I have a bone to pick with intensional type theorists. Today I “corrected” someone’s spelling of “intentional” (as an ordinary English word) to “intensional”. Only when I read this discussion, hours later, did I realize that I had done wrong. Then I had to eat humble pie.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2012

    Tom, can you elaborate? Which discussion made you realize that which use of terms was wrong?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeApr 25th 2012

    I don’t actually see much relationship in meaning between “intensional” and “intentional”. I agree it’s unfortunate that they’re spelled so similarly. I have no idea why the word “intensional” is used to mean what it does, but I don’t spend much time worrying about it. I generally take it as a gift when we have a word in mathematics that doesn’t occur in common everyday language, like “operad” or “simplex” or “topos”, because then we can just give it a definition without worrying about to what extent that definition matches its everyday usage.

    Roughly, an intensional collection is one specified by the properties possesed by its elements, rather than by specifying its elements themselves (extensional). Similarly, an intensional function is given by specifying a rule, rather than by specifying the output associated to each input (extensional). Intensional identity is given by specifying a way or reason that two things are the same, rather than observing the fact of their equality (extensional).

    In everyday language, something is “intentional” when I did it on purpose. It seems to me that both intensional and extensional definitions are usually given on purpose. In philosophy, “intentional” appears to have another meaning that I’m not so familiar with, but which is also of questionable relationship to “intensional”; Wikipedia takes me to this page.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeApr 25th 2012

    Perhaps one should think of “intensional” as being derived from the same origin as “intensive quantity” (and similarly for their contrastive terms), rather than having anything to do with “intent”. I don’t know whether that’s etymologically correct, but it seems not unlikely.

    • CommentRowNumber9.
    • CommentAuthorZhen Lin
    • CommentTimeApr 25th 2012

    I always thought it was so that there would be a neat pairing between ‘intension’ and ‘extension’. Better to usurp an obscure word than a common one, really.

    Perhaps it’s also a matter of tradition. OED’s earliest citation is Hamilton [1840, Lectures on logic]:

    The Internal Quantity of a notion,—its Intension or Comprehension, is made up of‥the various characters connected by the concept itself into a single whole in thought.

    • CommentRowNumber10.
    • CommentAuthorTom Leinster
    • CommentTimeApr 25th 2012

    Urs, there’s nothing profound behind what I wrote. The document I was reading (someone else’s draft grant proposal) used “intentional” in its ordinary non-mathematical sense. Corrupted by seeing too many instances of the logic word “intensional”, I thought the spelling “intentional” looked wrong, and I mistakenly changed it to an s. Later, by chance, I read the discussion here and realized I’d goofed up. It’s sort of like when you read “latex pants” and accidentally mispronounce it, through mathematical conditioning.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeApr 25th 2012
    • (edited Apr 25th 2012)

    The word “intensional” in this sense is much older than Martin-Löf, so don’t blame type theorists. I’m surprised that David didn’t already give us a lecture about it. It indeed contrasts with “extensional”.

    The point of this, as I understand it, is given by T1 and T2 in the link found by Mike earlier. (Offhand, I would probably model this in a relative way: a functor between universes links intension in its domain with extension in its codomain, but no universe is inherently intensional or extensional.)

    The Stanford Encyclopedia has a page on intensional logic; the introduction “What is this about?” is just what it says on the tin. Again, we could model this with a map.

    The bit about substituting equals for equals (and the failure thereof) explains the type-theorists’ usage: one can substitute intensionally equal terms in all contexts but extensionally equal terms only when an appropriate law of extensionality holds. (That is,

    f(a)=f(b),P(a)P(b)f(a) = f(b),\; P(a) \;\vdash\; P(b)

    only when PP is ff-congruent.)

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 25th 2012

    As I said, I’m sure intension and intention derive etymologically from the same word intendere. There is then a very complicated story to be told about their histories, both lay and technical uses. But this is surely not surprising. Many meanings diverge from the same root. Spelling was rather more flexible in earlier times, and the availability of two participle forms does the rest.

    As Zhen Lin points out, Hamilton will certainly appear in the history. See this page of some lectures for a further term: intension, extension, protension.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2012
    • (edited Apr 25th 2012)

    Thanks, all. This is maybe not worth spending all our time with debating about. I’ll just summarize some reactions, but on my part we don’t need to further debate this. Thanks.

    Anyway, here is a summary feeling.

    I agree with all points about not abusing words with established meaning for mathematics. But this is why I find this instance here all the more unfortunate, instead of less, as it calls for confusion with an established meaning. When you talk to an audience about “intensional equality” you will have to tell them that while they will hear you say “intentional equality” all the time, that’s not what you are actually saying, and that while they might think that you are referring to intended equality of terms, this is indeed pretty much what you mean only that you insist to mean something just a tad different, really. Because the intention of the very notation 22 is that it is equal to s(s(0))s(s(0)), whereas nobody in the beginning intended equalities like exp(πi)+1=0\exp(\pi i ) + 1 = 0. This came pretty unintentional to mathematicians, when they first discovered it.

    All in all, a very unfortunate choice of terminology, to me. And while I do appreciate that “intensional” is modeled on “extensional”, I don’t see that, in turn, “extensional” is such a great term that we should model anything on it.

    Okay, that just to articulate my feelings. Of course these feeling are irrelevant, I do understand the technical points being made and thanks for all your input. Let’s not further dwell on this. I should have just announced an edit to the nnLab page instead of making it a question, I guess. :-)

    But if one of you finds the time to add more along the lines of the useful comments above to relevant nnLab pages, I think that would be a good service to the community.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeApr 25th 2012

    Many meanings diverge from the same root.

    cf. knight and knave. (-:

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeApr 25th 2012

    while they might think that you are referring to intended equality of terms, this is indeed pretty much what you mean only that you insist to mean something just a tad different, really

    I wouldn’t even mention this.

    cf. knight and knave. (-:

    If I asked you whether “knight” and “knave” derive from the same root, what answer would you give?

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeApr 25th 2012

    The examples under type theory at equality are a bit arbitrary. These say that 2=s(s(0))2 = s(s(0)) by definition, while 2+2=42 + 2 = 4 not by definition. But one can certainly write definitions down such that these are not the case. (It would be a bit perverse to write definitions that switched these, but it’s easy to write definitions that make both equalities definitional or neither.) A better example might be a+b=b+aa + b = b + a (as a term in a context where aa and bb are free variables for natural numbers). I don’t know any definition of addition of natural numbers (and suspect that none is possible) in which this holds by definition (although one can always add a rule that make the intensional equality hold by fiat).

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeApr 25th 2012

    If I asked you whether “knight” and “knave” derive from the same root, what answer would you give?

    I think I’ve been told that they do, but I have to admit to not doing the research myself. (-:

    These say that 2=s(s(0)) by definition, while 2+2=4 not by definition

    Moreover, many type theorists use the phrase “definitional equality” to mean “computational/conversional equality”, under which meaning 2+2=4 does hold (that is, 2+2 β\beta-reduces to 4).

    • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeApr 26th 2012

    Yes, that’s what I meant.

    • CommentRowNumber19.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 26th 2012
    • (edited Apr 26th 2012)

    @Mike 17 and Toby 15

    See the addendum at http://www.20kweb.com/etymology_dictionary_K/origin_of_the_word_knave.htm for a little hint, but I shall let the two of you continue as you see fit

    • CommentRowNumber20.
    • CommentAuthorjcmckeown
    • CommentTimeJun 8th 2012

    Hmmm... I see my confusion is not entirely endogenous, now, for I came here from HoTT-dot-o-r-g (the conversation was diverging from HoTT-proper) and the nlab page intending to quibble that " 2 + 2 = 4 " isn't part of the definition of "4" (nor of "2") but IS sometimes part of the definiton of "+"; and now I see Mike once said

    many type theorists use the phrase "definitional equality" to mean "computational/conversional equality"

    So... I'm not sure quite what to conclude. The practical question for me at the moment is: what adjective should one use instead of "definitional" in a publicly-readable website when one is trying to say that two structures, presented differently, still trivially encode the same information?

    • CommentRowNumber21.
    • CommentAuthorTobyBartels
    • CommentTimeJun 8th 2012

    I would probably have said ‘intensional’, but maybe that’s not right if intensional equality is a formal concept in one’s language and one uses a rule stating by fiat that certain things are intensionally equal even when they do not trivially encode the same information.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJun 8th 2012

    I don’t think I would recommend the blanket use of any particular adjective independent of the formal context, since the meaning of “presented”, “trivially”, “encode”, and “information” may vary. In a sense, higher category theory is all about distinguishing between precise gradations of the possible meanings of these words! (Also, as Toby points out, mathematicians have a distressing tendency to take words that used to be used informally and give them formal meanings, so that we have to find new words to use when we want to talk informally.)

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJul 19th 2012

    I have no time to take care of it right now, but maybe somebody reading this here has: by email I receive the following comment on the entry equality:


    At

    http://ncatlab.org/nlab/show/equality

    one can read “2+2” and “4” are not definitionally equal (but that “2” and “S(S(0))” are). Is it clear? One defines

    2 = S(S(0)) 4 = S(S(S(S(0))))

    and

    x+0 = x x+S(y) = S(x+y)

    the equality there being definitional (definition of +). It follows that

    2 + 2 = S(S(0)) + S(S(0)) = S(S(S(0)) + S(0)) = S(S(S(S(0)) + 0)) = S(S(S(S(0)))) = 4

    where all equalities are definitional.

    Martin-Lof (in talks) had a reference to Godel’s 58 Dialectica paper (I have only the 72 version here) where he talks in footnote 7 about the equality being understood as “intensional equality… This is always decidable for two given functions”. This reference might be relevant.

    • CommentRowNumber24.
    • CommentAuthorTobyBartels
    • CommentTimeJul 19th 2012

    Yeah, we had a discussion about that somewhere around here. In fact, just above!

    • CommentRowNumber25.
    • CommentAuthorTobyBartels
    • CommentTimeJul 19th 2012

    I’ve edited equality in light of that.

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeJul 20th 2012

    I thought that what you wrote was confusing, so I did some expansion.

    • CommentRowNumber27.
    • CommentAuthorTobyBartels
    • CommentTimeJul 20th 2012

    I like it!

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeJul 21st 2012

    Thanks!!

    • CommentRowNumber29.
    • CommentAuthorTobyBartels
    • CommentTimeJul 21st 2012

    Thierry Coquand sent me further stuff by email, which has gone into the article under References (and a clarifying comment).

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeJul 23rd 2012

    Thanks. The many uses of “extensional” really are a mess.

    • CommentRowNumber31.
    • CommentAuthorTobyBartels
    • CommentTimeJul 23rd 2012

    But they are all related! Each one makes sense (to me) in its own terms.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeJul 24th 2012

    In some way, that makes it worse that they are nevertheless logically independent. (-:

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2013

    Added to the References-section at equality a pointer to Science of Logic, volume 1, book 2, “Die Lehre vom Wesen”.

    • CommentRowNumber34.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 24th 2017

    Would somebody be willing to answer this MO question about equality in structural set theory?

    • CommentRowNumber35.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 24th 2017

    I've written something. Mike might want to comment as well (also Tom Leinster).

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 24th 2017

    I don’t think I have much to add to Toby’s answer.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)