 A set or property can be represented by a function (often called characteristic function) which maps elements to truth values, so that an element is in the set, or has the property, in question iff the function representing the set or property maps that element to truth. When a statement is asserted, the speaker means that it is true, so that \(s x\) means that \(s x\) is true, which also expresses the assertions that s maps x to truth and that \(x \in s\). In other words, \(x \in s\) iff \(s x\). We take \({o}\) as the type symbol denoting the type of truth values, so we may speak of any function of type \(({o}\alpha)\) as a set of elements of type α. A function of type \((({o}\alpha)\beta)\) is a binary relation between elements of type β and elements of type α. For example, if \(\sigma\) is the type of the natural numbers, and \(&lt;\) is the order relation between natural numbers, \(&lt;\) has type \(({o}\sigma \sigma)\), and for all natural numbers x and \(y, {&lt;}x y\) (which we ordinarily write as \(x &lt; y)\) has the value truth iff x is less than y. Of course, \(&lt;\) can also be regarded as the function which maps each natural number x to the set \(&lt;x\) of all natural numbers y such that x is less than y. Thus sets, properties, and relations may be regarded as particular kinds of functions. Church’s type type theory is thus a logic of functions, and, in this sense, it is in the tradition of the work of Frege’s Begriffsschrift. The opposite approach would be to reduce functions to relations, which was the approach taken by Whitehead and Russell (1927a) in the Principia Mathematica.