Firstorder logic

Firstorder predicate calculus or firstorder logic (FOL) permits the formulation of quantified statements such as "there exists an x such that..." (<math>\exists x<math>) or "for any x, it is the case that..." (<math>\forall x<math>), where x is a member of the domain of discourse. A firstorder theory is a theory that can be axiomatised as an extension of firstorder logic by adding a recursive set of firstorder sentences as axioms.
Firstorder logic is Mathematical logic that is distinguished from higherorder 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..." (<math>\forall P<math>) or "there exists a property P such that..." (<math>\exists P<math>).
Nevertheless, firstorder 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 secondorder logic.
Contents 
Defining firstorder logic
A predicate calculus consists of
 formation rules (i.e. recursive definitions for forming wellformed 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 nonlogical axioms which are true under a special, i.e. the standard, interpretation of the theory of which they are part. For example, the nonlogical 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 wellformed 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
 Uppercase letters P, Q, R,... which are predicate variables.
 Lowercase letters a, b, c,... which are (individual) constants.
 Lowercase letters x, y, z,... which are (individual) variables.
 Lowercase letters f, g, h,... which are function variables.
 Symbols denoting logical operators: ¬ (logical not), <math>\wedge<math> (logical and), <math>\vee<math> (logical or), → (logical conditional), ↔ (logical biconditional).
 Symbols denoting quantifiers: <math>\forall<math> (universal quantification), <math>\exists<math> (existential quantification).
 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) <math>\wedge<math> (Q → P). The minimum number of operators and quantifiers needed is three; for example, ¬, <math>\wedge<math>, and <math>\forall<math> suffice. A term is a constant, variable, or function symbol of n≥0 arguments.
Formation rules
The set of wellformed formulas (wffs) is recursively defined by the following rules:
 Simple and complex predicates If P is an nadic (n ≥ 0) predicate, then <math>Pa_1,...,Pa_n<math> is wellformed. If n ≤ 1, P is atomic.
 Inductive Clause I: If φ is a wff, then ¬ φ is a wff.
 Inductive Clause II: If φ and ψ are wffs, then <math>(\phi \wedge \psi)<math>, <math>(\phi \vee \psi)<math>, (φ → ψ), (φ ↔ ψ) are wffs.
 Inductive Clause III: If φ is a wff containing a free instance of variable x, then <math> \forall x \, \varphi <math> and <math> \exists x \, \varphi <math> are wffs. (Then any instance of x is said to be bound — not free — in <math> \forall x \, \varphi <math> and <math> \exists x \, \varphi <math>.)
 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:
 PRED1: <math> \forall x Z(x) \rightarrow Z(y) <math>
 PRED2: <math> Z(y) \rightarrow \exists x Z(x) <math>
 PRED3: <math> \forall x (W \rightarrow Z(x)) \rightarrow (W \rightarrow \forall x Z(x)) <math>
 PRED4: <math> \forall x (Z(x) \rightarrow W) \rightarrow (\exists x Z(x) \rightarrow W) <math>
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
 <math>\mathit{if} \vdash Z(x), \mathit{then} \vdash \forall x Z(x)<math>
where Z(x) is supposed to stand for an alreadyproven 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
 <math>\mathit{if} \vdash P, \mathit{then} \vdash \Box P<math>.
Metalogical theorems of firstorder logic
Some important metalogical theorems are listed below in bulleted form.
 Unlike the propositional calculus, firstorder 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.)
 The decision problem for validity is semidecidable. As Gödel's completeness theorem shows, for any valid formula P, P is provable.
 Monadic predicate logic (i.e., predicate logic with only predicates of one argument) is decidable.
See also
References
 Article on classical logic (http://plato.stanford.edu/entries/logicclassical/) by Stewart Shapiro at the Stanford Encyclopedia of Philosophy, which covers the definition, model theory and soundness and completeness results for firstorder logic characterised in a natural deduction style.
 Introduction to mathematical logic (http://www.ltn.lv/~podnieks/) by Karl Podnieks.
 Metamath (http://us.metamath.org/index.html): a project to construct mathematics using an axiomatic system based on propositional calculus, predicate calculus, and set theory
de:Prädikatenlogik fr:Calcul des prédicats hu:Elsőrendű logika pl:Klasyczny rachunek logiczny sv:Predikatlogik ru:Логика первого порядка zh:一階邏輯