Definition and Syntax
Here, HOL denotes classical simple type theory based on the simply typed lambda calculus. The base types \iota (individuals) and o (truth values) generate function types \sigma\to\tau.
Terms are built from typed variables, constants, application, and lambda abstraction. Formulas are terms of type o. Quantifiers may bind variables of arbitrary types, including predicates and functions.
Semantics and Example
In standard models, D_{\sigma\to\tau}=D_\tau^{D_\sigma}. Henkin models may have smaller function domains; in particular, those domains must suffice to interpret all lambda terms [1].
\forall P_{\iota\to o}\,\forall x_\iota\,(P(x)\lor\neg P(x))
This formula quantifies over predicates and is classically valid.
Properties and Decidability
Relative to suitable Henkin models, simple type theory admits a sound and complete effective proof calculus [1]. Validity is therefore semidecidable, but undecidable. Under full standard semantics, there is no sound and complete effective calculus.
First-order logic can be embedded in HOL. Additional axioms, such as choice or infinity, must be specified separately; they are not silently included in the definition used here.
References
- Leon Henkin (1950). Completeness in the Theory of Types. Journal of Symbolic Logic 15(2), 81–91. DOI.