Primitive recursive selection functions for existential assertions over abstract algebras

We generalize to abstract many-sorted algebras the classical proof-theoretic result due to Parsons, Mints and Takeuti that an assertion ∀x∃yP(x,y) (where P is Σ10), provable in Peano arithmetic with Σ10 induction, has a primitive recursive selection function. This involves a corresponding generalization to such algebras of the notion of primitive recursiveness. The main difficulty encountered in carrying out this generalization turns out to be …