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,

    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.

    • CommentRowNumber37.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 23rd 2020

    Should we organise things better here? We have ’definitional equality’ as a redirect for equality, and a section dealing with that form of equality on this page. Then we have judgmental equality which is all too brief. At the very least surely we need to note that definitional and judgmental equality are taken as synonyms in HoTT. Do other systems distinguish them?

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeAug 24th 2020

    The page equality has some philosophical remarks. I don’t know of any formal system that has a formal notion called “definitional equality” that’s distinct from judgmental equality, but some people use them with different philosophical meanings.

    • CommentRowNumber39.
    • CommentAuthorTobyBartels
    • CommentTimeAug 31st 2020

    I saw that propositional equality redirects to both equality and identity type, so I made it redirect only to the latter. We could similarly make definitional equality redirect to judgmental equality, except that there is very little written there, so I'm not doing that now.

    • CommentRowNumber40.
    • CommentAuthorTobyBartels
    • CommentTimeAug 31st 2020

    Actually, I got error 524, so I'm not sure if it worked.

    • CommentRowNumber41.
    • CommentAuthorGuest
    • CommentTimeSep 21st 2021
    Hi, I'm coming here directed by Mike after a discussion on HoTT Zulip. The discussion was about the diversity of terminology used to talk about equality in type theory (judgmental, definitional, intensional, computational, ...), sometimes with philosophical connotations, sometimes with implicit assumptions such as being decidable or not for judgmental equality, or such as whether β, or even η, have to be thought as "definitional" or not.

    I'm not an expert of all the diversity of literature on the subject but I was thinking that, maybe, it could be worth at least to make a short update of the pages judgmental equality and of the section type theory of the page equality so as to give a bit more context on the different definitions.

    Typically, my basic idea would be:

    - To join the paragraphs "definitional" and "computational" into one called "judgmental equality" (though still mentioning the alternative terminology "definitional" and "computational", with explanations of what they convey), with link to the page judgmental equality.

    - To then restructurate the three paragraphs "definitional", "computational" and "propositional" into two paragraphs of roughly equal size contrasting "judgmental equality" with "propositional equality".

    - The first paragraph would link to judgmental equality and condense the current two paragraphs "definitional" and "computational", moving part of the contents to the page judgmental equality so that the two paragraphs "judgmental equality" and "propositional equality" are well-balanced. It would discuss the different usages of the expression definitional equality (alpha-conversion, delta-conversion, optionally beta-reduction, optionally eta-conversion, ...). It would discuss the question of the decidability of the equality and of the orientation of the generators of the equality so that decidability can be achieved. I would mention the decidability issues with eta in recursive types (natural numbers, streams, ...).

    I'm not familiar with the terminology computational equality and I did not find many resources about it on the web, but I will mention that it is sometimes used as a synonym of judgmental equality. I would mention the difference between typed and untyped judgmental equality telling that the terminology "convertible" is commonly used in place of judgmental equality when it is untyped, especially in the context of Pure Type Systems.

    I would mention what kind of extensionality is achieved with eta-rules and that judgmental equality, thanks to the xi rule, has full functional extensionality. Maybe the xi rule should be discussed as its inclusion is sometimes questioned (see e.g. Martin-Löf 1975 http://archive-pml.github.io/martin-lof/pdfs/About-Models-for-Intuitionistic-Type-Theories-and-the-notion-of-Definitional-Equality-1975.pdf), but I know no reasonable type theory which excludes it, so maybe it is not worth mentioning the issue.

    I would mention further extensions of the idea of judgmental equality, where any arbitrary complex decidable rewriting system can serve as hard-wired equality. I'm thinking here to ideas present in the Calculus of Algebraic Constructions, Coq Modulo Theories, Deduction Modulo, ... even if they break with the purely "intensional" spirit providing only the canonical beta-delta-way to compute normal forms.

    - The second paragraph would list the identity type (linking to identity types), the (impredicative) definition of Leibniz equality, and the (heterogeneous) cubical equality (linking to cubical type theory even if cubical equality is not described there). It would explain that "propositional equality" is equality seen as a connective (or type former) so that it can be a component of arbitrary complex formulas. It would say that "propositional" is a historical terminology which is not necessarily well-chosen in retrospect of HoTT (since equality as a connective is not necessarily a proposition in the HoTT sense). It would explain how "propositional equality" leads to Martin-Löf's Extensional Type Theory when reflected back to judgmental equality (inheriting functional extensionality and proof-irrelevance).

    Maybe should it be mentioned that several equality type formers can coexist (as in two-level type theory).

    Probably further details would show up when trying to implement this plan but my first question is to get feedback on the idea. Would such update be ok for the maintainers of this page? If yes, are there things to take into account that I would not be aware of, etc.

    Note: I have no idea about what ∞-reduction and ∞-conversion are. Should this be dropped?
    • CommentRowNumber42.
    • CommentAuthorHugo Herbelin
    • CommentTimeSep 21st 2021
    It seems that my login timed out and I was moved to guest.
    • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeSep 21st 2021

    Just to say that if you are on top of these issues and have the vision and the energy that you seem to have in comment #41, then it would be best if you go ahead and make edits!

  1. adding some more information about definitional equality

    Anonymous

    diff, v27, current

    • CommentRowNumber45.
    • CommentAuthorGuest
    • CommentTimeSep 3rd 2022

    In my opinion, propositional equality in the context of type theory should be called “typal equality”, because many type theorists nowadays don’t call types “propositions”; they only call the (-1)-truncated types “propositions”. So “proposiitonal equalty” should be restricted in usage to the identity types which are actually valued in propositions/subsingletons/(-1)-truncated types.

  2. adding sentence saying that objective type theory does not have definitional equality

    Anonymous

    diff, v28, current

  3. Moving the stuff about objective type theory to the right section “computational equality” rather than “definitional equality”.

    Anonymous

    diff, v29, current

    • CommentRowNumber48.
    • CommentAuthorGuest
    • CommentTimeOct 25th 2022

    The notions of “computational equality” and “judgmental equality” aren’t the same. Judgmental equality is the equality which is defined as a judgment. Computational equality is the equality used in the beta conversion rules of types, and it could either be judgmental, as in Martin-Löf type theory for types which are not higher inductive types, or propositional, as in

  4. Moving the stuff about judgmental equality to its own section

    Anonymous

    diff, v29, current

    • CommentRowNumber50.
    • CommentAuthorGuest
    • CommentTimeOct 25th 2022

    One should also distinguish between typal equality (i.e. the identity type), and propositional equality (i.e. the type theory has two layers, one for types and one for propositions, and equality is a proposition).

    • CommentRowNumber51.
    • CommentAuthorGuest
    • CommentTimeOct 25th 2022

    One should also distinguish between equality of terms and equality of types. Identity types are only for equality of terms, while judgmental equality comes with variants for both equality of terms and equality of types.

    Similarly with computational equality, the notion of definitional equality of terms could be expressed in both judgmental and typal variants. Judgmental equality is used for definitional equality in the type theories with judgmental equality, such as Martin-Löf type theory and cubical type theory. The identity type is used in objective type theory for definitional equality of terms, as there is no judgmental equality, and everything is done through transport.

  5. Added a section on comparing judgmental and propositional equality

    Anonymous

    diff, v30, current

  6. Expanded lede of type theory section

    Anonymous

    diff, v30, current

  7. Added a table distinguishing the different notions of equality

    Anonymous

    diff, v31, current

  8. Added rules for definitions

    Anonymous

    diff, v36, current

  9. Most of the material on definitional equality moved to definition since it was actually about defining things using equality

    Anonymous

    diff, v36, current

  10. Similarly moved to definition

    Anonymous

    diff, v36, current

  11. moved information regarding conversional equality over to conversion rule

    Anonymous

    diff, v39, current

  12. added section on syntactic equality and alpha equivalence

    Anonymous

    diff, v43, current

  13. added section about equality in classical and constructive mathematics

    Anonymous

    diff, v49, current

  14. split contexts not needed for propositional equality

    Anonymous

    diff, v50, current

  15. fix typo

    Anonymous

    diff, v51, current

  16. Adding reference:

    Anonymouse

    diff, v56, current

    • CommentRowNumber64.
    • CommentAuthorUrs
    • CommentTimeMay 21st 2024

    Interesting the nature of that article by Buzzard (arXiv:2405.10387).

    It starts out on p. 1 with the phenomenon of non-unique isomorphism, but on p. 3 complains that the notion of equality in HoTT is “too weak, as things can be equal in more than one way”.

    I can understand that a practitioner in proof formalization may find 0-truncated systems more convenient and as such not find the further expressive freedom in HoTT to be useful.

    But a general treatise on the notion of equality might be more clear on the role of non-unique identity proofs.