**First-order logic**, also known as **quantification theory** and **predicate calculus** is a term that refers to predicate logics in which quantified predicates may range over a single domain of discourse that contains distinct objects. There are several first order logics, but the most commonly studied is *classical first-order logic*, which is supposed to be an "extension" of Propositional logic.

## Syntax

### Alphabet

- The Quantifiers: . Respectively, the Universal Quantifier and the Existential Quantifier.
- The logical connectives: Respectively, Conjunction, Disjunction, Material conditional, biconditional. Other logical connectives may also be added.
- A set of infinite variables: . They may be identified with letters such as .
- A set of parentheses and other punctuation marks.

- For every integer n, there is a set of n-ary Predicate symbols: . These may be letters such as
- For every integer , there is a set of n-ary function symbols.: . If the arity of these symbols is equal to 0, then it is said to be an individual constant. These may be letters such as

### Formation rules

**Terms**: The set of terms is defined as:

- Any expression of arguments (where is a term and is a function symbol) is a term.
- Individual constants are terms.
- Any variable is a term.

**Formulas**

**Predicates:**If is an n-ary predicate symbols, and are terms, then is a wff (*wff*is an abbrevation for a well-formed formula).**Quantifiers**: If is a wff and is a variable, then and are wffs.**Negation**: If is a wff then is a wff.**Binary connectives**: If and are wffs and is a binary connective, then is a wff.**Equality Symbol**: if equality is a part of first-order logic and and are wffs, then is a wff.

## Semantics

The non-logical symbols of a first-order logic are usually interpreted with a first-order model, which is an ordered pair , where is the domain of discourse, is the *signature*, and is the interpretation function which assigns meaning to the non-logical symbols. The signature is an ordered pair where is the set of predicate or relation symbols, is the set of function symbols, and is a mapping which assigns a natural number called an arity. The notation for an interpretation of a non-logical symbol is .

Each predicate symbol or relation symbol is assigned a n-ary relation or equivalently an n-ary function (where is the boolean domain or some other truth set).

Each function symbol f is assigned an n-ary function . If is a nullary function (that is an individual constant) its interpretation is . Individual constants may be assigned a value, such as .

A T-Schema could be defined inductively in the following way:

- A logical connective is given a truth value based on it's truth function or truth table, just as in Propostional logic.
- Let be the evaluations of the terms . Then is true if and only if . (Function symbols are evalauted in the following way: Given terms that have been evaulated to , the -ary function value evaulates to .
- is true if and only if and evaulate to the same
- is true if for all .
- is true if and only if there exists such that .

## Rules of inference

The rules of inference for first-order logic depends on what formal system is being used. It is common to add the rules of inference of propositional logic, universal instantiation, universal generalization, existential instantiation, and existential generalization. Formal systems may also include Change of quantifier.

## Axioms

If equality is part of a first-order logic system, then reflexivity, symmetry, transitivity, substitution for formulas, substitution for functions are added as axioms.