Skip to main content
1 of 2
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 240

You are looking for realizability toposes and related categories, as was already pointed out in the comments. Let me make a quick summary of how things work and why we can completely circumvent the dilemmas involving arbitrary codings of objects with strings.

To understand what is going on we do not need realizability toposes, as these are quite technically involved. We can use the much simpler assemblies. First we fix a model of computation $A$. Formally, $A$ should be a partial combinatory algebra, but informally you can just imagine Turing machines, or programs in a general-purpose programming language. An assembly $(S, \Vdash_S)$ is a set $S$ together with a realizability relation ${\Vdash_S} \subseteq A \times S$. We read $p \Vdash_S x$ as "program $p$ is a code of element $x \in S$". We require that $\Vdash_S$ have the property $\forall x \in S . \exists p \in A . p \Vdash_S x$, i.e., every element has to have at least one code. (But the same code may be shared between elements.) The notion of an assembly is very natural and it precisely captures the idea the the elements of an abstract set are encoded in some way by programs.

A morphism of assemblies $f : (S, \Vdash_S) \to (T, \Vdash_T)$ is map $f : S \to T$ which is realized, by which we mean that there is a program $q \in A$ such that $$p \Vdash_S x \implies q \cdot p \Vdash_T f(x).$$ This again is a completely natural idea which captures precisely the fact that the program $q$ operates on codes the way $f$ operates on the corresponding elements. It is what programmers do when you ask them to implement a mathematical function.

The category of assemblies is not a topos, but it is good enough to allow interpretation of lots of constructions and of intuitionistic first-order logic. The interpretation is completely standard (predicates are interpreted as subobjects, and everything else follows from that).

Here is the punch line: take an object of interest, say the real numbers. Characterize the real numbers in the language of first-order logic (or higher-order logic if needed, but then we have to use the topos), for instance "the Cauchy-complete archimedean ordered field". Up to isomorphism there is at most one assembly which satisfies this characterization. Therefore, there is no question about how real numbers should be represented! As soon as we say precisely what structure we expect of the reals, the encoding is imposed by the ambient category of assemblies (or the topos).

This trick works over and over again. You can start with the natural numbers, except that the first-order Peano axioms are the wrong thing to use. The correct thing to say is that $\mathbb{N}$ is the free algebra for the signature $(0, 1)$, i.e., the free structure with one constant and one unary operation. I think Dedekind said that first, didn't he? Since initial algebras are unique up to unique isomorphisms, the assembly of natural numbers is determined.

We can go on:

  • interegers are the free commutative unital ring
  • raitonals are the field of fractions of the integers
  • complex numbers are the algebraic closure of the reals

Eventually it gets a bit tricky, for instance $L^p[0,1]$ is doable for $p < \infty$, it is not really doable for $L^\infty[0,1]$ (because this space is intuitionistically problematic anyhow), and I don't know whether spaces of distributions have been handled properly. As a rule of thumb, anything that constructive mathematicians can do, you can interpret in realizaiblity to obtain a computable version.

So your hunch was correct: categorical logic (which is just model theory in categories instead of sets) and realizaibility provide the answer.

Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 240