Editing Logical framework (section)

==LF==
In the case of the '''LF logical framework''', the meta-language is the [[λΠ-calculus]]. This is a system of first-order dependent function types which are related by the [[propositions as types principle]] to [[first-order logic|first-order]] [[minimal logic]]. The key features of the λΠ-calculus are that it consists of entities of three levels: objects, types and kinds (or type classes, or families of types). It is [[Impredicativity|predicative]], all well-typed terms are [[strongly normalizing]] and [[Church-Rosser]] and the property of being well-typed is [[Decidability (logic)|decidable]]. However, [[type inference]] is undecidable.

A logic is represented in the '''LF logical framework''' by the judgements-as-types representation mechanism. This is inspired by [[Per Martin-Löf]]'s development of [[Immanuel Kant|Kant]]'s notion of [[judgement (mathematical logic)|judgement]], in the 1983 Siena Lectures. The two higher-order judgements, the hypothetical <math>J\vdash K</math> and the general, <math>\Lambda x\in J. K(x)</math>, correspond to the ordinary and dependent function space, respectively. The methodology of judgements-as-types is that judgements are represented as the types of their proofs. A [[logical system]] <math>{\mathcal L}</math> is represented by its signature which assigns kinds and types to a finite set of constants that represents its syntax, its judgements and its rule schemes. An object-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements <math>\Lambda x\in C. J(x)\vdash K</math>.

An implementation of the LF logical framework is provided by the [[Twelf]] system at [[Carnegie Mellon University]]. Twelf includes
* a logic programming engine
* meta-theoretic reasoning about logic programs (termination, coverage, etc.)
* an inductive [[meta-logic]]al theorem prover