I'm trying to understand the notion of a logical framework and how/why/when it's used to define type theories. I'm looking at Luo's "Computation and Reasoning" (1994), where he considers LF, a typed version of Martin-Lof's logical framework.
LF is a simple type system with terms of the following forms:
$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$
where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.
(Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)
There are five forms of judgements in LF:
And then he gives rules for infering judgements in LF (one and two).
In general, a specification of a type theory will consist of a collection of declarations of new constants and a collection of computation rules (usually about the new constants).
For example, sigma types can be specified by declaring the following constants:
I have several questions about this set up, but the most basic (and general) one is this: suppose somebody wants to define a type theory with sigma types. What are the benefits of invoking LF to define it?
As far as I understand, there's a more "direct" way to define it — for example, as in Appendix A2 of the HoTT book, where sigma types are introduced by giving rules of formation, introduction, elimination, computation (as opposed to introducing several "constants").
Also, I don't really have intuition on why one needs to single out $El(A)$; I suppose it's related to universes (see this answer), but again I don't have a strong intuition about that.
Edit: I just looked at Lungu's PhD thesis "Subtyping in signatures" written under Luo, and there constants for product types are defined and inference rules for product types are given, which makes me even more confused — I guess I don't understand why we need to declare types like $(x:K)K'$ and $[x:K]k'$ beforehand if we eventually define expressions like $\Pi(A,B):Type$ when stating inference rules for product types.
Edit 2: Okay I think can kind of see how Luo's particular LF makes it easy to introduce Pi and Lambda in the object theory. Correct me if I'm wrong but I think the idea is that if we have these rules specified in LF and if we introduce Pi and Lambda by declaring these constants, then we don't need to postulate these rules for Pi and Lambda separately because they follow automatically from the rules for dependent products that are part of the definition of LF. And similarly for sigma types: if we want to introduce Sigma in the object theory and if we do this by declaring these constants, then the standard inference rules for sigma types will automatically follow from the rules for dependent types in LF. And if we want to introduce some new constant in the object theory, its type must have one of the following forms: $\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k)$, and then all desirable inference rules for the newly introduced constant will follow from the dependent type rules in LF.
Best Answer
The motivation for LFs (there are multiple LFs!) is that we want to specify theories without explicitly mentioning contexts, binders and substitution. The "direct" definition can be easily multiple times the size of the LF definition, and all of the extra size is just mechanically derivable boilerplate. I've recently written a small tutorial/comparison of LF-style and first-order specification for a not-too-complicated concrete type theory.
An LF needs at least a type of object-theoretic types and a family over it which represents object-theoretic terms. We need to keep the different levels in mind. The LF is itself a type theory and has type formers, but it's used as a specification language for other theories, and not as a general-purpose mathematical language. If I interpret your source right, $\mathsf{Type}$ is the type of object-theoretic types and $El$ is the type family of object-theoretic terms. A type and a type family together can be viewed as a Tarski-style universe which is closed under no type formers at all, hence the $El$ notation. I'd prefer to write $Tm$ instead of $El$ in this context.
It can be confusing when we switch between first-order specification (which mentions contexts) and second-order or higher-order (which doesn't). When introducing an LF, it is usually specified in a first-order way. The motivation here is usually that first-order specification is viewed as more basic, and we want to build our infrastructure on top of basic things. If we already have an LF, then it makes perfect sense to specify other theories inside that, including other LFs.