  Church uses a notion he calls a concept, where anything that is the sense of a name for something can serve as a concept of that something. There is no attempt to make this more precise—indeed it is not really clear how that might be done. It is explicit that concepts are language independent, and might even be uncountable. There is a type \(\omicron_{0}\) of the two truth values. Then, there is a type \(\omicron_{1}\) of concepts of members of \(\omicron_{0}\), which are called propositional concepts. There is a type \(\omicron_{2}\) of concepts of members of \(\omicron_{1}\), and so on. There a type \(\iota_{0}\) of individuals, a type \(\iota_{1}\) of concepts of members of \(\iota_{0}\), a type \(\iota_{2}\) of concepts of members of \(\iota_{1}\), and so on. And finally, for any two types \(\alpha\) and \(\beta\) there is a type \((\alpha\,\beta )\) of functions from items of type \(\beta\) to items of type \(\alpha\). Church makes a simplifying assumption concerning functional types. In order to state it easily he introduces some special notation: if \(\alpha\) is a type symbol, for example \(((\iota_{3}\,\omicron_{2})(\omicron_{5}\,\iota_{4}))\), then \(\alpha_{1}\) is the result of increasing each subscript by 1, in our example we get \(((\iota_{4}\,\omicron_{3})(\omicron_{6}\,\iota_{5}))\). (There is a similar definition for \(\alpha_{n}\) for each positive integer \(n\), but we will not need it here.) Church’s assumption is that the concepts of members of the functional type \((\alpha\,\beta )\) are the members of the type \((\alpha_{1}\,\beta_{1})\). With this assumption, uniformly the concepts of members of any type \(\alpha\) are the members of type \(\alpha_{1}\).