Contributions to the Model Theory of Higher-Order Logic

Abstract

In this thesis, we develop the model theory of higher-order logic by working in Alonzo, a classical higher-order logic based on Church's formulation of simple type theory that extends first-order logic and that admits undefined expressions. In particular, we sharpen the Löwenheim-Skolem theorem (Theorem 9.39 in William M. Farmer's Simple Type Theory) such that there exists a structural relationship between the starting and produced models, we develop model-theoretic types and prove a corresponding higher-order version of the omitting types theorem, and we give syntactic and semantic characterizations of how first-order theories are embedded in Alonzo.