 Before we state the definition of a “formula”, a word of caution is in order. The reader may be accustomed to thinking of a formula as an expression which plays the role of an assertion in a formal language, and of a term as an expression which designates an object. Church’s terminology is somewhat different, and provides a uniform way of discussing expressions of many different types. What we call well-formed formula of type α (\(\textrm{wff}_{\alpha}\)) below would in more standard terminology be called term of type α, and then only certain terms, namely those with type \({o}\), would be called formulas. Anyhow, in this entry we have decided to stay with Church’s original terminology. Another remark concerns the use of some specific mathematical notation. In what follows, the entry distinguishes between the symbols \(\imath\), \(\iota_{(\alpha({o}\alpha))}\), and \(\atoi\). The first is the symbol used for the type of individuals; the second is the symbol used for a logical constant (see  Section 1.2.1  below); the third is the symbol used as a variable-binding operator that represents the definite description “the” (see  Section 1.3.4).  The reader should not confuse them and check to see that the browser is displaying these symbols correctly.