Editing First-order logic (section)

==Semantics==
An [[Interpretation (logic)|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 (logic)|formal semantics]]. What follows is a description of the standard or [[Truth definition#Tarski.27s Theory|Tarskian]] semantics for first-order logic. (It is also possible to define [[Game semantics#Classical logic|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 herein.)

===First-order structures===
{{Main|Structure (mathematical logic)}}

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 {{mvar|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, <math>\exists x P(x)</math> 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 [[Integer|integers]].

Non-logical symbols are interpreted as follows:

* The interpretation of an ''n''-ary function symbol is a function from ''D''<sup>''n''</sup> 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 {{tmath|I(f)}} which, in this interpretation, is addition.

* The interpretation of a constant symbol (a function symbol of arity 0) is a function from ''D''<sup>0</sup> (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 <math>I(c)=10</math> to the constant symbol <math>c</math>.

* 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 <math>I(P)</math> 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 function]]s from ''D''<sup>''n''</sup> to <math>\{\mathrm{true, false}\}</math>.

===Evaluation of truth values===
{{unsourced section|date=July 2023}}

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 <math>y = x</math>. 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 <math>t_1, \ldots, t_n</math> that have been evaluated to elements <math>d_1, \ldots, d_n</math> of the domain of discourse, and a ''n''-ary function symbol ''f'', the term <math>f(t_1, \ldots, t_n)</math> evaluates to <math>(I(f))(d_1,\ldots,d_n)</math>.

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 <math>P(t_1,\ldots,t_n)</math> is associated the value true or false depending on whether <math>\langle v_1,\ldots,v_n \rangle \in I(P)</math>, where <math>v_1,\ldots,v_n</math> are the evaluation of the terms <math>t_1,\ldots,t_n</math> and <math>I(P)</math> is the interpretation of <math>P</math>, which by assumption is a subset of <math>D^n</math>.
* ''Atomic formulas (2)''. A formula <math>t_1 = t_2</math> is assigned true if <math>t_1</math> and <math>t_2</math> evaluate to the same object of the domain of discourse (see the section on equality below).
* ''Logical connectives''. A formula in the form <math>\neg \varphi</math>, <math>\varphi \rightarrow
\psi</math>, etc. is evaluated according to the [[truth table]] for the connective in question, as in propositional logic.
* ''Existential quantifiers''. A formula <math>\exists x \varphi(x)</math> is true according to ''M'' and <math>\mu</math> if there exists an evaluation <math>\mu'</math> of the variables that differs from <math>\mu</math> at most regarding the evaluation of ''x'' and such that φ is true according to the interpretation ''M'' and the variable assignment <math>\mu'</math>. This formal definition captures the idea that <math>\exists x \varphi(x)</math> 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 <math>\forall x \varphi(x)</math> is true according to ''M'' and <math>\mu</math> if φ(''x'') is true for every pair composed by the interpretation ''M'' and some variable assignment <math>\mu'</math> that differs from <math>\mu</math> at most on the value of ''x''. This captures the idea that <math>\forall x \varphi(x)</math> 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 <math>\mu</math> if and only if it is true according to ''M'' and every other variable assignment <math>\mu'</math>.

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''<sub>''d''</sub> 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 <math>\exists x \varphi(x)</math> is true according to ''M'' if there is some ''d'' in the domain of discourse such that <math>\varphi(c_d)</math> holds. Here <math>\varphi(c_d)</math> is the result of substituting  ''c''<sub>''d''</sub> for every free occurrence of ''x'' in φ.
* ''Universal quantifiers (alternate)''. A formula <math>\forall x \varphi(x)</math> is true according to ''M'' if, for every ''d'' in the domain of discourse, <math>\varphi(c_d)</math> 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===
{{see also|Satisfiability}}
If a sentence φ evaluates to ''true'' under a given interpretation ''M'', one says that ''M'' ''satisfies'' φ; this is denoted<ref>It seems that symbol <math>\vDash</math> was introduced by Kleene, see footnote 30 in Dover's 2002 reprint of his book Mathematical Logic, John Wiley and Sons, 1967.</ref> <math>M \vDash \varphi</math>. A sentence is ''satisfiable'' if there is some interpretation under which it is true. This is a bit different from the symbol <math>\vDash</math> from model theory, where <math>M\vDash\phi</math> denotes satisfiability in a model, i.e. "there is a suitable assignment of values in <math>M</math>'s domain to variable symbols of <math>\phi</math>".<ref>F. R. Drake, ''Set theory: An introduction to large cardinals'' (1974)</ref>

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 <math>x_1</math>, ..., <math>x_n</math> 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 <math>x_1</math>, ..., <math>x_n</math>. This has the same effect as saying that a formula φ is satisfied if and only if its [[universal closure]] <math>\forall x_1 \dots \forall x_n \phi (x_1, \dots, x_n)</math> is satisfied.

A formula is ''logically valid'' (or simply ''valid'') if it is true in every interpretation.<ref>Rogers, R. L., ''Mathematical Logic and Formalized Theories: A Survey of Basic Concepts and Results'' (Amsterdam/London: [[Elsevier#Imprints|North-Holland Publishing Company]], 1971), [https://books.google.com/books?id=fJziBQAAQBAJ&pg=PA39 p. 39].</ref> These formulas play a role similar to [[tautology (logic)|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 algebra]]s 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 Van Orman Quine|Willard Quine]].
These [[algebra]]s are all [[lattice (order)|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]].<ref>[[Chris Brink|Brink, C.]], Kahl, W., & [[Gunther Schmidt|Schmidt, G.]], eds., ''Relational Methods in Computer Science'' ([[Berlin]] / [[Heidelberg]]: [[Springer Science+Business Media|Springer]], 1997), [https://books.google.com/books?id=p0qqCAAAQBAJ&pg=PA32&redir_esc=y#v=onepage&q&f=false pp. 32–33].</ref>{{rp|32–33}} 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 function]]s.<ref>Anon., ''[[Mathematical Reviews]]'' ([[Providence, Rhode Island|Providence]]: [[American Mathematical Society]], 2006), p. 803.</ref>{{rp|803}}

===First-order theories, models, and elementary classes===
A ''first-order theory'' of a particular signature is a set of [[axiom]]s, 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 number]]s with their usual operations. However, the Löwenheim–Skolem theorem shows that most first-order theories will also have other, [[nonstandard model]]s.

A theory is ''[[consistency|consistent]]'' (within a [[First-order logic#Deductive_systems|deductive system]]) if it is not possible to prove a contradiction from the axioms of the theory. A theory is ''[[complete theory|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 first-order theories that include a sufficient portion of the theory of the natural numbers can never be both consistent and complete.

===Empty domains===
{{Main|Empty domain}}
The definition above requires that the domain of discourse of any interpretation must be nonempty. 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 first-order 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 valid only when the domain of discourse is required to be nonempty. One example is the rule stating that <math>\varphi \lor \exists x \psi</math> implies <math>\exists x (\varphi \lor \psi)</math> when ''x'' is not a free variable in <math>\varphi</math>. 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.