Although we will go on to give some consideration to derivations for the description operator, our system of derivations is now essentially complete. It is intended to capture entailments that derive from truth-functional logic and the logical properties of identity, predication, and the quantifiers. This range of logical forms is the concern of first-order logic. (Usage varies a little, and sometimes identity is not included; in that case, our subject is “first-order logic with identity.”) The qualification first-order derives from the fact that we analyze quantification only over individuals and not over properties and relations. Thus we cannot analyze the sentence Objects a and b are identical if and only if every property of one is a property of the other and we cannot ask whether this sentence is a tautology. The representation of such higher-order quantification symbolically would present few new problems. We would need bindable variables that functioned syntactically as predicates, notation for complex predicates of predicates (with our quantifiers serving as simple predicates of predicates), and quantifiers applying to such predicates of predicates. This would give us second-order logic. To go further, we might introduce quantification for predicates of predicates—and so on. If this process is continued to all (finite) orders, we end up with what is known as higher-order logic or (simple) type theory.
While higher-order logic introduces nothing really new in its syntax, the account of entailment for it is a completely different game, and the new problems appear already with second-order logic. In particular, there can be no sound system for settling questions of validity for second-order logic that is even complete, much less decisive. Indeed, a full understanding of validity for second-order logic would provide a full understanding of all truths concerning positive integers. But it was shown by Kurt Gödel in the early 1930s that these truths cannot be captured by anything like a system of derivations. (This is the result mentioned in 7.7.1 as the basis on which Church showed that there could be no system of derivations for first-order logic that was decisive as well as sound and complete.)
So there is a reason for distinguishing the theory of first-order quantification, from higher-order logic. Frege’s work did not make this distinction. The subject matter he addressed included the whole of what is now known as type theory because he was interested in connections with arithmetic, whose truths he wished to explain as logical tautologies. Although he provided what was essentially a complete account of validity for first-order logic, his treatment of other areas introduced inconsistencies. These were repaired shortly after (in the first decade of the 20th century) by Bertrand Russell, whose work led to the current conception of type theory. First-order logic came to be distinguished within type theory and was permanently set in its present form by Gödel when he showed that Frege’s initial ideas provided a complete account of validity for this part of logic.