\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$ $\Leftrightarrow$ $\lnot$ $\bot$ $($ $)$
\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$.

        The BNF definition of a formula is:
        \[
            F := \texttt{atomic\_proposition} \,|\, F \land F \,|\, F \vee F \,|\,  
                F \Rightarrow F \,|\, F \Leftrightarrow F \,|\, \lnot F \,|\, (F) 
        \]
        % \[ 
        %     \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}
        % \]
\end{description}


\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 $\mathcal{I}$ of $F$ is is a pair $(D, I)$ where:
        \begin{itemize}
            \item $D$ is the domain. Truth values in the case of propositional logic.
            \item $I$ is the interpretation mapping that assigns
                to the atoms $\{ A_1, \dots, A_n \}$ an element of $D$.
        \end{itemize}

        Note: given a formula $F$ of $n$ distinct atoms, there are $2^n$ distinct interpretations.

        \begin{description}
            \item[Model] \marginnote{Model}
                If $F$ is true under the interpretation $\mathcal{I}$, 
                we say that $\mathcal{I}$ is a model of $F$ ($\mathcal{I} \models F$).
        \end{description}

    \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 logic is decidable if there is a terminating method to decide if a formula is valid.

        Propositional logic is decidable.

    \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 following order:
        \[ \Leftrightarrow, \Rightarrow, \vee, \land, \lnot \]
        Formulas in parenthesis have higher priority.

   \item[Logical consequence] \marginnote{Logical consequence} 
        Let $\Gamma = \{F_1, \dots, F_n\}$ be a set of formulas (premises) and $G$ a formula (conclusion).
        $G$ is a logical consequence of $\Gamma$ ($\Gamma \models G$)
        if in all the possible interpretations $\mathcal{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 \equiv G \iff F \models G \land G \models F$.

       Common equivalences are:
       \begin{descriptionlist}
            \footnotesize
            \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}


\subsection{Normal forms}

\begin{description}
    \item[Negation normal form (NNF)] \marginnote{Negation normal form}
        A formula is in negation normal form iff negations appear 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{Reasoning}

\begin{description}
    \item[Reasoning method] \marginnote{Reasoning method}
        Systems to work with symbols.
        
        Given a set of formulas $\Gamma$, a formula $F$ and a reasoning method $E$,
        we denote with $\Gamma \vdash^E F$ the fact that $F$ can be deduced from $\Gamma$
        using the reasoning method $E$.

        \begin{description}
            \item[Sound] \marginnote{Soundness}
                A reasoning method $E$ is sound iff:
                \[ (\Gamma \vdash^E F) \Rightarrow (\Gamma \models F) \]

            \item[Complete] \marginnote{Completeness}
                A reasoning method $E$ is complete iff:
                \[ (\Gamma \models F) \Rightarrow (\Gamma \vdash^E F) \]
        \end{description}

    \item[Deduction theorem] \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 $\mathcal{I}$ in which $(F_1 \land \dots \land F_n)$ is true, 
                    $G$ is also true.
                    Therefore, $\mathcal{I} \models (F_1 \land \dots \land F_n) \Rightarrow G$.
        
                    Moreover, for each interpretation $\mathcal{I}'$ in which $(F_1 \land \dots \land F_n)$ is false,
                    $(F_1 \land \dots \land F_n) \Rightarrow G$ is true.
                    Therefore, $\mathcal{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}

    \item[Refutation theorem] \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{description}




\subsection{Natural deduction}
\begin{description}
    \item[Proof theory] \marginnote{Proof theory}
        Set of rules that allows to derive conclusions from premises by exploiting syntactic manipulations.
\end{description}

\begin{description}
    \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 hypotheses can prove the premise.
        Another tree can be built on top of the premises to prove them.

        \begin{descriptionlist}
            \item[Introduction] \marginnote{Introduction rules}
                Usually used to prove the conclusion by splitting it.
                
                Note that $\lnot \psi \equiv (\psi \Rightarrow \bot)$. \\
                \begin{minipage}{.4\linewidth}
                    \begin{prooftree}
                        \AxiomC{$\psi$}
                        \AxiomC{$\varphi$}
                        \RightLabel{$\land_\text{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_\text{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_\text{e}$}\UnaryInfC{$\varphi$}
                    \end{prooftree}
                \end{minipage}
                \begin{minipage}{.25\linewidth}
                    \begin{prooftree}
                        \AxiomC{$\varphi \land \psi$}
                        \RightLabel{$\land_\text{e}$}\UnaryInfC{$\psi$}
                    \end{prooftree}
                \end{minipage}
                \begin{minipage}{.3\linewidth}
                    \begin{prooftree}
                        \AxiomC{$\varphi$}
                        \AxiomC{$\varphi \Rightarrow \psi$}
                        \RightLabel{$\Rightarrow_\text{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 hypotheses.
                \begin{prooftree}
                    \AxiomC{$\psi$}
                    \AxiomC{$\lnot \psi$}
                    \BinaryInfC{$\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}