First-order predicate calculus

First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as "there exists an x such that..." () or "for any x, it is the case that..." (), where x is a member of the domain of discourse. A first-order theory is a theory that can be axiomatised as an extension of first-order logic by adding a recursive set of first-order sentences as axioms.

First-order logic is distinguished from higher-order logic in that it does not allow quantification over properties; i.e. it cannot express statements such as "for every property P, it is the case that..." () or "there exists a property P such that..." ().

Nevertheless, first-order logic is strong enough to formalize all of set theory and thereby virtually all of mathematics. Its restriction to quantification over individuals makes it difficult to use for the purposes of topology, but it is the classical logical theory underlying mathematics. It is a stronger theory than sentential logic, but a weaker theory than second-order logic.

Defining first-order logic

A predicate calculus consists of

• formation rules (i.e. recursive definitions for forming well-formed formulas).
• transformation rules (i.e. inference rules for deriving theorems).
• a (possibly countably infinite) set of axioms or axiom schemata.

There are two types of axioms: logical axioms which are valid with respect to the predicate calculus and non-logical axioms which are true under a special, i.e. the standard, interpretation of the theory of which they are part. For example, the non-logical Peano axioms are true under the standard interpretation of the symbolism of arithmetic, but they are not valid with respect to the predicate calculus.

When the set of axioms is infinite, it is required that there is an algorithm which can decide for a given well-formed formula whether it is an axiom or not. Furthermore, there should be an algorithm which can decide whether a given application of an inference rule is correct or not.

Vocabulary

The "vocabulary" is composed of

1. Uppercase letters P, Q, R,... which are predicate variables.
2. Lowercase letters a, b, c,... which are (individual) constants.
3. Lowercase letters x, y, z,... which are (individual) variables.
4. Lowercase letters f, g, h,... which are function variables.
5. Symbols denoting logical operators: ¬ (logical not), (logical and), (logical or), → (logical conditional), ↔ (logical biconditional).
6. Symbols denoting quantifiers: (universal quantification), (existential quantification).
7. Left and right parenthesis.

Some symbols may be omitted as primitive and taken as abbreviations instead; e.g. (P ↔ Q) is an abbreviation for (P → Q) (Q → P). The minimum number of operators and quantifiers needed is three; for example, ¬, , and suffice. A term is a constant, variable, or function symbol of n≥0 arguments.

Formation rules

The set of well-formed formulas (wffs) is recursively defined by the following rules:

1. Simple and complex predicates If P is an n-adic (n ≥ 0) predicate, then Pa₁,...,Pa_n is well-formed. If n ≤ 1, P is atomic.
2. Inductive Clause I: If φ is a wff, then ¬ φ is a wff.
3. Inductive Clause II: If φ and ψ are wffs, then , , (φ → ψ), (φ ↔ ψ) are wffs.
4. Inductive Clause III: If φ is a wff containing a free instance of variable x, then and are wffs. (Then any instance of x is said to be bound — not free — in and .)
5. Closure Clause: Nothing else is a wff.

Transformation (Inference) rules

Modus ponens suffices as the sole rule of inference. If there are axiom schemata, then a rule of substitution is also required.

Calculus

The predicate calculus is an extension of the propositional calculus. If the propositional calculus is defined with eleven axioms and one inference rule (modus ponens), not counting some auxiliary laws for the logical equivalence operator, then the predicate calculus can be defined by appending four additional axioms and one additional inference rule.

Axiomatic Extension

The following four logical axioms characterize a predicate calculus:

• PRED-1:
• PRED-2:
• PRED-3:
• PRED-4:

These are actually axiom schemata, because the predicate letters W and Z in them can be replaced by any other predicate letters, without altering the validity of these formulae.

Inference rule

The inference rule called Universal Generalization is characteristic of the predicate calculus. It can be stated as

where Z(x) is supposed to stand for an already-proven theorem of predicate calculus and ∀xZ(x) is its closure with respect to the variable x. The predicate letter Z can be replaced by any other predicate letter.

Notice that Generalization is analogous to the Necessitation Rule of modal logic, which is

.

Metalogical theorems of first-order logic

Some important metalogical theorems are listed below in bulleted form.

1. Unlike the Propositional calculus, first-order logic is undecidable. There is provably no decision procedure for determining for an arbitrary formula P, whether or not P is valid (see Halting problem). (Results came independently from Church and Turing.)
2. The decision problem for validity is semidecidable. As Gödel's completeness theorem shows, for any valid formula P, P is provable.
3. Monadic predicate logic (i.e., predicate logic with only predicates of one argument) is decidable.

See also

• Gödel's incompleteness theorem

References

• Introduction to mathematical logic
• Metamath: a project to construct mathematics using an axiomatic system based on propositional calculus, predicate calculus, and set theory