A recursive second order initial algebra specification of primitive recursion

Theoretical results on the scope and limits of first order algebraic specifications can be used to show that certain natural algebras have no recursively enumerable equational specification under first order initial algebra semantics. A well known example is the algebraP of primitive recursive functions over the natural numbers. In this paper we show thatP has a recursive equational specification under second order initial algebra semantics. It follows that higher order initial algebra specifications are strictly more powerful than first order initial algebra specifications.