The set of terms of first-order logic (also known as first-order predicate calculus) is defined by the following rules:

1. A variable is a term.

2. If f is an n-place function symbol (with n>=0) and t_1, ..., t_n are terms, then f(t_1,...,t_n) is a term.

If P is an n-place predicate symbol (again with n>=0) and t_1, ..., t_n are terms, then P(t_1,...,t_n) is an atomic statement.

Da UnB Agência

Consider the sentential formulas  forall xB and  exists xB, where B is a sentential formula,  forall  is the universal quantifier ("for all"), and  exists  is the existential quantifier ("there exists"). B is called the scope of the respective quantifier, and any occurrence of variable x in the scope of a quantifier is bound by the closest  forall x or  exists x. The variable x is free in the formula B if at least one of its occurrences in B is not bound by any quantifier within B.

The set of sentential formulas of first-order predicate calculus is defined by the following rules:

1. Any atomic statement is a sentential formula.

2. If B and C are sentential formulas, then ¬B (NOT B), B ^ C (B AND C), B v C (B OR C), and B=>C (B implies C) are sentential formulas (cf. propositional calculus).

3. If B is a sentential formula in which x is a free variable, then  forall xB and  exists xB are sentential formulas.

In formulas of first-order predicate calculus, all variables are object variables serving as arguments of functions and predicates. (In second-order predicate calculus, variables may denote predicates, and quantifiers may apply to variables standing for predicates.) The set of axiom schemata of first-order predicate calculus is comprised of the axiom schemata of propositional calculus together with the two following axiom schemata:

 forall xF(x)=>F(r)
F(r)=> exists xF(x),

where F(x) is any sentential formula in which x occurs free, r is a term, F(r) is the result of substituting r for the free occurrences of x in sentential formula F, and all occurrences of all variables in r are free in F.

Rules of inference in first-order predicate calculus are the Modus Ponens and the two following rules:

(G=>F(x))/(G=> forall xF(x))
(F(x)=>G)/( exists xF(x)=>G),

where F(x) is any sentential formula in which x occurs as a free variable, x does not occur as a free variable in formula G, and the notation means that if the formula above the line is a theorem formally deducted from axioms by application of inference rules, then the sentential formula below the line is also a formal theorem.

Similarly to propositional calculus, rules for introduction and elimination of  forall  and  exists  can be derived in first-order predicate calculus. For example, the following rule holds provided that F(r) is the result of substituting variable r for the free occurrences of x in sentential formulaF and all occurrences of r resulting from this substitution are free in F,

 ( forall xF(x))/(F(r)).

Gödel's completeness theorem established equivalence between valid formulas of first-order predicate calculus and formal theorems of first-order predicate calculus. In contrast to propositional calculus, use of truth tables does not work for finding valid sentential formulas in first-order predicate calculus because its truth tables are infinite. However, Gödel's completeness theorem opens a way to determine validity, namely by proof.