In this paper we define a logical framework, called
&;lambda;TT, that is well suited for semantic
analysis. We introduce the notion of a fibration
[Lscr ]1 : [Fscr ]1 [xrarr ] [Cscr ]
1 being internally definableThe
definability as used in
this paper should not be confused with Bénabou's
‘definability’ (Bénabou 1985). in a fibration
[Lscr ]2 : [Fscr ]2 [xrarr ] [Cscr ]
2. This notion amounts to distinguishing an internal category
L
in [Lscr ]2 and relating [Lscr ]1 to the externalization
of
L through a pullback. When both [Lscr ]1 and [Lscr ]2
are term models of typed calculi [Lscr ]1 and [Lscr ]2,
respectively, we say that [Lscr ]1 is an internal
typed calculus definable in the frame language [Lscr ]2.
We will show by examples that if an
object language is adequately represented in λTT,
then it is an internal typed calculus
definable in the frame language λTT. These examples
also show a general phenomenon: if
the term model of an object language has categorical structure S,
then an
adequate encoding
of the language in λTT imposes an explicit internal
categorical structure S in the term model
of λTT and the two structures are related via
internal
definability. Our categorical investigation of logical frameworks indicates
a
sensible model theory of encodings.