[FOM] A Foundational Path via Elementary PRA constructions

[Andreas Blass]

Let me make a short technical comment on the following part of Rex  
Butler's post.

> 2.  A. Define a primitive to be a pair (A,~) where A is a primitive
> recursive
>     predicate and ~ is a primitive recursive equivalence relation.
>
>     B. Define a function between two primitives (A,~) and (B,~) to  
> be a
>     primitive recursive function f: N --> N such that PRA proves
>
>         If x in A then f(x) in B and
>         If x,y in A and x ~ y  then  f(x) ~ f(y).

Since part B talks about PRA proving things about A, B, ~, and f,  
these four entities should presumably be primitive recursive  
definitions of two predicates, a relation, and a function, not simply  
the predicates, relation, and function themselves.  The point is that  
the same function f could have different constructions (using the  
basic functions, composition, and primitive recursion) that are not  
provably equivalent in PRA.  So the choice of the construction could  
affect what is provable.  A related point is that one should probably  
assume not only that ~ is an equivalence relation but that PRA proves  
that it's an equivalence relation.

Andreas Blass