 Church’s formalism—originally introduced in Church 1932, 1933 as a set of postulates for the foundation of formal logic—includes conversion (i.e., computational) rules, which allow the replacement of terms with intensionally equivalent ones, and rules for asserting certain terms as “true”. The syntax yields a general notation system for functions, based on an applicative language, where there is one basic category of terms (well-formed formulas in his terminology). Some terms are formally provable (or assertable) and are classified as true. Terms are inductively defined from a set of basic constants and variables by means of application and the characteristic lambda abstraction operator: if \(M\) is a term containing the variable \(x, \lambda x.M\) is a term, naming the function defined by \(M\). The basic constants designate logical operations: (a kind of restricted) formal implication; existential quantifier, conjunction, negation, description operation, and generalized abstraction (i.e., if \(F\) is formal logical equivalence, \(A(F, M)\) is “what \(M\) has in common with any \(N\) formally equivalent to \(M\)”). It turns out that Church’s logic can interpret naive class theory and hence the system is suspiciously strong and expressive (strength and expressivity are inherited by the formalism which was devised out of Church’s: see the entry on  the lambda calculus).  Church’s hope was that contradictions could be avoided by ensuring the possibility that a propositional function be undefined for some argument.