# zbMATH — the first resource for mathematics

Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion. (English) Zbl 1046.03015
Summary: 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.
##### MSC:
 03B70 Logic in computer science 68N18 Functional programming and lambda calculus 03D20 Recursive functions and relations, subrecursive hierarchies
Full Text:
##### References:
  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  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  Gödel, K., On undecidable propositions of formal mathematical systems, (), (lecture notes taken by Kleene and Rosser at the Institute for Advanced Study, 1934)  Hájek, P.; Pudlák, P., Metamathematics of first-order arithmetic, (1993), Springer Berlin · Zbl 0781.03047  Kleene, S.C., Introduction to metamathematics, (1952), Wolters-Noordhof Groningen · Zbl 0047.00703  Leivant, D., Termination proofs and complexity certification, (), 183-200 · Zbl 1087.68545  Leivant, D., Intrinsic reasoning about functional programs ifirst order theories, Ann. pure appl. logic, 114, 117-153, (2002) · Zbl 0992.03037  Seldin, J., On the proof theory of the intermediate logic MH, J. symbolic logic, 52, 626-647, (1986) · Zbl 0639.03022  Simpson, S., Subsystems of second-order arithmetic, (1999), Springer Berlin · Zbl 0909.03048  Stalmarck, G., Normalization theorems for full first order classical natural deduction, J. symbolic logic, 56, 129-149, (1991) · Zbl 0735.03028  Troelstra, A.S.; Schwichtenberg, H., Basic proof theory, (2000), Cambridge University Press Cambridge · Zbl 0957.03053  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.