Definition 5.1.  We define:
Var:=: {(n) | n ∈ }
(m) = (n)  :⇔  m = n  (m ∈ , n ∈ )
We write “let v be a variable” for “let v ∈ Var.”

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.