• People
• Events
• Research

Representing Logics in Type Theory

Abstract: Computer Science today contains many examples of logics given by proof systems. Although one intuitively knows how to use these systems and recognise correct derivations, there is no definitive account which captures this intuition. It is therefore natural to seek a framework for representing logics, which unifies the structure common to all logics. We introduce such a framework, called ELF+ and based on the Edinburgh Logical Framework (ELF). The major advantage of ELF+ is that it allows us to give, apparently for the first time, general definitions of correct representation; such definitions are not possible with ELF since information is lost during encoding. We rectify this deficiency using the extra distinctions between terms provided by the universes of a Pure Type System which yields a simple presentation of the type theory of ELF+. To do this, we extend these type systems to include signatures and Bn-equivalence.

Using the ideas underlying representation in ELF+, we give a standard presentation of the logics under consideration, based on Martin-Löf's notion of judgements and Aczel's work on Frege structures. The presentation forms a reference point from which to investigate representations in ELF+; it is not itself a framework since we do not specify a logic using a finite amount of information. Logics which do not fit this pattern are particularly interesting as they are more difficult, if not impossible, to encode.

The syntactic definitions of representation have elegant algebraic formulations which utilise the abstract view of logics as consequence relations. The properties of the ELF+ entailment relation determine the behaviour of the variables and consequence relations of the logics under consideration. Encodings must preserve this common structure. This motivates the presentation of the logics and their corresponding type theories as strict indexed categories (or split fibrations) so that encodings give rise to indexed functors. Our syntactic notions of correct representation now have simple formulations as indexed isormorphisms, which both confirms that our approach is a natural one and provides the beginnings of an algebraic framework for representing logics.

PhD Thesis - Price £8.00

LFCS report ECS-LFCS-92-227 (also published as CST-93-92)