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 …