[FOM] A Category of Godel Codings. Comments?
rexbutler at hotmail.com
Fri Aug 26 21:26:39 EDT 2005
While not studying for prelims, I've spent much of my summer thinking
extensively about foundations of mathematics, in particular the foundations
of recursion theory. Now that I have passed, I think it would be good to
flesh out a few of my ideas with those more experienced in foundations of
I have been studying basic recursion/computability theory lately, and one
thing in particular has been troubling me. It is commonly pointed out, in
textbooks and elsewhere, that we don't lose much by focusing our study of
computability to only the set of natural numbers. After all, following the
example of Godel, we just equate the discrete set of our study with a
certain subset of the natural numbers via an intuitively effective map, and
then proceed from there. For most purposes, this is well enough, especially
as a theoretical simplification.
However, let me make an analogy. Assuming the axiom of choice, every vector
space V (over R, say) has a basis. In this way we may equate V with a
vector space with is the direct sum of R dim V times. However, regardless
of this fact, practically no one regards the study of vector spaces over R
as the study of such direct sums. Likewise, it seems somewhat disingenuous
to equate the study of computability on a particular class of discrete
structures with computability on N, because in like manner, we must make an
arbitrary choice to associate the discrete set in question with N.
For example, suppose I want to choose a coding method for, say, graphs with
rationally weighted edges. In computer science parlance, I need a 'file
format.' [Note a file is little more than a element of N padded by zeros.]
Once I know the existence of such a coding, constructing a particular
desired coding is as much an exercise in engineering and aesthetics as it is
mathematics. To be brief, the process of coding discrete objects requires
subjective choices and is highly non-canonical. This lack of universality
is somewhat disturbing.
I have spent many hours thinking about this and related issues, finally I
came up with the following construction. On further reflection, I am
extremely surprised I have not seen it yet. The construction itself is very
simple. My experience in foundations is limited, so I would appreciate any
The construction goes as follows:
[Note that using 'recursive' instead of 'primitive recursive' below results
in a rather boring theory]
Definition: A primitive recursive type, or a primitive, is a pair (A,~)
where A and ~ are unary and binary function symbols in Primitive Recursive
Arithmetic respectively, such that PRA proves A and ~ are characteristic
functions and ~ induces a equivalence relation. Notationally we use A and
~ as if they were sets/relations. Given primitives (A,~) and (B,~) and a
unary function f in PRA, we say that f induces a map from A to B if PRA
(x in A and y in A and x ~ y) => f(x) ~ f(y)
[Which equivalence ~ denotes will be clear from the context]
If f and g induce a map from A to B, and PRA proves
x in A => f(x) = g(x)
then we write f /simeq g.
For each primitive A there is an obvious identity map 1_A.
This gives us a category PRT whose objects are primitives (A,~) and whose
morphisms f: (A,~) -> (B,~) are the unary primitive recursive functions
which induce maps from A to B, modulo /simeq.
If we wish, we can now consider the purely categorical properties of PRT,
and thus avoid the issue of canonicalism completely. Note each object in
PRT has exactly countably many isomorphic object (Replace A with 2^A,and
modify ~ appropriately, etc...).
The isomorphism problem for this category is unsolvable, as follows:
Consider any Pi_1 statement B, which we can represent as ForAll x A(x) where
A(x)is primitive recursive. Let (A',=) be the corresponding primitive,
where A' is the unary function symbol representing A and =, to abuse
notation, is the characteristic function of equality. Define (A'',=) by
A''(x) = A'(x - 1) if x > 0 and 1 if x = 0. Now the identity function on N
is an isomorphism between A' and A'' in the category PRT if and only if
ForAll x A(x), i.e. if and only if B holds. Since B was arbitrary, this
shows the isomorphism problem in PRT is undecidable.
After a few definitions, there is wealth of primitives we can construct
First off, by considering regular equality, there is a primitive for
everything primitive recursive subset of N.
Given primitives A and B we can construct, using standard codings:
1. A x B: The Cartesian and categorical product of A and B,
2. A + B: The disjoint union/ categorical sum of A and B,
3. A^*: The primitive of finite A-sequences
4. P_f(A): The primitive of finite subsets of A
5. f^-1(1): The subset of A that maps to 1 under f: A -> 2
6. A x ~~: Given (A,~), and a primitive recursive equivalence ~~,
consider the equivalence x % y iff x ~ y and x ~~ y. This comes
with a standard map pi: (A,%) -> (A,~).
Construction 6 is especially important, as it is a sort of separation
Using these constructions we can describe primitives for just about every
conceivable combinatorial structure, labeled or unlabeled.
Immediately a whole slew of questions come to mind.
1. Can we axiomatize PRT via its categorical properties?
2. In general, in what other ways can we specify PRT?
2. Can we find a reasonable formal system for PRT, the 'universe' of
2. What if we replace the use of 'primitive recursive' above with Delta_0
in PA or with various complexity classes like NP and P? The Isomorphism
problem in these categories corresponds to what?
RexButler at hotmail.com
More information about the FOM