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(f) &=& \{ (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)
\] What is the truth value of this formula \[
\exists x.\, \forall y. dvd(x,y)
\]
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?
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} \]