Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
I don’t understand; is the word “intentional” used in mathematics? What distinction are we drawing here?
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.
:-)
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.
Tom, can you elaborate? Which discussion made you realize that which use of terms was wrong?
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.
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.
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.
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.
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,
only when is -congruent.)
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.
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 is that it is equal to , whereas nobody in the beginning intended equalities like . 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 Lab 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 Lab pages, I think that would be a good service to the community.
Many meanings diverge from the same root.
cf. knight and knave. (-:
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?
The examples under type theory at equality are a bit arbitrary. These say that by definition, while 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 (as a term in a context where and 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).
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 -reduces to 4).
Yes, that’s what I meant.
@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
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?
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.
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.)
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.
Yeah, we had a discussion about that somewhere around here. In fact, just above!
I’ve edited equality in light of that.
I thought that what you wrote was confusing, so I did some expansion.
I like it!
Thanks!!
Thierry Coquand sent me further stuff by email, which has gone into the article under References (and a clarifying comment).
Thanks. The many uses of “extensional” really are a mess.
But they are all related! Each one makes sense (to me) in its own terms.
In some way, that makes it worse that they are nevertheless logically independent. (-:
Added to the References-section at equality a pointer to Science of Logic, volume 1, book 2, “Die Lehre vom Wesen”.
Would somebody be willing to answer this MO question about equality in structural set theory?
I've written something. Mike might want to comment as well (also Tom Leinster).
I don’t think I have much to add to Toby’s answer.
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?
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.
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.
Actually, I got error 524, so I'm not sure if it worked.
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!
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.
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
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).
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.
Most of the material on definitional equality moved to definition since it was actually about defining things using equality
Anonymous
moved information regarding conversional equality over to conversion rule
Anonymous
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.
1 to 64 of 64