added ndprop chapter

compile

@@ -104,7 +104,7 @@ compile_wrapper() {
 
 compile_chapter() {
   #for chapter in smtzthree proplogic satsolver ndpred predlogic ndpred smt bdd eqchecking symbenc temporal
-  for chapter in bdd satsolver proplogic
+  for chapter in ndprop
   do
     set_chapter "\\chapter${chapter}true"
     compile_wrapper "$chapter" "$@"

main.tex

@@ -78,6 +78,12 @@
   \pagebreak
 \fi
 
+\ifchapterndprop
+  \setsectionnum{3}
+  \section{Natural Deduction for Propositional Logic}
+  \input{natural_deduction_propositional_logic/natural_deduction_prop_logic.tex}
+  \pagebreak
+\fi
 
 %---------------------------------------------------------
 

natural_deduction_propositional_logic/0001.tex

@@ -0,0 +1 @@
+\item \lect $p, q, r \ent p \land (q \land r)$

natural_deduction_propositional_logic/0001_sol.tex

@@ -0,0 +1,9 @@
+This sequent is provable.
+
+\begin{logicproof}{2}
+    p & prem. \\
+    q & prem. \\
+    r & prem. \\
+    q \land r & $\land$i 2,3 \\
+    p \land (q \land r) & $\land$i 1,4
+\end{logicproof}

natural_deduction_propositional_logic/0002.tex

@@ -0,0 +1 @@
+\item \lect $p \land (q \land r) \ent q$

natural_deduction_propositional_logic/0002_sol.tex

@@ -0,0 +1,7 @@
+This sequent is provable.
+
+\begin{logicproof}{2}
+    p \land (q \land r) & prem. \\
+    q \land r & $\land$e2 1 \\
+    q & $\land$e1 2
+\end{logicproof}

natural_deduction_propositional_logic/0003.tex

@@ -0,0 +1 @@
+\item \lect $p \land q, \lnot q \land r \ent \lnot \lnot p \land \lnot \lnot r$

natural_deduction_propositional_logic/0003_sol.tex

@@ -0,0 +1,22 @@
+This sequent is provable.
+
+\emph{Solution 1:}
+\begin{logicproof}{2}
+    p \land q & prem. \\
+    \lnot q \land r & prem. \\
+    p & $\land$e1 1 \\
+    r & $\land$e2 2 \\
+    \lnot \lnot p & $\lnot \lnot$i 3 \\
+    \lnot \lnot r & $\lnot \lnot$i 4 \\
+    \lnot \lnot p \land \lnot \lnot r & $\land$i 5,6
+\end{logicproof}
+
+\emph{Solution 2:}
+\begin{logicproof}{2}
+    p \land q & prem. \\
+    \lnot q \land r & prem. \\
+    q & $\land$e2 1 \\
+    \lnot q & $\land$e1 2 \\
+    \bot & $\lnot$e 3,4 \\
+    \lnot \lnot p \land \lnot \lnot r & $\bot$e 5
+\end{logicproof}

natural_deduction_propositional_logic/0004.tex

@@ -0,0 +1 @@
+\item \lect $\lnot \lnot \lnot p \land q, \lnot \lnot r \ent r \land \lnot p \land \lnot \lnot q$

natural_deduction_propositional_logic/0004_sol.tex

@@ -0,0 +1,13 @@
+This sequent is provable.
+
+\begin{logicproof}{2}
+    \lnot \lnot \lnot p \land q & \prem \\
+    \lnot \lnot r & \prem \\
+    \lnot \lnot \lnot p & $\ande{1}1$ \\
+    q & $\ande{2}1$ \\
+    r & $\negnege2$ \\
+    \lnot p & $\negnege3$ \\
+    \lnot \lnot q & $\negnegi4$ \\
+    r \land \lnot p & $\andi 5,6$ \\
+    r \land \lnot p \land \lnot \lnot q & $\andi 8,7$
+\end{logicproof}

natural_deduction_propositional_logic/0005.tex

@@ -0,0 +1,4 @@
+\item \ifassignmentsheet \points{2}
+\else \prac
+\fi
+$p \land q, q \imp \lnot \lnot r \ent p \land r$

natural_deduction_propositional_logic/0005_sol.tex

@@ -0,0 +1,11 @@
+This sequent is provable.
+
+\begin{logicproof}{2}
+    p \land q & \prem \\
+    q \imp \lnot \lnot r & \prem \\
+    q & $\ande{2} 1$\\
+    \lnot \lnot r & $\impe 2,3$ \\
+    r & $\negnege 4$ \\
+    p & $\ande{1} 1$ \\
+    p \land r & $\andi 6,5$
+\end{logicproof}

natural_deduction_propositional_logic/0006.tex

@@ -0,0 +1 @@
+\item \lect $\lnot p \imp q, \lnot \lnot \lnot q \land r \ent p \land \lnot \lnot \lnot q$

natural_deduction_propositional_logic/0006_sol.tex

@@ -0,0 +1,11 @@
+This sequent is provable.
+
+\begin{logicproof}{2}
+    \lnot p \imp q & \prem \\
+    \lnot \lnot \lnot q \land r & \prem \\
+    \lnot \lnot \lnot q & $\ande{1} 2$ \\
+    \lnot q & $\negnege 3$ \\
+    \lnot\lnot p & $\MT 1,4$ \\
+    p & $\negnege 5$  \\
+    p \land \lnot \lnot \lnot q & $\andi 6,3$
+\end{logicproof}

natural_deduction_propositional_logic/0007.tex

@@ -0,0 +1,8 @@
+\item \self
+Translate the following reasoning into a sequent. If the sequent is valid, proof it using the rules of natural deduction.
+If the sequent is not valid, provide a counter example.
+  \begin{quote}
+    If I press the button, the window opens. \\
+    I pressed the button.\\
+    Therefore, the window is open.\\
+  \end{quote}

natural_deduction_propositional_logic/0007_sol.tex

@@ -0,0 +1,18 @@
+Translation: \\
+$p:$ \quad I press the button. \\
+$q:$ \quad The window is open.
+\begin{tabbing}
+    If I press the button, the window opens. \quad \= $p \imp q$ \\
+    I pressed the button. \> $p$ \\
+    The window is open. \> $q$
+\end{tabbing}
+
+\emph{Sequent:} \quad $p \imp q, p \vdash q$ \\
+
+This sequent is provable.
+
+\begin{logicproof}{1}
+    p \imp q & \prem \\
+    p & \prem \\
+    q & $\impe 1,2$
+\end{logicproof}

natural_deduction_propositional_logic/0008.tex

@@ -0,0 +1 @@
+\item \lect $p \imp (q \land r), q \imp s \ent p \imp (s \land r)$

natural_deduction_propositional_logic/0008_sol.tex

@@ -0,0 +1,15 @@
+This sequent is provable.
+
+\begin{logicproof}{2}
+    p \imp (q \land r) & \prem \\
+    q \imp s & \prem \\
+    \begin{subproof}
+        p & \assum \\
+        q \land r & $\impe 1,3$ \\
+        q & $\ande{1} 4$ \\
+        s & $\impe 2,5$ \\
+        r & $\ande{2} 4$ \\
+        s \land r & $\andi 6,7$
+    \end{subproof}
+    p \imp (s \land r) & $\impi 3-8$
+\end{logicproof}

natural_deduction_propositional_logic/0009.tex

@@ -0,0 +1 @@
+\item \lect $p \land q, r \imp s \ent (p \lor (r \imp s)) \land (q \lor ((t \lor r) \imp u))$

natural_deduction_propositional_logic/0009_sol.tex

@@ -0,0 +1,11 @@
+This sequent is provable.
+
+\begin{logicproof}{1}
+    p \land q & \prem \\
+    r \imp s & \prem \\
+    p & $\ande{1} 1$ \\
+    p \lor (r \imp s) & $\ori{1} 3$ \\
+    q & $\ande{2} 1$ \\
+    q \lor ((t \lor r) \imp u) & $\ori{1} 5$ \\
+    (p \lor (r \imp s)) \land (q \lor ((t \lor r) \imp u)) & $\andi 4,6$
+\end{logicproof}

natural_deduction_propositional_logic/0010.tex

@@ -0,0 +1 @@
+\item \lect $p \lor \lnot \lnot q, \lnot p \land \lnot q \ent s \lor \lnot t$

natural_deduction_propositional_logic/0010_sol.tex

@@ -0,0 +1,19 @@
+This sequent is provable.
+
+\begin{logicproof}{1}
+    p \lor \lnot \lnot q & \prem \\
+    \lnot p \land \lnot q & \prem \\
+    \begin{subproof}
+        p & \assum \\
+        \lnot p & $\ande{1} 2$ \\
+        \bot & $\nege 3,4$ \\
+        s \lor \lnot t & $\bote 5$
+    \end{subproof}
+    \begin{subproof}
+        \lnot \lnot q & \assum \\
+        \lnot q & $\ande{2} 2$ \\
+        \bot & $\nege 7,8$\\
+        s \lor \lnot t & $\bote 9$
+    \end{subproof}
+    s \lor \lnot t & $\ore 1, 3-6, 7-10$
+\end{logicproof}

natural_deduction_propositional_logic/0011.tex

@@ -0,0 +1 @@
+\item \lect $\lnot q \lor \lnot p \ent \lnot (q \land p)$

natural_deduction_propositional_logic/0011_sol.tex

@@ -0,0 +1,20 @@
+This sequent is provable.
+
+\begin{logicproof}{2}
+    \lnot q \lor \lnot p & \prem \\
+    \begin{subproof}
+        q \land p & \assum \\
+        \begin{subproof}
+            \lnot q & \assum \\
+            q & $\ande{1} 2$ \\
+            \bot & $\nege 3,4$
+        \end{subproof}
+        \begin{subproof}
+            \lnot p & \assum \\
+            p & $\ande{2} 2$ \\
+            \bot & $\nege 6,7$
+        \end{subproof}
+        \bot & $\ore 1, 3-5, 6-8$
+    \end{subproof}
+    \lnot (q \land p) & $\negi 2-9$
+\end{logicproof}

natural_deduction_propositional_logic/0012.tex

@@ -0,0 +1 @@
+\item \lect $\ent ((p \imp q) \imp p) \imp p$

natural_deduction_propositional_logic/0012_sol.tex

@@ -0,0 +1,20 @@
+This sequent is provable.
+
+\begin{logicproof}{3}
+    \begin{subproof}
+        (p \imp q) \imp p & \assum \\
+        \begin{subproof}
+            \lnot p & \assum \\
+            \lnot (p \imp q) & $\MT 1,2$ \\
+            \begin{subproof}
+                p & \assum \\
+                \bot & $\nege 2,4$ \\
+                q & $\bote 5$
+            \end{subproof}
+            p \imp q & $\impi 4-6$ \\
+            \bot & $\nege 3,7$
+        \end{subproof}
+        p & $\PBC 2-8$
+    \end{subproof}
+    ((p \imp q) \imp p) \imp p & $\impi 1-9$
+\end{logicproof}

natural_deduction_propositional_logic/0013.tex

@@ -0,0 +1,2 @@
+\item \points{4}
+$\lnot (q \land p) \ent \lnot q \lor \lnot p$

natural_deduction_propositional_logic/0014.tex

@@ -0,0 +1 @@
+\item \lect $p \rightarrow q,  q \rightarrow r \ent r$.

natural_deduction_propositional_logic/0014_sol.tex

@@ -0,0 +1,5 @@
+This sequent is not provable.
+
+$\mathcal{M} : p = F, q = F, r = F$ \\
+$\mathcal{M} \models p \imp q, q \imp r$ \\
+$\mathcal{M} \nmodels r$

natural_deduction_propositional_logic/0015.tex

@@ -0,0 +1,7 @@
+\item \lect Translate the following reasoning into a sequent. If the sequent is valid, proof it using the rules of natural deduction.
+If the sequent is not valid, provide a counter example.
+  \begin{quote}
+    If I press the button, the window opens. \\
+    The window is open.\\
+    Therefore, I pressed the button.\\
+  \end{quote}

natural_deduction_propositional_logic/0015_sol.tex

@@ -0,0 +1,16 @@
+Translation: \\
+$p:$ \quad Press button. \\
+$q:$ \quad Open window. 
+\begin{tabbing}
+    If I press the button, the window opens. \quad \= $p \imp q$ \\
+    The window is open. \> $q$ \\
+    Therefore, I pressed the button. \> $\vdash p$ 
+\end{tabbing}
+
+\emph{sequent:} \quad $p \imp q, q \vdash p$ \\
+
+This sequent is not provable.
+
+$\mathcal{M} : p = F, q = T$ \\
+$\mathcal{M} \models p \imp q, q$ \\
+$\mathcal{M} \nmodels p$

natural_deduction_propositional_logic/0016.tex

@@ -0,0 +1 @@
+\item $x \land (y \land z) \ent (x \land y) \land z$

natural_deduction_propositional_logic/0017.tex

@@ -0,0 +1 @@
+\item \self $\lnot \lnot p \land \lnot \lnot q, r \land s \ent (p \land r) \land \lnot \lnot s$

natural_deduction_propositional_logic/0017_sol.tex

@@ -0,0 +1,11 @@
+\begin{logicproof}{2}
+    \lnot \lnot p \land \lnot \lnot q & \prem \\
+    r \land s & \prem \\
+    \lnot \lnot p & $\ande{1} 1$ \\
+    p & $\lnot \nege 3$ \\
+    r & $\ande{1} 2$ \\
+    s & $\ande{2} 2$ \\
+    \lnot \lnot s & $\negnegi 6$ \\
+    p \land r & $\andi 4,5$ \\
+    (p \land r) \land \lnot \lnot s & $\andi 8,7$
+\end{logicproof}

natural_deduction_propositional_logic/0018.tex

@@ -0,0 +1 @@
+\item \self $(p \imp q) \land (q \imp r), p \ent \lnot \lnot r \land \lnot p$

natural_deduction_propositional_logic/0019.tex

@@ -0,0 +1 @@
+\item \self $(\lnot p \imp q) \land (q \imp r), \lnot r \ent \lnot \lnot \lnot r \land \lnot p$

natural_deduction_propositional_logic/0019_sol.tex

@@ -0,0 +1,4 @@
+This sequent is not provable, counter example: \\
+$\mathcal{M} : p = T, q = F, r = F$ \\
+$\mathcal{M} \models (\lnot p \implies q) \land (q \implies r), \lnot r$ \\
+$\mathcal{M} \nmodels \lnot \lnot \lnot r \land \lnot p$

natural_deduction_propositional_logic/0020.tex

@@ -0,0 +1 @@
+\item \self $(p \imp q) \imp r \ent \lnot r \land \lnot s \imp \lnot (p \imp q)$

natural_deduction_propositional_logic/0020_sol.tex

@@ -0,0 +1,10 @@
+\begin{logicproof}{2}
+(p \implies q)
+    \implies r & \prem \\
+    \begin{subproof}
+        \lnot r \land \lnot s & \assum \\
+        \lnot r & $\ande{1} 2$ \\
+        \lnot (p \implies q) & $\MT 1,3$
+    \end{subproof}
+    \lnot r \land \lnot s \implies \lnot (p \implies q) & $\impi 2-4$
+\end{logicproof}

natural_deduction_propositional_logic/0021.tex

@@ -0,0 +1 @@
+\item \self $p \imp q \ent (r \imp p) \imp (r \imp q)$

natural_deduction_propositional_logic/0021_sol.tex

@@ -0,0 +1,13 @@
+\begin{logicproof}{2}
+    p \implies q & \prem \\
+    \begin{subproof}
+        r \implies p & \assum \\
+        \begin{subproof}
+            r & \assum \\
+            p & $\impe 2,3$ \\
+            q & $\impe 1,4$
+        \end{subproof}
+        r \implies q & $\impi 3-5$
+    \end{subproof}
+    (r \implies p) \implies (r \implies q) & $\impi 2-6$
+\end{logicproof}

natural_deduction_propositional_logic/0022.tex

@@ -0,0 +1 @@
+\item \self $p \imp q, p \land (r \lor q) \ent (q \imp p) \imp ((s \land t) \lor q) \land (r \lor q)$

natural_deduction_propositional_logic/0022_sol.tex

@@ -0,0 +1,13 @@
+\begin{logicproof}{2}
+		p \implies q & \prem \\
+		p \land (r \lor q) & \prem \\
+		\begin{subproof}
+			q \implies p & \assum \\
+			r \lor q & $\ande{2} 2$ \\
+			p & $\ande{1} 2$ \\
+			q & $\impe 1,5$ \\
+      (s \land t) \lor q & $\ori{2} 6$ \\
+			((s \land t) \lor q) \land (r \lor q) & $\andi 7,4$
+		\end{subproof}
+		(q \implies p) \implies ((s \land t) \lor q) \land (r \lor q) & $\impi 3-7$
+	\end{logicproof}

natural_deduction_propositional_logic/0023.tex

@@ -0,0 +1 @@
+\item \self $p \lor q, \neg p \lor r \ent q \lor r$

natural_deduction_propositional_logic/0023_sol.tex

@@ -0,0 +1,22 @@
+\begin{logicproof}{2}
+    p \lor q & \prem \\
+    \lnot p \lor r & \prem \\
+    \begin{subproof}
+        p & \assum \\
+        \begin{subproof}
+            \lnot p & \assum \\
+            \false & $\nege 3,4$ \\
+            q \lor r & $\bote 5$
+        \end{subproof}
+        \begin{subproof}
+            r & \assum \\
+            q \lor r & $\ori{2} 7$
+        \end{subproof}
+        q \lor r & $\ore 2,4-6,7-8$
+    \end{subproof}
+    \begin{subproof}
+        q & \assum \\
+        q \lor r & $\ori{1} 10$
+    \end{subproof}
+    q \lor r & $\ore 1,3-9,10-11$
+\end{logicproof}

natural_deduction_propositional_logic/0024.tex

@@ -0,0 +1 @@
+\item \self $p \imp q, p \land r \lor q \ent (q \imp p) \imp ((s \land t) \lor q) \land (r \lor q)$

natural_deduction_propositional_logic/0024_sol.tex

@@ -0,0 +1,30 @@
+\begin{logicproof}{2}
+    p \implies q & \prem \\
+    (p \land r) \lor q & \prem \\
+    \begin{subproof}
+        q \implies p & \assum \\
+        \begin{subproof}
+            p \land r & \assum \\
+            r & $\ande{2} 4$ \\
+            r \lor q & $\ori{1} 5$
+        \end{subproof}
+        \begin{subproof}
+            q & \assum \\
+            r \lor q & $\ori{2} 7$
+        \end{subproof}
+        r \lor q & $\ore 2,4-6,7-8$ \\
+        \begin{subproof}
+            p \land r & \assum \\
+            p & $\ande{1} 10 $\\
+            q & $\impe  1,11$ \\
+            (s \land t) \lor q & $\ori{2} 12$
+        \end{subproof}
+        \begin{subproof}
+            q & \assum \\
+            (s \land t) \lor q & $\ori{2} 14$
+        \end{subproof}
+        (s \land t) \lor q & $\ore 2,10-13,14-15 $\\
+        ((s \land t) \lor q) \land (r \lor q) & $\andi 16,9$
+    \end{subproof}
+    (q \implies p) \implies ((s \land t) \lor q) \land (r \lor q) & $\impi 3-17$
+\end{logicproof}

natural_deduction_propositional_logic/0025.tex

@@ -0,0 +1 @@
+\item \self $p \lor q, p \imp r, \lnot s \imp \lnot q \ent r \lor s$

natural_deduction_propositional_logic/0025_sol.tex

@@ -0,0 +1,16 @@
+\begin{logicproof}{2}
+    p \lor q & \prem \\
+    p \implies r & \prem \\
+    \lnot s \implies \lnot q & \prem \\
+    \begin{subproof}
+        p & \assum \\
+        r & $\impe 4,2$ \\
+        r \lor s & $\ori{1} 5$
+    \end{subproof}
+    \begin{subproof}
+        q & \assum \\
+        s & $\MT 3,7$ \\
+        r \lor s & $\ori{2} 8$
+    \end{subproof}
+    r \lor s & $\ore 1,4-6,7-9$
+\end{logicproof}

natural_deduction_propositional_logic/0027.tex

@@ -0,0 +1,8 @@
+\item \self
+Translate the following reasoning into a sequent. If the sequent is valid, proof it using the rules of natural deduction.
+If the sequent is not valid, provide a counter example.
+  \begin{quote}
+    If I press the button, the window opens. \\
+    The window is not open.\\
+    Therefore, I didn't press the button.\\
+  \end{quote}

natural_deduction_propositional_logic/0027_sol.tex

@@ -0,0 +1,16 @@
+$b = $ I press the button. \\
+$w = $ The window is open. \\
+
+\bigskip
+
+$b \implies w, \lnot w \entails \lnot b$
+\begin{logicproof}{2}
+    b \implies w & \prem \\
+    \lnot w & \prem \\
+    \begin{subproof}
+        b & \assum \\
+        w & $\impe 1,3$ \\
+        \false & $\nege 2,4$
+    \end{subproof}
+    \lnot b & $\negi 3-5$
+\end{logicproof}

natural_deduction_propositional_logic/0028.tex

@@ -0,0 +1 @@
+\item \self $\lnot q \lor p \ent q \imp (p \lor r)$

natural_deduction_propositional_logic/0028_sol.tex

@@ -0,0 +1,17 @@
+\begin{logicproof}{2}
+    \lnot q \lor p & \prem \\
+    \begin{subproof}
+        q & \assum \\
+        \begin{subproof}
+            \lnot q & \assum \\
+            \false & $\nege 2,3$ \\
+            p \lor r & $\bote 4$
+        \end{subproof}
+        \begin{subproof}
+            p & \assum \\
+            p \lor r & $\ori{1} 6$
+        \end{subproof}
+        p \lor r & $\ore 1,3-5,6-7$
+    \end{subproof}
+    q \implies (p \lor r) & $\impi 2-8$
+\end{logicproof}

natural_deduction_propositional_logic/0029.tex

@@ -0,0 +1 @@
+\item \self $p \imp (q \lor r), \lnot q \land \lnot r \ent \lnot p$

natural_deduction_propositional_logic/0029_sol.tex

@@ -0,0 +1,20 @@
+\begin{logicproof}{2}
+    p \implies (q \lor r) & \prem \\
+    \lnot q \land \lnot r & \prem \\
+    \begin{subproof}
+        p & \assum \\
+        q \lor r & $\impe 1,3$ \\
+        \begin{subproof}
+            q & \assum \\
+            \lnot q & $\ande{1} 2$ \\
+            \false & $\nege 5,6$
+        \end{subproof}
+        \begin{subproof}
+            r & \assum \\
+            \lnot r & $\ande{2} 2$ \\
+            \false & $\nege 8,9$
+        \end{subproof}
+        \false & $\ore 4,5-7,8-10$
+    \end{subproof}
+    \lnot p & $\negi 3-11$
+\end{logicproof}

natural_deduction_propositional_logic/0030.tex

@@ -0,0 +1 @@
+\item \self $\lnot (q \lor p) \ent \lnot q \land p$

natural_deduction_propositional_logic/0030_sol.tex

@@ -0,0 +1,4 @@
+This sequent is not provable, counter example: \\
+$\mathcal{M} : p = F, q = F$ \\
+$\mathcal{M} \models \lnot (q \lor p)$ \\
+$\mathcal{M} \nmodels \lnot q \land p$

natural_deduction_propositional_logic/0031.tex

@@ -0,0 +1 @@
+\item \self $\ent (p \imp q) \lor (q \imp r)$

natural_deduction_propositional_logic/0031_sol.tex

@@ -0,0 +1,23 @@
+\begin{logicproof}{2}
+    q \lor \lnot q & $\LEM$ \\
+    \begin{subproof}
+        q & \assum\\
+        \begin{subproof}
+            p & \assum\\
+            q & $\copying 2$
+        \end{subproof}
+        p \imp q & $\impi 3-4$ \\
+        (p \to q) \lor (q \to r) & $\ori{1} 5$
+    \end{subproof}
+    \begin{subproof}
+        \lnot q & \assum\\
+        \begin{subproof}
+            q & \assum\\
+            \bot & $\nege 7,8$ \\
+            r & $\bote 9$
+        \end{subproof}
+        q \imp r & $\impi 8-10$ \\
+        (p \imp q) \lor (q \imp r) & $\ori{2} 11$
+    \end{subproof}
+    (p \to q) \lor (q \to r) & $\ore 1, 2-6,7-12$
+\end{logicproof}

natural_deduction_propositional_logic/0032.tex

@@ -0,0 +1 @@
+\item \self $(p \imp q) \land (q \imp p) \ent (p \land q) \lor (\lnot p \land \lnot q)$

natural_deduction_propositional_logic/0032_sol.tex

@@ -0,0 +1,20 @@
+\begin{logicproof}{2}
+(p \implies q)
+    \land (q \implies p) & \prem \\
+    p \lor \lnot p & $\LEM$ \\
+    \begin{subproof}
+        p & \assum \\
+        p \implies q & $\ande{1} 1$ \\
+        q & $\impe 3,4$ \\
+        p \land q & $\andi 3,5$ \\
+        (p \land q) \lor (\lnot p \land \lnot q) & $\ori{1} 6$
+    \end{subproof}
+    \begin{subproof}
+        \lnot p & \assum \\
+        q \implies p & $\ande{2} 1$ \\
+        \lnot q & $\MT 8,9$ \\
+        \lnot p \land \lnot q & $\andi 8,10$ \\
+        (p \land q) \lor (\lnot p \land \lnot q) & $\ori{2} 11$
+    \end{subproof}
+    (p \land q) \lor (\lnot p \land \lnot q) & $\ore 2,3-7,8-12$
+\end{logicproof}

natural_deduction_propositional_logic/0033.tex

@@ -0,0 +1 @@
+\item \self $\lnot (p \lor \lnot q) \ent p$

natural_deduction_propositional_logic/0033_sol.tex

@@ -0,0 +1,4 @@
+This sequent is not provable, counter example: \\
+$\mathcal{M} : p = F, q = T$ \\
+$\mathcal{M} \models \lnot (p \lor \lnot q)$ \\
+$\mathcal{M} \nmodels p$

natural_deduction_propositional_logic/0035.tex

@@ -0,0 +1 @@
+\item \self $p \implies q \vdash ((p \lor q) \implies p) \land (p \implies (p \lor q))$

natural_deduction_propositional_logic/0035_sol.tex

@@ -0,0 +1,4 @@
+This sequent is not provable, counter example: \\
+$\mathcal{M} : p = F, q = T$ \\
+$\mathcal{M} \models p \implies q$ \\
+$\mathcal{M} \nmodels ((p \lor q) \implies p) \land (p \implies (p \lor q))$

natural_deduction_propositional_logic/0036.tex

@@ -0,0 +1 @@
+\item \self $p \lor q, \lnot q \lor r \ent r$

natural_deduction_propositional_logic/0036_sol.tex

@@ -0,0 +1,4 @@
+This sequent is not provable, counter example: \\
+$\mathcal{M} : p = T, q = F, r = F$ \\
+$\mathcal{M} \models p \lor q, \lnot q \lor r$ \\
+$\mathcal{M} \nmodels r$

natural_deduction_propositional_logic/0037.tex

@@ -0,0 +1 @@
+\item \self $(p \land q) \imp (\lnot r \land \lnot s), \lnot r \land \lnot s \ent p$

natural_deduction_propositional_logic/0037_sol.tex

@@ -0,0 +1,4 @@
+This sequent is not provable, counter example: \\
+$\mathcal{M} : p = F, q = F, r = F, s = F$ \\
+$\mathcal{M} \models (p \land q) \implies (\lnot r \land \lnot s), \lnot r \land \lnot s$ \\
+$\mathcal{M} \nmodels p$

natural_deduction_propositional_logic/0038.tex

@@ -0,0 +1,3 @@
+\item \lect
+Give the definition of a sequent.
+Give an example of a sequent and name the parts the sequent consists of.

natural_deduction_propositional_logic/0038_sol.tex

@@ -0,0 +1,10 @@
+A sequent is an expression of the form 
+
+\begin{center}
+\setlength{\abovedisplayskip}{-15pt}
+$\phi_1, \phi_2,\!..., \phi_n \ent \psi.$
+\end{center}
+
+$\phi_1, \phi_2,\!..., \phi_n$ are called premises. $\psi$ is called the conclusion.
+The premises entail the conclusion.
+This means that for any valid sequence, we can proof that the conclusion follows from the premises. 

natural_deduction_propositional_logic/0039.tex

@@ -0,0 +1 @@
+\item \lect State the \emph{AND-introduction} rule ($\land$i). Explain how the rule works.

natural_deduction_propositional_logic/0039_sol.tex

@@ -0,0 +1,12 @@
+\begin{center}
+\vspace{-0.5cm}
+\begin{prooftree}
+\AxiomC{$ \varphi $}
+\AxiomC{$ \psi $}
+\RightLabel{$ \land $i}
+\BinaryInfC{$ \varphi \land \psi $}
+\end{prooftree}
+\end{center}
+
+If we have two formulas that are known to be true separately, then we can
+conclude that the conjunction of the two premises must also be true.

natural_deduction_propositional_logic/0040.tex

@@ -0,0 +1,3 @@
+\item \self Provide a natural deduction proof for the following sequent without using the \emph{Modus Tollens} rule:
+
+$$\varphi \imp \psi, \lnot\psi \entails \lnot\varphi$$

natural_deduction_propositional_logic/0040_sol.tex

@@ -0,0 +1,10 @@
+\begin{logicproof}{2}
+    \lnot\psi & \prem \\
+    \varphi \imp \psi & \prem \\
+    \begin{subproof}
+        \varphi & \assum \\
+        \psi    & $\impe 1,2$ \\
+        \bot    & $\nege 1,4$
+    \end{subproof}
+    \lnot\varphi & $\negi 3-5$
+\end{logicproof}

natural_deduction_propositional_logic/0041.tex

@@ -0,0 +1,3 @@
+\item \self
+Explain the concept of boxes in deduction rules and why they are needed. What does it mean if you make an \textit{assumption} within a box?
+Where is this assumption valid?

natural_deduction_propositional_logic/0041_sol.tex

@@ -0,0 +1,4 @@
+
+Assumptions assume that within the box, a certain formula holds that can be used to prove something within the box.
+The assumption is only valid within the box.
+Therefore, any formulas proven within the box are only valid inside the box, because they are proven under a given assumption that is only valid in the scope of the box.

natural_deduction_propositional_logic/0042.tex

@@ -0,0 +1 @@
+\item \self Why are there two rules for the \textit{$\lor$-introduction} rule. Explain, why you are able to connect any formula to a certain formula $\phi$ using the connective $\lor$.

natural_deduction_propositional_logic/0042_sol.tex

@@ -0,0 +1,20 @@
+\begin{center}
+  \begin{minipage}{0.2\textwidth}
+    \begin{prooftree}
+      \AxiomC{$ \varphi$}
+      \RightLabel{$ \ori1$}
+      \UnaryInfC{$ \varphi \lor \psi$}
+    \end{prooftree}
+  \end{minipage}
+  \begin{minipage}{0.2\textwidth}
+    \begin{prooftree}
+      \AxiomC{$ \varphi$}
+      \RightLabel{$ \ori2$}
+      \UnaryInfC{$ \psi \lor \varphi$}
+    \end{prooftree}
+  \end{minipage}
+\end{center}
+
+If we know that $\varphi$ holds, we can derive that $\varphi \lor \psi$ holds and that
+$\psi \lor \varphi$ holds. This is true for any $\psi$.
+

natural_deduction_propositional_logic/0043.tex

@@ -0,0 +1 @@
+\item \self Explain the \emph{OR-elimination} (\textit{$\lor$-e}) rule of the natural deduction calculus. In particular, why does it rule require two boxes?

natural_deduction_propositional_logic/0043_sol.tex

@@ -0,0 +1,43 @@
+From a given formula $\varphi \lor \psi$, we want to proof some other formula $\chi$.
+We only know that $\varphi$ \emph{or} $\psi$ holds. It could be that both of them are true,
+but it could also be that only $\psi$ is true, or only $\varphi$ is true.
+Sine we don't know which sub-formula is true, we have to give two separate proofs:
+\begin{itemize}
+    \item First box: We assume $\varphi$ is true and need to find a proof for $\chi$.
+    \item Second box: We assume $\psi$ is true and need to find a proof for $\chi$.
+\end{itemize}
+Only if we can prove $\chi$ in the first and in the second box, then we can conclude that $\chi$ holds also outside of the box.
+
+The $\ore$ rules says that we can only derive $\chi$ from $ \varphi \lor \psi$ if we can derive $\chi$
+from the assumption $ \varphi$ as well as from the assumption $\psi$.
+Formally the rule is written as:
+\begin{center}
+  \begin{prooftree}
+    \AxiomC{\begin{tabular}{l}
+      \vspace*{0.95ex}\\
+      \vspace*{0.95ex}\\
+      $ \varphi \lor \psi $\\
+    \end{tabular}}
+    \AxiomC{\begin{tabular}{|l|}
+      \hline
+      $ \varphi $ ass.\\
+      \hspace*{0.2em}$ \vdots $\\
+      $ \chi  $\\
+      \hline
+    \end{tabular}}
+    \AxiomC{\begin{tabular}{|l|}
+      \hline
+      $ \psi $ ass.\\
+      \hspace*{0.2em}$ \vdots $\\
+      $ \chi  $\\
+      \hline
+    \end{tabular}}
+    \RightLabel{$ \ore$}
+    \TrinaryInfC{$ \chi $}
+  \end{prooftree}
+\end{center}
+
+
+
+
+

natural_deduction_propositional_logic/0044.tex

@@ -0,0 +1 @@
+\item \self Explain in your own words, how to proof a sequent in the natural deduction calculus. What steps do you need to take and which tips can be helpful when solving such proofs?

natural_deduction_propositional_logic/0044_sol.tex

@@ -0,0 +1,14 @@
+\begin{itemize}
+    \item \textbf{Start a proof.} At the top of your page write the premises, at the bottom write the conclusion.
+    \item \textbf{Work in both directions to fill the gap.} Work from the top to the bottom
+by working with the premises, and simultaneously work upwards by using the conclusion.
+    \item \textbf{Look at the conclusion first.} If the conclusion is of the form $\varphi \rightarrow \psi$, then immediately apply $\impi$.
+    You still have to fill the gap in the box, but you have an extra assumption to work with and a simpler conclusion you try to reach. Similar, if your conclusion is of fhe form $\neg \varphi$, apply $\negi$ to make your life easier.
+    \item \textbf{Assumption boxes.} At any time you can introduce a formula as assumption, by choosing a proof rule that opens the box.
+The box defines the scope of the assumption. By opening a box you introduce an assumption.
+But don't forget, you have to close the box precisely as
+defined by the applied proof rule.
+    \item \textbf{What rule should you apply?} The rules $\impi$ and $\negi$  make your life easier, apply them whenever you can.
+    There is no easy recipe for when to use the other rules. The best way to get the hang of it is doing many proofs
+    by yourself.
+\end{itemize}

natural_deduction_propositional_logic/0045.tex

@@ -0,0 +1,2 @@
+\item \lect "Natural deduction for propositional logic is \emph{sound} and
+    \emph{complete}." Explain in your own words what this means.

natural_deduction_propositional_logic/0045_sol.tex

@@ -0,0 +1,13 @@
+\begin{itemize}
+  \item \emph{Natural deduction for propositional logic is sound. Therefore, any sequent that can be proven is a correct semantic entailment.}
+
+    Natural deduction is sound. This means that any sequent $\varphi_1, \varphi_2, \dots \entails \psi$  that is provable states a correct semantic entailment $\varphi_1, \varphi_2, \dots \models \psi$.
+    %Conversely, if the semantic entailmant relation does not hold for a statement, the according sequent is not provable.
+    A correct semantic entailment tells us that under all models that satisfy $\varphi_i$ for all $i$ the conclusion $\psi$ evaluates to true.
+
+    In short: Anything that is provable by natural deduction is true with respect to semantics.
+
+  \item \emph{Natural deduction for propositional logic is complete. Therefore, any sequent that is a correct semantic entailment can be proven.}
+
+    Natural deduction is complete. This means that for any statement that is true, i.e. the statement is a correct semantic entailment, there exists a proof.
+\end{itemize}

natural_deduction_propositional_logic/0046.tex

@@ -0,0 +1,2 @@
+
+\item \lect How can you show that a sequent is not valid? Is this a consequence of soundness or completeness. Explain your answer.

natural_deduction_propositional_logic/0046_sol.tex

@@ -0,0 +1,7 @@
+In order to show that a sequent is not valid, we provide a \emph{counter example}, which is a model that satisfies all premises but falsifies the conclusion.
+
+This is a consequence of soundness. We know from the definition of soundness that
+
+$$\varphi_1, \varphi_2,\!..., \varphi_n \nmodels \psi \qquad \Rightarrow \qquad \varphi_1, \varphi_2,\!..., \varphi_n \nvdash \psi$$
+
+A counterexample is enough to tell us that the left-hand side of this implication is true, hence the sequent is not valid.

natural_deduction_propositional_logic/0047.tex

@@ -0,0 +1 @@
+\item \self Explain the \emph{implication-introduction} rule ($\imp$i).

natural_deduction_propositional_logic/0048.tex

@@ -0,0 +1,2 @@
+\item \self Explain the \textit{$\bot$-elimination} rule of the natural deduction
+    calculus. Why can you deduce a formula $\phi$ from something, that is wrong?

natural_deduction_propositional_logic/0049.tex

@@ -0,0 +1 @@
+\item \self Derive the \textit{Proof-By-Contradiction}-rule from the \textit{$\lnot$-introduction} rule.

natural_deduction_propositional_logic/0050.tex

@@ -0,0 +1,2 @@
+\item \self Explain what it means that natural deduction for propositional logic is \textit{sound}. What is the difference to \emph{completeness}?
+

natural_deduction_propositional_logic/0051.tex

@@ -0,0 +1 @@
+\item \self Explain what it means that natural deduction for propositional logic is \textit{sound}. What is the difference to \emph{completeness}?

natural_deduction_propositional_logic/0052.tex

@@ -0,0 +1 @@
+\item \self Given an invalid sequent, how do you show its invalidity?

natural_deduction_propositional_logic/0053.tex

@@ -0,0 +1,9 @@
+\item \lect Look at the following statements and tick them if they are true.
+
+\begin{itemize}
+\item[$\square$] In a sequent, premises entail a conclusion.
+\item[$\square$] In a sequent, conclusions entail a premise.
+\item[$\square$] A sequent is valid, independent on whether a proof can be found.
+\item[$\square$] A sequent is valid, if a proof for it can be found.
+
+\end{itemize}

natural_deduction_propositional_logic/0053_sol.tex

@@ -0,0 +1,9 @@
+\item \lect Look at the following statements and tick them if they are true.
+
+\begin{itemize}
+\item[$\ticked$] In a sequent, premises entail a conclusion.
+\item[$\square$] In a sequent, conclusions entail a premise.
+\item[$\square$] A sequent is valid, independent on whether a proof can be found.
+\item[$\ticked$] A sequent is valid, if a proof for it can be found.
+
+\end{itemize}

natural_deduction_propositional_logic/0056.tex

@@ -0,0 +1,9 @@
+\item \self Look at the following statements and tick them if they are true.
+
+\begin{itemize}
+\item[$\square$] Any sequent that is a correct semantic entailment can be proven.
+\item[$\square$] Any sequent that can be proven is a correct semantic entailment.
+\item[$\square$] If a sequent is not provable, the  semantic entailment relation does hold.
+\item[$\square$] If for a sequent the semantic entailment relation does not hold, it cannot be proven with natural deduction.
+
+\end{itemize}

natural_deduction_propositional_logic/0057.tex

@@ -0,0 +1,27 @@
+\item \self Natural deduction for propositional logic is sound and
+    complete. In the following list, mark each statement with either
+    \textbf{S}, \textbf{C}, \textbf{B}, or \textbf{N}, depending on
+    whether the corresponding statement follows from
+    \textbf{S}oundness, \textbf{C}ompleteness, \textbf{B}oth, or
+    \textbf{N}either.
+    (Note: If a statement is in itself factually wrong, or has nothing to do with soundness and completeness, mark it
+    \textbf{N}, since it follows from neither soundness nor completeness.)
+
+\begin{itemize}
+\item[\Large{$\square$}] There is no correct sequent for which
+    there is no proof.
+\item[\Large{$\square$}] Every sequent has a proof.
+\item[\Large{$\square$}] If all models that satisfy the premise(s)
+    of a given sequent also satisfy the conclusion of the
+    sequent, there exists a proof for the sequent.
+\item[\Large{$\square$}] A sequent has a proof if and only if it
+    is semantically correct.
+\item[\Large{$\square$}] An incorrect sequent does not have a
+    proof.
+\item[\Large{$\square$}] Every propositional formula is either
+    valid or not valid.
+\item[\Large{$\square$}] If a model satisfies the premise(s) of a
+    given sequent, but does not satisfy the conclusion of the
+    sequent, it is not possible to construct a proof for the
+    sequent.
+\end{itemize}

natural_deduction_propositional_logic/0058.tex

@@ -0,0 +1,27 @@
+\item \self Natural deduction for propositional logic is sound and
+    complete. In the following list, mark each statement with either
+    \textbf{S}, \textbf{C}, \textbf{B}, or \textbf{N}, depending on
+    whether the corresponding statement follows from
+    \textbf{S}oundness, \textbf{C}ompleteness, \textbf{B}oth, or
+    \textbf{N}either.
+    (Note: If a statement is in itself factually wrong, or has nothing to do with soundness and completeness, mark it
+    \textbf{N}, since it follows from neither soundness nor completeness.)
+
+\begin{itemize}
+\item[\Large{$\square$}] A sequent has a proof if and only if it
+    is semantically correct.
+\item[\Large{$\square$}] If a model satisfies the premise(s) of a
+    given sequent, but does not satisfy the conclusion of the
+    sequent, it is not possible to construct a proof for the
+    sequent.
+\item[\Large{$\square$}] There is no correct sequent for which
+    there is no proof.
+\item[\Large{$\square$}] Every sequent has a proof.
+\item[\Large{$\square$}] An incorrect sequent does not have a
+    proof.
+\item[\Large{$\square$}] Every propositional formula is either
+    valid or not valid.
+\item[\Large{$\square$}] If all models that satisfy the premise(s)
+    of a given sequent also satisfy the conclusion of the
+    sequent, there exists a proof for the sequent.
+\end{itemize}

natural_deduction_propositional_logic/0059.tex

@@ -0,0 +1 @@
+\item \self $(p \imp (q \imp r)) \land (q \imp (r \imp s)) \ent p \imp (q \imp s)$

natural_deduction_propositional_logic/0059_sol.tex

@@ -0,0 +1,19 @@
+This sequent is provable.
+
+\begin{logicproof}{2}
+    (p \imp (q \imp r)) \land (q \imp (r \imp s)) & \prem \\
+    \begin{subproof}
+        p & \assum \\
+        p \imp (q \imp r) & $\ande{1} 1$ \\
+        q \imp (r \imp s) & $\ande{2} 1$ \\
+        q \imp r & $\impe 2,3$ \\
+        \begin{subproof}
+            q & \assum \\
+            r & $\impe 5,6$\\
+            r \imp s & $\impe 4,6$\\
+            s & $\impe 7,8$
+        \end{subproof}
+        q \imp s & $\impi 6-9$
+    \end{subproof}
+    p \imp (q \imp s) & $\impi 2-10$
+\end{logicproof}