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.

  • $\begingroup$ A computable surjection of $\mathbb N$ onto a set $X$ exists iff $X$ is nonempty and recursively enumerable. While your description is a bit vague, I’d assume that your sets are recursively enumerable. $\endgroup$ – Emil Jeřábek supports Monica Dec 13 '16 at 16:43
  • $\begingroup$ If you mean the axiom schemas and rules themselves, I am assuming a finiteness condition, so yes. Whether or not it follows that the set of terms of an arbitrary type itself is recursively enumerable I suppose is just another way of phrasing my question. $\endgroup$ – Nathan BeDell Dec 13 '16 at 17:10
  • 1
    $\begingroup$ Rather trivial, but consider a type theory with an uninhabited type. Or one in which it's undecidable whether a type is inhabited (e.g. each type is a formula of first-order logic and a term of this type is a proof of the formula). $\endgroup$ – Alexey Romanov Dec 13 '16 at 17:58
  • $\begingroup$ The empty set is computably enumerable. No need to make unihabited types special here. $\endgroup$ – Andrej Bauer Dec 14 '16 at 7:34
  • 1
    $\begingroup$ Wait, why is this on cstheory? It's not research-level, can we please migrate to cs.stackexchange.com? $\endgroup$ – Andrej Bauer Dec 14 '16 at 12:27

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.


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.