LF is a logical framework based on the dependently typed lambda calculus with two universes,
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:
kindis a universe. That means:
kindis inhabitable (may occur as a type of constants) and every symbol
kindis also inhabitable.
typeis a universe as well.
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:
B(x)is inhabitable for any
x:A, then has 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:
Bdoes 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:
x:A, then has type .
λ 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:
fhas type and
f ahas type
B(a)is the result of substituting
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
ofor the expressions of our logic,
Jwith a type
TJas the type of proofs that the judgment
Jby constructing an element of the type
ofrom declared elements of
⊦J(for some judgment
The last point is worth looking at more closely: Usually, proof rules are denoted in the form of:
, which translates to:
φ_1is provable and … and judgment
φ_nis provable), then judgment
, 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
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