[FMFP] Mostly summarized formal reasoning

semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/00_syntax.tex

@@ -0,0 +1,12 @@
+\subsection{Propositional logic}
+\subsubsection{Syntax}
+\inlinedefinition For a set of variables $\cV$, the \bi{language of propositional logic} $\cL_P$ is the smallest set where
+\begin{multicols}{2}
+    \begin{itemize}
+        \item $X \in \cL_P$ if $X \in \cV$
+        \item $\bot \in \cL_P$
+        \item $A \land B \in \cL_P$ if $A \in \cL_P$ and $B \in \cL_P$
+        \item $A \lor B \in \cL_P$ if $A \in \cL_P$ and $B \in \cL_P$
+        \item $A \rightarrow B \in \cL_P$ if $A \in \cL_P$ and $B \in \cL_P$
+    \end{itemize}
+\end{multicols}

semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/01_semantics.tex

@@ -0,0 +1,19 @@
+\subsubsection{Semantics}
+\inlinedefinition[Valuation] $\sigma : \cV \rightarrow \{ \texttt{True}, \texttt{False} \}$ maps variables to truth values.
+They are the simple models (i.e. \textit{interpretations}). \bi{Valuations} is the set of valuations.
+
+\inlinedefinition[Satisfiability] smallest relation $\models \; \subseteq$ \textit{Valuations} $\times \cL_P$ such that
+\begin{multicols}{2}
+    \begin{itemize}
+        \item $\sigma \models X$ if $\sigma(X) = \texttt{True}$
+        \item $\sigma \models A \land B$ if $\sigma \models A$ and $\sigma \models B$
+        \item $\sigma \models A \lor B$ if $\sigma \models A$ or $\sigma \models B$
+        \item $\sigma \models A \rightarrow B$ if whenever $\sigma \models A$ then $\sigma \models B$
+    \end{itemize}
+\end{multicols}
+
+\inlinedefinition[satisfiable formula] A formula $A \in \cL_P$ is \bi{satisfiable} if $\sigma \models A$ for \textbf{some} valuation $\sigma$
+
+\inlinedefinition[tautology, valid formula] A formula $A \in \cL_P$ is \bi{valid} (a \bi{tautology}) if $\sigma \models A$ for \textbf{all} valuations $\sigma$
+
+\inlinedefinition[Semantic entailment] $A_1, \ldots , A_n \models A$ if $\forall \sigma$ we have $\sigma \models A_1, \ldots, \sigma \models A_n$, then $\sigma \models A$

semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/02_deductive-system.tex

@@ -0,0 +1,10 @@
+\newpage
+\subsubsection{Requirements for a deductive system}
+The derivation rules (syntactic entailment) and truth tables (semantic entailment) should agree.
+For that we have two requirements, for $\Gamma = A_1, \ldots, A_n$ a collection of formulas:
+\begin{itemize}
+    \item \bi{Soundness:} If $\Gamma \vdash A$ can be derived, then $\Gamma \models A$
+    \item \bi{Completeness:} If $\Gamma \models A$, then $\Gamma \vdash A$ can be derived
+\end{itemize}
+
+\bi{Decidability} is also desirable, i.e. having checks of the attributes be of low complexity.

semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex

@@ -0,0 +1,19 @@
+\subsubsection{Natural deduction for propositional formulas}
+\inlinedefinition[Sequent] Is an assertion of form $A_1, \ldots, A_n \vdash A$, with $A, A_1, \ldots, A_n$ being propositional formulas.
+
+\inlineintuition $A$ follows from the $A_i$ and if the system is sound, the $A_i$ semantically entail $A$.
+
+\inlinedefinition[Axiom] is the starting point (usually the leaves) of the derivation trees and are usually of the form
+\[
+    \begin{prooftree}
+        \infer0[axiom]{\ldots, A, \ldots \vdash A}
+    \end{prooftree}
+\]
+i.e. when coming up with a derivation tree for a \bi{proof}, we want to reach a leaf where $A$ is contained in $\Gamma$.
+
+\inlinedefinition[Proof] of $A$ is a derivation tree with \texttt{root} $\vdash A$. If a deductive system is \textit{sound}, then $A$ is a tautology.
+
+There are two kinds of rules, \bi{introduce} and \bi{eliminate} connectives. If you are confused about the order when applying them when coming up with a deduction tree,
+they are oriented top-down, so e.g. the introduction rule is inverted when coming up with the deduction tree.
+
+If all rules are sound (i.e. they preserve semantic entailment), then the logic is sound.

semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex

@@ -0,0 +1,77 @@
+\subsubsection{Derivation rules for propositional logic}
+Remember that $E$ means \textit{elimination} and $I$ means \textit{introduction}, with $L$ and $R$ being the side (so $ER$ means elimination on the right)
+\paragraph{Conjunction}
+\begin{align*}
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A}
+        \hypo{\Gamma \vdash B}
+        \infer2[$\land$-I]{\Gamma \vdash A \land B}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A \land B}
+        \infer1[$\land$-EL]{\Gamma \vdash A}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A \land B}
+        \infer1[$\land$-ER]{\Gamma \vdash B}
+    \end{prooftree}
+\end{align*}
+
+\paragraph{Disjunction}
+\begin{align*}
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A}
+        \infer1[$\lor$-IL]{\Gamma \vdash A \lor B}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash B}
+        \infer1[$\lor$-IR]{\Gamma \vdash A \lor B}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A \lor B}
+        \hypo{\Gamma, A \vdash C}
+        \hypo{\Gamma, B \vdash C}
+        \infer3[$\lor$-E]{\Gamma \vdash C}
+    \end{prooftree}
+\end{align*}
+
+\paragraph{Implication}
+\begin{align*}
+    \begin{prooftree}
+        \hypo{\Gamma, A \vdash B}
+        \infer1[$\rightarrow$-I]{\Gamma \vdash A \rightarrow B}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A \rightarrow B}
+        \hypo{\Gamma \vdash A}
+        \infer2[$\rightarrow$-E]{\Gamma \vdash B}
+    \end{prooftree}
+\end{align*}
+
+\paragraph{Others}
+\begin{align*}
+    \begin{prooftree}
+        \hypo{\Gamma \vdash \bot}
+        \infer1[$\bot$-E]{\Gamma \vdash A}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash \neg A}
+        \hypo{\Gamma \vdash A}
+        \infer2[$\neg$-E]{\Gamma \vdash B}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma, \neg A \vdash \bot}
+        \infer1[RAA]{\Gamma \vdash A}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \infer0[axiom]{\ldots, A, \ldots \vdash A}
+    \end{prooftree}
+\end{align*}