Predicate logic, also known as first-order logic and first-order predicate calculus, is a formalization of the language of mathematics, proposed by Gottlob Frege, between the end of the nineteenth century and the beginning of the twentieth century. In predicate logic, we can reason on statements like “All x is friendly” and “There exists an x such that for all y, x is friend with y” in symbols:
∀x friendly(x) and ∃x∀y friends(x,y).
The characteristic features of the predicate logic are:
- the use of variables like x, y, etc. to denote elements of a set;
- the use of predicates (or relations) on the elements;
- the use of logical connectors (and, or, etc.);
- the use of two quantifiers, one “universal” (“Whatever”, “for all” noted ∀) and the other “existential” (“there is at least one … such as,” noted ∃).
The egalitarian first-order predicate calculus, adds to the calculus of the predicates a symbol of relation, equality, the interpretation of which is obligatory: it is the identity of the elements of the model, and which is axiomatized accordingly. Depending on the context, we can simply speak of predicate logic for the first-order predicate calculus (or first-order logic).
We speak of first-order logic as opposed to higher-order logic, where we can also quantify predicates or functions in addition to variables. Here we deal only with classical first-order logic, but it should be noted that there is also a logic of the first intuitionist order.
Immanuel Kant wrongly believed that the logic of his time, that of Aristotle, was a complete and definitively completed science (preface to the second edition of the Critique of pure reason, 1787). Logicians of the nineteenth century realized that Aristotle’s theory says little or nothing about the logic of relationships. Gottlob Frege and many others have filled this gap by defining the first-order predicate calculus.
Kurt Gödel demonstrated in 1929 (in his doctoral thesis) that the calculation of predicates is complete, in the sense that we can give a finite number of principles (logical axioms, logical axiom schemes and deduction rules) sufficient to deduce mechanically all the logical laws (Gödel’s Completeness Theorem). There is equivalence between the semantic presentation and the syntactic presentation of the predicate calculus. Any universally valid statement (that is, true in any model of the language used) is a theorem (that is, it can be deduced from a computation, a system of logical rules and axioms, equivalently a Hilbert system, natural deduction, or the calculation of sequents), and vice versa. The logic of the first order is thus completed in the sense that the problem of the logical correction of the demonstrations is solved. It continues however to be the subject of important researches: theory of the models, theory of the demonstration, mechanization of the reasoning …
It is used from the alphabet:
- a set of symbols called variables, always infinite: x, y, z, etc. ;
- a set of symbols called constants, possibly empty: a, b, c, etc. ;
- a set of function symbols: f, g, h, etc. ;
- a set of predicate symbols: P, Q, R, etc.
Each function symbol and predicate symbol has an arity: it is the number of arguments or objects to which it is applied. For example, the predicate B for “is blue” has an arity equal to 1 (it is said to be unary or monadic), while the predicate friends to “be friends” has an arity of two (we say that it is binary or dyadic).
- The symbols ∀ (whatever) and ∃ (it exists), called quantifiers.
- The symbols ¬ (non), ∧ (and), ∨ (or) and → (implies), which are connectors that also have the propositional calculus.
- The punctuation symbols “)” and “(“.
One could be satisfied with a single quantizer ∀ and two logical connectors, ¬ and ∧, by defining the other connectors and quantizer from them. For example, ∃xP(x) is defined as ¬(∀x ¬P(x)).
The formulas of the calculation of the first order predicates are defined by induction:
- P(t1, … , tn) if P is a symbol of a predicate of arity n and t1, …, tn are terms (such a formula is called an atom or an atomic formula);
- ¬e if e is a formula;
- (e1 ∧ e2) if e1 and e2 are formulas;
- (e1 ∨ e2) if e1 and e2 are formulas;
- (e1 → e2) if e1 and e2 are formulas;
- ∀x e if e is a formula;
- ∃x e if e is a formula.
We call stated a formula whose variables are linked by a quantizer (which does not have a free variable).