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.



Logical symbols:

Non-logical symbols

  • For every integer n, there is a set of n-ary Predicate symbols: P_1,P_2,P_3,\ldots . These may be letters such as A,B,C,D,\ldots,Y,Z
  • For every integer n , there is a set of n-ary function symbols.: f_1,f_2,f_3,\ldots . 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 a,b,c,d,\ldots,t,u,v,w

Formation rules

Terms: The set of terms is defined as:

  • Any expression f(t_1,\ldots,t_n) of n arguments (where t_n is a term and f is a function symbol) is a term.
  • Individual constants are terms.
  • Any variable is a term.


  • Predicates: If P is an n-ary predicate symbols, and t_1,\ldots,t_n are terms, then P(t_1,\ldots,t_n) is a wff (wff is an abbrevation for a well-formed formula).
  • Quantifiers: If \phi is a wff and x is a variable, then \forall x\phi and \exists x\phi are wffs.
  • Negation: If \phi is a wff then \neg\phi is a wff.
  • Binary connectives: If \phi and \psi are wffs and \Box is a binary connective, then \phi\Box\psi is a wff.
  • Equality Symbol: if equality is a part of first-order logic and \phi and \psi are wffs, then \phi=\psi is a wff.


The non-logical symbols of a first-order logic are usually interpreted with a first-order model, which is an ordered pair \mathcal A=(A,\sigma,I) , where A is the domain of discourse, is the signature, and I is the interpretation function which assigns meaning to the non-logical symbols. The signature is an ordered pair \sigma=(\sigma_f,\sigma_r,ar) where \sigma_r is the set of predicate or relation symbols, \sigma_f is the set of function symbols, and is a mapping ar:\sigma_r\cup\sigma_f\to\N which assigns a natural number called an arity. The notation for an interpretation of a non-logical symbol x is I(x)=x^\mathcal A .

Each predicate symbol or relation symbol R is assigned a n-ary relation R^\mathcal A\subseteq A^n or equivalently an n-ary function R^\mathcal A:D^n \to \mathbb B (where \mathbb B is the boolean domain or some other truth set).

Each function symbol f is assigned an n-ary function f^\mathcal A:D^n\to D. If f is a nullary function (that is an individual constant) its interpretation is f^\mathcal A\in D . Individual constants may be assigned a value, such as f^\mathcal A=100 .

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 v_1,\ldots,v_n be the evaluations of the terms t_1,\ldots,t_n. Then P(t_1,\ldots,t_n) is true if and only if (v_1,\ldots,v_n)\in P^\mathcal{A} . (Function symbols are evalauted in the following way: Given terms t_1,\ldots,t_n that have been evaulated to d_1,\ldots,d_n , the n-ary function value f(t_1,\ldots,t_n) evaulates to f^\mathcal{A}(d_1,\ldots,d_n) .
  • t_1=t_2is true if and only if t_1 and t_2 evaulate to the same x\in D
  • \forall x\phi(x) is true if \phi(x) for all x\in D .
  • \exists x\phi(x) is true if and only if there exists x\in D such that \phi(x) .

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.


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

External links