Found:

Type logic

**SEMANTICS: **logical system based on Russell's theory of types. Every
expression of a type-logical language belongs to a particular type indicating the set-theoretical denotation of that expression. There are two basic types, the type e (from entity) and the type t (from **truth value**). The formulas of
**predicate logic** and **propositional logic** are expressions
of type t in type logic, denoting truth values; the
**individual constant**s of predicate logic are expressions of type e in type logic, denoting individuals. All other
expressions in type-logic are functional, i.e. they take an expression of type a as their argument and yield an expression of type b, which is indicated in their type as follows: <a,b>. The one-place predicates of predicate logic are of type <e,t> in type logic, denoting a function from entities to truth-values, which is another way to define a set. Two-place predicates are of type <e,<e,t>>. Type logic also allows functions of higher order. Noun modifiers can be treated as expressions of type <<e,t>,<e,t>>, mapping a set into a set. NPs are of type <<e,t>,t>, i.e. functions from sets to truth values, or equivalently, sets of sets. Determiners are relations between sets: <<e,t>,<<e,t>,t>>. In combination with lambda-abstraction, type logic is a very powerful logic for semantic representation. It has been fruitfully applied in **Montague Grammar**.

LIT. | Gamut, L.T.F. (1991) Montague, R. (1974) |