TOPICS
Search

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:

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

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))
(3)
(F(x)=>G)/( exists xF(x)=>G),
(4)

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,

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

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

Deduction Theorem, Interpretation, Peano Arithmetic, Predicate Calculus, Propositional Calculus

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

Explore with Wolfram|Alpha

References

Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.Kleene, S. C. Mathematical Logic. New York: Dover, 2002.Mendelson, E. Introduction to Mathematical Logic, 4th ed. London: Chapman & Hall, p. 12, 1997.

Referenced on Wolfram|Alpha

First-Order Logic

Cite this as:

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

Subject classifications