[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
More information about the FOM
mailing list