Type logic

From Glottopedia
Jump to: navigation, search


Type logic is a 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 constants 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.



  • Gamut, L.T.F. 1991. Logic, language, and meaning, Univ. of Chicago Press, Chicago.
  • Montague, R. 1974. Formal philosophy: selected papers of Richard Montague, edited and with an introduction by Richmond H. Thomason, Yale University Press, New Haven

CAT This article needs proper categorization. You can help Glottopedia by categorizing it
Please do not remove this block until the problem is fixed.