diff --git a/src/languages-and-algorithms-for-ai/module2/sections/_first_order_logic.tex b/src/languages-and-algorithms-for-ai/module2/sections/_first_order_logic.tex index d9e171f..51df88c 100644 --- a/src/languages-and-algorithms-for-ai/module2/sections/_first_order_logic.tex +++ b/src/languages-and-algorithms-for-ai/module2/sections/_first_order_logic.tex @@ -17,7 +17,7 @@ The symbols of propositional logic are: \item[Predicate symbols] Function $P^{(n)}$ applied on $n$ constants to obtain a truth value. - \item[Connectives] $\forall$ $\exists$ $\land$ $\vee$ $\rightarrow$ $\lnot$ $\leftrightarrow$ $\bot$ $($ $)$ + \item[Connectives] $\forall$ $\exists$ $\land$ $\vee$ $\rightarrow$ $\lnot$ $\leftrightarrow$ $\top$ $\bot$ $($ $)$ \end{descriptionlist} Using the basic syntax, the following constructs can be defined: @@ -27,7 +27,7 @@ Using the basic syntax, the following constructs can be defined: \item[Proposition] Denotes truth values. \[ - P := \bot \,|\, P \land P \,|\, P \vee P \,|\, P \rightarrow P \,|\, P \leftrightarrow P \,|\, + P := \top \,|\, \bot \,|\, P \land P \,|\, P \vee P \,|\, P \rightarrow P \,|\, P \leftrightarrow P \,|\, \lnot P \,|\, \forall x. P \,|\, \exists x. P \,|\, (P) \,|\, P^{(n)}(t_1, \dots, t_n) \] \end{descriptionlist} @@ -41,4 +41,111 @@ Using the basic syntax, the following constructs can be defined: \item If S is well-formed, $\exists X. S$ is well-formed. Where $X$ is a variable. \item If S is well-formed, $\forall X. S$ is well-formed. Where $X$ is a variable. \end{itemize} + + \item[Free variables] \marginnote{Free variables} + The universal and existential quantifiers bind their variable within the scope of the formula. + Let $F_v(F)$ be the set of free variables in a formula $F$, $F_v$ is defined as follows: + \begin{itemize} + \item $F_v(p(t)) = \bigcup \texttt{vars}(t)$ + \item $F_v(\top) = F_v(\bot) = \varnothing$ + \item $F_v(\lnot F) = F_v(F)$ + \item $F_v(F_1 \land F_2) = F_v(F_1 \vee F_2) = F_v(F_1 \rightarrow F_2) = F_v(F_1) \cup F_v(F_2)$ + \item $F_v(\forall X.F) = F_v(\exists X.F) = F_v(F) \smallsetminus \{ X \}$ + \end{itemize} + + \begin{description} + \item[Closed formula/Sentence] \marginnote{Sentence} + Proposition without free variables. + + \item[Theory] \marginnote{Theory} + Set of sentences. + + \item[Ground term/Formula] \marginnote{Formula} + Proposition without variables. + \end{description} +\end{description} + + + +\section{Semantics} + +\begin{description} + \item[Interpretation] \marginnote{Interpretation} + An interpretation in first order logic $\mathcal{I}$ is a pair $(D, I)$: + \begin{itemize} + \item $D$ is the domain of the terms. + \item $I$ is the interpretation function such that: + \begin{itemize} + \item $I(f): D^n \rightarrow D$ for every n-ary function symbol. + \item $I(p) \subseteq D^n$ for every n-ary predicate symbol. + \end{itemize} + \end{itemize} + + \item[Variable evaluation] \marginnote{Variable evaluation} + Given an interpretation $\mathcal{I} = (D, I)$ and a set of variables $\mathcal{V}$, + a variable is evaluated through $\eta: \mathcal{V} \rightarrow D$. + + \item[Model] \marginnote{Model} + Given an interpretation $\mathcal{I}$ and a formula $F$, + $\mathcal{I}$ models $F$ ($\mathcal{I} \models F$) + when $\mathcal{I}, \eta \models F$ for every variable evaluation $\eta$. + + A sentence $S$ is: + \begin{descriptionlist} + \item[Valid] $S$ is satisfied by every interpretation ($\forall \mathcal{I}: \mathcal{I} \models S$). + \item[Satisfiable] $S$ is satisfied by some interpretations ($\exists \mathcal{I}: \mathcal{I} \models S$). + \item[Falsifiable] $S$ is not satisfied by some interpretations ($\exists \mathcal{I}: \mathcal{I} \cancel{\models} S$). + \item[Unsatisfiable] $S$ is not satisfied by any interpretation ($\forall \mathcal{I}: \mathcal{I} \cancel{\models} S$). + \end{descriptionlist} + + \item[Logical consequence] \marginnote{Logical consequence} + A sentence $T_1$ is a logical consequence of $T_2$ ($T_2 \models T_1$) if + every model of $T_2$ is also model of $T_1$: + \[ \mathcal{I} \models T_2 \rightarrow \mathcal{I} \models T_1 \] + + \begin{theorem} + It is undecidable to determine if a first order logic formula is a tautology. + \end{theorem} + + \item[Equivalence] \marginnote{Equivalence} + A sentence $T_1$ is equivalent to $T_2$ if $T_1 \models T_2$ and $T_2 \models T_1$. +\end{description} + +\begin{theorem} + The following statements are equivalent: + \begin{enumerate} + \item $F_1, \dots, F_n \models G$. + \item $(\bigwedge_{i=1}^{n} F_i) \rightarrow G$ is valid. + \item $(\bigwedge_{i=1}^{n} F_i) \land \lnot G$ is unsatisfiable. + \end{enumerate} +\end{theorem} + + +\section{Substitution} + +\begin{description} + \item[Substitution] \marginnote{Substitution} + A substitution $\sigma: \mathcal{V} \rightarrow \mathcal{T}$ is a mapping from variables to terms. + It is written as $\{ X_1 \mapsto t_1, \dots, X_n \mapsto t_n \}$. + + The application of a substitution is the following: + \begin{itemize} + \item $p(t_1, \dots, t_n)\sigma = p(t_1\sigma, \dots, t_n\sigma)$ + \item $f(t_1, \dots, t_n)\sigma = fp(t_1\sigma, \dots, t_n\sigma)$ + \item $\bot\sigma = \bot$ and $\top\sigma = \top$ + \item $(\lnot F)\sigma = (\lnot F\sigma)$ + \item $(F_1 \star F_2)\sigma = (F_1\sigma \star F_2\sigma)$ for $\star \in \{ \land, \vee, \rightarrow \}$ + \item $(\forall X.F)\sigma = \forall X' (F \sigma[X \mapsto X'])$ where $X'$ is a fresh variable (i.e. does not appear in $F$). + \item $(\exists X.F)\sigma = \exists X' (F \sigma[X \mapsto X'])$ where $X'$ is a fresh variable. + \end{itemize} + + \item[Unifier] \marginnote{Unifier} + A substitution $\sigma$ is a unifier for $e_1, \dots, e_n$ if $e_1\sigma = \dots = e_n\sigma$. + + \begin{description} + \item[Most general unifier] \marginnote{Most general unifier} + A unifier $\sigma$ is the most general unifier (MGU) for $\bar{e} = e_1, \dots, e_n$ if + every unifier $\tau$ for $\bar{e}$ is an instance of $\sigma$ ($\tau$ = $\sigma\rho$ for some substitution $\rho$). + In other words, $\sigma$ is the smallest substitution to unify $\bar{e}$. + \end{description} \end{description} \ No newline at end of file