Primitive Recursive Selection Functions over Abstract Algebras

We generalise to abstract many-sorted algebras the classical proof-theoretic result due to Parsons and Mints that an assertion $${\forall} x {\exists} y {\it P}(x,y)$$ (where P is ∑$$^{\rm 0}_{\rm 1}$$), provable in Peano arithmetic with ∑$$^{\rm 0}_{\rm 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 given here is to develop an appropriate concept of realisability of existential assertions over such algebras, and to work in an intuitionistic proof system. This investigation gives some insight into the relationship between verifiable specifications and computability on topological data types such as the reals, where the atomic formulae, i.e., equations between terms of type real, are not computable.