Model theory for the higher order predicate calculus
Steven Orey · Transactions of the American Mathematical Society · 1959
The theory of models for elementary (often called order) axiom systems has grown considerably in the last years. This theory has been developed both for its own interest and as a tool for algebra. There is no corresponding development for model theory for higher order systems. One important reason for this is that much of the first order theory is based on the Godel completeness theorem or extensions of this theorem guaranteeing the existence of models for consistent sets of formulas. For consistent sets of higher order formulas there need be no models; the Henkin completeness theorem of [2 ] merely assures the existence of general models. There are, however, formulas c which we call (strongly) standard [with respect to the set of formulas H] such that if M1 is a general model [for H] and M2 is a (general) model [for H] and if M1 and M2 have the same ground class (and the higher order universes of M2 include those of M1) then either M1 is not a general model for q5 or M2 is a (general) model for q5. All elementary formulas are strongly standard; on the other hand for standard (a fortiori for strongly standard) formulas much of the elementary theory carries over. The main problem we consider is the syntactic characterization of (strongly) standard formulas('). We call two closed formulas (logically) equivalent [relative to H] if every (general) model [for H] is a general model for both or neither. From Theorem I we obtain a sufficient syntactic condition for a formula to be strongly standard. It follows from Theorems II and III that if H is any finite (or infinite) set of formulas q5 is (strongly) standard relative to H only if it is (logically) equivalent relative to H (and the union of a certain set of formulas I0,H) to a formula having the syntactic property referred to in the preceding sentence. Since logical equivalence can be defined syntactically, as was shown in [2], we have syntactic conditions which are sufficient for (relative) strong standardness. For a large class of H we obtain necessary and sufficient syntactic conditions for q5 to be strongly standard relative to H. For finite H we show that any formula standard relative to H must be equivalent relative to H