# [FOM] A Foundational Path via Elementary PRA constructions

Andreas Blass ablass at umich.edu
Thu May 4 10:26:45 EDT 2006

```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
```