Metalogical Frameworks

In computer science we speak of implementing a logic; this done in a programming language, such as Lisp, called here the implementation language. We also reason about the logic, as in understanding how to search for proofs or in knowing it is consistent; in the terminology of mathematical logic, these arguments are conducted in the metalanguage of the object language being implemented. We also reason about the implementation itself, say to know it is correct. This is done in a programming logic. How do all these logics relate? This paper considers that question and more. We show that by taking the view that the metalogic is primary, these other parts are related in standard ways. The metalogic must be suitably rich so that the object logic can be presented as an abstract data type, and it must be suitably computational (or constructive) so that an instance of that type is an implementation. The data type abstractly encodes all that is relevant for metareasoning, i.e. not only the term constructing functions but also the principles for reasoning about arbitrary terms and computing with them. Our work can also be seen as an approach to the task of finding a generic way to present logics and their implementations, which is for example the goal of the Edinburgh Logical Frameworks (ELF) effort. This approach extends well beyond proof-construction and includes computational metatheory as well