## Representing Logics in Type Theory

**Philippa Gardner**
*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)*

Previous |

Index |

Next