On systems of definitions,induction and recursion

Primitive recursion can be seen as the computational interpretation of induction through the Curry-Howard interpretation of propositions-as-types. In the present paper we discuss what happens if we apply this idea to possible non monotone inductive definitions. We start with a logical interpretation of a class of inductive definitions, thepartial inductive definitions. Then we internalise induction over such definitions as a rule of inference and consider a Curry-Howard interpretation of these definitions as type systems. As a basic example we discuss what meaning this interpretation gives to primitive recursion on a definition likeN=NN.