Not signed in (Sign In)

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,