In mathematics, philosophy, linguistics, and computer science, first-order logic (FOL), also called predicate logic, predicate calculus, or quantificational logic, is a type of formal system. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables. Rather than propositions such as "all humans are mortal", in first-order logic one can have expressions in the form "for all x, if x is a human, then x is mortal", where "for all x" is a quantifier, x is a variable, and "... is a human" and "... is mortal" are predicates. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, first-order logic is an extension of propositional logic. A theory about a topic, such as set theory, a theory for groups, or a formal theory of arithmetic, is usually a first-order logic together with a specified domain of discourse (over which the quantified variables range), finitely many functions from that domain to itself, finitely many predicates defined on that domain, and a set of axioms believed to hold about them. "Theory" is sometimes understood in a more formal sense as just a set of sentences in first-order logic. The term "first-order" distinguishes first-order logic from higher-order logic, in which there are predicates having predicates or functions as arguments, or in which quantification over predicates, functions, or both, are permitted. In first-order theories, predicates are often associated with sets. In interpreted higher-order theories, predicates may be interpreted as sets of sets. There are many deductive systems for first-order logic which are both sound, i.e. all provable statements are true in all models; and complete, i.e. all statements which are true in all models are provable. Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first-order logic. First-order 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. First-order logic is the standard for the formalization of mathematics into axioms, and is studied in the foundations of mathematics. Peano arithmetic and Zermelo–Fraenkel set theory are axiomatizations of number theory and set theory, respectively, into first-order logic. No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the natural numbers or the real line. Axiom systems that do fully describe these two structures, i.e. categorical axiom systems, can be obtained in stronger logics such as second-order logic. Historically speaking, the foundations of first-order logic were developed independently by Gottlob Frege and Charles Sanders Peirce in the 1880s. However, the distinction between first-order and higher-order logic was not well understood until metalogical ideas and results arrived, such as Gödel's completeness theorem in 1929. By the 1940s, first-order logic had become the dominant language of mathematical foundations.
Introduction
While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification. A predicate evaluates to true or false for an entity or entities in the domain of discourse. Consider the two sentences "Socrates is a philosopher" and "Plato is a philosopher". In propositional logic, these sentences themselves are viewed as the individuals of study, and might be denoted, for example, by variables such as p and q. They are not viewed as an application of a predicate, such as isPhilosopher {\displaystyle {\text{isPhilosopher}}} , to any particular objects in the domain of discourse, instead viewing them as purely an utterance which is either true or false. However, in first-order logic, these two sentences may be framed as statements that a certain individual or non-logical object has a property. In this example, both sentences happen to have the common form isPhilosopher ( x ) {\displaystyle {\text{isPhilosopher}}(x)} for some individual x {\displaystyle x} , in the first sentence the value of the variable x is "Socrates", and in the second sentence it is "Plato". Due to the ability to speak about non-logical individuals along with the original logical connectives, first-order logic includes propositional logic. The truth of a formula such as "x is a philosopher" depends on which object is denoted by x and on the interpretation of the predicate "is a philosopher". Consequently, "x is a philosopher" alone does not have a definite truth value of true or false, and is akin to a sentence fragment. Relationships between predicates can be stated using logical connectives. For example, the first-order formula "if x is a philosopher, then x is a scholar", is a conditional statement with "x is a philosopher" as its hypothesis, and "x is a scholar" as its conclusion, which again needs specification of x in order to have a definite truth value. Quantifiers can be applied to variables in a formula. The variable x in the previous formula can be universally quantified, for instance, with the first-order sentence "For every x, if x is a philosopher, then x is a scholar". The universal quantifier "for every" in this sentence expresses the idea that the claim "if x is a philosopher, then x is a scholar" holds for all choices of x. The negation of the sentence "For every x, if x is a philosopher, then x is a scholar" is logically equivalent to the sentence "There exists x such that x is a philosopher and x is not a scholar". The existential quantifier "there exists" expresses the idea that the claim "x is a philosopher and x is not a scholar" holds for some choice of x. The predicates "is a philosopher" and "is a scholar" each take a single variable. In general, predicates can take several variables. In the first-order sentence "Socrates is the teacher of Plato", the predicate "is the teacher of" takes two variables. An interpretation (or model) of a first-order formula specifies what each predicate means, and the entities that can instantiate the variables. These entities form the domain of discourse or universe, which is usually required to be a nonempty set. For example, consider the sentence "There exists x such that x is a philosopher." This sentence is seen as being true in an interpretation under which the domain of discourse consists of all human beings, and the predicate "is a philosopher" is understood as "was the author of the Republic." It is thus true in the case of Plato. There are two key parts of first-order logic. The syntax determines which finite sequences of symbols are well-formed expressions in first-order logic, while the semantics determines the meanings behind these expressions.
Syntax
Unlike natural languages, such as English, the language of first-order logic is completely formal, so that it can be mechanically determined whether a given expression is well formed. There are two key types of well-formed expressions: terms, which intuitively represent objects, and formulas, which intuitively express statements that can be true or false. The terms and formulas of first-order logic are strings of symbols, where all the symbols together form the alphabet of the language.
Alphabet
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 non-logical symbols, whose meaning varies by interpretation. For example, the logical symbol ∧ {\displaystyle \land } always represents "and"; it is never interpreted as "or", which is represented by the logical symbol ∨ {\displaystyle \lor } . However, a non-logical 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
Logical symbols are a set of characters that vary by author, but usually include the following:
Quantifier symbols: ∀ for universal quantification, and ∃ for existential quantification Logical connectives: ∧ for conjunction, ∨ for disjunction, → for implication, ↔ for biconditional, ¬ for negation. Some authors use Cpq instead of → and Epq instead of ↔, especially in contexts where → is used for other purposes. Moreover, the horseshoe ⊃ may replace →; the triple-bar ≡ may replace ↔; a tilde (~), Np, or Fp may replace ¬; a double bar ‖ {\displaystyle \|} , + {\displaystyle +} , or Apq may replace ∨; and an ampersand &, Kpq, or the middle dot ⋅ may replace ∧, especially if these symbols are not available for technical reasons. 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: x0, x1, x2, ... . An equality symbol (sometimes, identity symbol) = (see § Equality and its axioms below). Not all of these symbols are required in first-order logic. Either one of the quantifiers along with negation, conjunction (or disjunction), variables, brackets, and equality suffices. Other logical symbols include the following:
Truth constants: T, or ⊤ for "true" and F, or ⊥ for "false". Without any such logical operators of valence 0, these two constants can only be expressed using quantifiers. Additional logical connectives such as the Sheffer stroke, Dpq (NAND), and exclusive or, Jpq.
Non-logical symbols Non-logical symbols represent predicates (relations), functions and constants. It used to be standard practice to use a fixed, infinite set of non-logical symbols for all purposes:
For every integer n ≥ 0, there is a collection of n-ary, or n-place, predicate symbols. Because they represent relations between n elements, they are also called relation symbols. For each arity n, there is an infinite supply of them: For every integer n ≥ 0, there are infinitely many n-ary function symbols: When the arity of a predicate symbol or function symbol is clear from context, the superscript n is often omitted. In this traditional approach, there is only one language of first-order logic. This approach is still common, especially in philosophically oriented books. A more recent practice is to use different non-logical symbols according to the application one has in mind. Therefore, it has become necessary to name the set of all non-logical symbols used in a particular application. This choice is made via a signature. Typical signatures in mathematics are {1, ×} or just {×} for groups, or {0, 1, +, ×, <} for ordered fields. There are no restrictions on the number of non-logical symbols. The signature can be empty, finite, or infinite, even uncountable. Uncountable signatures occur for example in modern proofs of the Löwenheim–Skolem theorem. Though signatures might in some cases imply how non-logical symbols are to be interpreted, interpretation of the non-logical symbols in the signature is separate (and not necessarily fixed). Signatures concern syntax rather than semantics. In this approach, every non-logical 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 are often denoted by uppercase letters such as P, Q and R. Examples: In P(x), P is a predicate symbol of valence 1. One possible interpretation is "x is a man". In Q(x,y), Q is a predicate symbol of valence 2. Possible interpretations include "x is greater than y" and "x is the father of y". Relations of valence 0 can be identified with propositional variables, which can stand for any statement. One possible interpretation of R is "Socrates is a man". A function symbol, with some valence greater than or equal to 0. These are often denoted by lowercase roman letters such as f, g and h. Examples: f(x) may be interpreted as "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 such as a, b and c. The symbol a may stand for Socrates. In arithmetic, it may stand for 0. In set theory, it 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 non-logical 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 context-free (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 symbol is a term. Functions. If f is an n-ary function symbol, and t1, ..., tn are terms, then f(t1,...,tn) is a term. In particular, symbols denoting individual constants are nullary function symbols, and thus are 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 well-formed formulas or WFFs) is inductively defined by the following rules:
Predicate symbols. If P is an n-ary predicate symbol and t1, ..., tn are terms then P(t1,...,tn) is a formula. Equality. If the equality symbol is considered part of logic, and t1 and t2 are terms, then t1 = t2 is a formula. Negation. If φ {\displaystyle \varphi } is a formula, then ¬ φ {\displaystyle \lnot \varphi } is a formula. Binary connectives. If φ {\displaystyle \varphi } and ψ {\displaystyle \psi } are formulas, then ( φ → ψ {\displaystyle \varphi \rightarrow \psi } ) is a formula. Similar rules apply to other binary logical connectives. Quantifiers. If φ {\displaystyle \varphi } is a formula and x is a variable, then ∀ x φ {\displaystyle \forall x\varphi } (for all x, φ {\displaystyle \varphi } holds) and ∃ x φ {\displaystyle \exists x\varphi } (there exists x such that φ {\displaystyle \varphi } ) are formulas. Only expressions which can be obtained by finitely many applications of rules 1–4 are formulas. The formulas obtained from the first rule are said to be atomic formulas. For example:
∀ x ∀ y ( P ( f ( x ) ) → ¬ ( P ( x ) → Q ( f ( y ) , x , z ) ) ) {\displaystyle \forall x\forall y(P(f(x))\rightarrow \neg (P(x)\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. However,
∀ x x → {\displaystyle \forall x\,x\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 (i.e., 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.
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:
¬ {\displaystyle \lnot } is evaluated first
∧ {\displaystyle \land } and ∨ {\displaystyle \lor } are evaluated next Quantifiers are evaluated next
→ {\displaystyle \to } and ↔ {\displaystyle \leftrightarrow } are evaluated last. Moreover, extra punctuation not required by the definition may be inserted—to make formulas easier to read. Thus the formula:
¬ ∀ x P ( x ) → ∃ x ¬ P ( x ) {\displaystyle \lnot \forall xP(x)\to \exists x\lnot P(x)}
might be written as:
( ¬ [ ∀ x P ( x ) ] ) → ∃ x [ ¬ P ( x ) ] . {\displaystyle (\lnot [\forall xP(x)])\to \exists x[\lnot P(x)].}
Free and bound variables
In a formula, a variable may occur free or bound (or both). One formalization of this notion is due to Quine, first the concept of a variable occurrence is defined, then whether a variable occurrence is free or bound, then whether a variable symbol overall is free or bound. In order to distinguish different occurrences of the identical symbol x, each occurrence of a variable symbol x in a formula φ is identified with the initial substring of φ up to the point at which said instance of the symbol x appears.p. 297 Then, an occurrence of x is said to be bound if that occurrence of x lies within the scope of at least one of either ∃ x {\displaystyle \exists x} or ∀ x {\displaystyle \forall x} . Finally, x is bound in φ if all occurrences of x in φ are bound.pp. 142–143 Intuitively, a variable symbol is free in a formula if at no point is it quantified:pp. 142–143 in ∀y P(x, y), the sole occurrence of variable x is free while that of y is bound. The free and bound variable occurrences in a formula are defined inductively as follows.
Atomic formulas If φ is an atomic formula, then x occurs free in φ if and only if x occurs in φ. Moreover, there are no bound variables in any atomic formula. Negation x occurs free in ¬φ if and only if x occurs free in φ. x occurs bound in ¬φ if and only if x occurs bound in φ Binary connectives x occurs free in (φ → ψ) if and only if x occurs free in either φ or ψ. x occurs bound in (φ → ψ) if and only if x occurs bound in either φ or ψ. The same rule applies to any other binary connective in place of →. Quantifiers x occurs free in ∀y φ, if and only if x occurs free in φ and x is a different symbol from y. Also, x occurs bound in ∀y φ, if and only if x is y or x occurs bound in φ. The same rule holds with ∃ in place of ∀. For example, in ∀x ∀y (P(x) → Q(x,f(x),z)), x and y occur only bound, z occurs only free, and w is neither because it does not occur in the formula. Free and bound variables of a formula need not be disjoint sets: in the formula P(x) → ∀x Q(x), the first occurrence of x, as argument of P, is free while the second one, as argument of Q, is bound. A formula in first-order logic with no free variable occurrences is called a first-order sentence. These are the formulas that will have well-defined 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 ∃x Phil(x) will be either true or false in a given interpretation.
Example: ordered 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 ( ∀ x ∀ y [ ≤ ( + ( x , y ) , z ) → ∀ x ∀ y + ( x , y ) = 0 ) ] {\displaystyle (\forall x\forall y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \forall x\,\forall y\,\mathop {+} (x,y)=0)]} is a formula, which is usually written as ∀ x ∀ y ( x + y ≤ z ) → ∀ x ∀ y ( x + y = 0 ) . {\displaystyle \forall x\forall y(x+y\leq z)\to \forall x\forall y(x+y=0).} This formula has one free variable, z. The axioms for ordered abelian groups can be expressed as a set of sentences in the language. For example, the axiom stating that the group is commutative is usually written ( ∀ x ) ( ∀ y ) [ x + y = y + x ] . {\displaystyle (\forall x)(\forall y)[x+y=y+x].}
Semantics An interpretation of a first-order language assigns a denotation to each non-logical symbol (predicate symbol, function symbol, or constant symbol) 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, each predicate is assigned a property of objects, and each sentence is assigned a truth value. In this way, an interpretation provides semantic meaning to the terms, predicates, 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 first-order logic. (It is also possible to define game semantics for first-order logic, but aside from requiring the axiom of choice, game semantics agree with Tarskian semantics for first-order logic, so game semantics will not be elaborated here.)
First-order 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 domain of discourse D and an interpretation function I mapping non-logical symbols to predicates, functions, and constants. The domain of discourse D is a nonempty set of "objects" of some kind. Intuitively, given an interpretation, a first-order formula becomes a statement about these objects; for example, ∃ x P ( x ) {\displaystyle \exists xP(x)} states the existence of some object in D for which the predicate P is true (or, more precisely, for which the predicate assigned to the predicate symbol P by the interpretation is true). For example, one can take D to be the set of integers. Non-logical symbols are interpreted as follows:
The interpretation of an n-ary function symbol is a function from Dn to D. For example, if the domain of discourse is the set 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 ) {\displaystyle I(f)} which, in this interpretation, is addition. The interpretation of a constant symbol (a function symbol of arity 0) is a function from D0 (a set whose only member is the empty tuple) to D, which can be simply identified with an object in D. For example, an interpretation may assign the value I ( c ) = 10 {\displaystyle I(c)=10} to the constant symbol c {\displaystyle c} . The interpretation of an n-ary predicate symbol is a set of n-tuples of elements of D, giving the arguments for which the predicate is true. For example, an interpretation I ( P ) {\displaystyle 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 its second argument. Equivalently, predicate symbols may be assigned Boolean-valued functions from Dn to { t r u e , f a l s e } {\displaystyle \{\mathrm {true,false} \}} .
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 {\displaystyle y=x} . The truth value of this formula changes depending on the values that x and y denote. 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 , … , t n {\displaystyle t_{1},\ldots ,t_{n}} that have been evaluated to elements d 1 , … , d n {\displaystyle d_{1},\ldots ,d_{n}} of the domain of discourse, and a n-ary function symbol f, the term f ( t 1 , … , t n ) {\displaystyle f(t_{1},\ldots ,t_{n})} evaluates to ( I ( f ) ) ( d 1 , … , d n ) {\displaystyle (I(f))(d_{1},\ldots ,d_{n})} . Next, each formula is assigned a truth value. The inductive definition used to make this assignment is called the T-schema.
Atomic formulas (1). A formula P ( t 1 , … , t n ) {\displaystyle P(t_{1},\ldots ,t_{n})} is associated the value true or false depending on whether ⟨ v 1 , … , v n ⟩ ∈ I ( P ) {\displaystyle \langle v_{1},\ldots ,v_{n}\rangle \in I(P)} , where v 1 , … , v n {\displaystyle v_{1},\ldots ,v_{n}} are the evaluation of the terms t 1 , … , t n {\displaystyle t_{1},\ldots ,t_{n}} and I ( P ) {\displaystyle I(P)} is the interpretation of P {\displaystyle P} , which by assumption is a subset of D n {\displaystyle D^{n}} . Atomic formulas (2). A formula t 1 = t 2 {\displaystyle t_{1}=t_{2}} is assigned true if t 1 {\displaystyle t_{1}} and t 2 {\displaystyle 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 ¬ φ {\displaystyle \neg \varphi } , φ → ψ {\displaystyle \varphi \rightarrow \psi } , etc. is evaluated according to the truth table for the connective in question, as in propositional logic. Existential quantifiers. A formula ∃ x φ ( x ) {\displaystyle \exists x\varphi (x)} is true according to M and μ {\displaystyle \mu } if there exists an evaluation μ ′ {\displaystyle \mu '} of the variables that differs from μ {\displaystyle \mu } at most regarding the evaluation of x and such that φ is true according to the interpretation M and the variable assignment μ ′ {\displaystyle \mu '} . This formal definition captures the idea that ∃ x φ ( x ) {\displaystyle \exists x\varphi (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 ∀ x φ ( x ) {\displaystyle \forall x\varphi (x)} is true according to M and μ {\displaystyle \mu } if φ(x) is true for every pair composed by the interpretation M and some variable assignment μ ′ {\displaystyle \mu '} that differs from μ {\displaystyle \mu } at most on the value of x. This captures the idea that ∀ x φ ( x ) {\displaystyle \forall x\varphi (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 thus 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 μ {\displaystyle \mu } if and only if it is true according to M and every other variable assignment μ ′ {\displaystyle \mu '} . 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 cd 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 ∃ x φ ( x ) {\displaystyle \exists x\varphi (x)} is true according to M if there is some d in the domain of discourse such that φ ( c d ) {\displaystyle \varphi (c_{d})} holds. Here φ ( c d ) {\displaystyle \varphi (c_{d})} is the result of substituting cd for every free occurrence of x in φ. Universal quantifiers (alternate). A formula ∀ x φ ( x ) {\displaystyle \forall x\varphi (x)} is true according to M if, for every d in the domain of discourse, φ ( c d ) {\displaystyle \varphi (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 ⊨ φ {\displaystyle M\vDash \varphi } . A sentence is satisfiable if there is some interpretation under which it is true. This is a bit different from the symbol ⊨ {\displaystyle \vDash } from model theory, where M ⊨ ϕ {\displaystyle M\vDash \phi } denotes satisfiability in a model, i.e. "there is a suitable assignment of values in M {\displaystyle M} 's domain to variable symbols of ϕ {\displaystyle \phi } ". 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 x 1 {\displaystyle x_{1}} , ..., x n {\displaystyle x_{n}} 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 x 1 {\displaystyle x_{1}} , ..., x n {\displaystyle x_{n}} . This has the same effect as saying that a formula φ is satisfied if and only if its universal closure ∀ x 1 … ∀ x n ϕ ( x 1 , … , x n ) {\displaystyle \forall x_{1}\dots \forall x_{n}\phi (x_{1},\dots ,x_{n})} 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 first-order logic proceeds via abstract algebra. This approach generalizes the Lindenbaum–Tarski algebras of propositional logic. There are three ways of eliminating quantified variables from first-order logic that do not involve replacing quantifiers with other variable binding term operators:
Cylindric algebra, by Alfred Tarski, et al.; Polyadic algebra, by Paul Halmos; Predicate functor logic, primarily by Willard Quine. These algebras are all lattices that properly extend the two-element Boolean algebra. Tarski and Givant (1987) showed that the fragment of first-order 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 Zermelo–Fraenkel set theory (ZFC). They also prove that first-order logic with a primitive ordered pair is equivalent to a relation algebra with two ordered pair projection functions.
First-order theories, models, and elementary classes A first-order 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 first-order 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öwenh