Browse Source

added sound and complete for prop nd chapter

main
sp 2 weeks ago
parent
commit
43ce98c27c
  1. 8
      decidability/0001.tex
  2. 14
      decidability/0002.tex
  3. 9
      decidability/0003.tex
  4. 9
      decidability/0004.tex
  5. 5
      decidability/0005.tex
  6. 6
      decidability/0006.tex
  7. 8
      decidability/decidability.tex
  8. 2
      main.tex
  9. 1
      util/allchapter.tex
  10. 5
      util/styling_macros.tex

8
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}

14
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}

9
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.

9
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.

5
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}

6
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.

8
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}

2
main.tex

@ -130,7 +130,7 @@
\ifchapterdecidability
\setsectionnum{10}
\section{Decidability}
\section{Soundness and Completeness of Natural Deduction}
\input{decidability/decidability.tex}
\pagebreak
\fi

1
util/allchapter.tex

@ -10,3 +10,4 @@
\chaptereqcheckingtrue
\chaptersymbenctrue
\chaptertemporaltrue
\chapterdecidabilitytrue

5
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}
}

Loading…
Cancel
Save