 In order to adopt a formal language, one first devises what Church calls “a particular theory or system” (1956a [BE: 373]), which is a syntactic theory. This specifies the primitive symbols and formation rules for building the well-formed expressions (the wffs) of the theory, as well as what are the axioms and inference rules. The theorems are the wffs that occur at the end of proofs, which are themselves specified as finite sequences of wffs that are either axioms or inferable from prior wffs in the sequence according to the inference rules. In order for this theory to serve as a language, it must be provided with semantic rules that assign designata (or denotations) to the names of the theory, as well as values to expressions containing free occurrences of variables.