diff --git a/decidability/0001.tex b/decidability/0001.tex index 90061a6..9e0e209 100644 --- a/decidability/0001.tex +++ b/decidability/0001.tex @@ -1 +1,7 @@ -\item TODO +\item +\begin{questionEnumerate} +\item Explain what it means that natural deduction for propositional logic is \emph{sound}? \newline +\item The soundness of natural deduction for propositional logic can be proven via a mathematical induction proof. +Discuss the proof idea by stating the \emph{induction hypothesis}, and what needs to be shown for the \emph{induction base-case} as well as for the \emph{induction step}. + +\end{questionEnumerate} diff --git a/decidability/0002.tex b/decidability/0002.tex index 90061a6..3f66d43 100644 --- a/decidability/0002.tex +++ b/decidability/0002.tex @@ -1 +1,13 @@ -\item TODO +\item +The soundness of natural deduction for propositional logic can be proven via a \emph{mathematical course-of-values induction on the length of the Natural Deduction proof}. Let $M(k)$ be the following assertion: + +$M(k)\coloneqq$ „For all sequents $\phi_1,\phi_2,\dots,\phi_n\vdash \psi$ which have a proof of length $k$, +it is the case that $\phi_1,\phi_2,\dots,\phi_n\models \psi$ holds.” + +Your tasks: +\begin{enumerate} +\setlength{\itemsep}{-0.1em} +\item Proof the induction base-case, i.e., $M(1)$ holds. +\item Explain the proof idea of the induction step: +$M(1)\wedge M(2) \land \dots \land M(k-1) \rightarrow M(k)$. +\end{enumerate} diff --git a/decidability/0003.tex b/decidability/0003.tex index 90061a6..b912446 100644 --- a/decidability/0003.tex +++ b/decidability/0003.tex @@ -1 +1,8 @@ -\item TODO +\item +The soundness of natural deduction for propositional logic can be proven via a \emph{mathematical course-of-values induction on the length of the Natural Deduction proof}. Let $M(k)$ be the following assertion: + +$M(k)\coloneqq$ „For all sequents $\phi_1,\phi_2,\dots,\phi_n\vdash \psi$ which have a proof of length $k$, +it is the case that $\phi_1,\phi_2,\dots,\phi_n\models \psi$ holds.” + +Discuss the \textbf{induction step} +$M(1)\land M(2) \land \dots \land M(k-1) \imp M(k)$ under the assumption that the \textbf{$\nege$} was applied as a final rule to prove the conclusion. diff --git a/decidability/0004.tex b/decidability/0004.tex index 90061a6..fb27aa1 100644 --- a/decidability/0004.tex +++ b/decidability/0004.tex @@ -1 +1,8 @@ -\item TODO +\item +The soundness of natural deduction for propositional logic can be proven via a \emph{mathematical course-of-values induction on the length of the Natural Deduction proof}. Let $M(k)$ be the following assertion: + +$M(k)\coloneqq$ „For all sequents $\phi_1,\phi_2,\dots,\phi_n\vdash \psi$ which have a proof of length $k$, +it is the case that $\phi_1,\phi_2,\dots,\phi_n\models \psi$ holds.” + +Discuss the \textbf{induction step} +$M(1)\wedge M(2) \wedge \dots \wedge M(k-1) \rightarrow M(k)$ under the assumption that the \textbf{$\andi$} was applied as a final rule to prove the conclusion. diff --git a/decidability/0005.tex b/decidability/0005.tex new file mode 100644 index 0000000..70f9c7c --- /dev/null +++ b/decidability/0005.tex @@ -0,0 +1,5 @@ +\item +\begin{questionEnumerate}[0.2em] +\item Explain what it means that natural deduction for propositional logic is \emph{complete}? +\item Sketch the idea of the \emph{proof for completeness} of natural deduction for propositional logic. List the three sub-proofs that need to be performed to prove completeness and briefly discuss the idea of each individual sub-proof. +\end{questionEnumerate} diff --git a/decidability/0006.tex b/decidability/0006.tex new file mode 100644 index 0000000..c82f6c0 --- /dev/null +++ b/decidability/0006.tex @@ -0,0 +1,6 @@ +\item The proof of completeness for natural deduction for propositional logic contains the following sub-proof: + +$$\text{If~} \models \phi \text{~holds, then so does~} \vdash \phi.$$ + +Discuss the proof idea of performing this step of the completeness-proof. + diff --git a/decidability/decidability.tex b/decidability/decidability.tex index 34c667d..7440d61 100644 --- a/decidability/decidability.tex +++ b/decidability/decidability.tex @@ -1,4 +1,4 @@ -\begin{questionSection}{Decidability} +\begin{questionSection}{Soundness and Completeness of Natural Deduction} \question{decidability/0001.tex} {no_solution} {3cm} @@ -11,4 +11,10 @@ \question{decidability/0004.tex} {no_solution} {3cm} +\question{decidability/0005.tex} + {no_solution} + {3cm} +\question{decidability/0006.tex} + {no_solution} + {3cm} \end{questionSection} diff --git a/main.tex b/main.tex index 3feca7d..788cbac 100644 --- a/main.tex +++ b/main.tex @@ -130,7 +130,7 @@ \ifchapterdecidability \setsectionnum{10} - \section{Decidability} + \section{Soundness and Completeness of Natural Deduction} \input{decidability/decidability.tex} \pagebreak \fi diff --git a/util/allchapter.tex b/util/allchapter.tex index 3569757..2a5d675 100644 --- a/util/allchapter.tex +++ b/util/allchapter.tex @@ -10,3 +10,4 @@ \chaptereqcheckingtrue \chaptersymbenctrue \chaptertemporaltrue +\chapterdecidabilitytrue diff --git a/util/styling_macros.tex b/util/styling_macros.tex index 79a4bc4..fb08cee 100644 --- a/util/styling_macros.tex +++ b/util/styling_macros.tex @@ -107,6 +107,11 @@ {\begin{itemize}\setlength{\itemsep}{#1}} {\end{itemize}} +\newenvironment{questionEnumerate}[1][-1em] + {\mbox{}\vspace{-0.7em}% + \begin{enumerate}[label=(\alph*)]\setlength{\itemsep}{#1}} + {\end{enumerate}} + \newcommand\TODONOTE[1]{ \marginnote{\color{red}\footnotesize TODO} }