 This, of course, is the now conventional model-theoretic treatment of logical consequence originally due to Tarski (1937 [1941]) and extended to the logic of higher orders by Church’s student Leon Henkin (1950), which is presented in Church (1956a). (For more on Henkin’s contribution, see the entries on  second and higher order logic  and on  Church’s type theory.)  It should be noted that Church, in addition to working in classical model theory with restricted universes that can be accommodated in ZF set theory, was also willing to allow the existence of a universal set (1974c). Further, he not only distinguished between sharply between model theoretic interpretations and intended interpretations (1956a), but also argued that giving a particular model theoretic interpretation of a formal language was not sufficient for describing its logic. In particular, he argued that giving a formal language containing empty names (like ‘Pegasus’) an interpretation with inner and outer domains that invalidates Existential Generalization (as well as, presumably, Universal Instantiation) was not sufficient for describing the logic of that language (1965).