[FMFP] Fix errors

semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex

@@ -7,7 +7,7 @@ We write $f^k$ (or $p^k$, for predicates) to indicate that it has \textit{arity}
 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)
+\inlinedefinition[Term] is the terms of first-order logic and is the 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)

semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex

@@ -1,5 +1,5 @@
 \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
+\inlinedefinition[Structure] is a pair $\cS = \langle U_\cS, I_\cS \rangle$, where $U_\cS$ is the universe (non-empty set) and $I_\cS$ is a mapping:
 \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$)

semester4/fmfp/parts/01_formal-reasoning/05_correctness/03_induction.tex

@@ -9,7 +9,7 @@ To prove $\forall n \in \N. P$ (with $n$ free in $P$), we do the following:
 
 \shade{blue}{Base case} We show that $P[n \mapsto 0]$ is correct
 
-\shade{green}{Step case} For an arbitrary $m$ not free in $P$, we show that $P[n \mapsto m + 1]$ is correct under the assumption that $P[n \mapsto m]$
+\shade{green}{Step case} For an arbitrary $m$ not free in $P$, we show that $P[n \mapsto m + 1]$ is correct under the assumption that $P[n \mapsto m]$ is correct.
 
 For \bi{well-founded} domains, we have to adjust the induction hypothesis slightly: We assume $\forall l \in \N. l < m \rightarrow P[n \mapsto l]$
 and then prove $P[n \mapsto m]$ under our assumption.

semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex

@@ -1,6 +1,6 @@
 \subsubsection{Lambda calculus}
 To prove that types are correct, the lambda calculus comes in handy.
-It is based on the same concept as natural deduction trees
+The proofs are again structured as derivation trees.
 
 \paragraph{Core rules for Lambda-Calculus}
 \[

semester4/fmfp/parts/02_typing/01_mini-haskell/03_type-inference.tex

@@ -7,7 +7,7 @@ Finally, apply constraints / unification to get possible types.
 
 \paragraph{Self application}
 This means that you apply a function to itself.
-In Haskell, this is not typeable because there would need to be an infinite function type, but all \bi{Haskell types are finite} 
+In Haskell, this is not typeable because there would need to be an infinite function type, but all \bi{Haskell types are finite}
 
 
 \paragraph{Curry-Howard isomorphism}