First-order logic (FOL), also known as first-order predicate calculus (FOPC), is a system of deduction extending propositional logic (equivalently, sentential logic). It is in turn extended by second-order logic.
The atomic sentences of first-order logic have the form P(t1, ..., tn) (a predicate with one or more "arguments") rather than being propositional letters as in propositional logic. This is usually written without parentheses or commas, as below.
The new ingredient of first-order logic not found in propositional logic is quantification: where φ is any sentence, the new constructions ∀x φ and ∃x φ -- read "for all x, φ" and "for some x, φ" -- are introduced. For convenience in explaining our intentions, we write φ as φ(x) and let φ(a) represent the result of replacing all (free) occurrences of x in φ(x) with a, then ∀x φ(x) means that φ(a) is true for any value of a and ∃x φ(x) means that there is an a such that φ(a) is true. Values of the variables are taken from an understood universe of discourse; a refinement of first-order logic allows variables ranging over different kinds of objects.
First-order logic has sufficient expressive power for the formalization of virtually all of mathematics. A first-order theory consists of a set of axioms (usually finite or recursively enumerable) and the statements deducible from them. The usual set theory ZFC is an example of a first-order theory, and it is generally accepted that all of classical mathematics can be formalized in ZFC. There are other theories that are commonly formalized independently in first-order logic (though they do admit implementation in set theory) such as Peano arithmetic....