Given a type system T, and a type $A$ in that type system, is there an (effective) surjection from $\mathbb{N}$ onto the set of terms of that type?

Question

I assume that in hoping for an effective bijection, we run into undecidability issues, but intuitively, it seems like there should at least be a surjection from $\mathbb{N}$ to the terms of any type, since well-typed terms of type theories are essentially finite trees, the set of which has cardinality $\aleph_0$. So, given a type theory* $T$ and a (non-empty) type $A$ in that type theory, can we always construct such a surjection? If possible, I would like to get a reference describing such an algorithm, if anyone has explicitly described it.

* I suppose I should specify formally what I mean by type theory, but I am not aware of any name for "type theories in general," so what I mean is a system consisting of a finite number of axioms (or axiom schemas), and rules, where we say $t : T$ if any only if there is a deduction (which is a finite tree whose leaves are axioms, and whose edges are rules) with conclusion $t:T$. So, examples would be simple type theory, homotopy type theory, one of the various forms of Martin-Lof type theory, etc...

This question is related to mine, but what I am asking is more general.

Answer 1

As @cody already pointed out, you cannot hope to have such a surjection inside type theory because nat → nat is always internally uncountable by Cantor's diagonalization, i.e., given any alleged surjection f : nat → (nat → nat), the function λ n . (f n n) + 1 is not in the image of f.

Under very general assumptions the terms of all types, even uninhabited ones, are computably enumerable (or recursively enumerable in the old terminology). There is no need to exclude the empty set (an enumeration is allowed to skip). For instance, suppose that in a given type theory

1. The rules of inference are computably enumerable, and
2. It is semidecidable whether an instance of a rule is correctly used

Then, given any type A, we can enumerate its terms by dovetailing: in parallel we semidecide for every $n$ whether $n$ encodes a derivation of a term of type A. Note however that the program so obtained (when $A$ is nat) typically will not be expressible inside the type theory. It is a fun exercise to try to do it inside type theory anyway and figure out which bit does not work. Can you tell?

All type theories which we meet in practice satisfy these conditions, and so do all other formal systems that people come up with. (In fact, real-world formal systems have decidable sets of decidable rules, so clearly semidecidable as well.) That's because a formal system for which we cannot even tell whether it is being used correctly, is closer to transcedental meditation than to logic.

Answer 2

One could ask the same of set theory: isn't the set of terms that can be written down countable? Why isn't there a surjection from $\aleph_0$ to any set?

The answer, of course, is in the difference between internal truth and external truth.

Externally, the set of well typed terms of type $A$ (say in the empty context) is recursively enumerable in any reasonable type theory (like MLTT), so there is an effective surjection from $\mathbb{N}$ to that set iff it is non-empty, by a classical result in recursion theory.

Internally however, it is generally not possible to prove that such a surjection exists. In particular, a bijection between say, $\mathbb{N}$ and $\mathbb{N}\rightarrow\mathbb{N}$ implies a contradiction by a simple diagonalization argument (see, e.g., here).

In fact the proof works even if we only require a retract instead of a bijection. However this doesn't preclude a surjection from $\mathbb{N}$ to $\mathbb{N}\rightarrow\mathbb{N}$! It's only necessary that this surjection does not have a right inverse (in set theory, these right inverses always exist, but the proof of that requires the axiom of choice).

It is in fact consistent, but not provable, to assume that such a surjection exists.