Predicate logic
Basic logic in effect concerns itself with whole statements (or "propositions") that are each either True or False. Predicate logic on the other hand takes into account how such statements are built up from other constructs—like those in mathematics. A simple statement in predicate logic is ∀x (∀y x y) ∨ ∀x (∃y (¬ x y)), where ∀ is "for all" and ∃ is "there exists" (defined in terms of ∀ on page 774)—and this particular statement can be proved True from the axioms. In general statements in predicate logic can contain arbitrary so-called predicates, say p[x] or r[x, y], that are each either True or False for given x and y. When predicate logic is used as part of other axiom systems, there are typically axioms which define properties of the predicates. (In real algebra, for example, the predicate > satisfies a > b ⇒ a ≠ b.) But in pure predicate logic the predicates are not assumed to have any particular properties.
Notions of quantifiers like ∀ and ∃ were already discussed in antiquity, particularly in the context of syllogisms. The first explicit formulation of predicate logic was given by Gottlob Frege in 1879, and by the 1920s predicate logic had become widely accepted as a basis for mathematical axiom systems. (Predicate logic has sometimes also been used as a model for general reasoning—and particularly in the 1980s was the basis for several initiatives in artificial intelligence. But for the most part it has turned out to be too rigid to capture directly typical everyday reasoning processes.)
Monadic pure predicate logic—in which predicates always take only a single argument—reduces in effect to basic logic and is not universal. But as soon as there is even one arbitrary predicate with two arguments the system becomes universal (see page 784). And indeed this is the case even if one considers only statements with quantifiers ∀ ∃ ∀. (The system is also universal with one two-argument function or two one-argument functions.)
In basic logic any statement that is true for all possible assignments of truth values to variables can always be proved from the axioms of basic logic. In 1930 Kurt Gödel showed a similar result for pure predicate logic: that any statement that is true for all possible explicit values of variables and all possible forms of predicates can always be proved from the axioms of predicate logic. (This is often called Gödel's Completeness Theorem, but is not related to completeness of the kind I discuss on page 782 and elsewhere in this section.)
In discussions of predicate logic there is often much said about scoping of variables. A typical issue is that in, say, ∀x (∃y (¬ x y)), x and y are dummy variables whose specific names are not supposed to be significant; yet the names become significant if, say, x is replaced by y. In Mathematica most such issues are handled automatically. The axioms for predicate logic given here follow the work of Alfred Tarski in 1962 and use properties of to minimize issues of variable scoping.
(See also higher-order logics on page 1167.)
