LF is a logical framework based on the dependently typed lambda calculus with two universes, `type`

and `kind`

. If you know what this means, you can safely skip this section.

A thorough description of both LF’s abstract formalization as well as how to use it in practice can be found in Part V here.

As seen in the previous section, LF declares a symbol `type`

, which is a *universe*. LF has a second universe `kind`

. Their behaviour is governed by the following rules:

`kind`

is a*universe*. That means:`kind`

is*inhabitable*(may occur as a type of constants) and every symbol`c`

with type`kind`

is also inhabitable.`type`

is a universe as well.`type:kind`

, i.e.`type`

has type`kind`

.

We can mostly ignore `kind`

, since it rarely comes into play. For most purposes, we are only interested in types.

LF has a single *type constructor*, that allows us to construct new types from existing ones, namely the *dependent product type* . Its behaviour is governed by the following *formation rule*:

If

`A:type`

and`B(x)`

is inhabitable for any`x:A`

, then has type`type`

is the type of functions, that take an element `a:A`

and return an element `b:B(a)`

. Note, that the *return type* of the function may depend on the *argument*. If `B`

does **not** depend on the argument, we get the *simple* function type we already used:

If

`B`

does not depend on`x`

, then .

Next, we need a way to construct elements of these function types. This is done using the `λ`

-operator, which is governed by the following *introduction rule*:

If

`A:type`

and`t(x):B(x)`

for any`x:A`

, then has type .

So `λ`

allows us to construct functions out of terms. Of course, functions are useless if we can’t apply them. The behaviour of function applications is governed by this *elimination rule*:

If

`f`

has type and`a:A`

, then`f a`

has type`B(a)`

(where`B(a)`

is the result of substituting`x`

by`a`

in`B(x)`

)

Additional *computation rules* make sure, that e.g. `λ x. (f x)`

is the same as `λ y. (f y)`

, which is the same as `f`

, etc., but those rules are intuitive enough to not require much explanation.

LF is a *logical framework*, i.e., it is intended to allow for conveniently specifying the syntax and proof theories of various logics. This might be surprising, given that LF only provides dependent function types. This is where the *judgments-as-types*-paradigm comes into play. It is based on the observation, that there is a natural correspondence between the *judgments* of a logic (e.g. “`φ`

holds”, or in symbols : `⊦ φ`

) and some associated type `A`

being *inhabited* (i.e. there is some `a`

with `a:A`

):

- We introduce a type
`o`

for the expressions of our logic, - we associate every judgment
`J`

with a type`⊦J`

, - we interpret the type
`TJ`

as the type of*proofs*that the judgment`J`

holds, - correspondingly we can “prove” the judgment
`J`

by constructing an element of the type`⊦J`

. - The
*syntax*of our logic thus reduces to functions, that construct new propositions from atomic propositions - i.e. new elements of the type`o`

from declared elements of`o`

, - The
*proof theory*of our logic corresponds to constructing elements of the judgment types`⊦J`

(for some judgment`J`

).

The last point is worth looking at more closely: Usually, proof rules are denoted in the form of:

, which translates to:

If(judgment`φ_1`

is provableand…andjudgment`φ_n`

is provable),thenjudgment`φ`

is provable.

, where a *context* is a list of assumptions. Since the judgments correspond to types, such a rule translates to a *function* taking proofs of the *premises* as arguments and returning a proof of the *conclusion*, i.e.

In the case of propositional logic, we have a single judgment for every proposition `φ:prop`

, namely the judgment `⊦ φ`

that `φ`

holds. Correspondingly, we declared the function `proof`

, that maps a proposition `φ`

to the associated type of proofs `⊦ φ`

. The syntax we have already taken care of, by declaring the connectives as functions on the type `prop`

.

In the next section we will use dependend function types to implement the rules of the *natural deduction* calculus as functions, that yield elements of the proof types `⊦ φ`

.

> 4 - Natural Deduction for Intuitionistic Propositional Logic