diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf
index 70f8c2c..690e427 100644
Binary files a/semester4/fmfp/formal-methods-functional-programming-summary.pdf and b/semester4/fmfp/formal-methods-functional-programming-summary.pdf differ
diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.tex b/semester4/fmfp/formal-methods-functional-programming-summary.tex
index df0eb88..2c992a8 100644
--- a/semester4/fmfp/formal-methods-functional-programming-summary.tex
+++ b/semester4/fmfp/formal-methods-functional-programming-summary.tex
@@ -3,7 +3,10 @@
 \input{~/projects/latex/janishutz-helpers.tex}
 
 \usepackage{lmodern}
+\usepackage{ebproof}
+\ebproofset{separation=2.5em}
 \setFontType{sans}
+\multicolsep 5pt plus 2pt minus 2pt
 
 \setup{Formal Methods \& Functional Programming}
 
@@ -30,7 +33,7 @@
     FS2026, ETHZ
 
     \begin{Large}
-        Summary of the Script and Lectures
+        Summary of the Lectures
     \end{Large}
 \end{center}
 
@@ -45,5 +48,19 @@
 \input{parts/00_haskell/01_syntax.tex}
 
 
+\newsection
+\section{Formal Reasoning}
+\input{parts/01_formal-reasoning/00_formal-proofs.tex}
+\input{parts/01_formal-reasoning/01_natural-deduction.tex}
+\input{parts/01_formal-reasoning/02_propositional-logic/00_syntax.tex}
+\input{parts/01_formal-reasoning/02_propositional-logic/01_semantics.tex}
+\input{parts/01_formal-reasoning/02_propositional-logic/02_deductive-system.tex}
+\input{parts/01_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex}
+\input{parts/01_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex}
+\input{parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex}
+\input{parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex}
+\input{parts/01_formal-reasoning/03_first-order-logic/02_quantifiers.tex}
+% \input{parts/01_formal-reasoning/}
+
 
 \end{document}
diff --git a/semester4/fmfp/parts/01_formal-reasoning/00_formal-proofs.tex b/semester4/fmfp/parts/01_formal-reasoning/00_formal-proofs.tex
new file mode 100644
index 0000000..3558c92
--- /dev/null
+++ b/semester4/fmfp/parts/01_formal-reasoning/00_formal-proofs.tex
@@ -0,0 +1,41 @@
+\subsection{Formal proofs}
+Given a language like $\cL = \{ \oplus, \otimes, +, \times \}$, and derivation rules
+\begin{multicols}{2}
+    \begin{itemize}
+        \item $\alpha$: If $+$, then $\otimes$
+        \item $\beta$: If $+$, then $\times$
+        \item $\gamma$: If $\otimes$ and $\times$, then $\oplus$
+        \item $\delta$: $+$ holds
+    \end{itemize}
+    or displayed using graphical notation:
+    \begin{align*}
+        \frac{+}{\otimes} \; \alpha
+        \qquad \frac{+}{\times} \; \beta \\
+        \frac{\otimes \quad \times}{\oplus} \; \gamma
+        \qquad \frac{}{+} \; \delta
+    \end{align*}
+\end{multicols}
+
+Rules like $\delta$ above are also commonly referred to as an \textit{axiom}.
+
+To prove $\oplus$ in this language, we can either write the following or draw a derivation tree:
+\begin{multicols}{2}
+    \begin{itemize}
+        \item $+$ holds by $\delta$
+        \item $\otimes$ holds by $\alpha$ with 1.
+        \item $\times$ holds by $\beta$ with 1.
+        \item $\oplus$ holds by $\gamma$ with 2 and 3
+    \end{itemize}
+    Or as derivation tree
+    \[
+        \begin{prooftree}
+            % Left branch
+            \infer0[$\delta$]{+}
+            \infer1[$\alpha$]{\otimes}
+            % Right branch
+            \infer0[$\delta$]{+}
+            \infer1[$\beta$]{\times}
+            \infer2[$\gamma$]{ \oplus }
+        \end{prooftree}
+    \]
+\end{multicols}
diff --git a/semester4/fmfp/parts/01_formal-reasoning/01_natural-deduction.tex b/semester4/fmfp/parts/01_formal-reasoning/01_natural-deduction.tex
new file mode 100644
index 0000000..ea30879
--- /dev/null
+++ b/semester4/fmfp/parts/01_formal-reasoning/01_natural-deduction.tex
@@ -0,0 +1,8 @@
+\subsection{Natural deduction}
+The rules from above here are used to construct derivations under assumptions, e.g.
+$A_1, \ldots, A_n \vdash A$, which is read as ``$A$ follows from $A_1, \ldots, A_n$''.
+
+The derivations are always represented as derivation trees and a \bi{proof} is a derivation whose root has no assumptions.
+
+Since we have to prove a statement, we have to draw the derivation trees from the bottom up, with the goal of reaching an axiom or a rule that is an assumption
+using the other rules of the rule set.
diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/00_syntax.tex b/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/00_syntax.tex
new file mode 100644
index 0000000..fcbd28a
--- /dev/null
+++ b/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}
diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/01_semantics.tex b/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/01_semantics.tex
new file mode 100644
index 0000000..659e31c
--- /dev/null
+++ b/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$
diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/02_deductive-system.tex b/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/02_deductive-system.tex
new file mode 100644
index 0000000..1f9809c
--- /dev/null
+++ b/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.
diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex b/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex
new file mode 100644
index 0000000..56295d5
--- /dev/null
+++ b/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.
diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex b/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex
new file mode 100644
index 0000000..5fb5a5e
--- /dev/null
+++ b/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*}
diff --git a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex
new file mode 100644
index 0000000..63f0b4b
--- /dev/null
+++ b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex
@@ -0,0 +1,38 @@
+\newsection
+\subsection{First-Order Logic}
+\subsubsection{Syntax}
+\inlinedefinition[Signature] consists of a set of function symbols $\cF$ and a set of predicate symbols $\cP$, as well as their arities.
+
+We write $f^k$ (or $p^k$, for predicates) to indicate that it has \textit{arity} $k \in \N$.
+Constant functions have arity $0$, linear functions have arity $1$, thus, the arity of a given function (or predicate) is given by
+the number of parameters to uniquely describe it, minus one.
+
+\inlinedefinition[Term] is the terms of first-order logic is smallest set, where (with $\cV$ again a set of variables)
+\begin{enumerate}
+    \item $x \in \textit{Term}$ if $x \in \cV$
+    \item $f^n(t_1, \ldots, t_n) \in \textit{Term}$ if $f^n \in \cF$ and $t_i \in \textit{Term}$, $\forall 1 \leq i \leq n$ (description of form of formulas)
+\end{enumerate}
+
+\inlinedefinition[Form] is the formulas of first-order logic, is the smallest set where
+\begin{enumerate}
+    \item $\bot \in \textit{Form}$
+    \item $p^n(t_1, \ldots, t_n) \in \textit{Form}$ if $p^n \in \cP$  and $t_j \in \textit{Term}$, $\forall 1\leq j \leq n$ (description of form of predicates)
+    \item $A \circ B \in \textit{Form}$ if $A \in \textit{Form}$, $B \in \textit{Form}$ and $\circ \in \{ \land, \lor, \rightarrow \}$ (i.e. formulas with logic symbols)
+    \item $Qx.A \in \textit{Form}$ if $A \in \textit{Form}$, $x \in \cV$ and $Q \in \{ \forall, \exists \}$ (i.e. formulas with quantifiers)
+\end{enumerate}
+
+
+\paragraph{Binding}
+\inlinedefinition[Bound variable] A variable that occurs in a quantifier in scope ({\color{blue} blue in example below})
+
+\inlinedefinition[Free variable] A variable that is not bound by a quantifier in scope ({\color{red} red in example below})
+
+\inlineexample $(q({\color{red} x}) \lor \exists {\color{blue} x}.\forall {\color{blue} y}. p(f({\color{blue} x}), {\color{red} z}) \land q({\color{red} a}))
+\lor \forall {\color{blue} x}.r({\color{blue} x}, {\color{red} z}, g({\color{blue} x}))$
+
+\inlinedefinition[$\alpha$-conversion] A \bi{bound} variable can be renamed at any time, but must preserve binding structure.
+
+
+\paragraph{Precedences} 
+$\neg > \land > \lor > \rightarrow$, with $>$ a total order of precedences.
+Quantifiers extend as far right as possible, bounded by the end of line or a going out of scope by closing parenthesis.
diff --git a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex
new file mode 100644
index 0000000..b9c63c5
--- /dev/null
+++ b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex
@@ -0,0 +1,40 @@
+\subsubsection{Semantics}
+\inlinedefinition[Structure] is a pair $\cS = \langle U_\cS, I_\cS \rangle$, where $U_\cS$ is the universe and it is a non-empty set and $I_\cS$ is a mapping with
+\begin{enumerate}
+    \item $I_\cS(p^n)$ is an $n$-ary relation on $U_\cS$ for $p^n \in \cP$ (short $p^\cS$)
+    \item $I_\cS(f^n)$ is an $n$-ary (total) function on $U_\cS$ for $f^n \in \cF$ short ($f^\cS$)
+\end{enumerate}
+\inlineintuition The $I_\cS$ is essentially assigning to each predicate and formula its definition in the universe of the structure, noted as a relation.
+
+\inlinedefinition[Interpretation] is a pair $\cI = \langle \cS, v \rangle$, with $v : \cV \rightarrow U_\cS$ a valuation\\
+\inlineintuition it assigns definitions to the formulas and predicates (through the structure), as well as values to the variables (through the valuation).
+
+\inlinedefinition[Value] of a term $t$ under $\cI$ is written as $\cI(t)$ and defined by $\cI(x) = v(x)$ for $x \in \cV$ and\\
+$\cI(f(t_1, \ldots, t_n)) = f^\cS(\cI(t_1), \ldots, \cI(t_n))$
+
+\inlinedefinition[Satisfiability] $\models \subseteq$ Interpretations $\times$ \textit{Form} is the smallest relation satisfying
+\begin{align*}
+     & \langle \cS, v \rangle \models p(t_1, \ldots, t_n) &  & \text{ if } (\cI(t_1), \ldots, \cI(t_n)) \in p^\cS \text{ where } \cI = \langle \cS, v \rangle \\
+     & \langle \cS, v \rangle \models \forall x. A        &  & \text{ if } \langle \cS, v[x \mapsto a] \rangle \models A, \text{ for all } a \in \U_\cS       \\
+     & \langle \cS, v \rangle \models \exists x. A        &  & \text{ if } \langle \cS, v[x \mapsto a] \rangle \models A, \text{ for some } a \in \U_\cS      \\
+\end{align*}
+
+\inlinedefinition[Model] When $\langle \cS, v \rangle \models A$, then $\langle \cS, v \rangle$ is a \bi{model} for $A$.
+If $A$ does not have free variables, the satisfaction does not depend on the valuation $v$ and we write $\cS \models A$
+
+\inlinedefinition[Validity] When every interpretation is a model, we write $\models A$, and we say that $A$ is \bi{valid}
+
+\inlinedefinition[Satisfiability] $A$ is \bi{satisfiable}, if there exists at least one model for $A$.
+
+\inlineexample Given $\forall x.p(x, s(x))$, we a model would be
+\begin{align*}
+    U_\cS & = \N                                                                   \\
+    p^\cS & = \{ (m, n) \divider m, n \in U_\cS \text{ and } m < n \}              \\
+    s^\cS & = \text{ successor function on } U_\cS, \text{ i.e. } s^\cS(x) = x + 1
+\end{align*}
+
+
+\paragraph{Substitution}
+\inlinedefinition[Substitution] Replace all occurrences of a free variable $x$ with some term $t$ in $A$.
+To denote a substitution, we write $A[x \mapsto t]$. \hl{Important} All free variables in $t$ must still be free in $A[x \mapsto t]$.
+If that would not be true anymore, do a $\alpha$-conversion first.
diff --git a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/02_quantifiers.tex b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/02_quantifiers.tex
new file mode 100644
index 0000000..0d737a1
--- /dev/null
+++ b/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/02_quantifiers.tex
@@ -0,0 +1,31 @@
+\subsubsection{Quantifiers}
+\paragraph{Universal quantification}
+Additional rules are needed for the universal quantifier. * side condition is that $x$ is not free in any assumption of $\Gamma$
+\begin{align*}
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A}
+        \infer1[$\forall$-I*]{\Gamma \vdash \forall x.A}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash \forall x.A}
+        \infer1[$\forall$-E]{\Gamma \vdash A[x \rightarrow t]}
+    \end{prooftree}
+\end{align*}
+Again here be mindful not to capture free variables.
+
+\paragraph{Existential quantification}
+Additional rules are needed for the existential quantifier. ** side condition is that $x$ is neither free in B nor free in $\Gamma$
+\begin{align*}
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A[x \mapsto t]}
+        \infer1[$\exists$-I]{\Gamma \vdash \exists x.A}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash \exists x.A}
+        \hypo{\Gamma, A \vdash B}
+        \infer2[$\exists$-E**]{\Gamma \vdash A[x \rightarrow t]}
+    \end{prooftree}
+\end{align*}
+Again here be mindful not to capture free variables.
diff --git a/semester4/fmfp/parts/01_natural-deduction/00_intro.tex b/semester4/fmfp/parts/01_formal-reasoning/04_equality.tex
similarity index 100%
rename from semester4/fmfp/parts/01_natural-deduction/00_intro.tex
rename to semester4/fmfp/parts/01_formal-reasoning/04_equality.tex