> For example, 6 has an additive inverse in ℤ but not in ℕ [...] (this is the reason why int often makes more sense than unsigned int in C, even when you have an unsigned value)
`unsigned int` isn't actually ℕ though, it's ℤ∕nℤ [1], i.e., the integers modulo n, which does have an additive inverse of 6 (being n−6).
The reason `int` often makes more sense is because it's a useful property that the additive inverse of 6 actually be less than 6 -- or more generally, that `int` isn't modular.
Agree with the overall point though, that 6 is an element of many "types". Of the CAS-adjacent languages I'm experienced with, TLA+ gets this right; SMTLIBv2 does not.
`unsigned int` isn't actually ℕ though, it's ℤ∕nℤ [1], i.e., the integers modulo n, which does have an additive inverse of 6 (being n−6).
The reason `int` often makes more sense is because it's a useful property that the additive inverse of 6 actually be less than 6 -- or more generally, that `int` isn't modular.
Agree with the overall point though, that 6 is an element of many "types". Of the CAS-adjacent languages I'm experienced with, TLA+ gets this right; SMTLIBv2 does not.
[1] https://en.wikipedia.org/wiki/Modular_arithmetic#Integers_mo...