 LSD was originally formulated in a simply typed λ-calculus (of the kind described in  supplement D),  which allows the subject matter of the theory to be sorted into various type hierarchies. Individuals (like Hesperus) are of type \(\iota_0\). Senses (which Church calls “concepts”) that determine individuals—i.e., “individual concepts”—are of type \(\iota_1\) etc. In another hierarchy, truth values are of type \(o_0\), concepts of truth values—i.e., propositions—are of type \(o_1\), concepts of propositions—i.e., “propositional concepts”—are of type \(o_2\) etc. (Individuals are designated by constants, truth values are designated by sentences while propositions are designated by complex names corresponding to “that”-clauses.) In addition to typed hierarchies of concepts of individuals and concepts of truth values, there is also a hierarchy of functions and concepts of functions; for any types \(\alpha_k\) and \(\beta_k\), there exists a type \(\ulcorner\)(\(\alpha_k\) \(\beta_k )\urcorner\) of functions from entities of \(\beta_k\) to entities of type \(\alpha_k\).