A New Type Theory for Representing Logics


  • Philippa Gardner


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.


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


Source Materials