This definition formalizes an infinite supply of variables. Each variable is identified by a natural number, but that number is not used anywhere. In fact, any infinite set would do.

Therefore, variables in the modelled language do not carry a name. Instead, we use bound variables in HLM (i.e. in the meta language) to model variables in the target language, and these bound variables have a name in HLM.

As a consequence, α-equivalent terms are never distinguishable.