Most current research on automated theorem proving is concerned with proving theorems of first-order logic, the basic features of which (connectives and quantifiers) occur in most formal languages. However, in certain contexts, type theory (higher-order logic) has clear practical advantages over first-order logic. An example of this is provided by the theorem that if some iterate of a function f has a unique fixed point, then f has a fixed point. The TPS Theorem Proving System ~\cite{Andrews96b} can prove this theorem automatically in about two minutes when it is expressed in type theory. The search procedure tries various ways of instantiating quantifiers on higher-order variables with terms which introduce connectives and quantifiers in a very general way, then searches (with the aid of a higher-order unification algorithm) for a relation called a mating between the literals of the resulting expanded form of the theorem. When this search succeeds, the exact terms needed to instantiate the quantifiers are known. From this and other information acquired in the search process, a proof of the theorem in natural deduction style is constructed without further search. The formal proof thus obtained for this theorem in type theory is 35 lines long. However, as noted in ~\cite{Andrews96}, when the same theorem is expressed in first-order logic using a formulation of axiomatic set theory such as ~\cite{boyer86}, a formal proof requires approximately 8000 lines. The problem is that in axiomatic set theory the definitions of operations such as composition of functions are much more complex than in type theory, and one must go through a very long chain of deductive reasoning to prove the existence of sets and functions whose definitions can simply be written down in type theory. Any proof of this theorem in axiomatic set theory requires using the axioms of set theory many hundreds of times, so the problem of automatically deriving the theorem from these axioms is much more complex than the corresponding problem in type theory. From this and other examples it can be seen that one may pay a high price for forcing sets and functions, which are are essentially higher-order concepts, into a first-order context.
There are also theoretical arguments for the advantages of using higher orders of logic for certain problems. In his paper "On the Length of Proofs" (translated in ~\cite{Godel86}), Godel asserted that "passing to the logic of the next higher order has the effect, not only of making provable certain propositions that were not provable before, but also of making it possible to shorten, by an extraordinary amount, infinitely many of the proofs already available." A complete proof of this may be found in ~\cite{Buss94}. A related result by Statman ~\cite{Statman78}) establishes that the minimal length of a proof in first-order logic of a theorem of first-order logic may be extraordinarily longer than that the minimal length of a proof of the same theorem in second-order logic. It might be thought that examples of this phenomenon are so exotic as to be of little interest, but this is not the case. As shown in ~\cite{McCarthy64}, one can use first-order logic to express in a very concise and elegant way the fact that if one removes diagonally opposite squares from a checkerboard, it cannot be tiled by dominoes so that each domino covers exactly two adjacent squares. By making the checkerboard sufficiently large, one can make this theorem arbitrarily hard to prove in first-order logic by methods which involve exhaustive enumeration of the possibilities. However, as shown in ~\cite{Andrews96}, in higher-order logic there is a proof of this theorem which gets only moderately longer as the checkerboard is made larger.