diff --git a/compile b/compile index cc3d758..4e82664 100755 --- a/compile +++ b/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 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" "$@" diff --git a/main.tex b/main.tex index cd870d7..b174c5b 100644 --- a/main.tex +++ b/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 diff --git a/natural_deduction_predicate_logic/0001.tex b/natural_deduction_predicate_logic/0001.tex new file mode 100644 index 0000000..5a456b1 --- /dev/null +++ b/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).$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0001_sol.tex b/natural_deduction_predicate_logic/0001_sol.tex new file mode 100644 index 0000000..68a9ef2 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0002.tex b/natural_deduction_predicate_logic/0002.tex new file mode 100644 index 0000000..23a557b --- /dev/null +++ b/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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0002_sol.tex b/natural_deduction_predicate_logic/0002_sol.tex new file mode 100644 index 0000000..44f63bd --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0003.tex b/natural_deduction_predicate_logic/0003.tex new file mode 100644 index 0000000..754a29b --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0003_sol.tex b/natural_deduction_predicate_logic/0003_sol.tex new file mode 100644 index 0000000..83c1d43 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/0004.tex b/natural_deduction_predicate_logic/0004.tex new file mode 100644 index 0000000..9380031 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/0004_sol.tex b/natural_deduction_predicate_logic/0004_sol.tex new file mode 100644 index 0000000..e08cb7d --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0005.tex b/natural_deduction_predicate_logic/0005.tex new file mode 100644 index 0000000..ddfad28 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/0005_sol.tex b/natural_deduction_predicate_logic/0005_sol.tex new file mode 100644 index 0000000..604ea01 --- /dev/null +++ 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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0006.tex b/natural_deduction_predicate_logic/0006.tex new file mode 100644 index 0000000..8d0b3b0 --- /dev/null +++ b/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}? \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0007.tex b/natural_deduction_predicate_logic/0007.tex new file mode 100644 index 0000000..abb3e9a --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0007_sol.tex b/natural_deduction_predicate_logic/0007_sol.tex new file mode 100644 index 0000000..637127f --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0008.tex b/natural_deduction_predicate_logic/0008.tex new file mode 100644 index 0000000..6ec1bee --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/0008_sol.tex b/natural_deduction_predicate_logic/0008_sol.tex new file mode 100644 index 0000000..aa78df1 --- /dev/null +++ b/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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0009.tex b/natural_deduction_predicate_logic/0009.tex new file mode 100644 index 0000000..8a7e856 --- /dev/null +++ b/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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0009_sol.tex b/natural_deduction_predicate_logic/0009_sol.tex new file mode 100644 index 0000000..308a4a0 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0010.tex b/natural_deduction_predicate_logic/0010.tex new file mode 100644 index 0000000..591411e --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0010_sol.tex b/natural_deduction_predicate_logic/0010_sol.tex new file mode 100644 index 0000000..d9981a0 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0011.tex b/natural_deduction_predicate_logic/0011.tex new file mode 100644 index 0000000..78d9e32 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0011_sol.tex b/natural_deduction_predicate_logic/0011_sol.tex new file mode 100644 index 0000000..2c7d65e --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0012.tex b/natural_deduction_predicate_logic/0012.tex new file mode 100644 index 0000000..48b4369 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/0012_sol.tex b/natural_deduction_predicate_logic/0012_sol.tex new file mode 100644 index 0000000..6af32dc --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0013.tex b/natural_deduction_predicate_logic/0013.tex new file mode 100644 index 0000000..7f685a0 --- /dev/null +++ b/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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0013_sol.tex b/natural_deduction_predicate_logic/0013_sol.tex new file mode 100644 index 0000000..e59880e --- /dev/null +++ b/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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/0014.tex b/natural_deduction_predicate_logic/0014.tex new file mode 100644 index 0000000..9cb5cea --- /dev/null +++ b/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) $ diff --git a/natural_deduction_predicate_logic/0014_sol.tex b/natural_deduction_predicate_logic/0014_sol.tex new file mode 100644 index 0000000..ee29802 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/1001.tex b/natural_deduction_predicate_logic/1001.tex new file mode 100644 index 0000000..5ce3c07 --- /dev/null +++ b/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? \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1002.tex b/natural_deduction_predicate_logic/1002.tex new file mode 100644 index 0000000..18f2692 --- /dev/null +++ b/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)) )$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1002_sol.tex b/natural_deduction_predicate_logic/1002_sol.tex new file mode 100644 index 0000000..2f1f775 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/1003.tex b/natural_deduction_predicate_logic/1003.tex new file mode 100644 index 0000000..5eeaa2b --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/1003_sol.tex b/natural_deduction_predicate_logic/1003_sol.tex new file mode 100644 index 0000000..a93c504 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/1004.tex b/natural_deduction_predicate_logic/1004.tex new file mode 100644 index 0000000..09b762e --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1004_sol.tex b/natural_deduction_predicate_logic/1004_sol.tex new file mode 100644 index 0000000..28ca00c --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/1005.tex b/natural_deduction_predicate_logic/1005.tex new file mode 100644 index 0000000..2a38b96 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1005_sol.tex b/natural_deduction_predicate_logic/1005_sol.tex new file mode 100644 index 0000000..3601343 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/1006.tex b/natural_deduction_predicate_logic/1006.tex new file mode 100644 index 0000000..36a5367 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1006_sol.tex b/natural_deduction_predicate_logic/1006_sol.tex new file mode 100644 index 0000000..3b772e1 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1007.tex b/natural_deduction_predicate_logic/1007.tex new file mode 100644 index 0000000..fb1eec5 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1007_sol.tex b/natural_deduction_predicate_logic/1007_sol.tex new file mode 100644 index 0000000..40a63fe --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1008.tex b/natural_deduction_predicate_logic/1008.tex new file mode 100644 index 0000000..e9fe419 --- /dev/null +++ b/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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1008_sol.tex b/natural_deduction_predicate_logic/1008_sol.tex new file mode 100644 index 0000000..eff244b --- /dev/null +++ b/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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1009.tex b/natural_deduction_predicate_logic/1009.tex new file mode 100644 index 0000000..0d00cc2 --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/1009_sol.tex b/natural_deduction_predicate_logic/1009_sol.tex new file mode 100644 index 0000000..1281d2b --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1010.tex b/natural_deduction_predicate_logic/1010.tex new file mode 100644 index 0000000..f015fb4 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1010_sol.tex b/natural_deduction_predicate_logic/1010_sol.tex new file mode 100644 index 0000000..8bb284f --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1011.tex b/natural_deduction_predicate_logic/1011.tex new file mode 100644 index 0000000..0dcd687 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1011_sol.tex b/natural_deduction_predicate_logic/1011_sol.tex new file mode 100644 index 0000000..e3a45c6 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1012.tex b/natural_deduction_predicate_logic/1012.tex new file mode 100644 index 0000000..886ca97 --- /dev/null +++ b/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) $ diff --git a/natural_deduction_predicate_logic/1012_sol.tex b/natural_deduction_predicate_logic/1012_sol.tex new file mode 100644 index 0000000..694f943 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1013.tex b/natural_deduction_predicate_logic/1013.tex new file mode 100644 index 0000000..e8b6de3 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/1013_sol.tex b/natural_deduction_predicate_logic/1013_sol.tex new file mode 100644 index 0000000..7031884 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/1014.tex b/natural_deduction_predicate_logic/1014.tex new file mode 100644 index 0000000..c65fe3b --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/1014_sol.tex b/natural_deduction_predicate_logic/1014_sol.tex new file mode 100644 index 0000000..3239021 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/1015.tex b/natural_deduction_predicate_logic/1015.tex new file mode 100644 index 0000000..5341e74 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/1015_sol.tex b/natural_deduction_predicate_logic/1015_sol.tex new file mode 100644 index 0000000..3bada25 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/2001.tex b/natural_deduction_predicate_logic/2001.tex new file mode 100644 index 0000000..53de708 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/2001_sol.tex b/natural_deduction_predicate_logic/2001_sol.tex new file mode 100644 index 0000000..13135d0 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/2002.tex b/natural_deduction_predicate_logic/2002.tex new file mode 100644 index 0000000..be5eba2 --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/2002_sol.tex b/natural_deduction_predicate_logic/2002_sol.tex new file mode 100644 index 0000000..160352f --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/2003.tex b/natural_deduction_predicate_logic/2003.tex new file mode 100644 index 0000000..65cfb19 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/2003_sol.tex b/natural_deduction_predicate_logic/2003_sol.tex new file mode 100644 index 0000000..e65a297 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/2004.tex b/natural_deduction_predicate_logic/2004.tex new file mode 100644 index 0000000..5ff8dbd --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/2004_sol.tex b/natural_deduction_predicate_logic/2004_sol.tex new file mode 100644 index 0000000..aa6fd64 --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/2005.tex b/natural_deduction_predicate_logic/2005.tex new file mode 100644 index 0000000..1d1db09 --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/2005_sol.tex b/natural_deduction_predicate_logic/2005_sol.tex new file mode 100644 index 0000000..b6df17b --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/2006.tex b/natural_deduction_predicate_logic/2006.tex new file mode 100644 index 0000000..e40a632 --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/2006_sol.tex b/natural_deduction_predicate_logic/2006_sol.tex new file mode 100644 index 0000000..aefacc3 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/2007.tex b/natural_deduction_predicate_logic/2007.tex new file mode 100644 index 0000000..8709a6c --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/2007_sol.tex b/natural_deduction_predicate_logic/2007_sol.tex new file mode 100644 index 0000000..9e67c07 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/2008.tex b/natural_deduction_predicate_logic/2008.tex new file mode 100644 index 0000000..29da2e0 --- /dev/null +++ b/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).$ diff --git a/natural_deduction_predicate_logic/2999.tex b/natural_deduction_predicate_logic/2999.tex new file mode 100644 index 0000000..6d6b7f3 --- /dev/null +++ b/natural_deduction_predicate_logic/2999.tex @@ -0,0 +1,6 @@ +\item + \ifassignmentsheet \points{2} + \else \prac + \fi + + TBD diff --git a/natural_deduction_predicate_logic/9999_sol.tex b/natural_deduction_predicate_logic/9999_sol.tex new file mode 100644 index 0000000..a47a732 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/multiple_choice/4_1_fol_lect.tex b/natural_deduction_predicate_logic/multiple_choice/4_1_fol_lect.tex new file mode 100644 index 0000000..589e5aa --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/multiple_choice/4_1_fol_lect_sol.tex b/natural_deduction_predicate_logic/multiple_choice/4_1_fol_lect_sol.tex new file mode 100644 index 0000000..de23e80 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/natural_deduction_predicate_logic.tex b/natural_deduction_predicate_logic/natural_deduction_predicate_logic.tex new file mode 100644 index 0000000..cd5a98a --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/practical_questions/0_10_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_10_prac.tex new file mode 100644 index 0000000..f3a50e8 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/practical_questions/0_1_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_1_prac.tex new file mode 100644 index 0000000..3eade32 --- /dev/null +++ b/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} diff --git a/natural_deduction_predicate_logic/practical_questions/0_2_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_2_prac.tex new file mode 100644 index 0000000..6959230 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/practical_questions/0_3_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_3_prac.tex new file mode 100644 index 0000000..1feabe6 --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/practical_questions/0_4_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_4_prac.tex new file mode 100644 index 0000000..9083543 --- /dev/null +++ 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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/0_5_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_5_prac.tex new file mode 100644 index 0000000..d839465 --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/practical_questions/0_6_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_6_prac.tex new file mode 100644 index 0000000..d18e015 --- /dev/null +++ b/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 $ diff --git a/natural_deduction_predicate_logic/practical_questions/0_7_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_7_prac.tex new file mode 100644 index 0000000..f1e17c6 --- /dev/null +++ b/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)))$ diff --git a/natural_deduction_predicate_logic/practical_questions/0_8_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_8_prac.tex new file mode 100644 index 0000000..12fe7b4 --- /dev/null +++ b/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))$ diff --git a/natural_deduction_predicate_logic/practical_questions/0_9_prac.tex b/natural_deduction_predicate_logic/practical_questions/0_9_prac.tex new file mode 100644 index 0000000..7044f60 --- /dev/null +++ b/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)$ diff --git a/natural_deduction_predicate_logic/practical_questions/1_1_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/1_1_fol_lect.tex new file mode 100644 index 0000000..23a557b --- /dev/null +++ b/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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/1_1_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/1_1_fol_lect_sol.tex new file mode 100644 index 0000000..44f63bd --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/1_1_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/1_1_fol_self.tex new file mode 100644 index 0000000..18f2692 --- /dev/null +++ b/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)) )$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/1_2_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/1_2_fol_lect.tex new file mode 100644 index 0000000..754a29b --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/1_2_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/1_2_fol_lect_sol.tex new file mode 100644 index 0000000..4a4afca --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/1_2_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/1_2_fol_self.tex new file mode 100644 index 0000000..c2d9b64 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_1_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/2_1_fol_lect.tex new file mode 100644 index 0000000..0e778c2 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_1_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/2_1_fol_lect_sol.tex new file mode 100644 index 0000000..e08cb7d --- /dev/null +++ b/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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_1_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/2_1_fol_self.tex new file mode 100644 index 0000000..09b762e --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_2_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/2_2_fol_lect.tex new file mode 100644 index 0000000..9f2d78b --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_2_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/2_2_fol_lect_sol.tex new file mode 100644 index 0000000..604ea01 --- /dev/null +++ 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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_2_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/2_2_fol_self.tex new file mode 100644 index 0000000..2a38b96 --- /dev/null +++ b/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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_3_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/2_3_fol_lect.tex new file mode 100644 index 0000000..abb3e9a --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/2_3_fol_lect.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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_3_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/2_3_fol_lect_sol.tex new file mode 100644 index 0000000..637127f --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/2_3_fol_lect_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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_4_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/2_4_fol_lect.tex new file mode 100644 index 0000000..f6aba51 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/2_4_fol_lect.tex @@ -0,0 +1 @@ +\item \lect $\exists x \forall y \; (P(y) \imp Q(x)), \forall s \; \lnot Q(s) \land R(s) \quad \ent \quad R(s) \land \exists x \; P(x)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/2_4_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/2_4_fol_lect_sol.tex new file mode 100644 index 0000000..d182a37 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/2_4_fol_lect_sol.tex @@ -0,0 +1,16 @@ +\setlength\subproofhorizspace{1.1em} +\begin{logicproof}{1} + \exists x \forall y \; (P(y) \imp Q(x)) & prem.\\ + \forall s \; \lnot Q(s) \land R(s) & prem.\\ + \begin{subproof} + \llap{$t\enspace \;$} \forall y \; (P(y) \imp Q(t)) & ass.\\ + P(t) \imp Q(t) & $\forall \mathrm{e}$ 3\\ + \lnot Q(t) \land R(s) & $\forall \mathrm{e}$ 2\\ + \lnot Q(t) & $\land \mathrm{e}_1$ 5\\ + \lnot P(t) & MT 4,6\\ + \exists x \; \lnot P(t) & $\exists \mathrm{i}$ 7\\ + \lnot R(s) & $\land \mathrm{e}_2$ 5\\ + R(s) \imp \exists x \; \lnot P(t) & $\exists \mathrm{i}$ 7\\ + \end{subproof} + R(s) \imp \exists x \; \lnot P(t) & $\exists \mathrm{e}$ 3-10 +\end{logicproof} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/3_1_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/3_1_fol_lect.tex new file mode 100644 index 0000000..7c5e0af --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/3_1_fol_lect.tex @@ -0,0 +1 @@ +\item \lect $\forall x \forall y \; ( (x=y) \imp P(x,y) ) \quad \ent \quad \forall x \; P(x,x)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/3_1_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/3_1_fol_lect_sol.tex new file mode 100644 index 0000000..9f5ac4c --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/3_1_fol_lect_sol.tex @@ -0,0 +1,11 @@ +\setlength\subproofhorizspace{1.1em} +\begin{logicproof}{1} + \forall x \forall y \; ( (x=y) \imp P(x,y) ) & prem.\\ + \begin{subproof} + \llap{$t\enspace \;$} \forall y \; ((t=y) \imp P(t,y)) & $\forall \mathrm{e}$ 1\\ + (t=t) \imp P(t,t) & $\forall \mathrm{e}$ 2\\ + t=t & $= \mathrm{i}$\\ + P(t,t) & $\imp \mathrm{e}$ 3,4 + \end{subproof} + \forall x \; P(x,x) & $\forall \mathrm{i}$ 2-5 +\end{logicproof} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/3_1_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/3_1_fol_self.tex new file mode 100644 index 0000000..edad05e --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/3_1_fol_self.tex @@ -0,0 +1 @@ +\item \self $\forall x \forall y \; (x = y \imp P(x,y)) \quad \ent \quad \forall x \; (P(x,x))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/3_2_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/3_2_fol_lect.tex new file mode 100644 index 0000000..3e4423b --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/3_2_fol_lect.tex @@ -0,0 +1 @@ +\item \lect $x = g(y), \; f(g(y)) = z, \; f(x) = y \quad \ent \quad y = z$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/3_2_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/3_2_fol_lect_sol.tex new file mode 100644 index 0000000..360b0fd --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/3_2_fol_lect_sol.tex @@ -0,0 +1,8 @@ +\setlength\subproofhorizspace{1em} +\begin{logicproof}{0} + x = g(y) & prem.\\ + f(g(y)) = z & prem.\\ + f(x) = y & prem.\\ + f(x) = z & $= \mathrm{e}$ 2,1\\ + y = z & $= \mathrm{e}$ 4,3 +\end{logicproof} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/3_2_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/3_2_fol_self.tex new file mode 100644 index 0000000..c7403f0 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/3_2_fol_self.tex @@ -0,0 +1 @@ +\item \self $a = b \quad \ent \quad (a + c) = (b + c)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/3_3_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/3_3_fol_lect.tex new file mode 100644 index 0000000..5a9787d --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/3_3_fol_lect.tex @@ -0,0 +1 @@ +\item \lect $\forall x \; (z=x) \land (f(x) = f(z)) \quad \ent \quad y = z \imp \exists x (f(y) = f(x))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/3_3_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/3_3_fol_lect_sol.tex new file mode 100644 index 0000000..8203a8c --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/3_3_fol_lect_sol.tex @@ -0,0 +1,11 @@ +\setlength\subproofhorizspace{1em} +\begin{logicproof}{1} + \forall x \; (z=x) \land (f(x) = f(z)) & prem.\\ + (z=y) \land f(y) = f(z) & $\forall \mathrm{e}$ 1\\ + \begin{subproof} + y=z & ass.\\ + f(y) = f(z) & $\land \mathrm{e}_2$2\\ + \exists x \; f(y) = f(x) & $\exists \mathrm{i}$ 4 + \end{subproof} + y = z \imp \exists x (f(y) = f(x)) & $\imp \mathrm{i}$ 3-5 +\end{logicproof} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/4_1_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/4_1_fol_lect.tex new file mode 100644 index 0000000..591411e --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/4_1_fol_lect.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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/4_1_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/4_1_fol_lect_sol.tex new file mode 100644 index 0000000..d9981a0 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/4_1_fol_lect_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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/4_1_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/4_1_fol_self.tex new file mode 100644 index 0000000..36a5367 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/4_1_fol_self.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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/4_2_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/4_2_fol_lect.tex new file mode 100644 index 0000000..78d9e32 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/4_2_fol_lect.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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/4_2_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/4_2_fol_lect_sol.tex new file mode 100644 index 0000000..2c7d65e --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/4_2_fol_lect_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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/4_2_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/4_2_fol_self.tex new file mode 100644 index 0000000..fb1eec5 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/4_2_fol_self.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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/4_4_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/4_4_fol_lect.tex new file mode 100644 index 0000000..5a456b1 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/4_4_fol_lect.tex @@ -0,0 +1 @@ +\item \lect $\forall x \; \big(P(x) \imp Q(x)\big), \forall x \; P(x)\ent \forall x \; Q(x).$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/4_4_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/4_4_fol_lect_sol.tex new file mode 100644 index 0000000..68a9ef2 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/4_4_fol_lect_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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/5_1_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/5_1_fol_lect.tex new file mode 100644 index 0000000..c0d27f2 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/5_1_fol_lect.tex @@ -0,0 +1 @@ +\item \lect $\exists x \; \lnot P(x), \exists x \; \lnot Q(x) \quad \ent \quad \exists x \; (\lnot P(x) \land \lnot Q(x))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/5_1_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/5_1_fol_lect_sol.tex new file mode 100644 index 0000000..6af32dc --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/5_1_fol_lect_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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/5_1_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/5_1_fol_self.tex new file mode 100644 index 0000000..e9fe419 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/5_1_fol_self.tex @@ -0,0 +1 @@ +\item \self $\lnot \exists x \; \lnot P(x) \quad \ent \quad \forall x \; \lnot P(x)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/5_2_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/5_2_fol_lect.tex new file mode 100644 index 0000000..5341e74 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/5_2_fol_lect.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))$ diff --git a/natural_deduction_predicate_logic/practical_questions/5_2_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/5_2_fol_lect_sol.tex new file mode 100644 index 0000000..3bada25 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/5_2_fol_lect_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))$ diff --git a/natural_deduction_predicate_logic/practical_questions/5_2_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/5_2_fol_self.tex new file mode 100644 index 0000000..00e2e14 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/5_2_fol_self.tex @@ -0,0 +1 @@ +\item \self $\forall x \exists y \; ( f(x, y) = x ) \quad \ent \quad \exists y \forall x \; ( f(x, y) = x )$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_1_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/6_1_fol_lect.tex new file mode 100644 index 0000000..7f685a0 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_1_fol_lect.tex @@ -0,0 +1 @@ +\item \lect $\exists x \; (P(x) \imp Q(y)), \quad \exists x \; P(x) \quad \ent \quad Q(y)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_1_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/6_1_fol_lect_sol.tex new file mode 100644 index 0000000..e59880e --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_1_fol_lect_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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_1_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/6_1_fol_self.tex new file mode 100644 index 0000000..0d00cc2 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_1_fol_self.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)$ diff --git a/natural_deduction_predicate_logic/practical_questions/6_2_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/6_2_fol_lect.tex new file mode 100644 index 0000000..8a7e856 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_2_fol_lect.tex @@ -0,0 +1 @@ +\item \lect $\exists x \; (P(x) \imp Q(y)), \quad \forall x \; P(x) \quad \ent \quad Q(y)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_2_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/6_2_fol_lect_sol.tex new file mode 100644 index 0000000..308a4a0 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_2_fol_lect_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} \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_2_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/6_2_fol_self.tex new file mode 100644 index 0000000..f015fb4 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_2_fol_self.tex @@ -0,0 +1 @@ +\item \self $\exists y \forall x \; (P(x,y)) \quad \ent \quad \forall x \exists y \; (P(x,y))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_3_fol_lect.tex b/natural_deduction_predicate_logic/practical_questions/6_3_fol_lect.tex new file mode 100644 index 0000000..917787d --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_3_fol_lect.tex @@ -0,0 +1,18 @@ +\item \lect 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} diff --git a/natural_deduction_predicate_logic/practical_questions/6_3_fol_lect_sol.tex b/natural_deduction_predicate_logic/practical_questions/6_3_fol_lect_sol.tex new file mode 100644 index 0000000..aa78df1 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_3_fol_lect_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)$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_3_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/6_3_fol_self.tex new file mode 100644 index 0000000..6fbb312 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_3_fol_self.tex @@ -0,0 +1 @@ +\item \self $ \forall x \forall y (\lnot A(x,y) \imp \lnot (y = x)) \ent \forall x A(x,x) \lor \forall y A(y,y) $ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_4_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/6_4_fol_self.tex new file mode 100644 index 0000000..2b30b8c --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_4_fol_self.tex @@ -0,0 +1 @@ +\item \self $ \forall x \exists y (S(x) = T(y)) \ent \exists y \forall x (S(x) = T(y)) $ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_5_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/6_5_fol_self.tex new file mode 100644 index 0000000..0dcd687 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_5_fol_self.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))$ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_6_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/6_6_fol_self.tex new file mode 100644 index 0000000..886ca97 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_6_fol_self.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) $ diff --git a/natural_deduction_predicate_logic/practical_questions/6_7_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/6_7_fol_self.tex new file mode 100644 index 0000000..95e6119 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_7_fol_self.tex @@ -0,0 +1 @@ +\item \self $ (x = 0) \lor (x + x) > 0 \ent y = (x + x) \rightarrow \big((y > 0) \lor (y = (0 + 0))\big) $ \ No newline at end of file diff --git a/natural_deduction_predicate_logic/practical_questions/6_8_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/6_8_fol_self.tex new file mode 100644 index 0000000..6f79bd0 --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_8_fol_self.tex @@ -0,0 +1,14 @@ +\item \self 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} diff --git a/natural_deduction_predicate_logic/practical_questions/6_9_fol_self.tex b/natural_deduction_predicate_logic/practical_questions/6_9_fol_self.tex new file mode 100644 index 0000000..c65fe3b --- /dev/null +++ b/natural_deduction_predicate_logic/practical_questions/6_9_fol_self.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} diff --git a/natural_deduction_predicate_logic/theory_questions/1_1_fol_self.tex b/natural_deduction_predicate_logic/theory_questions/1_1_fol_self.tex new file mode 100644 index 0000000..5ce3c07 --- /dev/null +++ b/natural_deduction_predicate_logic/theory_questions/1_1_fol_self.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? \ No newline at end of file diff --git a/natural_deduction_predicate_logic/theory_questions/2_1_fol_lect.tex b/natural_deduction_predicate_logic/theory_questions/2_1_fol_lect.tex new file mode 100644 index 0000000..e525236 --- /dev/null +++ b/natural_deduction_predicate_logic/theory_questions/2_1_fol_lect.tex @@ -0,0 +1 @@ +\item \lect State the $\exists$-introduction rule ($\exists$i). Explain how the rule works. \ No newline at end of file diff --git a/natural_deduction_predicate_logic/theory_questions/2_2_fol_lect.tex b/natural_deduction_predicate_logic/theory_questions/2_2_fol_lect.tex new file mode 100644 index 0000000..8d0b3b0 --- /dev/null +++ b/natural_deduction_predicate_logic/theory_questions/2_2_fol_lect.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}? \ No newline at end of file diff --git a/natural_deduction_predicate_logic/theory_questions/2_3_fol_lect.tex b/natural_deduction_predicate_logic/theory_questions/2_3_fol_lect.tex new file mode 100644 index 0000000..a7efad9 --- /dev/null +++ b/natural_deduction_predicate_logic/theory_questions/2_3_fol_lect.tex @@ -0,0 +1 @@ +\item \lect In the context of \textit{Natural Deduction} in \textit{Predicate Logic}, what does it mean, if a variable is \textit{fresh}? Explain, why you need \textit{fresh variables} for certain proofs, for which proofs it is necessary to introduce \textit{fresh variables} and how they differ from other variables. \ No newline at end of file diff --git a/natural_deduction_predicate_logic/theory_questions/3_1_fol_lect.tex b/natural_deduction_predicate_logic/theory_questions/3_1_fol_lect.tex new file mode 100644 index 0000000..790b321 --- /dev/null +++ b/natural_deduction_predicate_logic/theory_questions/3_1_fol_lect.tex @@ -0,0 +1 @@ +\item \lect State the $=$-introduction ($=$i) and the $=$-elimination ($=$e) rule. Explain how both rules work using an example for both rules. \ No newline at end of file diff --git a/util/math_macros.tex b/util/math_macros.tex index 991cb21..b7235d9 100644 --- a/util/math_macros.tex +++ b/util/math_macros.tex @@ -26,8 +26,8 @@ \newcommand{\impi}{\ensuremath{\imp_i}} \newcommand{\impe}{\ensuremath{\imp_e}} \newcommand{\andi}{\ensuremath{\land_i}} -\newcommand{\ande}{\ensuremath{\land_e}} -\newcommand{\ori}{\ensuremath{\lor_i}} +\newcommand{\ande}[1]{\ensuremath{\land_{e_#1}}\xspace} +\newcommand{\ori}[1]{\ensuremath{\lor_{i_#1}}\xspace} \newcommand{\ore}{\ensuremath{\lor_e}} \newcommand{\negi}{\ensuremath{\neg_i}} \newcommand{\nege}{\ensuremath{\neg_e}} @@ -77,6 +77,12 @@ \def\PHI{#2}% \ensuremath{(\lnot \CHI \lor \lnot \PHI) \land (\CHI \lor \PHI)}% } +\newcommand{\tseitinImp}[3]{ + \def\CHI{#1}% + \def\PHI{#2}% + \def\PSI{#3}% + \ensuremath{(\lnot \CHI \lor \neg \PHI \lor \PSI) \land (\PHI \lor \CHI) \land (\neg \PSI \lor \CHI)}% +} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%