First-Order Logic

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.

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:

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:

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 formula F and all occurrences of r resulting from this substitution are free in F,

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.

See also

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

References

Referenced on Wolfram|Alpha

Cite this as:

Sakharov, Alex. "First-Order Logic." From MathWorld--A Wolfram Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/First-OrderLogic.html

Subject classifications