[FOM] A Category of Godel Codings. Comments?

[Rex Butler]

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 
mathematics.

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 
comments.

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 
proves

(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 
quickly
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 
principle.
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 
primitives?
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?

Rex Butler
RexButler at hotmail.com