• People
• Events
• Research

Equivalences between Logics and their Representing Type Theories

Abstract: We propose a new framework 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. A key property that permits such definitions is that logics with different consequence relations are represented by different specifications in LF+ . This property apparently does not hold for other frameworks. Using our definitions, we show that, for example, natural deduction first-order logic can be well-represented in LF+ , whereas linear and relevant logics cannot. We also show that our 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.

LFCS report ECS-LFCS-92-251, December 1992.