  We also might want to require the existence of choice functions. Suppose that we have somehow associated an object \(d_{\Gamma }\) with each state \(\Gamma\) of a model. If our way of choosing \(d_{\Gamma }\) can be specified by a formula of the language, we might want to say we have specified an intension. Requiring the validity of the following formula seems as close as we can come to imposing such an existence condition on FOIL models. For each formula \(\Phi\):