A new type theory for representing logics

Authors

  • Philippa Gardner

Abstract

We propose a new type theory for representing logics, called LF+ and based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions which capture how well a logic has been represented. Using our definitions, we show that, for example, first-order logic can be wellrepresented in LF+, whereas linear and relevant logics cannot. These syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one, and provides a link between type-theoretic and categorical approaches to frameworks.

Venue

Logic Programming and Automated Reasoning, 4th International Conference, LPAR’93, St. Petersburg, Russia, July 13–20, 1993 Proceedings, pp. 146–157

Publication Date

Jul 1993

Identifiers

Source Materials