Add LAAI2 propositional logic

src/ainotes.cls

@@ -19,6 +19,7 @@
 \usepackage{acro}
 \usepackage{subcaption}
 \usepackage{eurosym}
+\usepackage{bussproofs} % Deductive tree
 
 \geometry{ margin=3cm, lmargin=1.5cm, rmargin=4.5cm, marginparwidth=3cm }
 \hypersetup{ colorlinks, citecolor=black, filecolor=black, linkcolor=black, urlcolor=black, linktoc=all }

src/languages-and-algorithms-for-ai/module2/ainotes.cls

@@ -0,0 +1 @@
+../../ainotes.cls

src/languages-and-algorithms-for-ai/module2/main.tex

@@ -0,0 +1,11 @@
+\documentclass[11pt]{ainotes}
+
+\title{Languages and Algorithms for\\Artificial Intelligence\\(Module 2)}
+\date{2023 -- 2024}
+
+\begin{document}
+
+    \makenotesfront
+    \include{sections/_propositional_logic.tex}
+
+\end{document}

src/languages-and-algorithms-for-ai/module2/sections/_propositional_logic.tex

@@ -0,0 +1,284 @@
+\chapter{Propositional logic}
+
+\section{Syntax}
+\begin{description}
+    \item[Syntax] \marginnote{Syntax}
+        Rules and symbols to define well formed sentences.
+\end{description}
+
+The symbols of propositional logic are:
+\begin{descriptionlist}
+    \item[Proposition symbols] $p_0$, $p_1$, \dots
+    \item[Connectives] $\land$, $\vee$, $\rightarrow$, $\lnot$, $\leftrightarrow$, $\bot$
+    \item[Auxiliary symbols] $($ and $)$
+\end{descriptionlist}
+
+\begin{description}
+    \item[Well-formed formula] \marginnote{Well-formed formula}
+        The definition of a well-formed formula is recursive:
+        \begin{itemize}
+            \item An atomic proposition is a well-formed formula.
+            \item If $S$ is well-formed, $\lnot S$ is well-formed.
+            \item If $S_1$ and $S_2$ are well-formed, $S_1 \land S_2$ is well-formed.
+            \item If $S_1$ and $S_2$ are well-formed, $S_1 \vee S_2$ is well-formed.
+        \end{itemize}
+
+        Note that the implication $S_1 \rightarrow S_2$ can be written as $\lnot S_1 \vee S_2$.
+\end{description}
+
+\subsection{Propositional logic BNF}
+\[ 
+    \begin{split}
+        \texttt{<formula>} :=\,\, &\texttt{atomic\_proposition} \,|\,\\
+            &\lnot \texttt{<formula>} \,|\, \\
+            &\texttt{<formula>} \land \texttt{<formula>} \,|\, \\
+            &\texttt{<formula>} \vee \texttt{<formula>} \,|\, \\
+            &\texttt{<formula>} \rightarrow \texttt{<formula>} \,|\, \\
+            &\texttt{<formula>} \leftrightarrow \texttt{<formula>} \,|\, \\
+            &(\texttt{<formula>}) \\
+    \end{split}
+\]
+
+
+
+\section{Semantics}
+
+\begin{description}
+    \item[Semantics] \marginnote{Semantics}
+        Rules to associate a meaning to well formed sentences.
+        \begin{descriptionlist}
+            \item[Model theory] What is true.
+            \item[Proof theory] What is provable.
+        \end{descriptionlist}
+\end{description}
+
+\begin{description}
+    \item[Interpretation] \marginnote{Interpretation}
+        Given a propositional formula $F$ of $n$ atoms $ \{ A_1, \dots, A_n \}$,
+        an interpretation $I$ of $F$ is an assignment of truth values to $\{ A_1, \dots, A_n \}$.
+
+        Note: given a formula $F$ of $n$ distinct atoms, there are $2^n$ district interpretations.
+
+        \begin{description}
+            \item[Model] \marginnote{Model}
+                If $F$ is true under the interpretation $I$, 
+                we say that $I$ is a model of $F$ ($I \models F$).
+        \end{description}
+
+
+    \item[Truth table] \marginnote{Truth table}
+        Useful to define the semantics of connectives.
+        \begin{itemize}
+            \item $\lnot S$ is true iff $S$ is false.
+            \item $S_1 \land S_2$ is true iff $S_1$ is true and $S_2$ is true.
+            \item $S_1 \vee S_2$ is true iff $S_1$ is true or $S_2$ is true.
+            \item $S_1 \rightarrow S_2$ is true iff $S_1$ is false or $S_2$ is true.
+            \item $S_1 \leftrightarrow S_2$ is true iff $S_1 \rightarrow S_2$ is true and $S_1 \leftarrow S_2$ is true.
+        \end{itemize}
+
+
+    \item[Evaluation] \marginnote{Evaluation order}
+        The connectives of a propositional formula are evaluated in the order:
+        \[ \leftrightarrow, \rightarrow, \vee, \land, \lnot \]
+        Formulas in parenthesis have higher priority.
+
+    \item[Valid formula] \marginnote{Valid formula}
+        A formula $F$ is valid (tautology) iff it is true in all the possible interpretations.
+        It is denoted as $\models F$.
+
+    \item[Invalid formula] \marginnote{Invalid formula}
+        A formula $F$ is invalid iff it is not valid {\tiny(\texttt{:o})}.
+        
+        In other words, there is at least an interpretation where $F$ is false.
+
+    \item[Inconsistent formula] \marginnote{Inconsistent formula}
+        A formula $F$ is inconsistent (unsatisfiable) iff it is false in all the possible interpretations.
+    
+    \item[Consistent formula] \marginnote{Consistent formula}
+        A formula $F$ is consistent (satisfiable) iff it is not inconsistent.
+
+        In other words, there is at least an interpretation where $F$ is true.
+    
+    \item[Decidability] \marginnote{Decidability}
+         A propositional formula is decidable if there is a terminating method to decide if it is valid.
+
+    \item[Logical consequence] \marginnote{Logical consequence} 
+         Let $\Gamma = \{F_1, \dots, F_n\}$ be a set of formulas and $G$ a formula.
+         $G$ is a logical consequence of $\Gamma$ ($\Gamma \models G$)
+         if in all the possible interpretations $I$, 
+         if $F_1 \land \dots \land F_n$ is true, $G$ is true.
+
+    \item[Logical equivalence] \marginnote{Logical equivalence}
+        Two formulas $F$ and $G$ are logically equivalent ($F \equiv G$) iff the truth values of $F$ and $G$
+        are the same under the same interpretation.
+        In other words, $F \models G$ and $G \models F$.
+
+        Common equivalences are:
+        \begin{descriptionlist}
+            \item[Commutativity]: $(P \land Q) \equiv (Q \land P)$ and $(P \vee Q) \equiv (Q \vee P)$
+            \item[Associativity]: $((P \land Q) \land R) \equiv (P \land (Q \land R))$
+                and $((P \vee Q) \vee R) \equiv (P \vee (Q \vee R))$
+            \item[Double negation elimination]: $\lnot(\lnot P) \equiv P$
+            \item[Contraposition]: $(P \rightarrow Q) \equiv (\lnot Q \rightarrow \lnot P)$
+            \item[Implication elimination]: $(P \rightarrow Q) \equiv (\lnot P \vee Q)$
+            \item[Biconditional elimination]: $(P \leftrightarrow Q) \equiv ((P \rightarrow Q) \land (Q \rightarrow P))$
+            \item[De Morgan]: $\lnot(P \land Q) \equiv (\lnot P \vee \lnot Q)$ and $\lnot(P \vee Q) \equiv (\lnot P \land \lnot Q)$
+            \item[Distributivity of $\land$ over $\vee$]: $(P \land (Q \vee R)) \equiv ((P \land Q) \vee (P \land R))$
+            \item[Distributivity of $\vee$ over $\land$]: $(P \vee (Q \land R)) \equiv ((P \vee Q) \land (P \vee R))$
+        \end{descriptionlist}
+\end{description}
+
+\begin{theorem}[Deduction] \marginnote{Deduction theorem}
+    Given a set of formulas $\{ F_1, \dots, F_n \}$ and a formula $G$:
+    \[ (F_1 \land \dots \land F_n) \models G \,\iff\, \models (F_1 \land \dots \land F_n) \rightarrow G \]
+
+    \begin{proof} \phantom{}
+        \begin{description}
+            \item[$\rightarrow$])
+                By hypothesis $(F_1 \land \dots \land F_n) \models G$.
+
+                So, for each interpretation $I$ in which $(F_1 \land \dots \land F_n)$ is true, $G$ is also true.
+                Therefore, $I \models (F_1 \land \dots \land F_n) \rightarrow G$.
+
+                Moreover, for each interpretation $I'$ in which $(F_1 \land \dots \land F_n)$ is false,
+                $(F_1 \land \dots \land F_n) \rightarrow G$ is true.
+                Therefore, $I' \models (F_1 \land \dots \land F_n) \rightarrow G$.
+
+                In conclusion, $\models (F_1 \land \dots \land F_n) \rightarrow G$.
+
+            \item[$\leftarrow$]) 
+                By hypothesis $\models (F_1 \land \dots \land F_n) \rightarrow G$.
+                Therefore, for each interpretation where $(F_1 \land \dots \land F_n)$ is true,
+                $G$ is also true.
+
+                In conclusion, $(F_1 \land \dots \land F_n) \models G$.
+        \end{description}
+    \end{proof}
+\end{theorem}
+
+\begin{theorem}[Refutation] \marginnote{Refutation theorem}
+    Given a set of formulas $\{ F_1, \dots, F_n \}$ and a formula $G$:
+    \[ (F_1 \land \dots \land F_n) \models G \,\iff\, F_1 \land \dots \land F_n \land \lnot G \text{ is inconsistent} \]
+
+    Note: this theorem is not accepted in intuitionistic logic.
+
+    \begin{proof}
+        By definition, $(F_1 \land \dots \land F_n) \models G$ iff for every interpretation where 
+        $(F_1 \land \dots \land F_n)$ is true, $G$ is also true.
+        This requires that there are no interpretations where $(F_1 \land \dots \land F_n)$ is true and $G$ false.
+        In other words, it requires that $(F_1 \land \dots \land F_n \land \lnot G)$ is inconsistent.
+    \end{proof}
+\end{theorem}
+
+
+\subsection{Normal forms}
+\begin{description}
+    \item[Negation normal form (NNF)] \marginnote{Negation normal form}
+        A formula is in negation normal form iff negations appears only in front of atoms (i.e. not parenthesis).
+        
+    \item[Conjunctive normal form (CNF)] \marginnote{Conjunctive normal form}
+        A formula $F$ is in conjunctive normal form iff 
+        \begin{itemize}
+            \item it is in negation normal form;
+            \item it has the form $F := F_1 \land F_2 \dots \land F_n$, where each $F_i$ (clause) is a disjunction of literals.
+        \end{itemize}
+
+        \begin{example} \phantom{}\\
+            $(\lnot P \vee Q) \land (\lnot P \vee R)$ is in CNF.\\
+            $\lnot(P \vee Q) \land (\lnot P \vee R)$ is not in CNF (not in NNF).
+        \end{example}
+
+    \item[Disjunctive normal form (DNF)] \marginnote{Disjunctive normal form}
+        A formula $F$ is in disjunctive normal form iff 
+        \begin{itemize}
+            \item it is in negation normal form;
+            \item it has the form $F := F_1 \vee F_2 \dots \vee F_n$, where each $F_i$ is a conjunction of literals.
+        \end{itemize}
+\end{description}
+
+\section{Natural deduction}
+
+\begin{description}
+    \item[Proof theory] \marginnote{Proof theory}
+        Set of rules that allows to derive conclusions from premises by exploiting syntactic manipulations.
+
+    \item[Natural deduction] \marginnote{Natural deduction for propositional logic}
+        Set of rules to introduce or eliminate connectives.
+        We consider a subset $\{ \land, \rightarrow, \bot \}$ of functionally complete connectives.
+
+        Natural deduction can be represented using a tree like structure:
+        \begin{prooftree}
+            \AxiomC{[hypothesis]}
+            \noLine
+            \UnaryInfC{\vdots}
+            \noLine
+            \UnaryInfC{premise}
+            \RightLabel{rule name}\UnaryInfC{conclusion}
+        \end{prooftree}
+
+        The conclusion is true when the hypothesis are able to prove the premise.
+        Another tree can be built on top of premises to prove them.
+
+        \begin{descriptionlist}
+            \item[Introduction] \marginnote{Introduction rules}
+                Usually used to prove the conclusion by splitting it.\\
+                \begin{minipage}{.4\linewidth}
+                    \begin{prooftree}
+                        \AxiomC{$\psi$}
+                        \AxiomC{$\varphi$}
+                        \RightLabel{$\land$I}\BinaryInfC{$\varphi \land \psi$}
+                    \end{prooftree}
+                \end{minipage}
+                \begin{minipage}{.4\linewidth}
+                    \begin{prooftree}
+                        \AxiomC{[$\varphi$]}
+                        \noLine
+                        \UnaryInfC{\vdots}
+                        \noLine
+                        \UnaryInfC{$\psi$}
+                        \RightLabel{$\rightarrow$I}\UnaryInfC{$\varphi \rightarrow \psi$}
+                    \end{prooftree}
+                \end{minipage}
+            
+            \item[Elimination] \marginnote{Elimination rules}
+                Usually used to exploit hypothesis and derive a conclusion.\\
+                \begin{minipage}{.25\linewidth}
+                    \begin{prooftree}
+                        \AxiomC{$\varphi \land \psi$}
+                        \RightLabel{$\land$E}\UnaryInfC{$\varphi$}
+                    \end{prooftree}
+                \end{minipage}
+                \begin{minipage}{.25\linewidth}
+                    \begin{prooftree}
+                        \AxiomC{$\varphi \land \psi$}
+                        \RightLabel{$\land$E}\UnaryInfC{$\psi$}
+                    \end{prooftree}
+                \end{minipage}
+                \begin{minipage}{.3\linewidth}
+                    \begin{prooftree}
+                        \AxiomC{$\varphi$}
+                        \AxiomC{$\varphi \rightarrow \psi$}
+                        \RightLabel{$\rightarrow$E}\BinaryInfC{$\psi$}
+                    \end{prooftree}
+                \end{minipage}
+
+            \item[Ex falso sequitur quodlibet] \marginnote{Ex falso sequitur quodlibet}
+                From contradiction, anything follows.
+                This can be used when we have two contradicting hypothesis.
+                \begin{prooftree}
+                    \AxiomC{$\bot$}
+                    \RightLabel{$\bot$}\UnaryInfC{$\varphi$}
+                \end{prooftree}
+
+            \item[Reductio ad absurdum] \marginnote{Reductio ad absurdum}
+                Assume the opposite and prove a contradiction (not accepted in intuitionistic logic).
+                \begin{prooftree}
+                    \AxiomC{[$\lnot \varphi$]}
+                    \noLine
+                    \UnaryInfC{\vdots}
+                    \noLine
+                    \UnaryInfC{$\bot$}
+                    \RightLabel{RAA}\UnaryInfC{$\varphi$}
+                \end{prooftree}
+        \end{descriptionlist}
+\end{description}