Intrinsic reasoning about functional programs - II: unipolar induction and primitive-recursion

摘要

We continue from (Ann. Pure Appl. logic 114 (2002) 117) our study of reasoning about recursion equations in rudimentary theories for inductive data, dubbed intrinsic theories. We show that the functions that are provable using unipolar induction are precisely the primitive-recursive functions, where we call an instance of induction unipolar if data predicates do not occur in the induction formula both positively and negatively. Two special cases of this result are well known, namely induction over sum from 1 to 0 and ∏{sub}1{sup}0. Here, however, induction formulas may have unrestricted quantifier alternations as long as those quantifiers that are relativized to data do not violate the prescribed restriction. The main technical challenge is in showing that the functions provable by unipolar induction, even in classical logic, are primitive-recursive. The result is generic with respect to the underlying inductive data, suggesting a potentially useful formalization of primitive-recursive mathematics.