notxia/unibo-ai-notes
1
0
Fork 0
mirror of https://github.com/NotXia/unibo-ai-notes.git synced 2025-12-15 02:52:22 +01:00
Code Issues Packages Projects Releases Wiki Activity

Add LAAI2 propositional logic

Browse Source
This commit is contained in:
Tian Cheng (Riccardo) Xia
2023-11-09 21:03:15 +01:00
parent 6df916b1bf
commit fdf7065237
4 changed files with 297 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
src/ainotes.cls
View File

@ -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 }

1
src/languages-and-algorithms-for-ai/module2/ainotes.cls Symbolic link
View File

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

11
src/languages-and-algorithms-for-ai/module2/main.tex Normal file
View File

@ -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}

284
src/languages-and-algorithms-for-ai/module2/sections/_propositional_logic.tex Normal file
View File

@ -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}