Add LAAI2 first order logic

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}