Why are the set of variables in lambda calculus typically defined as countable infinite?

Question

When reading formal descriptions of the lambda calculus, the set of variables seems to always be defined as countably infinite. Why this set cannot be finite seems clear; defining the set of variables as finite would restrict term constructions in unacceptable ways. However, why not allow the set to be uncountably infinite?

Currently, the most sensible answer to this question I have received is that choosing a countably infinite set of variables implies we may enumerate variables making the description of how to choose fresh variables, say for an alpha rewrite, natural.

I am looking for a definitive answer to this question.

Answer 1

The reason that this set is required to be countable is quite simple. Imagine that you had a bag full of the variables. There would be no way to count the number of variables in this bag unless the set was denumerable.

Note that bags are isomorphic to sacks.

Answer 2

Most definitions and constructs in maths and logic include only the minimal apparatus that is required to achieve the desired end. As you note, more than a finite number of variables may be required. But since no more than a countable infinity is required, why allow more?

Answer 3

Having a countable number of variables, and a computable bijection between them and ℕ, lets us create a bijection between Λ and ℕ:

1. #v = ⟨0, f(v)⟩, where f is the computable bijection between and ℕ (exists because is countable) and ⟨m, n⟩ is a computable bijection between ℕ² and ℕ.
2. #(L M) = ⟨1, ⟨#L, #M⟩⟩
3. #(λv. L) = ⟨2, ⟨#v, #L⟩⟩

The notation ⌜L⌝ represents c_{#L}, the church numeral representing the encoding of L. For all sets S, #S represents the set {#L | L ∈ S}.

---

This allows us to prove that lambda calculus is not decidable:

Let A be a non-trivial (not ∅ or Λ) set closed under α and β equality (if L ∈ A and L β= M, M ∈ A). Let B be the set {L | L⌜L⌝ ∈ A}. Assume that set #A is recursive. Then f, for which f(x) = 1 if x ∈ A and 0 if x ∉ A, must be a μ-recursive function. All μ-recursive functions are λ-definable*, so there must be an F for which:

F⌜L⌝ = c_1 ⇔ ⌜L⌝ ∈ A
F⌜L⌝ = c_0 ⇔ ⌜L⌝ ∉ A

By letting G ≡ λn. iszero (F ⟨1, ⟨n, #n⟩⟩) M_0 M_1, where M_0 is any λ-term in B and M_1 is any λ-term not in B. Note that #n is computable and therefore λ-definable.

Now just ask the question "Is G⌜G⌝ in B?". If yes, then G⌜G⌝ = M_1 ∉ B, so G⌜G⌝ could not have been in B (remember that B is closed under β=). If no, then G⌜G⌝ = M_0 ∈ B, so it must have been in B.

This is a contradiction, so A could not have been recursive, therefore no closed-under-β= non-trivial set is recursive.

Note that {L | L β= true} is closed under β= and non-trivial, so it is therefore not recursive. This means lambda calculus is not decidable.

---

* The proof that all computable functions are λ-definable (we can have a λ-term F such that F c_{n1} c_{n2} ... = c_{f(n1, n2, ...)}), as well as the proof in this answer, can be found in "Lambda Calculi With Types" by Henk Barendregt (section 2.2).

Answer 4

Uncountable collections of things seem to usually have uncomputable elements. I'm not sure that all uncountable collections have this property, but I strongly suspect they do.

As a result, you could never even write out the name of those elements in any reasonable way. For example, unlike a number like pi, you cannot have a program that writes out the digits Chaitin's constant past a certain finite number of digits. The set of computable real numbers is countably infinite, so the "additional" reals you get are uncomputable.

I also don't believe you gain anything from the set being uncountably infinite. So you would introduce uncomputable names without benefit (as far as I can see).