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

*(English)*Zbl 1046.03015Summary: We continue our study, started in Part I [Ann. Pure Appl. Log. 114, 117–153 (2002; Zbl 0992.03037)], 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 \(\Sigma_1^0\) and \(\Pi_1^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.

Two special cases of this result are well known, namely induction over \(\Sigma_1^0\) and \(\Pi_1^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.

##### MSC:

03B70 | Logic in computer science |

68N18 | Functional programming and lambda calculus |

03D20 | Recursive functions and relations, subrecursive hierarchies |

PDF
BibTeX
XML
Cite

\textit{D. Leivant}, Theor. Comput. Sci. 318, No. 1--2, 181--196 (2004; Zbl 1046.03015)

Full Text:
DOI

##### References:

[1] | P. Clote, Partition relations in arithmetic, in: C.A. DiPrisco (Ed.), Methods in Mathematical Logic, Lecture Notes in Mathematics, Vol. 1130, 1985, pp. 32-68. · Zbl 0567.03029 |

[2] | David, R.; Nour, K., A short proof of the strong normalization of classical natural deduction with disjunction, J. symbolic logic, 68, 1277-1288, (2003) · Zbl 1066.03056 |

[3] | Gödel, K., On undecidable propositions of formal mathematical systems, (), (lecture notes taken by Kleene and Rosser at the Institute for Advanced Study, 1934) |

[4] | Hájek, P.; Pudlák, P., Metamathematics of first-order arithmetic, (1993), Springer Berlin · Zbl 0781.03047 |

[5] | Kleene, S.C., Introduction to metamathematics, (1952), Wolters-Noordhof Groningen · Zbl 0047.00703 |

[6] | Leivant, D., Termination proofs and complexity certification, (), 183-200 · Zbl 1087.68545 |

[7] | Leivant, D., Intrinsic reasoning about functional programs ifirst order theories, Ann. pure appl. logic, 114, 117-153, (2002) · Zbl 0992.03037 |

[8] | Seldin, J., On the proof theory of the intermediate logic MH, J. symbolic logic, 52, 626-647, (1986) · Zbl 0639.03022 |

[9] | Simpson, S., Subsystems of second-order arithmetic, (1999), Springer Berlin · Zbl 0909.03048 |

[10] | Stalmarck, G., Normalization theorems for full first order classical natural deduction, J. symbolic logic, 56, 129-149, (1991) · Zbl 0735.03028 |

[11] | Troelstra, A.S.; Schwichtenberg, H., Basic proof theory, (2000), Cambridge University Press Cambridge · Zbl 0957.03053 |

[12] | Wehmeier, K.F., Fragments of HA based on σ_1-induction, Arch. math. logic, 37, 37-49, (1997) · Zbl 0886.03040 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.