We generalise to abstract many-sorted algebras the classical proof-theoretic
result due to
Parsons and Mints that an assertion &forall x
&exist yP(x,y) (where P is
&Sigma^{0}_{1}),
provable in Peano
arithmetic with
&Sigma^{0}_{1} induction,
has a primitive recursive selection function. This involves
a corresponding generalisation to such algebras of the notion of
primitive recursiveness.
The main difficulty encountered in carrying out this generalisation turns out
to be the fact
that equality over these algebras may not be computable, and hence
atomic formulae in
their signatures may not be decidable. The solution is to
develop an appropriate concept
of realisability of existential assertions over
such algebras. This investigation may give
some insight into the relationship
between specifiability and computability for data types
such as the reals,
where the atomic formulae, i.e., equations between terms of type real,
are not computable.