Definition 5.1. We define:

Var :=: {(*n*) | *n* ∈ ℕ}

We write “let *v* be a variable” for “let *v* ∈ Var.”

Remarks.

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.