**, also known as**

First-order logic (FOL)

First-order logic (FOL)

**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*(*t*_{1}, ..., *t*_{n}) (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....

[More....]

## No comments:

Post a Comment