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.
1 to 8 of 8
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.
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.)
By the way, write [[equality]]
here to produce ‘equality’.
I guess that was my fault. Thanks for fixing it!
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?
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”.
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.
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)$.
1 to 8 of 8