The word “algorithm” suggests something effective, but here it is being used in a more general sense, as a set of instructions that, for reasons of our finitistic limitations, we may not be able to actually carry out. Consider again the paradigm formula, \eqref{whereformula}. If one of the \(\phi_i\) contains an existential quantifier in a positive position (or a universal quantifier in a negative position) it can be thought of as invoking a systematic search through the domain \(\bD\) for a verifying witness. This is plausible for reasonable domains. But if \(\phi_i\) should contain a universal quantifier in a positive position or an existential quantifier in a negative position, something must be verified for every member of the domain and unless the domain is finite, this is not a human task. Nonetheless, we generally believe we understand quantification. What we are dealing with is algorithms relative to that understanding.