On the proof-theoretic foundation of general definition theory

Lars Hallnäs

pp. 589-602

in: Proof-theoretic semantics, Synthese 148 (3), 2006.

Abstract

A general definition theory should serve as a foundation for the mathematical study of definitional structures. The central notion of such a theory is a precise explication of the intuitively given notion of a definitional structure. The purpose of this paper is to discuss the proof theory of partial inductive definitions as a foundation for this kind of a more general definition theory. Among the examples discussed is a suggestion for a more abstract definition of lambda-terms (derivations in natural deduction) that could provide a basis for a more systematic definitional approach to general proof theory.