A plea for weaker frameworks
N.G. de Bruijn · Cambridge University Press eBooks · 1991
It is to be expected that logical frameworks will become more and more important in the near future, since they can set the stage for an integrated treatment of verification systems for large areas of the mathematical sciences (which may contain logic, mathematics, and mathematical constructions in general, such as computer software and even computer hardware). It seems that the moment has come to try to get to some kind of a unification of the various systems that have been proposed. Over the years there has been the tendency to strengthen the frameworks by rules that enrich the notion of definitional equality, thus causing impurities in the backbones of those frameworks: the typed lambda calculi. In this paper a plea is made for the opposite direction: to expel those impurities from the framework, and to replace them by material in the books, where the role of definitional equality is taken over by (possibly strong) book equality. Introduction Verification systems A verification system consists of (i) a framework, to be called the frame , which defines how mathematical material (in the wide sense) can be written in the form of books , such that the correctness of those books is decidable by means of an algorithm (the checker ), (ii) a set of basic rules ( axioms ) that the user of the frame can proclaim in his books as a general basis for further work.