Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthordan
   • CommentTimeSep 5th 2013
   • (edited Sep 6th 2013)
   • PermaLink
   Author: dan
   Format: MarkdownItexFirst of all: Hello everyone! Thanks for the great work on the nLab. So far it was a joy to absorb a lot, but today I shall actively engage in the discussion for the first time. On the page about [[equality]] in the section about definitional equality the following is said: "The most basic one is **definitional equality or intensional equality**. ... " As well as: "For instance the symbols “2” and “s(s(0))” (meaning the successor of the successor of 0) are **definitionally/extensionally** equal terms (of type the natural numbers):" Can both these statements be true? If so, I think this is a bit confusing and some clarification would be great. Edit: Inserted Toby's link syntax hint.

   First of all: Hello everyone! Thanks for the great work on the nLab. So far it was a joy to absorb a lot, but today I shall actively engage in the discussion for the first time.

   On the page about equality in the section about definitional equality the following is said: “The most basic one is definitional equality or intensional equality. … “

   As well as: “For instance the symbols “2” and “s(s(0))” (meaning the successor of the successor of 0) are definitionally/extensionally equal terms (of type the natural numbers):”

   Can both these statements be true? If so, I think this is a bit confusing and some clarification would be great.

   Edit: Inserted Toby’s link syntax hint.

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeSep 5th 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI\'m pretty sure that the second one is a mistake; I\'ve fixed it. (Of course, they are *also* extensionally equal, since that is a weaker condition, but that\'s not the point.)

   I'm pretty sure that the second one is a mistake; I've fixed it. (Of course, they are also extensionally equal, since that is a weaker condition, but that's not the point.)

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeSep 5th 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexBy the way, write `[[equality]]` here to produce ‘[[equality]]’.

   By the way, write [[equality]] here to produce ‘equality’.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeSep 5th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexI guess that was my fault. Thanks for fixing it!

   I guess that was my fault. Thanks for fixing it!

5. • CommentRowNumber5.
   • CommentAuthordan
   • CommentTimeSep 6th 2013
   • PermaLink
   Author: dan
   Format: MarkdownItexSure, now I see! So a set of extensionally equal functions might contain one or more subsets of intensionally equal functions, because we are only looking at the relation that the function generates (semantics) and not the notation (syntax). But is it really definitional equality in the latter case? Can I not interchange different constructions for the natural numbers that "2" and "s(s(0))" represent? For example [von Neumann](https://en.wikipedia.org/wiki/Natural_numbers#A_standard_construction) or [this one](https://en.wikipedia.org/wiki/Natural_numbers#Other_constructions) (which I think is quite beautiful). Or would it be the case, that we define/construct the natural numbers and then decide on different kinds of syntactic sugar to represent them?

   Sure, now I see! So a set of extensionally equal functions might contain one or more subsets of intensionally equal functions, because we are only looking at the relation that the function generates (semantics) and not the notation (syntax). But is it really definitional equality in the latter case? Can I not interchange different constructions for the natural numbers that “2” and “s(s(0))” represent? For example von Neumann or this one (which I think is quite beautiful). Or would it be the case, that we define/construct the natural numbers and then decide on different kinds of syntactic sugar to represent them?

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeSep 7th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> So a set of extensionally equal functions might contain one or more subsets of intensionally equal functions Each extensional-equality-class of functions contains many distinct intensional-equality-classes; is that what you mean? > Can I not interchange different constructions for the natural numbers that "2" and "s(s(0))" represent? I would say that neither of those strings of symbols has any meaning until you've fixed a meaning of "the natural numbers".

   So a set of extensionally equal functions might contain one or more subsets of intensionally equal functions

   Each extensional-equality-class of functions contains many distinct intensional-equality-classes; is that what you mean?

   Can I not interchange different constructions for the natural numbers that “2” and “s(s(0))” represent?

   I would say that neither of those strings of symbols has any meaning until you’ve fixed a meaning of “the natural numbers”.

7. • CommentRowNumber7.
   • CommentAuthordan
   • CommentTimeSep 7th 2013
   • (edited Sep 7th 2013)
   • PermaLink
   Author: dan
   Format: MarkdownItex> Each extensional-equality-class of functions contains many distinct intensional-equality-classes; is that what you mean? Yep, need to get more into the formal language. > I would say that neither of those strings of symbols has any meaning until you’ve fixed a meaning of “the natural numbers”. Okay. That would be everything then. Thanks to everyone for helping me understand.

   Each extensional-equality-class of functions contains many distinct intensional-equality-classes; is that what you mean?

   Yep, need to get more into the formal language.

   I would say that neither of those strings of symbols has any meaning until you’ve fixed a meaning of “the natural numbers”. Okay. That would be everything then.

   Thanks to everyone for helping me understand.

8. • CommentRowNumber8.
   • CommentAuthorTobyBartels
   • CommentTimeSep 13th 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex>I would say that neither of those strings of symbols has any meaning until you've fixed a meaning of "the natural numbers". To follow up on that: The two different constructions in Wikipedia, linked earlier, are ways of fixing such a meaning in material set theory. This is different from any business about comparing $2$ to $s(s(0))$ (which may be interpreted in material set theory using either construction or may be interpreted in something much simpler, such as Peano arithmetic). In any case, we do always have $2 = s(s(0))$ by definitional equality, at least as long as $2$ is defined as $s(1)$ and $1$ is defined as $s(0)$.

   I would say that neither of those strings of symbols has any meaning until you’ve fixed a meaning of “the natural numbers”.

   To follow up on that: The two different constructions in Wikipedia, linked earlier, are ways of fixing such a meaning in material set theory. This is different from any business about comparing $2$ to $s(s(0))$ (which may be interpreted in material set theory using either construction or may be interpreted in something much simpler, such as Peano arithmetic). In any case, we do always have $2 = s(s(0))$ by definitional equality, at least as long as $2$ is defined as $s(1)$ and $1$ is defined as $s(0)$.