  Formulas are built up from atomic formulas in the usual way, using propositional connectives, modal operators, and two kinds of quantifiers: over object variables and over intension variables. In addition to the usual formula-creating machinery, we have the following. If \(X\) is a formula, \(x\) is an object variable, and \(f\) is an intension variable, then \([\lambda x\,X](f)\) is a formula, in which the free variable occurrences are those of \(X\) except for \(x\), together with the displayed occurrence of \(f\).