Nuprl as a General Logic

Abstract

Study of the architecture and design of proof development systems has become important lately as their use has spread and become closely tied to programming environments. One of the central issues is how to provide a general framework for defining and using a variety of logics in such systems; in particular, whether it is better to staart with a simple core system, such as the typed lambda-calculus with dependent function types, or start with a very rich theory providing a formalized metatheory. The first approach is exemplified by the Edinburgh LF. Here we illustrated the second approach by showing how to use Nuprl as a framework for defining logics in the style of the LF. Central to the viability of the second apprroach is a method of showing that the encoding of user defined logics in Nuprl is faithful. This paper presents a new semantic method to solve the problem. The method is applicable to the LF as well, and seems simpler than the syntactic methods that previously were used and which seem to hinder the use of rich thoeries as logical frameworks.