Models of higher-order languages
Andrew Bacon · 2023
Throughout this book, we have treated the language of higher-order logic, ℒ(Λ), as an interpreted language. Its sentences can be evaluated as true or false simpliciter , and we have used them to make claims, conjectures and so forth. Sometimes, however, it is useful to take the language of higher-order logic and assign it non-intended interpretations constructed from mathematical objects—i.e. models —for which we can introduce, within the language of set-theory, properties like being true in M for each model M . Sometimes when we are using a sentence of higher-order logic to make a conjecture or claim, we would like some guarantee that the sentence is consistent, in the sense that one cannot prove everything from the standard axioms. If a higher-order logic is sound with respect to a class of models then consistency can be secured by finding a model in which the sentence is true. If the logic is complete with respect to that class of models, then one can know that there will exist such a model if the sentence is indeed consistent. In Section 15.1 , a general class of models for this purpose are described, and in Sections 15.2 and 15.3 the soundness and completeness results are proved. Section 15.4 resolves a putative tension between the inconsistency of the quasi-syntactic structured view of reality ( Section 11.1 ) and the existence of very fine-grained models of higher-order languages. In the final two sections, we return to the study of the interpreted language of higher-order logic. Section 15.5 attends to the question of how to theorize about the intended interpretation of the language of higher-order logic. The question of soundness and completeness for uninterpreted languages is fairly uninteresting: according to the results in this chapter every higher-order logic is sound and complete with respect to some class of models. Nonetheless we might ask whether it is possible to provide a recursive axiomatization of the logical truths —a notion that applies only to an interpreted language and can be defined from truth simpliciter. In Section 15.6 , we employ Gödel’s incompleteness results to show that the logical truths of higher-order logic cannot be recursively axiomatized.