added ndpred chapter

compile

@@ -9,9 +9,7 @@ SINK=/dev/null
 
 VALID_ARGS="abdh"
 BURST=0
-DEBUG=0
-ANNOTATE=0
-
+DEBUG=0 ANNOTATE=0
 printUsage() {
   printf "A shell wrapper for this questionnaire using latexmk.\n"
   printf "Currently this wrapper supports compiling of the whole script and a burst mode,\nas well as three different <version>s: 'blank', solution, spacing and all which will compile all three in one run.\n\n"
@@ -104,7 +102,7 @@ compile_wrapper() {
 
 compile_chapter() {
   #for chapter in smtzthree proplogic satsolver ndpred predlogic ndpred smt bdd eqchecking symbenc temporal
-  for chapter in  eqchecking
+  for chapter in  ndpred
   do
     set_chapter "\\chapter${chapter}true"
     compile_wrapper "$chapter" "$@"

main.tex

@@ -107,7 +107,7 @@
 \fi
 
 \ifchapterndpred
-  \setsectionnum{5}
+  \setsectionnum{7}
   \section{Natural Deduction for Predicate Logic}
   \input{natural_deduction_predicate_logic/natural_deduction_predicate_logic.tex}
   \pagebreak

natural_deduction_predicate_logic/0001.tex

@@ -0,0 +1 @@
+\item \lect $\forall x \; \big(P(x) \imp Q(x)\big), \forall x \; P(x)\ent \forall x \; Q(x).$

natural_deduction_predicate_logic/0001_sol.tex

@@ -0,0 +1,10 @@
+\begin{logicproof}{1}
+	\forall x \; \big(P(x) \imp Q(x)\big)			& prem.\\
+	\forall x \; P(x) 										& prem.\\
+	\begin{subproof}
+		\llap{$x_0\quad$} P(x_0) \imp Q(x_0)	& $\forall \mathrm{e}$ 1 \\
+		P(x_0)												& $\forall \mathrm{e}$ 2 \\
+		Q(x_0)												& $\imp \mathrm{e}$ 3,4
+	\end{subproof}
+	\forall x \; Q(x)										& $\forall \mathrm{i}$ 3-5
+\end{logicproof}

natural_deduction_predicate_logic/0002.tex

@@ -0,0 +1 @@
+\item \lect $\forall x \; P(x) \land \forall x \; (P(y) \imp Q(x)) \quad \ent \quad Q(z)$

natural_deduction_predicate_logic/0002_sol.tex

@@ -0,0 +1,9 @@
+\setlength\subproofhorizspace{1em}
+\begin{logicproof}{0}
+  \forall x \; P(x) \land \forall x \; (P(y) \imp Q(x))     & prem.\\
+  \forall x \; P(x)                                         & $\land \mathrm{e}_1$ 1\\
+  \forall x \; (P(y) \imp Q(x))                             & $\land \mathrm{e}_2$ 1\\
+  P(y)                                                      & $\forall \mathrm{e}$ 2\\
+  P(y) \imp Q(z)                                            & $\forall \mathrm{e}$ 3\\
+  Q(z)                                                      & $\imp \mathrm{e}$ 5,4
+\end{logicproof}

natural_deduction_predicate_logic/0003.tex

@@ -0,0 +1 @@
+\item \lect $\forall x \; P(x) \lor \forall x \; Q(x) \quad \ent \quad \forall y \; (P(y) \lor Q(y))$

natural_deduction_predicate_logic/0003_sol.tex

@@ -0,0 +1,21 @@
+\setlength\subproofhorizspace{1.7em}
+\begin{logicproof}{2}
+  \forall x \; P(x) \lor \forall x \; Q(x)     & prem.\\
+  \begin{subproof}
+    \forall x \; P(x)                          & ass.\\
+    \begin{subproof}
+      \llap{$t\enspace \;$} P(t)               & $\forall \mathrm{e}$ 2\\
+      P(t) \lor Q(t)                           & $\lor \mathrm{i}_1$ 3
+    \end{subproof}
+    \forall y \; (P(y) \lor Q(y))               & $\forall \mathrm{i}$ 3-4
+  \end{subproof}
+  \begin{subproof}
+    \forall x \; Q(x)                          & ass.\\
+    \begin{subproof}
+      \llap{$s\enspace \;$} Q(s)               & $\forall \mathrm{e}$ 6\\
+      P(s) \lor Q(s)                           & $\lor \mathrm{i}_2$ 7
+    \end{subproof}
+    \forall y \; (P(y) \lor Q(y))               & $\forall \mathrm{i}$ 7-8
+  \end{subproof}
+ \forall y \; (P(y) \lor Q(y))                       & $\lor \mathrm{e}$ 1,2-5,6-9
+\end{logicproof}

natural_deduction_predicate_logic/0004.tex

@@ -0,0 +1 @@
+\item \ifassignmentsheet \points{2} \fi $\forall x \; (P(x) \imp Q(y)), \forall y \; (P(y) \land R(x)) \quad \ent \quad \exists x \; Q(x))$

natural_deduction_predicate_logic/0004_sol.tex

@@ -0,0 +1,10 @@
+\setlength\subproofhorizspace{1em}
+\begin{logicproof}{0}
+  \forall x \; (P(x) \imp Q(y))     & prem.\\
+  \forall y \; (P(y) \land R(x))    & prem.\\
+  P(t) \imp Q(y)                    & $\forall \mathrm{e}$ 1\\
+  P(t) \land R(x)                  & $\forall \mathrm{e}$ 2\\
+  P(t)                              & $\land \mathrm{e}_1$ 4\\
+  Q(y)                              & $\imp \mathrm{e}$ 3\\
+  \exists x \; Q(x)                 & $\exists \mathrm{i}$ 6
+\end{logicproof}

natural_deduction_predicate_logic/0005.tex

@@ -0,0 +1 @@
+\item \ifassignmentsheet \points{3} \fi $\forall a \forall b \; (P(a) \land Q(b)) \quad \ent \quad \forall a \exists b \; (P(a) \lor Q(b))$

natural_deduction_predicate_logic/0005_sol.tex

@@ -0,0 +1,12 @@
+\setlength\subproofhorizspace{1.1em}
+\begin{logicproof}{1}
+  \forall a \forall b \; (P(a) \land Q(b))                  & prem.\\
+  \begin{subproof}
+	  \llap{$t\enspace \;$} \forall b \; (P(s) \land Q(b))    & $\forall \mathrm{e}$ 1\\
+    P(s) \land Q(t)                                         & $\forall \mathrm{e}$ 2\\
+    P(s)                                                    & $\land \mathrm{e}_1$ 3\\
+    P(s) \lor Q(t)                                          & $\lor \mathrm{i}_1$ 4\\
+    \exists b \; (P(s) \lor Q(b))                           & $\exists \mathrm{i}$ 5
+  \end{subproof}
+  \forall a \exists b \; (P(a) \lor Q(b))                   & $\forall \mathrm{i}$ 2-6
+\end{logicproof}

natural_deduction_predicate_logic/0006.tex

@@ -0,0 +1 @@
+\item \lect Explain the $\exists$-elimination rule ($\exists$e). Why does this rule require a box and what does it mean that $x_0$ is \textit{fresh}?

natural_deduction_predicate_logic/0007.tex

@@ -0,0 +1 @@
+\item \lect $\exists x \; \lnot P(x), \forall x \; \lnot Q(x) \quad \ent \quad \exists x \; (\lnot P(x) \land \lnot Q(x))$

natural_deduction_predicate_logic/0007_sol.tex

@@ -0,0 +1,12 @@
+\setlength\subproofhorizspace{1.6em}
+\begin{logicproof}{1}
+  \exists x \; \lnot P(x)                       & prem.\\
+  \forall x \; \lnot Q(x)                       & prem.\\
+  \begin{subproof}
+	  \llap{$x_0\enspace \;$} \lnot P(x_0)        & ass.\\
+    \lnot Q(x_0)                                & $\forall \mathrm{e}$ 2\\
+    \lnot P(x_0) \land \lnot Q(x_0)             & $\land \mathrm{i}$ 3,4\\
+    \exists x \; (\lnot P(x) \land \lnot Q(x))  & $\exists \mathrm{i}$ 5
+  \end{subproof}
+  \exists x \; (\lnot P(x) \land \lnot Q(x))    & $\exists \mathrm{e}$ 3-6
+\end{logicproof}

natural_deduction_predicate_logic/0008.tex

@@ -0,0 +1,18 @@
+\item  \ifassignmentsheet \points{4} \fi Consider the following natural deduction proof for the sequent $$\forall x \; (P(x)\imp Q(x)), \quad \exists x \; P(x) \quad \ent \quad \forall x Q(x).$$
+Is the proof correct? If not, explain the error in the proof and either show how to correctly prove the sequent, or give a counterexample that proves the sequent invalid.
+
+\setlength\subproofhorizspace{1.1em}
+\begin{logicproof}{2}
+  \forall x \; (P(x)\imp Q(x))      & prem.\\
+  \exists x \; P(x)                 & prem.\\
+  \begin{subproof}
+    \llap{$x_0\enspace \;$}		      &\\
+    \begin{subproof}
+      P(x_0)                        & ass.\\
+      P(x_0) \imp Q(x_0)            & $\forall \mathrm{e}$ 1\\
+      Q(x_0)                        & $\imp \mathrm{e}$, 4,5
+    \end{subproof}
+    \forall x \; Q(x)               & $\forall \mathrm{i}$ 4-6
+  \end{subproof}
+  \forall x \; Q(x)                 & $\exists \mathrm{e}$ 2,3-7
+\end{logicproof}

natural_deduction_predicate_logic/0008_sol.tex

@@ -0,0 +1,13 @@
+This sequent is not provable.
+
+Model $\mathcal{M}$:\\
+\begin{minipage}{0.2\textwidth}
+  \begin{align*}
+  \mathcal{A} =& \; \{ a,b \}\\
+  P^\mathcal{M} =& \; \{ a \}\\
+  Q^\mathcal{M} =& \; \{ a \}\\
+\end{align*}
+\end{minipage}\\
+
+$\mathcal{M} \models \forall x \; (P(x)\imp Q(x)), \quad \exists x \; P(x)$\\
+$\mathcal{M} \nmodels \forall x Q(x)$

natural_deduction_predicate_logic/0009.tex

@@ -0,0 +1 @@
+\item \lect $\exists x \; (P(x) \imp Q(y)), \quad \forall x \; P(x) \quad \ent \quad  Q(y)$

natural_deduction_predicate_logic/0009_sol.tex

@@ -0,0 +1,11 @@
+\setlength\subproofhorizspace{1em}
+\begin{logicproof}{2}
+  \exists x \; (P(x) \imp Q(y))               & prem.\\
+  \forall x \; P(x)                           & prem.\\
+  \begin{subproof}
+    \llap{$x_0\enspace \;$} P(x_0) \imp Q(y)  & ass.\\
+    P(x_0)                                    & $\forall \mathrm{e}$ 2\\
+    Q(y)                                      & $\imp \mathrm{e}$ 3,4
+  \end{subproof}
+  Q(y)                                        & $\exists \mathrm{e}$ 3-5
+\end{logicproof} 

natural_deduction_predicate_logic/0010.tex

@@ -0,0 +1 @@
+\item \lect $\forall x \; \lnot (P(x) \land Q(x)) \quad \ent \quad \lnot \exists x \; (P(x) \land Q(x))$

natural_deduction_predicate_logic/0010_sol.tex

@@ -0,0 +1,14 @@
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{2}
+  \forall x \; \lnot (P(x) \land Q(x))        & prem.\\
+  \begin{subproof}
+    \exists x \; (P(x) \land Q(x))            & ass.\\
+    \begin{subproof}
+      \llap{$t\enspace \;$} P(t) \land Q(t)   & ass.\\    
+      \lnot P(t) \land Q(t)                   & $\forall \mathrm{e}$ 1\\  
+      \bot                                    & $\lnot \mathrm{e}$ 3,4  
+    \end{subproof}
+    \bot                                      & $\exists \mathrm{e}$ 3-5  
+  \end{subproof}
+  \lnot \exists x \; (P(x) \land Q(x))        & $\lnot \mathrm{i}$ 2-6
+\end{logicproof}

natural_deduction_predicate_logic/0011.tex

@@ -0,0 +1 @@
+\item \lect $\lnot \exists x \; (P(x) \land Q(x)) \quad \ent \quad \forall x \; \lnot (P(x) \land Q(x))$

natural_deduction_predicate_logic/0011_sol.tex

@@ -0,0 +1,14 @@
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{2}
+  \lnot \exists x \; (P(x) \land Q(x))        & prem.\\
+  \begin{subproof}
+    \llap{$t\enspace \;$}                     & \\
+    \begin{subproof}
+      P(t) \land Q(t)                         & ass.\\    
+      \exists x \; \lnot (P(x) \land Q(x))    & $\exists \mathrm{i}$ 3\\  
+      \bot                                    & $\lnot \mathrm{e}$ 1,4  
+    \end{subproof}
+    \lnot P(t) \land Q(t)                     & $\lnot \mathrm{i}$ 3-5      
+  \end{subproof}
+  \forall x \; \lnot (P(x) \land Q(x))        & $\forall \mathrm{i}$ 2-6
+\end{logicproof}

natural_deduction_predicate_logic/0012.tex

@@ -0,0 +1 @@
+\item \ifassignmentsheet \points{2} \fi $\exists x \; \lnot P(x), \exists x \; \lnot Q(x) \quad \ent \quad \exists x \; (\lnot P(x) \land \lnot Q(x))$

natural_deduction_predicate_logic/0012_sol.tex

@@ -0,0 +1,13 @@
+This sequent is not provable.
+
+Model $\mathcal{M}$:\\
+\begin{minipage}{0.2\textwidth}
+	\begin{align*}
+  \mathcal{A} =& \; \{ a,b \}\\
+  P^\mathcal{M} =& \; \{ a \}\\
+  Q^\mathcal{M} =& \; \{ b \}\\
+\end{align*}
+\end{minipage}\\
+
+$\mathcal{M} \models \exists x \; \lnot P(x), \exists x \; \lnot Q(x)$\\
+$\mathcal{M} \nmodels \exists x \; (\lnot P(x) \land \lnot Q(x))$

natural_deduction_predicate_logic/0013.tex

@@ -0,0 +1 @@
+\item \lect $\exists x \; (P(x) \imp Q(y)), \quad \exists x \; P(x) \quad \ent \quad  Q(y)$

natural_deduction_predicate_logic/0013_sol.tex

@@ -0,0 +1,14 @@
+This sequent is not provable.
+
+Model $\mathcal{M}$:\\
+\begin{minipage}{0.2\textwidth}
+  \begin{align*}
+  \mathcal{A} =& \; \{ a,b \}\\
+  P^\mathcal{M} =& \; \{ a \}\\
+  Q^\mathcal{M} =& \; \{ a \} \\
+  y \leftarrow \; b \\
+\end{align*}
+\end{minipage}\\
+
+$\mathcal{M} \models \exists x \; (P(x) \imp Q(y)), \quad \exists x \; P(x)$\\
+$\mathcal{M} \nmodels Q(y)$

natural_deduction_predicate_logic/0014.tex

@@ -0,0 +1 @@
+\item \lect $\forall x ( P(x) \land Q(x)) \ent \forall x P(x) \land \forall x Q(x) $

natural_deduction_predicate_logic/0014_sol.tex

@@ -0,0 +1,15 @@
+\setlength\subproofhorizspace{1.7em}
+\begin{logicproof}{1}
+  \forall x \;( P(x) \land  Q(x) )    & prem.\\
+  \begin{subproof}
+    \llap{$x_0\enspace \;$} P(x_0) \land Q(x_0) & $\forall \mathrm{e}$ 1\\
+    P(x_0)                                  & $\land \mathrm{e}$ 2
+  \end{subproof}
+  \forall x \; P(x)                       & $\forall \mathrm{i} 2-3$\\
+  \begin{subproof}
+    \llap{$x_1\enspace \;$} P(x_1) \land Q(x_1) & $\forall \mathrm{e}$ 1\\
+    Q(x_1)                                  & $\land \mathrm{e}$ 5
+  \end{subproof}
+  \forall x \; Q(x)                       & $\forall \mathrm{i} 5-6$\\
+  \forall x \; P(x) \land \forall x \; Q(x) & $\land \mathrm{i}$ 4,7
+\end{logicproof}

natural_deduction_predicate_logic/1001.tex

@@ -0,0 +1,4 @@
+\item \self Explain the $\forall$-introduction rule
+and the $\forall$-elimination rule.
+Explain why one rule needs a box while the other one does not.
+What does it mean that $x_0$ needs to be fresh?

natural_deduction_predicate_logic/1002.tex

@@ -0,0 +1 @@
+\item \self $\forall x \; (P(x) \land Q(x)) \quad \ent \quad \forall x \; ( (Q(x) \lor R(x)) \land (R(x) \lor P(x)) )$

natural_deduction_predicate_logic/1002_sol.tex

@@ -0,0 +1,14 @@
+
+\begin{logicproof}{2}
+  \forall x \; (P(x) \land Q(x))                   &\prem \\
+  \begin{subproof}
+                             & \freshVar{$x_0$} \\
+    P(x_0) \land Q(x_0)  & \foralle 1 $x_0$ \\  
+    P(x_0)                 & \ande{1}1 \\
+    Q(x_0)                 & \ande{2}1 \\
+    R(x_0) \lor P(x_0)         & \ori 4 \\
+    Q(x_0) \lor R(x_0) & \ori 5 \\
+    (Q(x_0) \lor R(x_0)) \land (R(x) \lor P(x)) & \andi 6,7
+  \end{subproof}
+  \forall x \; ((Q(x) \lor R(x)) \land (R(x) \lor P(x))) & \foralli 2-8
+\end{logicproof}

natural_deduction_predicate_logic/1003.tex

@@ -0,0 +1,2 @@
+\item \ifassignmentsheet \points{3} \fi
+$\forall x \; (P(x)\lor Q(x)),\quad \forall x \; (\lnot P(x)) \quad \ent \quad \forall x \; (Q(x))$

natural_deduction_predicate_logic/1003_sol.tex

@@ -0,0 +1,20 @@
+
+\begin{logicproof}{2}
+  \forall x \; (P(x) \lor Q(x))                   &\prem \\
+  \forall x \; (\lnot P(x))                       &\prem \\
+  \begin{subproof}
+    & \freshVar{$x_0$}\\
+    P(x_0) \lor Q(x_0)                            &$\foralle 1$  $x_0$  \\
+    \lnot P(x_0)                                  &$\foralle 2$ \\
+    \begin{subproof}
+      P(x_0)                                        &\assum \\
+      \bot                                          &$\nege 5,6$ \\
+      Q(x_0)                                        &$\bote 7$
+    \end{subproof}
+    \begin{subproof}
+      Q(x_0)                                        &\assum
+    \end{subproof}
+    Q(x_0)                                            &$\ore 4,6-8,9$
+  \end{subproof}
+  \forall x \; Q(x)                                &$\foralli 3-10 $
+\end{logicproof}

natural_deduction_predicate_logic/1004.tex

@@ -0,0 +1 @@
+\item \self $\exists x \; (Q(x) \imp R(x)),\quad \exists x \; (P(x)\land Q(x)) \quad \ent \quad \exists x \; (P(x) \land R(x))$

natural_deduction_predicate_logic/1004_sol.tex

@@ -0,0 +1,18 @@
+
+\begin{logicproof}{2}
+  \exists x \; (Q(x) \imp R(x))                   &\prem \\
+  \exists x \; (P(x)\land Q(x))                   &\prem \\
+  \begin{subproof}
+    Q(x_0) \imp R(x_0)              &\assum~\freshVar{$x_0$} \\
+    \begin{subproof}
+      P(x_0) \land Q(x_0)             &\assum~\freshVar{$x_0$}\\
+      P(x_0)                          &\ande{1} 4\\
+      Q(x_0)                          &\ande{2} 4\\
+      R(x_0)                          &\impe 5,3\\
+      P(x_0) \land R(x_0) & \andi 5,7\\
+      \exists x (P(x) \land R(x)) & \existi 8
+    \end{subproof}
+    \exists x \; (P(x) \land R(x)) & \existe 2,4-9
+  \end{subproof}
+  \exists x \; (P(x) \land R(x)) & \existe 1,3-10
+\end{logicproof}

natural_deduction_predicate_logic/1005.tex

@@ -0,0 +1 @@
+\item \self $\forall x \; (Q(x) \imp R(x)),\quad \exists x \; (P(x)\land Q(x)) \quad \ent \quad \exists x \; (P(x) \land R(x))$

natural_deduction_predicate_logic/1005_sol.tex

@@ -0,0 +1,15 @@
+
+\begin{logicproof}{2}
+  \forall x \; (Q(x) \imp R(x))                  &\prem \\
+  \exists x \; (P(x)\land Q(x))                  &\prem \\
+  \begin{subproof}
+    P(x_0) \land Q(x_0) & \assum~\freshVar{$x_0$}\\
+    Q(x_0) \imp R(x_0)  & \foralle 1 $x_0$\\
+    P(x_0)              & \ande{1} 3 \\
+    Q(x_0)              & \ande{2} 3 \\
+    R(x_0)              & \impe 6,4\\
+    P(x_0) \land R(x_0) & \andi 5,7\\
+    \exists x \; (P(x) \land R(x))  & \existi 8 
+  \end{subproof}
+  \exists x \; (P(x) \land R(x)) &\existe 2,3-9
+\end{logicproof}

natural_deduction_predicate_logic/1006.tex

@@ -0,0 +1 @@
+\item \self $\lnot \exists x \forall y \; (P(x) \land Q(y)) \quad \ent \quad \forall x \exists y \; \lnot (P(x) \land Q(y))$

natural_deduction_predicate_logic/1006_sol.tex

@@ -0,0 +1,27 @@
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{4}
+    \lnot \exists x \forall y \; (P(x) \land Q(y))              & \prem\\
+    \begin{subproof}
+        \begin{subproof}
+            \forall y (P(x_0)\land Q(y))                        & $\assum$ $\freshVar{$x_0$}$\\
+            \exists x \forall y (P(x)\land Q(y))                 & $\existi2$\\
+            \bot                                                & $\nege1,3$
+        \end{subproof}
+        \lnot \forall y (P(x_0)\land Q(y))                      & $\negi2-4$\\
+        \begin{subproof}
+            \lnot \exists y \lnot (P(x_0)\land Q(y))            & $\assum$\\
+            \begin{subproof}
+                \begin{subproof}
+                    \lnot (P(x_0)\land Q(y_0))                  & $\assum$ $\freshVar{$y_0$}$\\
+                    \exists y \lnot (P(x_0) \land Q(y))          & $\existi7$\\
+                    \bot                                        & $\nege6,8$
+                \end{subproof}
+                P(x_0) \land Q(y_0)                             & $PBC 7-9$
+            \end{subproof}
+            \forall y (P(x_0)\land Q(y))                        & $\foralli7-10$\\
+            \bot                                                & $\nege5,11$
+        \end{subproof}
+        \exists y \lnot (P(x_0)\land Q(y))                      & $PBC 6-12$
+    \end{subproof}
+    \forall x \exists y \; \lnot (P(x) \land Q(y))              & $\foralli2-13$
+\end{logicproof}

natural_deduction_predicate_logic/1007.tex

@@ -0,0 +1 @@
+\item \self $\forall x \exists y \; \lnot (P(x) \land Q(y)) \quad \ent \quad \lnot \exists x \forall y \; (P(x) \land Q(y))$

natural_deduction_predicate_logic/1007_sol.tex

@@ -0,0 +1,24 @@
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{2}
+    \forall x \exists y \; \lnot (P(x) \land Q(y))          & \prem\\
+    \exists y \lnot (P(x_0)\land Q(y))                       & $\foralle1$\\
+    \begin{subproof}
+        \lnot (P(x_0)\land Q(y_0))                          & $\assum$ $\freshVar{$y_0$}$\\
+        \begin{subproof}
+            \forall y (P(x_0)\land Q(y))                    & $\assum$\\
+            P(x_0)\land Q(y_0)                              & $\foralle4$\\
+            \bot                                            & $\nege3,5$
+        \end{subproof}
+        \lnot \forall y (P(x_0)\land Q(y))                  & $\negi4-6$
+    \end{subproof}
+    \lnot \forall y (P(x_0)\land Q(y))                      & $\existe2,3-7$\\
+    \begin{subproof}
+        \exists x \forall y (P(x)\land Q(y))                 & $\assum$\\
+        \begin{subproof}
+            \forall y (P(x_0)\land Q(y))                    & $\assum$ $\freshVar{$x_0$}$\\
+            \bot                                            & $\nege8,10$
+        \end{subproof}
+        \bot                                                & $\existe9,10-11$
+    \end{subproof}
+    \lnot \exists x \forall y \; (P(x) \land Q(y))          & $\negi9-12$
+\end{logicproof}

natural_deduction_predicate_logic/1008.tex

@@ -0,0 +1 @@
+\item \self $\lnot \exists x \; \lnot P(x) \quad \ent \quad \forall x \; \lnot P(x)$

natural_deduction_predicate_logic/1008_sol.tex

@@ -0,0 +1,12 @@
+This sequent is not provable.
+
+Model $\mathcal{M}$:\\
+\begin{minipage}{0.2\textwidth}
+  \begin{align*}
+  \mathcal{A} =& \; \{ a \}\\
+  P^\mathcal{M} =& \; \{ a\}
+  \end{align*}
+\end{minipage}\\
+
+$\mathcal{M} \models \lnot \exists x \lnot P(x)$\\
+$\mathcal{M} \nmodels \forall x \lnot P(x)$

natural_deduction_predicate_logic/1009.tex

@@ -0,0 +1 @@
+\item \self $P(x) \lor Q(y),\quad P(x)\imp R(z),\quad Q(y) \imp R(z) \quad \ent \quad R(z)$

natural_deduction_predicate_logic/1009_sol.tex

@@ -0,0 +1,15 @@
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{1}
+    P(x) \lor Q(y)                  &\prem\\
+    P(x)\imp R(z)                   &\prem\\
+    Q(y) \imp R(z)                  &\prem\\
+    \begin{subproof}
+        P(x)                        &$\assum$\\
+        R(z)                        &$\impe2,4$
+    \end{subproof}
+    \begin{subproof}
+        Q(y)                        &$\assum$\\
+        R(z)                        &$\impe3,6$
+    \end{subproof}
+    R(z)                            &$\ore1,4-5,6-7$
+\end{logicproof}

natural_deduction_predicate_logic/1010.tex

@@ -0,0 +1 @@
+\item \self $\exists y \forall x \; (P(x,y)) \quad \ent \quad \forall x \exists y \; (P(x,y))$

natural_deduction_predicate_logic/1010_sol.tex

@@ -0,0 +1,15 @@
+This sequent is provable.
+
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{2}
+    \exists y \forall x P(x,y) & \prem \\
+    \begin{subproof}
+        \forall x P(x,y_0) & $\assum$ $\freshVar{$y_0$}$ \\
+        \begin{subproof}
+            P(x_0,y_0) & $\foralle 2$ $\freshVar{$x_0$}$ \\
+            \exists y P(x_0,y) & $\existi 3$
+        \end{subproof}
+        \forall x \exists y P(x,y) & $\foralli3-4$
+    \end{subproof}
+    \forall x \exists y P(x,y) & $\existe 1,2-5$
+\end{logicproof}

natural_deduction_predicate_logic/1011.tex

@@ -0,0 +1 @@
+\item \self $\exists a \forall b \; (S(b,a) \land T(b,a)) \quad \ent \quad \forall b \forall a \; (S(b,a) \land T(b,a))$

natural_deduction_predicate_logic/1011_sol.tex

@@ -0,0 +1,13 @@
+This sequent is not provable.
+
+Model $\mathcal{M}$:\\
+\begin{minipage}{0.2\textwidth}
+  \begin{align*}
+  \mathcal{A} =& \; \{ 0,1 \}\\
+  S^\mathcal{M} =& \; \{ (0,1),(1,1) \}\\
+  T^\mathcal{M} =& \; \{ (0,1),(1,1) \}
+  \end{align*}
+\end{minipage}\\
+
+$\mathcal{M} \models \exists a \forall b \; (S(b,a) \land T(b,a))$\\
+$\mathcal{M} \nmodels \forall b \forall a \; (S(b,a) \land T(b,a))$

natural_deduction_predicate_logic/1012.tex

@@ -0,0 +1 @@
+\item \self $ P(y) \imp \forall x Q(x), \enspace\exists x \lnot Q(x) \ent \exists x \lnot P(x) $

natural_deduction_predicate_logic/1012_sol.tex

@@ -0,0 +1,17 @@
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{2}
+    P(y) \imp \forall x Q(x)                & \prem\\
+    \exists x \lnot Q(x)                    & \prem\\
+    \begin{subproof}
+        P(y)                                & $\assum$\\
+        \forall x Q(x)                      & $\impe1,3$\\
+        \begin{subproof}
+            \lnot Q(x_0)                    &$\assum$ $\freshVar{$x_0$}$\\
+            Q(x_0)                          &$\foralle4$\\
+            \bot                            &$\nege5,6$
+        \end{subproof}
+        \bot                                &$\existe2,5-7$
+    \end{subproof}
+    \lnot P(y)                              &$\negi3-8$\\
+    \exists x \lnot P(x)                    &$\existi9$
+\end{logicproof}

natural_deduction_predicate_logic/1013.tex

@@ -0,0 +1,14 @@
+\item Consider the following natural deduction proof for the sequent $$\exists x \; \lnot P(x) \quad \ent \quad \lnot \forall x \; P(x).$$
+Is the proof correct? If not, explain the error in the proof and either show how to correctly prove the sequent, or give a counterexample that proves the sequent invalid.
+
+\setlength\subproofhorizspace{1em}
+\begin{logicproof}{1}
+  \exists x \; \lnot P(x)           & prem.\\
+  \begin{subproof}
+    \forall x \; P(x)		            & ass.\\
+    P(x_0)                          & $\forall \mathrm{e}$ 2\\
+    \exists x \; P(x)               & $\exists \mathrm{i}$ 3\\
+    \bot                            & $\lnot \mathrm{e}$ 1,4
+  \end{subproof}
+  \lnot \forall x \; P(x)           & $\lnot \mathrm{e}$ 2-5
+\end{logicproof}

natural_deduction_predicate_logic/1013_sol.tex

@@ -0,0 +1,14 @@
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{2}
+  \exists x \; \lnot P(x)           & \prem\\
+  \begin{subproof}
+    \forall x \; P(x)		        & $\assum$\\
+    P(x_0)                          & $\foralle2$\\
+    \begin{subproof}
+        \lnot P(x_0)                & $\assum$ $\freshVar{$x_0$}$\\
+        \bot                        & $\nege3,4$
+    \end{subproof}
+    \bot                            & $\existe1,3-5$
+  \end{subproof}
+  \lnot \forall x \; P(x)           & $\negi2-5$
+\end{logicproof}

natural_deduction_predicate_logic/1014.tex

@@ -0,0 +1,24 @@
+\item \self Consider the following natural deduction proof for the sequent $$\quad \exists x \; P(x) \lor \exists x \; Q(x) \quad \ent \quad \exists x \; (P(x)\lor Q(x)).$$
+Is the proof correct? If not, explain the error in the proof and either show how to correctly prove the sequent, or give a counterexample that proves the sequent invalid.
+
+\setlength\subproofhorizspace{1.7em}
+\begin{logicproof}{2}
+  \exists x \; P(x) \lor \exists x \; Q(x) & prem.\\
+  \begin{subproof}
+    \exists x \; P(x)		                   & ass.\\
+    \begin{subproof}
+      \llap{$x_0\enspace \;$} P(x_0)       & ass.\\
+      P(x_0) \lor Q(x_0)                   & $\lor \mathrm{i}_1$ 3
+    \end{subproof}
+    \exists x \; (P(x) \lor Q(x))          & $\exists \mathrm{e}$ 2,3-4
+  \end{subproof}
+  \begin{subproof}
+    \exists x \; Q(x)		                   & ass.\\
+    \begin{subproof}
+      \llap{$x_0\enspace \;$} Q(x_0)	   	 & ass.\\
+      P(x_0) \lor Q(x_0)                   & $\lor \mathrm{i}_2$ 7
+    \end{subproof}
+    \exists x \; (P(x)\lor Q(x))           & $\exists \mathrm{e}$ 6,7-8
+  \end{subproof}
+  \exists x \; (P(x)\lor Q(x))             & $\lor \mathrm{e}$ 1,2-5,6-9
+\end{logicproof}

natural_deduction_predicate_logic/1014_sol.tex

@@ -0,0 +1,23 @@
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{2}
+  \exists x \; P(x) \lor \exists x \; Q(x) & \prem\\
+  \begin{subproof}
+    \exists x \; P(x)		               & $\assum$\\
+    \begin{subproof}
+      P(x_0)                               & $\assum$ $\freshVar{$x_0$}$\\
+      P(x_0) \lor Q(x_0)                   & $\ori3$\\
+      \exists x \; (P(x) \lor Q(x))        & $\existi4$
+    \end{subproof}
+    \exists x \; (P(x) \lor Q(x))          & $\existe2,3-5$
+  \end{subproof}
+  \begin{subproof}
+    \exists x \; Q(x)		               & $\assum$\\
+    \begin{subproof}
+      Q(x_0)	                           & $\assum$ $\freshVar{$x_0$}$\\
+      P(x_0) \lor Q(x_0)                   & $\ori8$\\
+      \exists x \; (P(x) \lor Q(x))        & $\existi9$
+    \end{subproof}
+    \exists x \; (P(x)\lor Q(x))           & $\existe7,8-10$
+  \end{subproof}
+  \exists x \; (P(x)\lor Q(x))             & $\ore1,2-6,7-11$
+\end{logicproof}

natural_deduction_predicate_logic/1015.tex

@@ -0,0 +1 @@
+\item \self $\forall x \exists y \; (P(x) \imp Q(y)), P(s) \quad \ent \quad \exists x \forall y \; (\lnot P(x) \lor Q(y))$

natural_deduction_predicate_logic/1015_sol.tex

@@ -0,0 +1,13 @@
+This sequent is not provable.
+
+Model $\mathcal{M}$:\\
+\begin{minipage}{0.2\textwidth}
+  \begin{align*}
+  \mathcal{A} =& \; \{ a,b \}\\
+  P^\mathcal{M} =& \; \{ a,b \}\\
+  Q^\mathcal{M} =& \; \{ a \}
+  \end{align*}
+\end{minipage}\\
+
+$\mathcal{M} \models \forall x \exists y \; (P(x) \imp Q(y)), P(s)$\\
+$\mathcal{M} \nmodels \exists x \forall y \; (\lnot P(x) \lor Q(y))$

natural_deduction_predicate_logic/2001.tex

@@ -0,0 +1,5 @@
+\item
+  \ifassignmentsheet \points{4}
+  \else \prac
+  \fi
+$\lnot \exists x~P(x) \lor \lnot \exists y~Q(y) \entails \forall z~\lnot(Q(z) \land P(z))$

natural_deduction_predicate_logic/2001_sol.tex

@@ -0,0 +1,27 @@
+
+\setlength{\subproofhorizspace}{1.5em}
+
+\begin{logicproof}{3}
+  \lnot \exists x~P(x) \lor \lnot \exists y~Q(y)    &prem \\
+  \begin{subproof}
+  \begin{subproof}
+    \hspace*{-2.75em}
+    \llap{$z_0\enspace \;$} \: \hspace{2.75em} Q(z_0) \land P(z_0)    &assum \\
+    \begin{subproof}
+      \lnot \exists x~P(x)                      & assum \\
+      P(z_0)                                      &$\land \mathrm{e} 2$ \\
+      \exists x~P(x)                            &$\exists \mathrm{i} 4$ \\
+      \bot                                      &$\lnot \mathrm{e} 3,5$
+    \end{subproof}
+    \begin{subproof}
+      \lnot \exists y~Q(y)                      & assum \\
+      Q(z_0)                                      &$\land \mathrm{e} 2$ \\
+      \exists y~Q(y)                            &$\exists \mathrm{i} 8$ \\
+      \bot                                      &$\lnot \mathrm{e} 7,9$
+    \end{subproof}
+    \bot                                        &$\lor \mathrm{e} 1,3-6,7-10$
+    \end{subproof}
+    \lnot(Q(z_0) \land P(z_0))                      &$\lnot \mathrm{i} 3-11$
+  \end{subproof}
+  \forall z \; \lnot(Q(z) \land P(z))           &$\forall \mathrm{i} 3-12$
+  \end{logicproof}

natural_deduction_predicate_logic/2002.tex

@@ -0,0 +1,5 @@
+\item
+  \ifassignmentsheet \points{2}
+  \else \prac
+  \fi
+$\lnot \exists x \; Q(x)\quad \ent \quad \forall x \; \lnot Q(x)$

natural_deduction_predicate_logic/2002_sol.tex

@@ -0,0 +1,17 @@
+
+\setlength{\subproofhorizspace}{1.5em}
+
+\begin{logicproof}{2}
+ \lnot \exists x \; Q(x)                        &prem \\
+  \begin{subproof}
+    \hspace*{-1.5em}
+    \llap{$x_0\enspace \;$}
+    \begin{subproof}
+    Q(x_0)                                     &assum   \\
+    \exists x \; Q(x)                           &$\exists \mathrm{i} 2$ \\
+    \bot                                        &$\lnot \mathrm{e} 1,3$
+    \end{subproof}
+    \lnot Q(x_0)                                &$\lnot \mathrm{i} 2-4$
+  \end{subproof}
+  \forall x \; \lnot Q(x)                        &$\forall \mathrm{i} 2-5$
+  \end{logicproof}

natural_deduction_predicate_logic/2003.tex

@@ -0,0 +1,5 @@
+\item
+  \ifassignmentsheet \points{2}
+  \else \prac
+  \fi
+$\forall x \; (P(x) \land Q(x)) \quad \ent \quad \exists x \; (P(x) \lor Q(x))$

natural_deduction_predicate_logic/2003_sol.tex

@@ -0,0 +1,7 @@
+\begin{logicproof}{0}
+ \forall x \; (P(x) \land Q(x))              &prem \\
+ P(x_0) \land Q(x_0)                         &$\forall \mathrm{e} 1$ \\
+ P(x_0)                                      &$\land \mathrm{e} 2$ \\
+ P(x_0) \lor Q(x_0)                          &$\lor \mathrm{i} 3$ \\
+ \exists x \; (P(x) \lor Q(x))               &$\exists \mathrm{i} 4$
+ \end{logicproof}

natural_deduction_predicate_logic/2004.tex

@@ -0,0 +1,2 @@
+\item \ifassignmentsheet \points{2} \else \prac \fi
+$\exists x~(P(x) \implies Q(x)) , ~\lnot Q(z) \entails \lnot P(z)$

natural_deduction_predicate_logic/2004_sol.tex

@@ -0,0 +1,14 @@
+This sequent is not provable.
+
+Model $\mathcal{M}$:\\
+\begin{minipage}{0.2\textwidth}
+	\begin{align*}
+  \mathcal{A} =& \; \{ a,z \}\\
+  P^\mathcal{M} =& \; \{ a,z \}\\
+  Q^\mathcal{M} =& \; \{ a\}
+\end{align*}
+\end{minipage}\\
+
+$\mathcal{M} \models \exists x \; P(x) \imp Q(x)$\\
+$\mathcal{M} \models \lnot Q(z)$\\
+$\mathcal{M} \nmodels \lnot P(z)$

natural_deduction_predicate_logic/2005.tex

@@ -0,0 +1,2 @@
+\item \ifassignmentsheet \points{2} \else \prac \fi
+  $\exists x \; (Q(y) \imp P(x)) \quad \ent \quad Q(y) \imp \exists x \; P(x)$

natural_deduction_predicate_logic/2005_sol.tex

@@ -0,0 +1,15 @@
+
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{3}
+  \exists x \;(Q(y) \imp P(x))                     & prem.\\
+  \begin{subproof}
+    \llap{$x_0\enspace \;$} Q(y) \imp P(x_0)           & ass.\\
+      \begin{subproof}
+        Q(y)                                       & ass.\\
+        P(x_0)                                    & $\imp \mathrm{e}$ 3,2 \\
+        \exists x \; P(x)                       & $\exists \mathrm{i}$ 4
+      \end{subproof}
+      Q(y) \imp \exists x \; P(x)                  & $\imp \mathrm{i}$ 3-5
+  \end{subproof}
+  Q(y) \imp \exists x \; P(x)                      & $\exists \mathrm{e}$ 1, 2-6
+\end{logicproof}

natural_deduction_predicate_logic/2006.tex

@@ -0,0 +1,2 @@
+\item \ifassignmentsheet \points{2} \else \prac \fi
+  $ \exists x \; (P(x) \land Q(x)) \quad\ent\quad \exists x \; P(x) \land \exists x \; Q(x)$

natural_deduction_predicate_logic/2006_sol.tex

@@ -0,0 +1,14 @@
+
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{1}
+  \exists x \;(P(x) \land Q(x))                     & prem.\\
+  \begin{subproof}
+    \llap{$x_0\enspace \;$} P(x_0) \land Q(x_0)     & ass.\\
+    P(x_0)                                          & $\land\mathrm{e} 2$\\
+    Q(x_0)                                          & $\land\mathrm{e} 2$\\
+    \exists x \; P(x)                               & $\exists\mathrm{i} 3$\\
+    \exists x \; Q(x)                               & $\exists\mathrm{i} 4$\\
+    \exists x \; P(x) \land \exists \; Q(x)         & $\land\mathrm{i} 5,6$
+  \end{subproof}
+  \exists x \;P(x) \land \exists x \; Q(x))         & $\exists\mathrm{e} 1,2-7$
+\end{logicproof}

natural_deduction_predicate_logic/2007.tex

@@ -0,0 +1,2 @@
+\item \ifassignmentsheet \points{2} \fi
+  $ \exists x \; (P(x) \lor Q(x)) \quad\ent\quad \exists x \; P(x) \lor \exists x \; Q(x)$

natural_deduction_predicate_logic/2007_sol.tex

@@ -0,0 +1,20 @@
+
+\setlength\subproofhorizspace{1.3em}
+\begin{logicproof}{2}
+  \exists x \;(P(x) \lor Q(x))                     & prem.\\
+  \begin{subproof}
+    \llap{$x_0\enspace \;$} P(x_0) \lor Q(x_0)     & ass.\\
+    \begin{subproof}
+      P(x_0)                                       & ass.\\
+      \exists x \; P(x)                            &$ \exists\mathrm{i} 3$\\
+      \exists x \; P(x) \lor \exists x \; Q(x)       &$ \lor\mathrm{i} 4$
+    \end{subproof}
+    \begin{subproof}
+      Q(x_0)                                       & ass.\\
+      \exists x \; Q(x)                            &$ \exists\mathrm{i} 6$\\
+      \exists x \; P(x) \lor \exists x \; Q(x)       &$ \lor\mathrm{i} 7$
+    \end{subproof}
+    \exists x \;P(x) \lor \exists x \; Q(x)       &$ \lor\mathrm{e} 2,3-8$
+  \end{subproof}
+  \exists x \;P(x) \lor \exists x \; Q(x)         & $\exists\mathrm{e} 1,2-9$
+\end{logicproof}

natural_deduction_predicate_logic/2008.tex

@@ -0,0 +1 @@
+\item \ifassignmentsheet \points{3} \fi $ \exists x \; \lnot P(x) \quad \ent \quad \lnot \forall x \; P(x).$

natural_deduction_predicate_logic/2999.tex

@@ -0,0 +1,6 @@
+\item
+  \ifassignmentsheet \points{2}
+  \else \prac
+  \fi
+
+  TBD

natural_deduction_predicate_logic/9999_sol.tex

@@ -0,0 +1,14 @@
+\begin{logicproof}{1}
+  \forall x \; (P(x) \land Q(x))                   &prem \\
+  \begin{subproof}
+    \llap{$x_0\enspace \;$} \: P(x_0) \land Q(x_0) &$\forall \mathrm{e} 1 $\\
+    P(x_0)                                         &$\land \mathrm{e} 2$
+  \end{subproof}
+  \forall x \; P(x)                                &$\forall \mathrm{i} 2-3 $\\
+  \begin{subproof}
+    \llap{$x_1\enspace \;$} \: P(x_1) \land Q(x_1) &$\forall \mathrm{e} 1 $\\
+    Q(x_1)                                         &$\land \mathrm{e} 5$
+  \end{subproof}
+  \forall x \; Q(x)                                &$\forall \mathrm{i} 5-6 $\\
+  \forall x \; P(x) \land \forall x \; Q(x)        &$\land \mathrm{i} 4,7$
+  \end{logicproof}

natural_deduction_predicate_logic/multiple_choice/4_1_fol_lect.tex

@@ -0,0 +1,8 @@
+\item \lect Considering \textit{Quantifier Equivalences} in \textit{Natural Deduction} for \textit{Predicate Logic}, tick all statements in the list, that are equivalent.
+
+\begin{itemize}
+    \item[$\square$] $\forall x \; \phi \equiv \exists x \; \lnot \phi$
+    \item[$\square$] $\forall x \; \phi \equiv \lnot \exists x \; \lnot \phi$
+    \item[$\square$] $\lnot \forall x \; \phi \equiv \exists x \; \lnot \phi$
+    \item[$\square$] $\exists x \; \lnot \phi \equiv \lnot \forall x \; \lnot \phi$
+\end{itemize}

natural_deduction_predicate_logic/multiple_choice/4_1_fol_lect_sol.tex

@@ -0,0 +1,8 @@
+\item \lect Considering \textit{Quantifier Equivalences} in \textit{Natural Deduction} for \textit{Predicate Logic}, tick all statements in the list, that are equivalent.
+
+\begin{itemize}
+    \item[$\square$] $\forall x \; \phi \equiv \exists x \; \lnot \phi$
+    \item[$\ticked$] $\forall x \; \phi \equiv \lnot \exists x \; \lnot \phi$
+    \item[$\ticked$] $\lnot \forall x \; \phi \equiv \exists x \; \lnot \phi$
+    \item[$\square$] $\exists x \; \lnot \phi \equiv \lnot \forall x \; \lnot \phi$
+\end{itemize}

natural_deduction_predicate_logic/natural_deduction_predicate_logic.tex

@@ -0,0 +1,151 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\ndDescription
+\begin{questionSection}{Natural Deduction Rules}
+
+\question{natural_deduction_predicate_logic/0001.tex}
+         {natural_deduction_predicate_logic/0001_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/0002.tex}
+         {natural_deduction_predicate_logic/0002_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/0014.tex}
+         {natural_deduction_predicate_logic/0014_sol.tex}
+         {3cm}
+
+
+\question{natural_deduction_predicate_logic/0003.tex}
+         {natural_deduction_predicate_logic/0003_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/0004.tex}
+         {natural_deduction_predicate_logic/0004_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/0007.tex}
+         {natural_deduction_predicate_logic/0007_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/0008.tex}
+         {natural_deduction_predicate_logic/0008_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/0009.tex}
+         {natural_deduction_predicate_logic/0009_sol.tex}
+         {3cm}
+
+
+
+
+
+\question{natural_deduction_predicate_logic/0010.tex}
+         {natural_deduction_predicate_logic/0010_sol.tex}
+         {3cm}
+
+
+\question{natural_deduction_predicate_logic/0012.tex}
+         {no_solution}
+         {3cm}
+
+
+\question{natural_deduction_predicate_logic/0013.tex}
+         {natural_deduction_predicate_logic/0013_sol.tex}
+         {3cm}
+
+
+\question{natural_deduction_predicate_logic/2003.tex}
+         {no_solution}
+         {3cm}
+\question{natural_deduction_predicate_logic/1003.tex}
+         {no_solution}
+         {3cm}
+\question{natural_deduction_predicate_logic/2002.tex}
+         {natural_deduction_predicate_logic/2002_sol.tex}
+         {3cm}
+\question{natural_deduction_predicate_logic/2001.tex}
+         {natural_deduction_predicate_logic/2001_sol.tex}
+         {3cm}
+\question{natural_deduction_predicate_logic/2005.tex}
+         {natural_deduction_predicate_logic/2005_sol.tex}
+         {3cm}
+         \ifsolution \clearpage\fi
+\question{natural_deduction_predicate_logic/2004.tex}
+         {natural_deduction_predicate_logic/2004_sol.tex}
+         {3cm}
+\question{natural_deduction_predicate_logic/2006.tex}
+         {natural_deduction_predicate_logic/2006_sol.tex}
+         {3cm}
+\question{natural_deduction_predicate_logic/2007.tex}
+         {no_solution}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/1001.tex}
+         {no_solution}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/1002.tex}
+         {natural_deduction_predicate_logic/1002_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/1004.tex}
+         {natural_deduction_predicate_logic/1004_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/1005.tex}
+         {natural_deduction_predicate_logic/1005_sol.tex}
+         {3cm}
+
+
+\question{natural_deduction_predicate_logic/1006.tex}
+         {natural_deduction_predicate_logic/1006_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/1007.tex}
+         {natural_deduction_predicate_logic/1007_sol.tex}
+         {3cm}
+
+
+\question{natural_deduction_predicate_logic/1008.tex}
+         {natural_deduction_predicate_logic/1008_sol.tex}
+         {3cm}
+\question{natural_deduction_predicate_logic/1009.tex}
+         {natural_deduction_predicate_logic/1009_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/1010.tex}
+         {natural_deduction_predicate_logic/1010_sol.tex}
+         {3cm}
+
+
+
+\question{natural_deduction_predicate_logic/1011.tex}
+         {natural_deduction_predicate_logic/1011_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/1012.tex}
+         {natural_deduction_predicate_logic/1012_sol.tex}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/1013.tex}
+         {no_solution}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/1014.tex}
+         {natural_deduction_predicate_logic/1014_sol.tex}
+         {3cm}
+
+
+\question{natural_deduction_predicate_logic/1015.tex}
+         {natural_deduction_predicate_logic/1015_sol.tex}
+         {3cm}
+
+
+\question{natural_deduction_predicate_logic/0005.tex}
+         {no_solution}
+         {3cm}
+
+\question{natural_deduction_predicate_logic/2008.tex}
+         {no_solution}
+         {3cm}
+\end{questionSection}

natural_deduction_predicate_logic/practical_questions/0_10_prac.tex

@@ -0,0 +1 @@
+\item \prac \textbf{[3.5 Point]} $\exists x \; P(x) \imp \exists x \; Q(x) \quad \ent \quad \exists x \; (P(x) \imp Q(x))$

natural_deduction_predicate_logic/practical_questions/0_1_prac.tex

@@ -0,0 +1,5 @@
+\item \prac \textbf{[2 Point]}
+  \begin{enumerate}
+    \item $(\forall x \; (\lnot A(x)) \lor (\exists x \; (B(x)) \quad \ent \quad \forall x \; (\lnot A(x) \lor B(x))$
+    \item $(\forall x \; (\lnot A(x)) \lor (\exists x \; (B(x)) \quad \ent \quad \exists x \; (\lnot A(x) \lor B(x))$
+  \end{enumerate}

natural_deduction_predicate_logic/practical_questions/0_2_prac.tex

@@ -0,0 +1 @@
+\item \prac \textbf{[2 Point]} $ \exists x P(x) \lor \exists x Q(x) \ent \exists x( P(x) \lor Q(x))$

natural_deduction_predicate_logic/practical_questions/0_3_prac.tex

@@ -0,0 +1 @@
+\item \prac \textbf{[3 Point]} $\exists b \; (a \imp B(b)) \quad \ent \quad a \imp \exists b \; B(b)$

natural_deduction_predicate_logic/practical_questions/0_4_prac.tex

@@ -0,0 +1 @@
+\item \prac \textbf{[1 Point]} $\ent \quad (x = y + y) \land (y = 1 \lor y = 2)$

natural_deduction_predicate_logic/practical_questions/0_5_prac.tex

@@ -0,0 +1 @@
+\item \prac \textbf{[3 Point]} $\exists x \; (S(x) \imp T(x)), \lnot T(z) \land \lnot T(y) \quad \ent \quad \lnot S(y)$

natural_deduction_predicate_logic/practical_questions/0_6_prac.tex

@@ -0,0 +1 @@
+\item \prac \textbf{[1 Point]} $\exists x \forall y \; f(x) = f(y) \quad \ent \quad \exists x \forall y \; x = y $

natural_deduction_predicate_logic/practical_questions/0_7_prac.tex

@@ -0,0 +1 @@
+\item \prac \textbf{[1 Point]} $\lnot \forall a \; \lnot \lnot (a = f(g(a))) \quad \ent \quad \lnot \lnot \exists a \; \lnot(a = f(g(a)))$

natural_deduction_predicate_logic/practical_questions/0_8_prac.tex

@@ -0,0 +1 @@
+\item \prac \textbf{[3 Point]} $\forall r \; U(r) \land \forall r \; (S(r) \imp T(r)) \quad \ent \quad \exists r \; \lnot T(x) \imp \exists r (\lnot S(r) \land U(r))$

natural_deduction_predicate_logic/practical_questions/0_9_prac.tex

@@ -0,0 +1 @@
+\item \prac \textbf{[3.5 Point]} $\exists a \; (P(a) \lor Q(a)),\quad \exists a \; P(a) \imp R(c),\quad \exists b \; Q(b) \imp R(c) \quad \ent \quad R(c)$

natural_deduction_predicate_logic/practical_questions/1_1_fol_lect.tex

@@ -0,0 +1 @@
+\item \lect $\forall x \; P(x) \land \forall x \; (P(y) \imp Q(x)) \quad \ent \quad Q(z)$

natural_deduction_predicate_logic/practical_questions/1_1_fol_lect_sol.tex

@@ -0,0 +1,9 @@
+\setlength\subproofhorizspace{1em}
+\begin{logicproof}{0}
+  \forall x \; P(x) \land \forall x \; (P(y) \imp Q(x))     & prem.\\
+  \forall x \; P(x)                                         & $\land \mathrm{e}_1$ 1\\
+  \forall x \; (P(y) \imp Q(x))                             & $\land \mathrm{e}_2$ 1\\
+  P(y)                                                      & $\forall \mathrm{e}$ 2\\
+  P(y) \imp Q(z)                                            & $\forall \mathrm{e}$ 3\\
+  Q(z)                                                      & $\imp \mathrm{e}$ 5,4
+\end{logicproof}

natural_deduction_predicate_logic/practical_questions/1_1_fol_self.tex

@@ -0,0 +1 @@
+\item \self $\forall x \; (P(x) \land Q(x)) \quad \ent \quad \forall x \; ( (Q(x) \lor R(x)) \land (R(x) \lor P(x)) )$

natural_deduction_predicate_logic/practical_questions/1_2_fol_lect.tex

@@ -0,0 +1 @@
+\item \lect $\forall x \; P(x) \lor \forall x \; Q(x) \quad \ent \quad \forall y \; (P(y) \lor Q(y))$

natural_deduction_predicate_logic/practical_questions/1_2_fol_lect_sol.tex

@@ -0,0 +1,21 @@
+\setlength\subproofhorizspace{1.7em}
+\begin{logicproof}{2}
+  \forall x \; P(x) \lor \forall x \; Q(x)     & prem.\\
+  \begin{subproof}
+    \forall x \; P(x)                          & ass.\\
+    \begin{subproof}
+      \llap{$t\enspace \;$} P(t)               & $\forall \mathrm{e}$ 2\\    
+      P(t) \lor Q(t)                           & $\lor \mathrm{i}_1$ 3
+    \end{subproof}
+    \forall y \; (P(y) \lor Q(y))               & $\forall \mathrm{i}$ 3-4
+  \end{subproof}
+  \begin{subproof}
+    \forall x \; Q(x)                          & ass.\\
+    \begin{subproof}
+      \llap{$s\enspace \;$} Q(s)               & $\forall \mathrm{e}$ 6\\    
+      P(s) \lor Q(s)                           & $\lor \mathrm{i}_2$ 7  
+    \end{subproof}
+    \forall y \; (P(y) \lor Q(y))               & $\forall \mathrm{i}$ 7-8
+  \end{subproof}
+ \forall y \; (P(y) \lor Q(y))                       & $\imp \mathrm{e}$ 1,2-5,6-9
+\end{logicproof}

natural_deduction_predicate_logic/practical_questions/1_2_fol_self.tex

@@ -0,0 +1 @@
+\item \self $\forall x \; (P(x)\lor Q(x)),\quad \forall x \; (\lnot P(x)) \quad \ent \quad \forall x \; (Q(x))$

natural_deduction_predicate_logic/practical_questions/2_1_fol_lect.tex

@@ -0,0 +1 @@
+\item \lect $\forall x \; (P(x) \imp Q(y)), \forall y \; (P(y) \land R(x)) \quad \ent \quad \exists x \; Q(x))$

natural_deduction_predicate_logic/practical_questions/2_1_fol_lect_sol.tex

@@ -0,0 +1,10 @@
+\setlength\subproofhorizspace{1em}
+\begin{logicproof}{0}
+  \forall x \; (P(x) \imp Q(y))     & prem.\\
+  \forall y \; (P(y) \land R(x))    & prem.\\
+  P(t) \imp Q(y)                    & $\forall \mathrm{e}$ 1\\
+  P(t) \land R(x)                  & $\forall \mathrm{e}$ 2\\
+  P(t)                              & $\land \mathrm{e}_1$ 4\\
+  Q(y)                              & $\imp \mathrm{e}$ 3\\
+  \exists x \; Q(x)                 & $\exists \mathrm{i}$ 6
+\end{logicproof}

natural_deduction_predicate_logic/practical_questions/2_1_fol_self.tex

@@ -0,0 +1 @@
+\item \self $\exists x \; (Q(x) \imp R(x)),\quad \exists x \; (P(x)\land Q(x)) \quad \ent \quad \exists x \; (P(x) \land R(x))$

natural_deduction_predicate_logic/practical_questions/2_2_fol_lect.tex

@@ -0,0 +1 @@
+\item \lect $\forall a \forall b \; (P(a) \land Q(b)) \quad \ent \quad \forall a \exists b \; (P(a) \lor Q(b))$

natural_deduction_predicate_logic/practical_questions/2_2_fol_lect_sol.tex

@@ -0,0 +1,12 @@
+\setlength\subproofhorizspace{1.1em}
+\begin{logicproof}{1}
+  \forall a \forall b \; (P(a) \land Q(b))                  & prem.\\
+  \begin{subproof}
+	  \llap{$t\enspace \;$} \forall b \; (P(s) \land Q(b))    & $\forall \mathrm{e}$ 1\\
+    P(s) \land Q(t)                                         & $\forall \mathrm{e}$ 2\\
+    P(s)                                                    & $\land \mathrm{e}_1$ 3\\
+    P(s) \lor Q(t)                                          & $\lor \mathrm{i}_1$ 4\\
+    \exists b \; (P(s) \lor Q(b))                           & $\exists \mathrm{i}$ 5
+  \end{subproof}
+  \forall a \exists b \; (P(a) \lor Q(b))                   & $\forall \mathrm{i}$ 2-6
+\end{logicproof}

natural_deduction_predicate_logic/practical_questions/2_2_fol_self.tex

@@ -0,0 +1 @@
+\item \self $\forall x \; (Q(x) \imp R(x)),\quad \exists x \; (P(x)\land Q(x)) \quad \ent \quad \exists x \; (P(x) \land R(x))$