N-sorted logic for automatic theorem-proving in higher-order logic

This work demonstrates how a first-order logical system with more than one type of individual variable can be used to prove theorems in higher-order logic. Certain of the types are considered to be individuals while other types are treated as predicates and functions. For each pair of types i,j where type i objects are to be predicates over type j objects, a special 2-place predicate symbol P is included which acts as a graph, i.e. P(a,b) iff a(b). The lambda operator could be implemented as a set of comprehension axioms. However, since the axioms needed for a particular theorem are not generally known ahead of time and the inclusion of axioms in a theorem-proving program usually decreases efficiency, a new rule of inference, called naming, is proposed instead. Completeness of the resulting procedure is shown for a small class of higher-order problems. Some suggestions for computer implementation are given.