Firstorder logic is a formal system used in mathematics, philosophy, linguistics, and computer science. It is also known as firstorder predicate calculus, the lower predicate calculus, quantification theory, and predicate logic. Firstorder logic is distinguished from propositional logic by its use of quantified variables.
A theory about some topic is usually firstorder logic together with a specified domain of discourse over which the quantified variables range, finitely many functions which map from that domain into it, finitely many predicates defined on that domain, and a recursive set of axioms which are believed to hold for those things. Sometimes "theory" is understood in a more formal sense, which is just a set of sentences in firstorder logic.
The adjective "firstorder" distinguishes firstorder logic from higherorder logic in which there are predicates having predicates or functions as arguments, or in which one or both of predicate quantifiers or function quantifiers are permitted.^{[1]} In firstorder theories, predicates are often associated with sets. In interpreted higherorder theories, predicates may be interpreted as sets of sets.
There are many deductive systems for firstorder logic that are sound (all provable statements are true) and complete (all true statements are provable). Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in firstorder logic. Firstorder logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem.
Firstorder logic is the standard for the formalization of mathematics into axioms and is studied in the foundations of mathematics. Mathematical theories, such as number theory and set theory, have been formalized into firstorder axiom schemata such as Peano arithmetic and Zermelo–Fraenkel set theory (ZF) respectively.
No firstorder theory, however, has the strength to describe fully and categorically structures with an infinite domain, such as the natural numbers or the real line. Categorical axiom systems for these structures can be obtained in stronger logics such as secondorder logic.
For a history of firstorder logic and how it came to dominate formal logic, see José Ferreirós (2001).
Introduction
While propositional logic deals with simple declarative propositions, firstorder logic additionally covers predicates and quantification.
A predicate takes an entity or entities in the domain of discourse as input and outputs either True or False. Consider the two sentences "Socrates is a philosopher" and "Plato is a philosopher". In propositional logic, these sentences are viewed as being unrelated and are denoted, for example, by p and q. However, the predicate "is a philosopher" occurs in both sentences which have a common structure of "a is a philosopher". The variable a is instantiated as "Socrates" in first sentence and is instantiated as "Plato" in the second sentence. The use of predicates, such as "is a philosopher" in this example, distinguishes firstorder logic from propositional logic.
Predicates can be compared. Consider, for example, the firstorder formula "if a is a philosopher, then a is a scholar". This formula is a conditional statement with "a is a philosopher" as hypothesis and "a is a scholar" as conclusion. The truth of this formula depends on which object is denoted by a, and on the interpretations of the predicates "is a philosopher" and "is a scholar".
Variables can be quantified over. The variable a in the previous formula can be quantified over, for instance, in the firstorder sentence "For every a, if a is a philosopher, then a is a scholar". The universal quantifier "for every" in this sentence expresses the idea that the claim "if a is a philosopher, then a is a scholar" holds for all choices of a.
The negation of the above sentence "For every a, if a is a philosopher, then a is a scholar" is logically equivalent to the sentence "There exists a such that a is a philosopher and a is not a scholar". The existential quantifier "there exists" expresses the idea that the claim "a is a philosopher and a is not a scholar" holds for some choice of a.
The predicates "is a philosopher" and "is a scholar" each take a single variable. Predicates can take several variables. In the firstorder sentence "Socrates is the teacher of Plato", the predicate "is the teacher of" takes two variables.
To interpret a firstorder formula, one specifies what each predicate means and the entities that can instantiate the predicated variables. These entities form the domain of discourse or universe, which is usually required to be a nonempty set. Given that the interpretation with the domain of discourse as consisting of all human beings and the predicate "is a philosopher" understood as "have written the Republic", the sentence "There exist a such that a is a philosopher" is seen as being true, as witnessed by Plato.
Syntax
There are two key parts of first order logic. The syntax determines which collections of symbols are legal expressions in firstorder logic, while the semantics determine the meanings behind these expressions.
Alphabet
Unlike natural languages, such as English, the language of firstorder logic is completely formal, so that it can be mechanically determined whether a given expression is legal. There are two key types of legal expressions: terms, which intuitively represent objects, and formulas, which intuitively express predicates that can be true or false. The terms and formulas of firstorder logic are strings of symbols which together form the alphabet of the language. As with all formal languages, the nature of the symbols themselves is outside the scope of formal logic; they are often regarded simply as letters and punctuation symbols.
It is common to divide the symbols of the alphabet into logical symbols, which always have the same meaning, and nonlogical symbols, whose meaning varies by interpretation. For example, the logical symbol $\backslash land$ always represents "and"; it is never interpreted as "or". On the other hand, a nonlogical predicate symbol such as Phil(x) could be interpreted to mean "x is a philosopher", "x is a man named Philip", or any other unary predicate, depending on the interpretation at hand.
Logical symbols
There are several logical symbols in the alphabet, which vary by author but usually include:
 The quantifier symbols ∀ and ∃
 The logical connectives: ∧ for conjunction, ∨ for disjunction, → for implication, ↔ for biconditional, ¬ for negation. Occasionally other logical connective symbols are included. Some authors use →, or Cpq, instead of →, and ↔, or Epq, instead of ↔, especially in contexts where $\backslash to$ is used for other purposes. Moreover, the horseshoe ⊃ may replace →; the triplebar ≡ may replace ↔, and a tilde (~), Np, or Fpq, may replace ¬; , or Apq may replace ∨; and &, Kpq, or the middle dot, ⋅, may replace ∧, especially if these symbols are not available for technical reasons. (Note: the aforementioned symbols Cpq, Epq, Np, Apq, and Kpq are used in Polish notation.)
 Parentheses, brackets, and other punctuation symbols. The choice of such symbols varies depending on context.
 An infinite set of variables, often denoted by lowercase letters at the end of the alphabet x, y, z, … . Subscripts are often used to distinguish variables: x_{0}, x_{1}, x_{2}, … .
 An equality symbol (sometimes, identity symbol) =; see the section on equality below.
It should be noted that not all of these symbols are required – only one of the quantifiers, negation and conjunction, variables, brackets and equality suffice. There are numerous minor variations that may define additional logical symbols:
 Sometimes the truth constants T, Vpq, or ⊤, for "true" and F, Opq, or ⊥, for "false" are included. Without any such logical operators of valence 0, these two constants can only be expressed using quantifiers.
 Sometimes additional logical connectives are included, such as the Sheffer stroke, Dpq (NAND), and exclusive or, Jpq.
Nonlogical symbols
The nonlogical symbols represent predicates (relations), functions and constants on the domain of discourse. It used to be standard practice to use a fixed, infinite set of nonlogical symbols for all purposes. A more recent practice is to use different nonlogical symbols according to the application one has in mind. Therefore it has become necessary to name the set of all nonlogical symbols used in a particular application. This choice is made via a signature.^{[2]}
The traditional approach is to have only one, infinite, set of nonlogical symbols (one signature) for all applications. Consequently, under the traditional approach there is only one language of firstorder logic.^{[3]} This approach is still common, especially in philosophically oriented books.
 For every integer n ≥ 0 there is a collection of nary, or nplace, predicate symbols. Because they represent relations between n elements, they are also called relation symbols. For each arity n we have an infinite supply of them:
 P^{n}_{0}, P^{n}_{1}, P^{n}_{2}, P^{n}_{3}, …
 For every integer n ≥ 0 there are infinitely many nary function symbols:
 f^{ n}_{0}, f^{ n}_{1}, f^{ n}_{2}, f^{ n}_{3}, …
In contemporary mathematical logic, the signature varies by application. Typical signatures in mathematics are {1, ×} or just {×} for groups, or {0, 1, +, ×, <} for ordered fields. There are no restrictions on the number of nonlogical symbols. The signature can be empty, finite, or infinite, even uncountable. Uncountable signatures occur for example in modern proofs of the LöwenheimSkolem theorem.
In this approach, every nonlogical symbol is of one of the following types.
 A predicate symbol (or relation symbol) with some valence (or arity, number of arguments) greater than or equal to 0. These which are often denoted by uppercase letters P, Q, R,... .
 Relations of valence 0 can be identified with propositional variables. For example, P, which can stand for any statement.
 For example, P(x) is a predicate variable of valence 1. One possible interpretation is "x is a man".
 Q(x,y) is a predicate variable of valence 2. Possible interpretations include "x is greater than y" and "x is the father of y".
 A function symbol, with some valence greater than or equal to 0. These are often denoted by lowercase letters f, g, h,... .
 Examples: f(x) may be interpreted as for "the father of x". In arithmetic, it may stand for "x". In set theory, it may stand for "the power set of x". In arithmetic, g(x,y) may stand for "x+y". In set theory, it may stand for "the union of x and y".
 Function symbols of valence 0 are called constant symbols, and are often denoted by lowercase letters at the beginning of the alphabet a, b, c,... . The symbol a may stand for Socrates. In arithmetic, it may stand for 0. In set theory, such a constant may stand for the empty set.
The traditional approach can be recovered in the modern approach by simply specifying the "custom" signature to consist of the traditional sequences of nonlogical symbols.
Formation rules
The formation rules define the terms and formulas of first order logic. When terms and formulas are represented as strings of symbols, these rules can be used to write a formal grammar for terms and formulas. These rules are generally contextfree (each production has a single symbol on the left side), except that the set of symbols may be allowed to be infinite and there may be many start symbols, for example the variables in the case of terms.
Terms
The set of terms is inductively defined by the following rules:
 Variables. Any variable is a term.
 Functions. Any expression f(t_{1},...,t_{n}) of n arguments (where each argument t_{i} is a term and f is a function symbol of valence n) is a term. In particular, symbols denoting individual constants are 0ary function symbols, and are thus terms.
Only expressions which can be obtained by finitely many applications of rules 1 and 2 are terms. For example, no expression involving a predicate symbol is a term.
Formulas
The set of formulas (also called wellformed formulas^{[4]} or wffs) is inductively defined by the following rules:
 Predicate symbols. If P is an nary predicate symbol and t_{1}, ..., t_{n} are terms then P(t_{1},...,t_{n}) is a formula.
 Equality. If the equality symbol is considered part of logic, and t_{1} and t_{2} are terms, then t_{1} = t_{2} is a formula.
 Negation. If φ is a formula, then $\backslash neg$φ is a formula.
 Binary connectives. If φ and ψ are formulas, then (φ $\backslash rightarrow$ ψ) is a formula. Similar rules apply to other binary logical connectives.
 Quantifiers. If φ is a formula and x is a variable, then $\backslash forall\; x\; \backslash varphi$ (for all x, $\backslash varphi$ holds) and $\backslash exists\; x\; \backslash varphi$ (there exists x such that $\backslash varphi$) are formulas.
Only expressions which can be obtained by finitely many applications of rules 1–5 are formulas. The formulas obtained from the first two rules are said to be atomic formulas.
For example,
 $\backslash forall\; x\; \backslash forall\; y\; (P(f(x))\; \backslash rightarrow\backslash neg\; (P(x)\; \backslash rightarrow\; Q(f(y),x,z)))$
is a formula, if f is a unary function symbol, P a unary predicate symbol, and Q a ternary predicate symbol. On the other hand, $\backslash forall\; x\backslash ,\; x\; \backslash rightarrow$ is not a formula, although it is a string of symbols from the alphabet.
The role of the parentheses in the definition is to ensure that any formula can only be obtained in one way by following the inductive definition (in other words, there is a unique parse tree for each formula). This property is known as unique readability of formulas. There are many conventions for where parentheses are used in formulas. For example, some authors use colons or full stops instead of parentheses, or change the places in which parentheses are inserted. Each author's particular definition must be accompanied by a proof of unique readability.
This definition of a formula does not support defining an ifthenelse function ite(c, a, b), where "c" is a condition expressed as a formula, that would return "a" if c is true, and "b" if it is false. This is because both predicates and functions can only accept terms as parameters, but the first parameter is a formula. Some languages built on firstorder logic, such as SMTLIB 2.0, add this.^{[5]}
Notational conventions
For convenience, conventions have been developed about the precedence of the logical operators, to avoid the need to write parentheses in some cases. These rules are similar to the order of operations in arithmetic. A common convention is:
 $\backslash lnot$ is evaluated first
 $\backslash land$ and $\backslash lor$ are evaluated next
 Quantifiers are evaluated next
 $\backslash to$ is evaluated last.
Moreover, extra punctuation not required by the definition may be inserted to make formulas easier to read. Thus the formula
 $(\backslash lnot\; \backslash forall\; x\; P(x)\; \backslash to\; \backslash exists\; x\; \backslash lnot\; P(x))$
might be written as
 $(\backslash lnot\; [\backslash forall\; x\; P(x)])\; \backslash to\; \backslash exists\; x\; [\backslash lnot\; P(x)].$
In some fields, it is common to use infix notation for binary relations and functions, instead of the prefix notation defined above. For example, in arithmetic, one typically writes "2 + 2 = 4" instead of "=(+(2,2),4)". It is common to regard formulas in infix notation as abbreviations for the corresponding formulas in prefix notation.
The definitions above use infix notation for binary connectives such as $\backslash to$. A less common convention is Polish notation, in which one writes $\backslash rightarrow$, $\backslash wedge$, and so on in front of their arguments rather than between them. This convention allows all punctuation symbols to be discarded. Polish notation is compact and elegant, but rarely used in practice because it is hard for humans to read it. In Polish notation, the formula
 $\backslash forall\; x\; \backslash forall\; y\; (P(f(x))\; \backslash rightarrow\backslash neg\; (P(x)\; \backslash rightarrow\; Q(f(y),x,z)))$
becomes "∀x∀y→Pfx¬→ PxQfyxz".
Free and bound variables
In a formula, a variable may occur free or bound. Intuitively, a variable is free in a formula if it is not quantified: in $\backslash forall\; y\backslash ,\; P(x,y)$, variable x is free while y is bound. The free and bound variables of a formula are defined inductively as follows.
 Atomic formulas. If φ is an atomic formula then x is free in φ if and only if x occurs in φ. Moreover, there are no bound variables in any atomic formula.
 Negation. x is free in $\backslash neg$φ if and only if x is free in φ. x is bound in $\backslash neg$φ if and only if x is bound in φ.
 Binary connectives. x is free in (φ $\backslash rightarrow$ ψ) if and only if x is free in either φ or ψ. x is bound in (φ $\backslash rightarrow$ ψ) if and only if x is bound in either φ or ψ. The same rule applies to any other binary connective in place of $\backslash rightarrow$.
 Quantifiers. x is free in $\backslash forall$y φ if and only if x is free in φ and x is a different symbol from y. Also, x is bound in $\backslash forall$y φ if and only if x is y or x is bound in φ. The same rule holds with $\backslash exists$ in place of $\backslash forall$.
For example, in $\backslash forall$x $\backslash forall$y (P(x)$\backslash rightarrow$ Q(x,f(x),z)), x and y are bound variables, z is a free variable, and w is neither because it does not occur in the formula.
Freeness and boundness can be also specialized to specific occurrences of variables in a formula. For example, in $P(x)\; \backslash rightarrow\; \backslash forall\; x\backslash ,\; Q(x)$, the first occurrence of x is free while the second is bound. In other words, the x in $P(x)$ is free while the $x$ in $\backslash forall\; x\backslash ,\; Q(x)$ is bound.
A formula in firstorder logic with no free variables is called a firstorder sentence. These are the formulas that will have welldefined truth values under an interpretation. For example, whether a formula such as Phil(x) is true must depend on what x represents. But the sentence $\backslash exists\; x\backslash ,\; \backslash text\{Phil\}(x)$ will be either true or false in a given interpretation.
Examples
Abelian groups
In mathematics the language of ordered abelian groups has one constant symbol 0, one unary function symbol −, one binary function symbol +, and one binary relation symbol ≤. Then:
 The expressions +(x, y) and +(x, +(y, −(z))) are terms. These are usually written as x + y and x + y − z.
 The expressions +(x, y) = 0 and ≤(+(x, +(y, −(z))), +(x, y)) are atomic formulas.
 These are usually written as x + y = 0 and x + y − z ≤ x + y.
 The expression $(\backslash forall\; x\; \backslash forall\; y\; \backslash ,\; \backslash mathop\{\backslash leq\}(\backslash mathop\{+\}(x,\; y),\; z)\; \backslash to\; \backslash forall\; x\backslash ,\; \backslash forall\; y\backslash ,\; \backslash mathop\{+\}(x,\; y)\; =\; 0)$ is a formula, which is usually written as $\backslash forall\; x\; \backslash forall\; y\; (\; x\; +\; y\; \backslash leq\; z)\; \backslash to\; \backslash forall\; x\; \backslash forall\; y\; (x+y\; =\; 0).$
Loving relation
There are 10 different formulas with 8 different meanings, that use the loving relation Lxy ("x loves y.") and the quantifiers ∀ and ∃:

The diagonal is nonempty/full:




The matrix is nonempty/full:






The logical matrices represent the formulas for the case that there are five individuals that can love (vertical axis) and be loved (horizontal axis). Except for the sentences 9 and 10, they are examples. E.g. the matrix representing sentence 5 stands for "b loves himself."; the matrix representing sentences 7 and 8 stands for "c loves b."
It's important and instructive to distinguish sentence 1, $\backslash forall\; x\; \backslash exist\; y\; Lyx$, and 3, $\backslash exist\; x\; \backslash forall\; y\; Lxy$: In both cases everyone is loved; but in the first case everyone is loved by someone, in the second case everyone is loved by the same person.
Some sentences imply each other — e.g. if 3 is true also 1 is true, but not vice versa. (See Hasse diagram)
Semantics
An interpretation of a firstorder language assigns a denotation to all nonlogical constants in that language. It also determines a domain of discourse that specifies the range of the quantifiers. The result is that each term is assigned an object that it represents, and each sentence is assigned a truth value. In this way, an interpretation provides semantic meaning to the terms and formulas of the language. The study of the interpretations of formal languages is called formal semantics. What follows is a description of the standard or Tarskian semantics for firstorder logic. (It is also possible to define game semantics for firstorder logic, but aside from requiring the axiom of choice, game semantics agree with Tarskian semantics for firstorder logic, so game semantics will not be elaborated herein.)
The domain of discourse D is a nonempty set of "objects" of some kind. Intuitively, a firstorder formula is a statement about these objects; for example, $\backslash exists\; x\; P(x)$ states the existence of an object x such that the predicate P is true where referred to it. The domain of discourse is the set of considered objects. For example, one can take $D$ to be the set of integer numbers.
The interpretation of a function symbol is a function. For example, if the domain of discourse consists of integers, a function symbol f of arity 2 can be interpreted as the function that gives the sum of its arguments. In other words, the symbol f is associated with the function I(f) which, in this interpretation, is addition.
The interpretation of a constant symbol is a function from the oneelement set D^{0} to D, which can be simply identified with an object in D. For example, an interpretation may assign the value $I(c)=10$ to the constant symbol $c$.
The interpretation of an nary predicate symbol is a set of ntuples of elements of the domain of discourse. This means that, given an interpretation, a predicate symbol, and n elements of the domain of discourse, one can tell whether the predicate is true of those elements according to the given interpretation. For example, an interpretation I(P) of a binary predicate symbol P may be the set of pairs of integers such that the first one is less than the second. According to this interpretation, the predicate P would be true if its first argument is less than the second.
Firstorder structures
The most common way of specifying an interpretation (especially in mathematics) is to specify a structure (also called a model; see below). The structure consists of a nonempty set D that forms the domain of discourse and an interpretation I of the nonlogical terms of the signature. This interpretation is itself a function:
 Each function symbol f of arity n is assigned a function I(f) from $D^n$ to $D$. In particular, each constant symbol of the signature is assigned an individual in the domain of discourse.
 Each predicate symbol P of arity n is assigned a relation I(P) over $D^n$ or, equivalently, a function from $D^n$ to $\backslash \{true,\; false\backslash \}$. Thus each predicate symbol is interpreted by a Booleanvalued function on D.
Evaluation of truth values
A formula evaluates to true or false given an interpretation, and a variable assignment μ that associates an element of the domain of discourse with each variable. The reason that a variable assignment is required is to give meanings to formulas with free variables, such as $y\; =\; x$. The truth value of this formula changes depending on whether x and y denote the same individual.
First, the variable assignment μ can be extended to all terms of the language, with the result that each term maps to a single element of the domain of discourse. The following rules are used to make this assignment:
 Variables. Each variable x evaluates to μ(x)
 Functions. Given terms $t\_1,\; \backslash ldots,\; t\_n$ that have been evaluated to elements $d\_1,\; \backslash ldots,\; d\_n$ of the domain of discourse, and a nary function symbol f, the term $f(t\_1,\; \backslash ldots,\; t\_n)$ evaluates to $(I(f))(d\_1,\backslash ldots,d\_n)$.
Next, each formula is assigned a truth value. The inductive definition used to make this assignment is called the Tschema.
 Atomic formulas (1). A formula $P(t\_1,\backslash ldots,t\_n)$ is associated the value true or false depending on whether $\backslash langle\; v\_1,\backslash ldots,v\_n\; \backslash rangle\; \backslash in\; I(P)$, where $v\_1,\backslash ldots,v\_n$ are the evaluation of the terms $t\_1,\backslash ldots,t\_n$ and $I(P)$ is the interpretation of $P$, which by assumption is a subset of $D^n$.
 Atomic formulas (2). A formula $t\_1\; =\; t\_2$ is assigned true if $t\_1$ and $t\_2$ evaluate to the same object of the domain of discourse (see the section on equality below).
 Logical connectives. A formula in the form $\backslash neg\; \backslash phi$, $\backslash phi\; \backslash rightarrow$
\psi, etc. is evaluated according to the truth table for the connective in question, as in propositional logic.
 Existential quantifiers. A formula $\backslash exists\; x\; \backslash phi(x)$ is true according to M and $\backslash mu$ if there exists an evaluation $\backslash mu\text{'}$ of the variables that only differs from $\backslash mu$ regarding the evaluation of x and such that φ is true according to the interpretation M and the variable assignment $\backslash mu\text{'}$. This formal definition captures the idea that $\backslash exists\; x\; \backslash phi(x)$ is true if and only if there is a way to choose a value for x such that φ(x) is satisfied.
 Universal quantifiers. A formula $\backslash forall\; x\; \backslash phi(x)$ is true according to M and $\backslash mu$ if φ(x) is true for every pair composed by the interpretation M and some variable assignment $\backslash mu\text{'}$ that differs from $\backslash mu$ only on the value of x. This captures the idea that $\backslash forall\; x\; \backslash phi(x)$ is true if every possible choice of a value for x causes φ(x) to be true.
If a formula does not contain free variables, and so is a sentence, then the initial variable assignment does not affect its truth value. In other words, a sentence is true according to M and $\backslash mu$ if and only if it is true according to M and every other variable assignment $\backslash mu\text{'}$.
There is a second common approach to defining truth values that does not rely on variable assignment functions. Instead, given an interpretation M, one first adds to the signature a collection of constant symbols, one for each element of the domain of discourse in M; say that for each d in the domain the constant symbol c_{d} is fixed. The interpretation is extended so that each new constant symbol is assigned to its corresponding element of the domain. One now defines truth for quantified formulas syntactically, as follows:
 Existential quantifiers (alternate). A formula $\backslash exists\; x\; \backslash phi(x)$ is true according to M if there is some d in the domain of discourse such that $\backslash phi(c\_d)$ holds. Here $\backslash phi(c\_d)$ is the result of substituting c_{d} for every free occurrence of x in φ.
 Universal quantifiers (alternate). A formula $\backslash forall\; x\; \backslash phi(x)$ is true according to M if, for every d in the domain of discourse, $\backslash phi(c\_d)$ is true according to M.
This alternate approach gives exactly the same truth values to all sentences as the approach via variable assignments.
Validity, satisfiability, and logical consequence
If a sentence φ evaluates to True under a given interpretation M, one says that M satisfies φ; this is denoted $M\; \backslash vDash\; \backslash phi$. A sentence is satisfiable if there is some interpretation under which it is true.
Satisfiability of formulas with free variables is more complicated, because an interpretation on its own does not determine the truth value of such a formula. The most common convention is that a formula with free variables is said to be satisfied by an interpretation if the formula remains true regardless which individuals from the domain of discourse are assigned to its free variables. This has the same effect as saying that a formula is satisfied if and only if its universal closure is satisfied.
A formula is logically valid (or simply valid) if it is true in every interpretation. These formulas play a role similar to tautologies in propositional logic.
A formula φ is a logical consequence of a formula ψ if every interpretation that makes ψ true also makes φ true. In this case one says that φ is logically implied by ψ.
Algebraizations
An alternate approach to the semantics of firstorder logic proceeds via abstract algebra. This approach generalizes the Lindenbaum–Tarski algebras of propositional logic. There are three ways of eliminating quantified variables from firstorder logic that do not involve replacing quantifiers with other variable binding term operators:
These algebras are all lattices that properly extend the twoelement Boolean algebra.
Tarski and Givant (1987) showed that the fragment of firstorder logic that has no atomic sentence lying in the scope of more than three quantifiers has the same expressive power as relation algebra. This fragment is of great interest because it suffices for Peano arithmetic and most axiomatic set theory, including the canonical ZFC. They also prove that firstorder logic with a primitive ordered pair is equivalent to a relation algebra with two ordered pair projection functions.
Firstorder theories, models, and elementary classes
A firstorder theory of a particular signature is a set of axioms, which are sentences consisting of symbols from that signature. The set of axioms is often finite or recursively enumerable, in which case the theory is called effective. Some authors require theories to also include all logical consequences of the axioms. The axioms are considered to hold within the theory and from them other sentences that hold within the theory can be derived.
A firstorder structure that satisfies all sentences in a given theory is said to be a model of the theory. An elementary class is the set of all structures satisfying a particular theory. These classes are a main subject of study in model theory.
Many theories have an intended interpretation, a certain model that is kept in mind when studying the theory. For example, the intended interpretation of Peano arithmetic consists of the usual natural numbers with their usual operations. However, the Löwenheim–Skolem theorem shows that most firstorder theories will also have other, nonstandard models.
A theory is consistent if it is not possible to prove a contradiction from the axioms of the theory. A theory is complete if, for every formula in its signature, either that formula or its negation is a logical consequence of the axioms of the theory. Gödel's incompleteness theorem shows that effective firstorder theories that include a sufficient portion of the theory of the natural numbers can never be both consistent and complete.
For more information on this subject see List of firstorder theories and Theory (mathematical logic)
Empty domains
Main article:
Empty domain
The definition above requires that the domain of discourse of any interpretation must be a nonempty set. There are settings, such as inclusive logic, where empty domains are permitted. Moreover, if a class of algebraic structures includes an empty structure (for example, there is an empty poset), that class can only be an elementary class in firstorder logic if empty domains are permitted or the empty structure is removed from the class.
There are several difficulties with empty domains, however:
 Many common rules of inference are only valid when the domain of discourse is required to be nonempty. One example is the rule stating that $\backslash phi\; \backslash lor\; \backslash exists\; x\; \backslash psi$ implies $\backslash exists\; x\; (\backslash phi\; \backslash lor\; \backslash psi)$ when x is not a free variable in φ. This rule, which is used to put formulas into prenex normal form, is sound in nonempty domains, but unsound if the empty domain is permitted.
 The definition of truth in an interpretation that uses a variable assignment function cannot work with empty domains, because there are no variable assignment functions whose range is empty. (Similarly, one cannot assign interpretations to constant symbols.) This truth definition requires that one must select a variable assignment function (μ above) before truth values for even atomic formulas can be defined. Then the truth value of a sentence is defined to be its truth value under any variable assignment, and it is proved that this truth value does not depend on which assignment is chosen. This technique does not work if there are no assignment functions at all; it must be changed to accommodate empty domains.
Thus, when the empty domain is permitted, it must often be treated as a special case. Most authors, however, simply exclude the empty domain by definition.
Deductive systems
A deductive system is used to demonstrate, on a purely syntactic basis, that one formula is a logical consequence of another formula. There are many such systems for firstorder logic, including Hilbertstyle deductive systems, natural deduction, the sequent calculus, the tableaux method, and resolution. These share the common property that a deduction is a finite syntactic object; the format of this object, and the way it is constructed, vary widely. These finite deductions themselves are often called derivations in proof theory. They are also often called proofs, but are completely formalized unlike naturallanguage mathematical proofs.
A deductive system is sound if any formula that can be derived in the system is logically valid. Conversely, a deductive system is complete if every logically valid formula is derivable. All of the systems discussed in this article are both sound and complete. They also share the property that it is possible to effectively verify that a purportedly valid deduction is actually a deduction; such deduction systems are called effective.
A key property of deductive systems is that they are purely syntactic, so that derivations can be verified without considering any interpretation. Thus a sound argument is correct in every possible interpretation of the language, regardless whether that interpretation is about mathematics, economics, or some other area.
In general, logical consequence in firstorder logic is only semidecidable: if a sentence A logically implies a sentence B then this can be discovered (for example, by searching for a proof until one is found, using some effective, sound, complete proof system). However, if A does not logically imply B, this does not mean that A logically implies the negation of B. There is no effective procedure that, given formulas A and B, always correctly decides whether A logically implies B.
Rules of inference
A rule of inference states that, given a particular formula (or set of formulas) with a certain property as a hypothesis, another specific formula (or set of formulas) can be derived as a conclusion. The rule is sound (or truthpreserving) if it preserves validity in the sense that whenever any interpretation satisfies the hypothesis, that interpretation also satisfies the conclusion.
For example, one common rule of inference is the rule of substitution. If t is a term and φ is a formula possibly containing the variable x, then φ[t/x] (often denoted φ[x/t]) is the result of replacing all free instances of x by t in φ. The substitution rule states that for any φ and any term t, one can conclude φ[t/x] from φ provided that no free variable of t becomes bound during the substitution process. (If some free variable of t becomes bound, then to substitute t for x it is first necessary to change the bound variables of φ to differ from the free variables of t.)
To see why the restriction on bound variables is necessary, consider the logically valid formula φ given by $\backslash exists\; x\; (x\; =\; y)$, in the signature of (0,1,+,×,=) of arithmetic. If t is the term "x + 1", the formula φ[t/y] is $\backslash exists\; x\; (\; x\; =\; x+1)$, which will be false in many interpretations. The problem is that the free variable x of t became bound during the substitution. The intended replacement can be obtained by renaming the bound variable x of φ to something else, say z, so that the formula after substitution is $\backslash exists\; z\; (\; z\; =\; x+1)$, which is again logically valid.
The substitution rule demonstrates several common aspects of rules of inference. It is entirely syntactical; one can tell whether it was correctly applied without appeal to any interpretation. It has (syntacticallydefined) limitations on when it can be applied, which must be respected to preserve the correctness of derivations. Moreover, as is often the case, these limitations are necessary because of interactions between free and bound variables that occur during syntactic manipulations of the formulas involved in the inference rule.
Hilbertstyle systems and natural deduction
A deduction in a Hilbertstyle deductive system is a list of formulas, each of which is a logical axiom, a hypothesis that has been assumed for the derivation at hand, or follows from previous formulas via a rule of inference. The logical axioms consist of several axiom schemes of logically valid formulas; these encompass a significant amount of propositional logic. The rules of inference enable the manipulation of quantifiers. Typical Hilbertstyle systems have a small number of rules of inference, along with several infinite schemes of logical axioms. It is common to have only modus ponens and universal generalization as rules of inference.
Natural deduction systems resemble Hilbertstyle systems in that a deduction is a finite list of formulas. However, natural deduction systems have no logical axioms; they compensate by adding additional rules of inference that can be used to manipulate the logical connectives in formulas in the proof.
Sequent calculus
The sequent calculus was developed to study the properties of natural deduction systems. Instead of working with one formula at a time, it uses sequents, which are expressions of the form
 $A\_1,\; \backslash ldots,\; A\_n\; \backslash vdash\; B\_1,\; \backslash ldots,\; B\_k,$
where A_{1}, ..., A_{n}, B_{1}, ..., B_{k} are formulas and the turnstile symbol $\backslash vdash$ is used as punctuation to separate the two halves. Intuitively, a sequent expresses the idea that $(A\_1\; \backslash land\; \backslash cdots\backslash land\; A\_n)$ implies $(B\_1\backslash lor\backslash cdots\backslash lor\; B\_k)$.
Tableaux method
Unlike the methods just described, the derivations in the tableaux method are not lists of formulas. Instead, a derivation is a tree of formulas. To show that a formula A is provable, the tableaux method attempts to demonstrate that the negation of A is unsatisfiable. The tree of the derivation has $\backslash lnot\; A$ at its root; the tree branches in a way that reflects the structure of the formula. For example, to show that $C\; \backslash lor\; D$ is unsatisfiable requires showing that C and D are each unsatisfiable; this corresponds to a branching point in the tree with parent $C\; \backslash lor\; D$ and children C and D.
Resolution
The resolution rule is a single rule of inference that, together with unification, is sound and complete for firstorder logic. As with the tableaux method, a formula is proved by showing that the negation of the formula is unsatisfiable. Resolution is commonly used in automated theorem proving.
The resolution method works only with formulas that are disjunctions of atomic formulas; arbitrary formulas must first be converted to this form through Skolemization. The resolution rule states that from the hypotheses $A\_1\; \backslash lor\backslash cdots\backslash lor\; A\_k\; \backslash lor\; C$ and $B\_1\backslash lor\backslash cdots\backslash lor\; B\_l\backslash lor\backslash lnot\; C$, the conclusion $A\_1\backslash lor\backslash cdots\backslash lor\; A\_k\backslash lor\; B\_1\backslash lor\backslash cdots\backslash lor\; B\_l$ can be obtained.
Provable identities
The following sentences can be called "identities" because the main connective in each is the biconditional.
 $\backslash lnot\; \backslash forall\; x\; \backslash ,\; P(x)\; \backslash Leftrightarrow\; \backslash exists\; x\; \backslash ,\; \backslash lnot\; P(x)$
 $\backslash lnot\; \backslash exists\; x\; \backslash ,\; P(x)\; \backslash Leftrightarrow\; \backslash forall\; x\; \backslash ,\; \backslash lnot\; P(x)$
 $\backslash forall\; x\; \backslash ,\; \backslash forall\; y\; \backslash ,\; P(x,y)\; \backslash Leftrightarrow\; \backslash forall\; y\; \backslash ,\; \backslash forall\; x\; \backslash ,\; P(x,y)$
 $\backslash exists\; x\; \backslash ,\; \backslash exists\; y\; \backslash ,\; P(x,y)\; \backslash Leftrightarrow\; \backslash exists\; y\; \backslash ,\; \backslash exists\; x\; \backslash ,\; P(x,y)$
 $\backslash forall\; x\; \backslash ,\; P(x)\; \backslash land\; \backslash forall\; x\; \backslash ,\; Q(x)\; \backslash Leftrightarrow\; \backslash forall\; x\; \backslash ,\; (P(x)\; \backslash land\; Q(x))$
 $\backslash exists\; x\; \backslash ,\; P(x)\; \backslash lor\; \backslash exists\; x\; \backslash ,\; Q(x)\; \backslash Leftrightarrow\; \backslash exists\; x\; \backslash ,\; (P(x)\; \backslash lor\; Q(x))$
 $P\; \backslash land\; \backslash exists\; x\; \backslash ,\; Q(x)\; \backslash Leftrightarrow\; \backslash exists\; x\; \backslash ,\; (P\; \backslash land\; Q(x))$ (where $x$ must not occur free in $P$)
 $P\; \backslash lor\; \backslash forall\; x\; \backslash ,\; Q(x)\; \backslash Leftrightarrow\; \backslash forall\; x\; \backslash ,\; (P\; \backslash lor\; Q(x))$ (where $x$ must not occur free in $P$)
Equality and its axioms
There are several different conventions for using equality (or identity) in firstorder logic. The most common convention, known as firstorder logic with equality, includes the equality symbol as a primitive logical symbol which is always interpreted as the real equality relation between members of the domain of discourse, such that the "two" given members are the same member. This approach also adds certain axioms about equality to the deductive system employed. These equality axioms are:
 Reflexivity. For each variable x, x = x.
 Substitution for functions. For all variables x and y, and any function symbol f,
 x = y → f(...,x,...) = f(...,y,...).
 Substitution for formulas. For any variables x and y and any formula φ(x), if φ' is obtained by replacing any number of free occurrences of x in φ with y, such that these remain free occurrences of y, then
 x = y → (φ → φ').
These are axiom schemes, each of which specifies an infinite set of axioms. The third scheme is known as Leibniz's law, "the principle of substitutivity", "the indiscernibility of identicals", or "the replacement property". The second scheme, involving the function symbol f, is (equivalent to) a special case of the third scheme, using the formula
 x = y → (f(...,x,...) = z → f(...,y,...) = z).
Many other properties of equality are consequences of the axioms above, for example:
 Symmetry. If x = y then y = x.
 Transitivity. If x = y and y = z then x = z.
Firstorder logic without equality
An alternate approach considers the equality relation to be a nonlogical symbol. This convention is known as firstorder logic without equality. If an equality relation is included in the signature, the axioms of equality must now be added to the theories under consideration, if desired, instead of being considered rules of logic. The main difference between this method and firstorder logic with equality is that an interpretation may now interpret two distinct individuals as "equal" (although, by Leibniz's law, these will satisfy exactly the same formulas under any interpretation). That is, the equality relation may now be interpreted by an arbitrary equivalence relation on the domain of discourse that is congruent with respect to the functions and relations of the interpretation.
When this second convention is followed, the term normal model is used to refer to an interpretation where no distinct individuals a and b satisfy a = b. In firstorder logic with equality, only normal models are considered, and so there is no term for a model other than a normal model. When firstorder logic without equality is studied, it is necessary to amend the statements of results such as the Löwenheim–Skolem theorem so that only normal models are considered.
Firstorder logic without equality is often employed in the context of secondorder arithmetic and other higherorder theories of arithmetic, where the equality relation between sets of natural numbers is usually omitted.
Defining equality within a theory
If a theory has a binary formula A(x,y) which satisfies reflexivity and Leibniz's law, the theory is said to have equality, or to be a theory with equality. The theory may not have all instances of the above schemes as axioms, but rather as derivable theorems. For example, in theories with no function symbols and a finite number of relations, it is possible to define equality in terms of the relations, by defining the two terms s and t to be equal if any relation is unchanged by changing s to t in any argument.
Some theories allow other ad hoc definitions of equality:
 In the theory of partial orders with one relation symbol ≤, one could define s = t to be an abbreviation for s ≤ t $\backslash wedge$ t ≤ s.
 In set theory with one relation $\backslash in$, one may define s = t to be an abbreviation for $\backslash forall$x (s $\backslash in$ x $\backslash leftrightarrow$ t $\backslash in$ x) $\backslash wedge$ $\backslash forall$x (x $\backslash in$ s $\backslash leftrightarrow$ x $\backslash in$ t). This definition of equality then automatically satisfies the axioms for equality. In this case, one should replace the usual axiom of extensionality, $\backslash forall\; x\; \backslash forall\; y\; [\; \backslash forall\; z\; (z\; \backslash in\; x\; \backslash Leftrightarrow\; z\; \backslash in\; y)\; \backslash Rightarrow\; x\; =\; y]$, by $\backslash forall\; x\; \backslash forall\; y\; [\; \backslash forall\; z\; (z\; \backslash in\; x\; \backslash Leftrightarrow\; z\; \backslash in\; y)\; \backslash Rightarrow\; \backslash forall\; z\; (x\; \backslash in\; z\; \backslash Leftrightarrow\; y\; \backslash in\; z)\; ]$, i.e. if x and y have the same elements, then they belong to the same sets.
Metalogical properties
One motivation for the use of firstorder logic, rather than higherorder logic, is that firstorder logic has many metalogical properties that stronger logics do not have. These results concern general properties of firstorder logic itself, rather than properties of individual theories. They provide fundamental tools for the construction of models of firstorder theories.
Completeness and undecidability
Gödel's completeness theorem, proved by Kurt Gödel in 1929, establishes that there are sound, complete, effective deductive systems for firstorder logic, and thus the firstorder logical consequence relation is captured by finite provability. Naively, the statement that a formula φ logically implies a formula ψ depends on every model of φ; these models will in general be of arbitrarily large cardinality, and so logical consequence cannot be effectively verified by checking every model. However, it is possible to enumerate all finite derivations and search for a derivation of ψ from φ. If ψ is logically implied by φ, such a derivation will eventually be found. Thus firstorder logical consequence is semidecidable: it is possible to make an effective enumeration of all pairs of sentences (φ,ψ) such that ψ is a logical consequence of φ.
Unlike propositional logic, firstorder logic is undecidable (although semidecidable), provided that the language has at least one predicate of arity at least 2 (other than equality). This means that there is no decision procedure that determines whether arbitrary formulas are logically valid. This result was established independently by Alonzo Church and Alan Turing in 1936 and 1937, respectively, giving a negative answer to the Entscheidungsproblem posed by David Hilbert in 1928. Their proofs demonstrate a connection between the unsolvability of the decision problem for firstorder logic and the unsolvability of the halting problem.
There are systems weaker than full firstorder logic for which the logical consequence relation is decidable. These include propositional logic and monadic predicate logic, which is firstorder logic restricted to unary predicate symbols and no function symbols. The Bernays–Schönfinkel class of firstorder formulas is also decidable. Decidable subsets of firstorder logic are also studied in the framework of description logics.
The Löwenheim–Skolem theorem
The Löwenheim–Skolem theorem shows that if a firstorder theory of cardinality λ has any infinite model then it has models of every infinite cardinality greater than or equal to λ. One of the earliest results in model theory, it implies that it is not possible to characterize countability or uncountability in a firstorder language. That is, there is no firstorder formula φ(x) such that an arbitrary structure M satisfies φ if and only if the domain of discourse of M is countable (or, in the second case, uncountable).
The Löwenheim–Skolem theorem implies that infinite structures cannot be categorically axiomatized in firstorder logic. For example, there is no firstorder theory whose only model is the real line: any firstorder theory with an infinite model also has a model of cardinality larger than the continuum. Since the real line is infinite, any theory satisfied by the real line is also satisfied by some nonstandard models. When the Löwenheim–Skolem theorem is applied to firstorder set theories, the nonintuitive consequences are known as Skolem's paradox.
The compactness theorem
The compactness theorem states that a set of firstorder sentences has a model if and only if every finite subset of it has a model. This implies that if a formula is a logical consequence of an infinite set of firstorder axioms, then it is a logical consequence of some finite number of those axioms. This theorem was proved first by Kurt Gödel as a consequence of the completeness theorem, but many additional proofs have been obtained over time. It is a central tool in model theory, providing a fundamental method for constructing models.
The compactness theorem has a limiting effect on which collections of firstorder structures are elementary classes. For example, the compactness theorem implies that any theory that has arbitrarily large finite models has an infinite model. Thus the class of all finite graphs is not an elementary class (the same holds for many other algebraic structures).
There are also more subtle limitations of firstorder logic that are implied by the compactness theorem. For example, in computer science, many situations can be modeled as a directed graph of states (nodes) and connections (directed edges). Validating such a system may require showing that no "bad" state can be reached from any "good" state. Thus one seeks to determine if the good and bad states are in different connected components of the graph. However, the compactness theorem can be used to show that connected graphs are not an elementary class in firstorder logic, and there is no formula φ(x,y) of firstorder logic, in the signature of graphs, that expresses the idea that there is a path from x to y. Connectedness can be expressed in secondorder logic, however, but not with only existential set quantifiers, as $\backslash Sigma\_1^1$ also enjoys compactness.
Lindström's theorem
Per Lindström showed that the metalogical properties just discussed actually characterize firstorder logic in the sense that no stronger logic can also have those properties (Ebbinghaus and Flum 1994, Chapter XIII). Lindström defined a class of abstract logical systems, and a rigorous definition of the relative strength of a member of this class. He established two theorems for systems of this type:
 A logical system satisfying Lindström's definition that contains firstorder logic and satisfies both the Löwenheim–Skolem theorem and the compactness theorem must be equivalent to firstorder logic.
 A logical system satisfying Lindström's definition that has a semidecidable logical consequence relation and satisfies the Löwenheim–Skolem theorem must be equivalent to firstorder logic.
Limitations
Although firstorder logic is sufficient for formalizing much of mathematics, and is commonly used in computer science and other fields, it has certain limitations. These include limitations on its expressiveness and limitations of the fragments of natural languages that it can describe.
For instance, firstorder logic is undecidable, meaning a sound, complete and terminating decision algorithm is impossible. This has led to the study of interesting decidable fragments such as C_{2}, firstorder logic with two variables and the counting quantifiers $\backslash exist^\{\backslash ge\; n\}$ and $\backslash exist^\{\backslash le\; n\}$ (these quantifiers are, respectively, "there exists at least n" and "there exists at most n") (Horrocks 2010).
Expressiveness
The Löwenheim–Skolem theorem shows that if a firstorder theory has any infinite model, then it has infinite models of every cardinality. In particular, no firstorder theory with an infinite model can be categorical. Thus there is no firstorder theory whose only model has the set of natural numbers as its domain, or whose only model has the set of real numbers as its domain. Many extensions of firstorder logic, including infinitary logics and higherorder logics, are more expressive in the sense that they do permit categorical axiomatizations of the natural numbers or real numbers. This expressiveness comes at a metalogical cost, however: by Lindström's theorem, the compactness theorem and the downward Löwenheim–Skolem theorem cannot hold in any logic stronger than firstorder.
Formalizing natural languages
Firstorder logic is able to formalize many simple quantifier constructions in natural language, such as "every person who lives in Perth lives in Australia". But there are many more complicated features of natural language that cannot be expressed in (singlesorted) firstorder logic. "Any logical system which is appropriate as an instrument for the analysis of natural language needs a much richer structure than firstorder predicate logic" (Gamut 1991, p. 75).
Type 
Example 
Comment

Quantification over properties 
If John is selfsatisfied, then there is at least one thing he has in common with Peter 
Requires a quantifier over predicates, which cannot be implemented in singlesorted firstorder logic: Zj→ ∃X(Xj∧Xp)

Quantification over properties 
Santa Claus has all the attributes of a sadist 
Requires quantifiers over predicates, which cannot be implemented in singlesorted firstorder logic: ∀X(∀x(Sx → Xx)→Xs)

Predicate adverbial 
John is walking quickly 
Cannot be analysed as Wj ∧ Qj; predicate adverbials are not the same kind of thing as secondorder predicates such as colour

Relative adjective 
Jumbo is a small elephant 
Cannot be analysed as Sj ∧ Ej; predicate adjectives are not the same kind of thing as secondorder predicates such as colour

Predicate adverbial modifier 
John is walking very quickly 


Relative adjective modifier 
Jumbo is terribly small 
An expression such as "terribly", when applied to a relative adjective such as "small", results in a new composite relative adjective "terribly small"

Prepositions 
Mary is sitting next to John 
The preposition "next to" when applied to "John" results in the predicate adverbial "next to John"

Restrictions, extensions, and variations
There are many variations of firstorder logic. Some of these are inessential in the sense that they merely change notation without affecting the semantics. Others change the expressive power more significantly, by extending the semantics through additional quantifiers or other new logical symbols. For example, infinitary logics permit formulas of infinite size, and modal logics add symbols for possibility and necessity.
Restricted languages
Firstorder logic can be studied in languages with fewer logical symbols than were described above.
 Because $\backslash exists\; x\; \backslash phi(x)$ can be expressed as $\backslash neg\; \backslash forall\; x\; \backslash neg\; \backslash phi(x)$, and $\backslash forall\; x\; \backslash phi(x)$ can be expressed as $\backslash neg\; \backslash exists\; x\; \backslash neg\; \backslash phi(x)$, either of the two quantifiers $\backslash exists$ and $\backslash forall$ can be dropped.
 Since $\backslash phi\; \backslash lor\; \backslash psi$ can be expressed as $\backslash lnot\; (\backslash lnot\; \backslash phi\; \backslash land\; \backslash lnot\; \backslash psi)$ and $\backslash phi\; \backslash land\; \backslash psi$ can be expressed as $\backslash lnot(\backslash lnot\; \backslash phi\; \backslash lor\; \backslash lnot\; \backslash psi)$, either $\backslash vee$ or $\backslash wedge$ can be dropped. In other words, it is sufficient to have $\backslash neg$ and $\backslash vee$, or $\backslash neg$ and $\backslash wedge$, as the only logical connectives.
 Similarly, it is sufficient to have only $\backslash neg$ and $\backslash rightarrow$ as logical connectives, or to have only the Sheffer stroke (NAND) or the Peirce arrow (NOR) operator.
 It is possible to entirely avoid function symbols and constant symbols, rewriting them via predicate symbols in an appropriate way. For example, instead of using a constant symbol $\backslash ;\; 0$ one may use a predicate $\backslash ;\; 0(x)$ (interpreted as $\backslash ;\; x=0$ ), and replace every predicate such as $\backslash ;\; P(0,y)$ with $\backslash forall\; x\; \backslash ;(0(x)\; \backslash rightarrow\; P(x,y))$. A function such as $f(x\_1,x\_2,...,x\_n)$ will similarly be replaced by a predicate $F(x\_1,x\_2,...,x\_n,y)$ interpreted as $y\; =\; f(x\_1,x\_2,...,x\_n)$. This change requires adding additional axioms to the theory at hand, so that interpretations of the predicate symbols used have the correct semantics.
Restrictions such as these are useful as a technique to reduce the number of inference rules or axiom schemes in deductive systems, which leads to shorter proofs of metalogical results. The cost of the restrictions is that it becomes more difficult to express naturallanguage statements in the formal system at hand, because the logical connectives used in the natural language statements must be replaced by their (longer) definitions in terms of the restricted collection of logical connectives. Similarly, derivations in the limited systems may be longer than derivations in systems that include additional connectives. There is thus a tradeoff between the ease of working within the formal system and the ease of proving results about the formal system.
It is also possible to restrict the arities of function symbols and predicate symbols, in sufficiently expressive theories. One can in principle dispense entirely with functions of arity greater than 2 and predicates of arity greater than 1 in theories that include a pairing function. This is a function of arity 2 that takes pairs of elements of the domain and returns an ordered pair containing them. It is also sufficient to have two predicate symbols of arity 2 that define projection functions from an ordered pair to its components. In either case it is necessary that the natural axioms for a pairing function and its projections are satisfied.
Manysorted logic
Ordinary firstorder interpretations have a single domain of discourse over which all quantifiers range. Manysorted firstorder logic allows variables to have different sorts, which have different domains. This is also called typed firstorder logic, and the sorts called types (as in data type), but it is not the same as firstorder type theory. Manysorted firstorder logic is often used in the study of secondorder arithmetic.
When there are only finitely many sorts in a theory, manysorted firstorder logic can be reduced to singlesorted firstorder logic. One introduces into the singlesorted theory a unary predicate symbol for each sort in the manysorted theory, and adds an axiom saying that these unary predicates partition the domain of discourse. For example, if there are two sorts, one adds predicate symbols $P\_1(x)$ and $P\_2(x)$ and the axiom
 $\backslash forall\; x\; (\; P\_1(x)\; \backslash lor\; P\_2(x))\; \backslash land\; \backslash lnot\; \backslash exists\; x\; (P\_1(x)\; \backslash land\; P\_2(x))$.
Then the elements satisfying $P\_1$ are thought of as elements of the first sort, and elements satisfying $P\_2$ as elements of the second sort. One can quantify over each sort by using the corresponding predicate symbol to limit the range of quantification. For example, to say there is an element of the first sort satisfying formula φ(x), one writes
 $\backslash exists\; x\; (P\_1(x)\; \backslash land\; \backslash phi(x))$.
Additional quantifiers
Additional quantifiers can be added to firstorder logic.
 Sometimes it is useful to say that "P(x) holds for exactly one x", which can be expressed as $\backslash exists!$x P(x). This notation, called uniqueness quantification, may be taken to abbreviate a formula such as $\backslash exists$x (P(x) $\backslash wedge\backslash forall$y (P(y) $\backslash rightarrow$ (x = y))).
 Firstorder logic with extra quantifiers has new quantifiers Qx,..., with meanings such as "there are many x such that ...". Also see branching quantifiers and the plural quantifiers of George Boolos and others.
 Bounded quantifiers are often used in the study of set theory or arithmetic.
Infinitary logics
Infinitary logic allows infinitely long sentences. For example, one may allow a conjunction or disjunction of infinitely many formulas, or quantification over infinitely many variables. Infinitely long sentences arise in areas of mathematics including topology and model theory.
Infinitary logic generalizes firstorder logic to allow formulas of infinite length. The most common way in which formulas can become infinite is through infinite conjunctions and disjunctions. However, it is also possible to admit generalized signatures in which function and relation symbols are allowed to have infinite arities, or in which quantifiers can bind infinitely many variables. Because an infinite formula cannot be represented by a finite string, it is necessary to choose some other representation of formulas; the usual representation in this context is a tree. Thus formulas are, essentially, identified with their parse trees, rather than with the strings being parsed.
The most commonly studied infinitary logics are denoted L_{αβ}, where α and β are each either cardinal numbers or the symbol ∞. In this notation, ordinary firstorder logic is L_{ωω}.
In the logic L_{∞ω}, arbitrary conjunctions or disjunctions are allowed when building formulas, and there is an unlimited supply of variables. More generally, the logic that permits conjunctions or disjunctions with less than κ constituents is known as L_{κω}. For example, L_{ω1ω} permits countable conjunctions and disjunctions.
The set of free variables in a formula of L_{κω} can have any cardinality strictly less than κ, yet only finitely many of them can be in the scope of any quantifier when a formula appears as a subformula of another.^{[6]} In other infinitary logics, a subformula may be in the scope of infinitely many quantifiers. For example, in L_{κ∞}, a single universal or existential quantifier may bind arbitrarily many variables simultaneously. Similarly, the logic L_{κλ} permits simultaneous quantification over fewer than λ variables, as well as conjunctions and disjunctions of size less than κ.
Nonclassical and modal logics
 Firstorder modal logic allows one to describe other possible worlds as well as this contingently true world which we inhabit. In some versions, the set of possible worlds varies depending on which possible world one inhabits. Modal logic has extra modal operators with meanings which can be characterized informally as, for example "it is necessary that φ" (true in all possible worlds) and "it is possible that φ" (true in some possible world). With standard firstorder logic we have a single domain and each predicate is assigned one extension. With firstorder modal logic we have a domain function that assigns each possible world its own domain, so that each predicate gets an extension only relative to these possible worlds. This allows us to model cases where, for example, Alex is a Philosopher, but might have been a Mathematician, and might not have existed at all. In the first possible world P(a) is true, in the second P(a) is false, and in the third possible world there is no a in the domain at all.
Higherorder logics
The characteristic feature of firstorder logic is that individuals can be quantified, but not predicates. Thus
 $\backslash exists\; a\; (\; \backslash text\{Phil\}(a))$
is a legal firstorder formula, but
 $\backslash exists\; \backslash text\{Phil\}\; (\; \backslash text\{Phil\}(a))$
is not, in most formalizations of firstorder logic. Secondorder logic extends firstorder logic by adding the latter type of quantification. Other higherorder logics allow quantification over even higher types than secondorder logic permits. These higher types include relations between relations, functions from relations to relations between relations, and other highertype objects. Thus the "first" in firstorder logic describes the type of objects that can be quantified.
Unlike firstorder logic, for which only one semantics is studied, there are several possible semantics for secondorder logic. The most commonly employed semantics for secondorder and higherorder logic is known as full semantics. The combination of additional quantifiers and the full semantics for these quantifiers makes higherorder logic stronger than firstorder logic. In particular, the (semantic) logical consequence relation for secondorder and higherorder logic is not semidecidable; there is no effective deduction system for secondorder logic that is sound and complete under full semantics.
Secondorder logic with full semantics is more expressive than firstorder logic. For example, it is possible to create axiom systems in secondorder logic that uniquely characterize the natural numbers and the real line. The cost of this expressiveness is that secondorder and higherorder logics have fewer attractive metalogical properties than firstorder logic. For example, the Löwenheim–Skolem theorem and compactness theorem of firstorder logic become false when generalized to higherorder logics with full semantics.
Automated theorem proving and formal methods
Automated theorem proving refers to the development of computer programs that search and find derivations (formal proofs) of mathematical theorems. Finding derivations is a difficult task because the search space can be very large; an exhaustive search of every possible derivation is theoretically possible but computationally infeasible for many systems of interest in mathematics. Thus complicated heuristic functions are developed to attempt to find a derivation in less time than a blind search.
The related area of automated proof verification uses computer programs to check that humancreated proofs are correct. Unlike complicated automated theorem provers, verification systems may be small enough that their correctness can be checked both by hand and through automated software verification. This validation of the proof verifier is needed to give confidence that any derivation labeled as "correct" is actually correct.
Some proof verifiers, such as Metamath, insist on having a complete derivation as input. Others, such as Mizar and Isabelle, take a wellformatted proof sketch (which may still be very long and detailed) and fill in the missing pieces by doing simple proof searches or applying known decision procedures: the resulting derivation is then verified by a small, core "kernel". Many such systems are primarily intended for interactive use by human mathematicians: these are known as proof assistants. They may also use formal logics that are stronger than firstorder logic, such as type theory. Because a full derivation of any nontrivial result in a firstorder deductive system will be extremely long for a human to write,^{[7]} results are often formalized as a series of lemmas, for which derivations can be constructed separately.
Automated theorem provers are also used to implement formal verification in computer science. In this setting, theorem provers are used to verify the correctness of programs and of hardware such as processors with respect to a formal specification. Because such analysis is timeconsuming and thus expensive, it is usually reserved for projects in which a malfunction would have grave human or financial consequences.
See also
Notes
References
 Andrews, Peter B. (2002); An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed., Berlin: Kluwer Academic Publishers. Available from Springer.
 Avigad, Jeremy; Donnelly, Kevin; Gray, David; and Raff, Paul (2007); "A formally verified proof of the prime number theorem", ACM Transactions on Computational Logic, vol. 9 no. 1 10.1145/1297658.1297660
 Barwise, Jon (1977); "An Introduction to FirstOrder Logic", in
 Barwise, Jon; and Etchemendy, John (2000); Language Proof and Logic, Stanford, CA: CSLI Publications (Distributed by the University of Chicago Press)
 Bocheński, Józef Maria (2007); A Précis of Mathematical Logic, Dordrecht, NL: D. Reidel, translated from the French and German editions by Otto Bird
 Ferreirós, José (2001); JStor
 Gamut, L. T. F. (1991); Logic, Language, and Meaning, Volume 2: Intensional Logic and Logical Grammar, Chicago, IL: University of Chicago Press, ISBN 0226280888
 Hilbert, David; and Ackermann, Wilhelm (1950); Principles of Mathematical Logic, Chelsea (English translation of Grundzüge der theoretischen Logik, 1928 German first edition)
 Hodges, Wilfrid (2001); "Classical Logic I: First Order Logic", in Goble, Lou (ed.); The Blackwell Guide to Philosophical Logic, Blackwell
 Ebbinghaus, HeinzDieter; Flum, Jörg; and Thomas, Wolfgang (1994); Mathematical Logic, Undergraduate Texts in Mathematics, Berlin, DE/New York, NY: SpringerVerlag, Second Edition, ISBN 9780387942582

 Tarski, Alfred and Givant, Steven (1987); A Formalization of Set Theory without Variables. Providence RI: American Mathematical Society.
External links
 Template:Springer
 Classical Logic". Covers syntax, model theory, and metatheory for firstorder logic in the natural deduction style.
 Magnus, P. D.; forall x: an introduction to formal logic. Covers formal semantics and proof theory for firstorder logic.
 Principia Mathematica modernized.
 Podnieks, Karl; Introduction to mathematical logic
 (typeset by John Fremlin). These notes cover part of a past Cambridge Mathematics Tripos course taught to undergraduates students (usually) within their third year. The course is entitled "Logic, Computation and Set Theory" and covers Ordinals and cardinals, Posets and Zorn's Lemma, Propositional logic, Predicate logic, Set theory and Consistency issues related to ZFC and other set theories.


 Overview 

 Academic areas  

 Foundations  


                

This article was sourced from Creative Commons AttributionShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, EGovernment Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a nonprofit organization.