 We have thus derived a well known law of quantification theory. We illustrate one possible interpretation of the wff \((7')\) (which is closely related to Axiom 6) by considering a situation in which a rancher puts some horses in a corral and leaves for the night. Later, he cannot remember whether he closed the gate to the corral. While reflecting on the situation, he comes to a conclusion which can be expressed by \((7')\) if we take the horses to be the elements of type \(\imath\), interpret \(p_{{o}}\) to mean “the gate was closed”, and interpret \(r_{{o}\imath}\) so that \(r_{{o}\imath}x_{\imath}\) asserts “\(x_{\imath}\) left the corral”. With this interpretation, \((7')\) says 