8.5.4. First-order logic

Although we will go on in 8.6 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.) Beginning about a century ago, first-order logic came to replace the theory of syllogisms as the commonly accepted core of deductive logic. In the current practice of mathematics, for example, even very abstract general principles falling beyond its scope would be treated as special axioms (of the theory of sets for example) while principles of first-order logic would be accepted as background assumptions within the context of which the consequences of special axioms are assessed.

The theory of syllogisms itself appears as an account of a very special collections of arguments. The outlines of this collection were sketched in 7.5.6, but having the existential quantifier makes it possible to provide more detail in a compact way. The four moods, the logical forms recognized by the theory, are as follows (with the vowels that serve as their traditional labels):

and the four figures are the following patterns of occurence of the three predicates that can appear in a syllogism (where the predicate shown on the left is the resticting predicate of the sentence and the one on the right is its quantified predicate):

Here μ is the middle term.

Of the 64 syllogisms of the first figure, the following four are valid:

Notice that the pattern of vowels in the traditional name shown below each argument matches the moods of its premises and conclusion. The proportion of valid arguments in the other figures is similar, and there are fifteen valid syllogisms all told.

One of the limitations of theory of syllogisms is an inability to consider logical relations between the restricitng and quantified predicates of a generalization or claim of exemplification. For example, using the resources of first-order logic, we can account for the fact that Every horse is a mammal implies Any head of a horse is a head of a mammal (an entailment mentioned in 7.1.1).

(The use of adjunction and existential generalization at stages 7 and 8 saves us having to enter ∀z ¬ (Mz ∧ Daz) as a supposition to be reduced to absurdity.) Even though this argument is closely related to syllogisms—the active resources and goal after the use of CP at stage 2 form a valid syllogism of the third figure known as Disamis—its validity cannot be explained without an analysis of the restricting and quantified predicates of the conclusion, something the theory of syllogisms does not provide for.

Although first-order logic forms the core of deductive logic, it is not the whole of it. One way to go beyond it is to study the sort of non-truth-functional connectives noted in 3.1.2. Another is to consider further sorts of quantifiers. 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 reason to distinguish 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 20^th 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.