On systems of definitions, induction and recursion (Q688731)

When Martin-Löf's natural deduction, and in particular his analysis of iterated inductive definitions [see \textit{P. Martin-Löf}, ``Hauptsatz for the intuitionistic theory of iterated inductive definitions'', Proc. Second Scand. Logic Symp. 1970, Stud. Logic Found. Math. 63, 179-216 (1971; Zbl 0231.02040)], is translated via the Curry-Howard isomorphism [see \textit{B. Nordström}, \textit{K. Petersson} and \textit{J. M. Smith}, Programming in Martin-Löf's type theory (1990; Zbl 0744.03029)], the elimination or contraction rules become primitive recursion. Hallnäs provides a similar analysis to partial inductive definitions. He had earlier developed a notion of a partial inductive definition as an inductive definition, possibly non-monotone, in which some of the elements may be partial, or, to phrase it logically, in which some of the Boolean atoms may be neither provable nor refutable. Here he identifies an appropriate principle of induction on a partial inductive definition in the context of a sequent calculus, constructs from the sequent calculus a system of natural deduction with contraction or cut elimination rules, and interprets these rules as primitive recursive computation rules on terms.