Online Encyclopedia
Firstorder predicate calculus
Firstorder predicate calculus or firstorder logic (FOL) is a theory in symbolic logic that permits the formulation of quantified statements such as "there is at least one X such that..." or "for any X, it is the case that...", where X is an element of a set called 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 distinguished from higherorder logic in that it does not allow statements such as "for every property, it is the case that..." or "there exists a set of objects such that..."
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 arithmetic, set theory, or secondorder logic.
Contents 
Defining firstorder logic
Like any logical theory, the calculus of firstorder logic consists of
 a specification of how to construct syntactically correct statements (the wellformed formulas)
 a set of axioms, each axiom being a wellformed formula itself
 a set of inference rules which allow one to prove theorems from axioms or earlier proven theorems.
There are two types of axioms: the logical axioms which embody the general truths about proper reasoning involving quantified statements, and the axioms describing the subject matter at hand, for instance axioms describing sets in set theory or axioms describing numbers in arithmetic.
While the set of inference rules in firstorder calculus is finite, the set of axioms may very well be and often is infinite. However we require that there is a general 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.
Wellformed formulas of firstorder logic
The wellformed formulas contain:
 variables such as x, y, ... which are place holders for objects of the domain under consideration (these can be called "variable terms")
 object constants such as 0, 1 or the empty set ř which stand for fixed individual objects in our domain (these can be called "constant terms"; it is also possible to use lower case letters such as a, b, c, ... , w to represent such constants, as long as they are different from the letters used for the variable terms)
 predicate constants such as < (lessThan), (isIn), = (equals) which stand for fixed relations between or properties of our objects. These are also called firstorder predicates to distinguish them from predicates that talk about predicates.
 function constants such as + , * which stand for fixed functions taking objects as arguments and returning objects as values
 logical connectives such as (and), (or), (conditional), (biconditional) (not), (thereExists or existential quantifier) and (forAll or universal quantifier). All of these except for the last two are also used in propositional logic.
Note that only , , and are needed for a complete set of logical connectives.
The object, predicate and function constants will typically depend on the particular domain we are talking about.
Examples of wellformed formulas
Instead of giving the lengthy definition of wellformed formulas, we will simply look at some examples from arithmetic together with their ordinary interpretation. Our domain here is the set of natural numbers:
 (i.e.: forAll x, thereExists y suchThat y isGreaterThan x )
For every number x there exists a bigger number y. That's true.
 (i.e.: thereExists y suchThat forAll x, y isGreaterThan x )
There exists a number y which is bigger than every number x. That's not true.
 (i.e.: forAll x, ( thereExists y suchThat 6*y=x) implies (thereExists y suchThat 3*y=x) )
If a number x is divisible by 6, then it is also divisible by 3. True.
 (i.e.: thereExists x suchThat (not ThereExists y suchThat y < x ) )
There exists a number x such that there doesn't exist a smaller number y. True (take x=0).
Now one would have to write down 15 logical axioms and 2 inference rules to completely specify the firstorder calculus. How can one be sure that those axioms and rules are enough? This is the subject of Gödel's completeness theorem: if you start out with some subject matter axioms and you look at a certain statement, then it is possible to prove that statement using only the subject matter axioms, the 15 logical axioms and the two inference rules if and only if the statement is true in every domain in which the subject matter axioms are true. (See also Leon Henkin)
An important type of well formed formulas: clauses
A term is defined as follows:
 A variable is a term.
 An object constant is a term.
 If t_{1}, ..., t_{k} are terms and f is a function constant of arity k, then f(t_{1},...,t_{k}) is a term.
A atom (or atomic formula) is a wellformed formula of the form P(t_{1},...,t_{k}), where P is a predicate constant of arity k and t_{1},...,t_{k} are k terms.
A literal is either an atom or the negation of an atom.
A clause is a wellformed formula of the form
 ,
where L_{1},...,L_{m} are literals and x_{1},...,x_{k} are variables in them. Alternatively, a clause can be thought of as the set of literals
 {L_{1},...,L_{m}}.
A unit clause is simply a clause with only one literal.
Grammar
The "vocabulary" is composed of
 Predicate letters which are capital letters of the alphabet.
 Lowercase letters which are designated to be constant terms.
 Lowercase letters which are designated to be variable terms.
 Function letters (optional: not necessary for a purely logical pred.calc.)
 Symbols denoting logical operators: ¬, , , →, ↔.
 Symbols denoting quantifiers: ∀, ∃.
 Left and right parenthesis.
The set of wellformed formulae (wffs) is recursively defined by the following rules:

Basis: Atomic formulae, defined as in the previous section about "clauses".
If an atomic formula contains variable terms, then the formula is an open sentence, and each time the variable appears in the sentence, it is called a "free instance" of that variable.  Inductive Clause I: If φ is a wff, then ¬ φ is a wff.
 Inductive Clause II: If φ and ψ are wffs, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) are wffs.
 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 .)
 Closure Clause: Nothing else is a wff.
Grammar pays no attention to the truthvalue of a wff. A wff may be valid, invalid, provable, decided, undecided, necessary, or contingent; grammar is not concerned with semantics, but only with syntax. Likewise, terms have no truthvalue. If function letters are chosen to be included in the vocabulary, then a function applied to its arguments does not (implicitly) return a truthvalue, but it does have a constant term as its returnvalue (especially if all the function's arguments are themselves constant terms). If a function is replaced by its returnvalue during evaluation, then the truthvalue of the wellformed formula remains unchanged. All wellformed formulae have truthvalues.
Calculus
Predicate calculus is an extension of propositional calculus. If propositional calculus is defined with eleven axioms and one inference rule (modus ponens), not counting some auxiliary laws for the logical equivalence operator, then 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:
 PRED2:
 PRED3:
 PRED4:
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 Generalization is characteristic of predicate calculus. It can be stated as
where Z(x) is supposed to stand for an alreadyproven theorem of predicate calculus. 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
 .
Case study: firstorder Peano axioms
The Peano axioms for the natural numbers are sometimes formulated as secondorder statements (the induction axiom talks about all "properties" or all "sets of numbers"), but this is not necessary if one is willing to allow infinitely many firstorder axioms. A firstorder version of the Peano axioms follows.
We are using the object constants 0 and 1, the function constants + and *, and the predicate constant =. Here are the axioms:

 i.e.: forAll x, not (0 = x + 1)
 i.e.: no number has 0 as its successor

 i.e.: forAll x, forAll y, not(x=y) implies not(x + 1 = y + 1)
 i.e.: if x ≠ y, then x+1 ≠ y+1

 i.e.: forAll x, x + 0 = x

 i.e.: forAll x, forAll y, x + (y + 1) = (x + y) + 1
 i.e.: for all x and y, x + (y + 1) = (x + y) + 1

 i.e.: forAll x, x * 0 = 0

 i.e.: forAll x, forAll y, x * (y + 1) = x * y + x
 i.e.: for all x and y, x * (y + 1) = x * y + x
 This is an axiom scheme consisting of infinitely many axioms. If P(x) is any formula involving the constants 0, 1, +, *, = and a single free variable x, then the following formula is an axiom:
 i.e.: ( P(0) and (forAll x, ( P(x) implies P(x + 1) ) ) ) implies (forAll x, P(x) )
 i.e.: if something is true for 0, and from its being true for x it follows that it is also true for x + 1, then it is true for all x (induction)
Axioms 1, 2 and 7 are the traditional Peano axioms while axioms 36 serve to define addition and multiplication. If one omits the function constant * and axioms 5 and 6 and allows in scheme 7 only formulas without *, then one gets the very interesting Presburger arithmetic.
See also
References
 Introduction to mathematical logic http://www.ltn.lv/~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