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

<p>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 <em>skip</em>). For instance, suppose that in a given type theory</p>

<ol>
<li>The rules of inference are computably enumerable, and</li>
<li>It is semidecidable whether an instance of a rule is correctly used</li>
</ol>

<p>Then, given any type <code>A</code>, we can enumerate its terms by <a href="https://en.wikipedia.org/wiki/Dovetailing_(computer_science)" rel="nofollow noreferrer">dovetailing</a>: in parallel we semidecide for every $n$ whether $n$ encodes a derivation of a term of type <code>A</code>. Note however that the program so obtained (when $A$ is <code>nat</code>) 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?</p>

<p>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 <em>decidable</em> sets of <em>decidable</em> 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.</p>

CC BY-SA 3.0
2016-12-14T07:32:23.883Z
2016-12-14T16:45:18.983Z
2016-12-14T16:45:18.983Z
Andrej Bauer
<p>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?</p>

<p>The answer, of course, is in the difference between <strong>internal truth</strong> and <strong>external truth</strong>.</p>

<p><strong>Externally</strong>, 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.</p>

<p><strong>Internally</strong> 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., <a href="http://muaddibspace.blogspot.com/2009/10/cantors-diagonalization-proof-in-coq.html" rel="nofollow noreferrer">here</a>).</p>

<p>In fact the proof works even if we only require a <em>retract</em> 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).</p>

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

CC BY-SA 3.0
2016-12-13T22:19:45.393Z
2016-12-13T22:19:45.393Z
cody
<p>I assume that in hoping for an effective <em>bijection</em>, 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.</p>

<p>* 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...</p>

<p><a href="https://stackoverflow.com/questions/28685232/what-is-a-mapping-between-natural-numbers-and-valid-simply-typed-lambda-calculus">This question</a> is related to mine, but what I am asking is more general.</p>

CC BY-SA 3.0
2016-12-13T16:43:13.923Z
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.
Emil Jeřábek
CC BY-SA 3.0
2016-12-13T17:10:10.067Z
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.
Nathan BeDell
CC BY-SA 3.0
2016-12-13T17:58:16.147Z
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).
Alexey Romanov
CC BY-SA 3.0
2016-12-14T07:34:11.677Z
The empty set is computably enumerable. No need to make unihabited types special here.
Andrej Bauer
CC BY-SA 3.0
2016-12-14T12:27:53.447Z
Wait, why is this on cstheory? It's not research-level, can we please migrate to cs.stackexchange.com?
Andrej Bauer
<reference-request><type-theory>
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?
Nathan BeDell
# 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?

(Asked by: username_0 on 2016-12-13)

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](https://stackoverflow.com/questions/28685232/what-is-a-mapping-between-natural-numbers-and-valid-simply-typed-lambda-calculus) is related to mine, but what I am asking is more general.

**Tags:** reference-request, type-theory

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  
> **username_2**: 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).  
> **username_3**: The empty set is computably enumerable. No need to make unihabited types special here.  
> **username_3**: Wait, why is this on cstheory? It's not research-level, can we please migrate to cs.stackexchange.com?  

---

## 2 answers

### Answer by username_3 on 2016-12-14. Score: 5 | Accepted answer

As @username_4 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](https://en.wikipedia.org/wiki/Dovetailing_(computer_science)): 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 by username_4 on 2016-12-13. Score: 7

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](http://muaddibspace.blogspot.com/2009/10/cantors-diagonalization-proof-in-coq.html)).

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.


---

