On systems of definitions, induction and recursion
type: Item
instance of: scholarly article
title: On systems of definitions, induction and recursion
zbMATH Open document ID: 0786.03028
DOI: 10.1007/BF01995107
author: Lars Hallnäs
published in: BIT
publication date: 1994-05-05T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03D70
zbMATH DE Number: 438467
zbMATH Keywords: sequent calculus
zbMATH Keywords: primitive recursion
zbMATH Keywords: natural deduction
zbMATH Keywords: Curry-Howard isomorphism
reviewed by: Robert S. Lubarsky
MaRDI profile type: Publication
cites work: Q3999860
cites work: Q5638283
full work available at URL: https://doi.org/10.1007/bf01995107
OpenAlex ID: W2041590892
description: scientific article; zbMATH DE number 438467