Lab for Automated Reasoning and Analysis LARA

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 ${\cal L}$ is the pair $I = (D,\alpha)$ where $D$ is a nonempty set, called the domain of interpretation, and $\alpha$ is the interpretation function, which assigns

  • to each first-order variable $x \in V$, an element $\alpha(x) \in D$
  • to each relation symbol $R \in {\cal L}$ with arity $ar(R)=n$, a relation $\alpha(R) \subseteq D^n$
  • to each function symbol $f \in {\cal L}$ with arity $ar(f)=n$, a function $\alpha(f) : D^n \to D$

If $I=(D,\alpha)$ we denote $D$ by $D_I$ and $\alpha$ by $\alpha_I$.

Because terms denote values from domain $D_I$ and formulas denote truth values from ${\cal B} = \{{\it false}, {\it true}\}$, we define two semantic evaluation functions:

  • $e_F : {\cal F} \to I \to {\cal B}$
  • $e_T : {\cal T} \to I \to D_I$

We evaluate terms by recursion on the structure of $T$:

\begin{equation*}
\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} 
\end{equation*}

We evaluate formulas by recursion on the structure of $F$:

\begin{equation*}
\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} 
\end{equation*}

How do we evaluate quantifiers?

We generalize this notion as follows: if $I$ is an interpretation and $T$ is a set of first-order formulas, we write $e_S(T)(I)={\it true}$ iff for every $F \in T$ we have $e_F(F)(I)={\it true}$ (set is treated as infinite conjunction). This is a generalization because $e_S(\{F\})(I) = e_F(F)(I)$.

A terminological note: in algebra, an interpretation is often called a structure. Instead of using $\alpha$ mapping language ${\cal L} = \{ f_1,\ldots,f_n, R_1,\ldots,R_m\}$ to interpretation of its symbols, the structure is denoted by a tuple $(D,\alpha(f_1),\ldots,\alpha(f_n),\alpha(R_1),\ldots,\alpha(R_n))$. For example, an interpretation with domain ${\can N}$, with one binary operation whose interpretation is $+$ and one binary relation whose interpretation is $\leq$ can be written as $({\cal N},+,\leq)$. This way we avoid writing $\alpha$ all the time, but it becomes more cumbersome to describe correspondence between structures.

Examples

Example with Finite Domain

Consider language ${\cal L} = \{ s, {<} \}$ where $s$ is a unary function symbol ($ar(s)=1$) and ${<}$ is a binary relation symbol ($ar({<})=2$). Let $I = (D,\alpha)$ be given by

\begin{equation*}\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}
\end{equation*}

Let us evaluate the truth value of these formulas:

  • $x < s(x)$

answer

  • $\exists x. \lnot (x < s(x))$

answer

  • $\forall x. \exists y. x < y$

answer

Example with Infinite Domain

Consider language ${\cal L} = \{ s, dvd \}$ where $s$ is a unary function symbol ($ar(s)=1$) and $dvd$ is a binary relation symbol ($ar(dvd)=2$). Let $I = (D,\alpha)$ where $D = \{7, 8, 9, 10, \ldots\}$. Let $dvd$ be defined as the “strictly divides” relation:

\begin{equation*}
   \alpha(dvd) = \{ (i,j).\  \exists k \in \{2,3,4,\ldots\}.\ j = k \cdot i \}
\end{equation*}

What is the truth value of this formula

\begin{equation*}
    \forall x.\, \exists y.\, dvd(x,y)
\end{equation*}

answer

What is the truth value of this formula

\begin{equation*}
    \exists x.\, \forall y. dvd(x,y)
\end{equation*}

answer

Domain Non-Emptiness

Let $I=(D,\alpha)$ be an arbitrary interpretation. Consider formula

\begin{equation*}
    (\forall x. P(x)) \rightarrow (\exists y. P(y))
\end{equation*}

What is its truth value in $I$? Which condition on definition of $I$ did we use?

This formula is true with the assumption that $D$ 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 $T$ is a set of formulas, a model of $T$ is an interpretation such that $e_S(T)$. A set $T$ of first-order formulas is satisfiable if there exists a model for $T$. A set $T$ is unsatisfiable (contradictory) iff it is not satisfiable (it has no model).

Note: taking $T = \{F\}$ we obtain notion of satisfiability for formulas.

Definition (semantic consequence): We say that a set of formulas $T_2$ is a semantic consequence of a set of formulas $T_1$ and write $T_1 \models T_2$, iff every model of $T_1$ is also a model of $T_2$.

Definition: Formula is valid, denoted $\models F$ iff $\emptyset \models F$.

Lemma: $\models F$ iff for every interpretation $I$ we have $e_F(F)(I)$.

Lemma: A set $T$ of formulas is unsatisfiable iff $T \models {\it false}$.

Lemma: Let $T$ be a set of formulas and $G$ a formula. Then $T \models \{G\}$ iff the set $T \cup \{\lnot G\}$ is contradictory.

Proof:

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 $T$:

\begin{equation*}
   Conseq(T) = \{ F \mid T \models F \}
\end{equation*}

Note $T \models F$ is equivalent to $F \in Conseq(T)$.

Lemma: The following properties hold:

\begin{equation*}
\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}
\end{equation*}

 
sav08/first-order_logic_semantics.txt · Last modified: 2015/04/21 17:30 (external edit)