# 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

## Discussion Tag Cloud

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

• CommentRowNumber1.
• CommentAuthordan
• CommentTimeSep 5th 2013
• (edited Sep 6th 2013)

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.

• CommentRowNumber2.
• CommentAuthorTobyBartels
• CommentTimeSep 5th 2013

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.)

• CommentRowNumber3.
• CommentAuthorTobyBartels
• CommentTimeSep 5th 2013

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

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeSep 5th 2013

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

• CommentRowNumber5.
• CommentAuthordan
• CommentTimeSep 6th 2013

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?

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeSep 7th 2013

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”.

• CommentRowNumber7.
• CommentAuthordan
• CommentTimeSep 7th 2013
• (edited Sep 7th 2013)

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.

• CommentRowNumber8.
• CommentAuthorTobyBartels
• CommentTimeSep 13th 2013

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)$.