This is an old revision of the document!
First-Order Logic Semantics
(Recall First-Order Logic Syntax and Propositional Logic Semantics as well as Predicate Logic Informally.)
An interpretation for first-order logic language is the pair where is a nonempty set, called the domain of interpretation, and is the interpretation function, which assigns
- to each first-order variable , an element
- to each relation symbol with arity , a relation
- to each function symbol with arity , a function
If we denote by and by .
Because terms denote values from domain and formulas denote truth values from , we define two semantic evaluation functions:
We evaluate terms by recursion on the structure of : \[ \begin{array}{rcl}
e_T(x)(I) & = & \alpha_I(x) \\ e_T(f(t_1,\ldots,t_n))(I) &=& \alpha_I(f)(e_T(t_1)(I),\ldots,e_T(t_2)(I))
\end{array} \] We evaluate formulas by recursion on the structure of : \[ \begin{array}{rcl}
e_F(R(t_1,\ldots,t_n)(I) &=& (e_T(t_1)(I),\, \ldots,\, e_T(t_n)(I)) \, \in \, \alpha_I(R) \\ e_F(t_1 = t_2)(I) &=& (e_T(t_1)(I) = e_T(t_2)(I)) \\ e_F(F_1 \land F_2)(I) &=& e_F(F_1)(I) \land e_F(F_2)(I) \\ e_F(F_1 \lor F_2)(I) &=& e_F(F_1)(I) \lor e_F(F_2)(I) \\ e_F(\lnot F)(I) &=& \lnot e_F(F)(I) \\
\end{array} \]
How do we evaluate quantifiers?
We generalize this notion as follows: if is an interpretation and is a set of first-order formulas, we write iff for every we have (set is treated as infinite conjunction). This is a generalization because .
Examples
Example with Finite Domain
Consider language where is a unary function symbol () and is a binary relation symbol (). Let be given by \[\begin{array}{rcl}
D &=& \{ 0,1, 2 \} \\ \alpha(x) &=& 1 \\ \alpha(s) &=& \{ (0,1), (1,2), (2,0) \} \\ \alpha({<}) &=& \{ (0,1), (0,2), (1,2) \}
\end{array} \]
Let us evaluate the truth value of these formulas:
Example with Infinite Domain
Consider language where is a unary function symbol () and is a binary relation symbol (). Let where . Let be defined as the “strictly divides” relation: \[
\alpha(dvd) = \{ (i,j).\ \exists k \in \{2,3,4,\ldots\}.\ j = k \cdot i \}
\] What is the truth value of this formula \[
\forall x.\, \exists y.\, dvd(x,y)
\] answer
What is the truth value of this formula \[
\exists x.\, \forall y. dvd(x,y)
\] answer
Domain Non-Emptiness
Let be an arbitrary interpretation. Consider formula \[
(\forall x. P(x)) \rightarrow (\exists y. P(y))
\] What is its truth value in ? Which condition on definition of did we use?
This formula is true with the assumption that is not empty.
With an empty domain, this formula would be false. There are other problems, for instance “how to evaluate a variable?”.
Satisfiability, Validity, and Semantic Consequence
Definition (satisfiability of set): If is a set of formulas, a model of is an interpretation such that . A set of first-order formulas is satisfiable if there exists a model for . A set is unsatisfiable (contradictory) iff it is not satisfiable (it has no model).
Note: taking we obtain notion of satisfiability for formulas.
Definition (semantic consequence): We say that a set of formulas is a semantic consequence of a set of formulas and write , iff every model of is also a model of .
Definition: Formula is valid, denoted iff .
Lemma: iff for every interpretation we have .
Lemma: A set of formulas is unsatisfiable iff .
Lemma: Let be a set of formulas and a formula. Then iff the set is contradictory.
One of the central questions is the study of whether a set of formulas is contradictory, many basic questions reduce to this problem.
Consequence Set
Definition: The set of all consequences of : \[
Conseq(T) = \{ F \mid T \models F \}
\]
Note is equivalent to .
Lemma: The following properties hold: \[ \begin{array}{rcl}
T &\subseteq & Conseq(T) \\ T_1 \subseteq T_2 &\rightarrow& Conseq(T_1) \subseteq Conseq(T_2) \\ Conseq(Conseq(T)) &=& Conseq(T) \\ T_1 \subseteq Conseq(T_2) \land T_2 \subseteq Conseq(T_1) & \rightarrow & Conseq(T_1) = Conseq(T_2)
\end{array} \]