14500
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{a{\isadigit{3}}}%
|
|
4 |
\isamarkupfalse%
|
|
5 |
%
|
|
6 |
\isamarkupsubsection{Natural deduction -- Propositional Logic \label{psv0304a3}%
|
|
7 |
}
|
|
8 |
\isamarkuptrue%
|
|
9 |
%
|
|
10 |
\begin{isamarkuptext}%
|
|
11 |
In this exercise, we will prove some lemmas of propositional
|
|
12 |
logic with the aid of a calculus of natural deduction.
|
|
13 |
|
|
14 |
For the proofs, you may only use
|
|
15 |
|
|
16 |
\begin{itemize}
|
|
17 |
\item the following lemmas: \\
|
|
18 |
\isa{notI{\isacharcolon}}~\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ False{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymnot}\ A},\\
|
|
19 |
\isa{notE{\isacharcolon}}~\isa{{\isasymlbrakk}{\isasymnot}\ A{\isacharsemicolon}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ B},\\
|
|
20 |
\isa{conjI{\isacharcolon}}~\isa{{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B},\\
|
|
21 |
\isa{conjE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymand}\ B{\isacharsemicolon}\ {\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C},\\
|
|
22 |
\isa{disjI{\isadigit{1}}{\isacharcolon}}~\isa{A\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B},\\
|
|
23 |
\isa{disjI{\isadigit{2}}{\isacharcolon}}~\isa{A\ {\isasymLongrightarrow}\ B\ {\isasymor}\ A},\\
|
|
24 |
\isa{disjE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymor}\ B{\isacharsemicolon}\ A\ {\isasymLongrightarrow}\ C{\isacharsemicolon}\ B\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C},\\
|
|
25 |
\isa{impI{\isacharcolon}}~\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymlongrightarrow}\ B},\\
|
|
26 |
\isa{impE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymlongrightarrow}\ B{\isacharsemicolon}\ A{\isacharsemicolon}\ B\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C},\\
|
|
27 |
\isa{mp{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymlongrightarrow}\ B{\isacharsemicolon}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ B}\\
|
|
28 |
\isa{iffI{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymLongrightarrow}\ B{\isacharsemicolon}\ B\ {\isasymLongrightarrow}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ A\ {\isacharequal}\ B}, \\
|
|
29 |
\isa{iffE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymlbrakk}A\ {\isasymlongrightarrow}\ B{\isacharsemicolon}\ B\ {\isasymlongrightarrow}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C}\\
|
|
30 |
\isa{classical{\isacharcolon}}~\isa{{\isacharparenleft}{\isasymnot}\ A\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A}
|
|
31 |
|
|
32 |
\item the proof methods \isa{rule}, \isa{erule} and \isa{assumption}
|
|
33 |
\end{itemize}%
|
|
34 |
\end{isamarkuptext}%
|
|
35 |
\isamarkuptrue%
|
|
36 |
\isacommand{lemma}\ I{\isacharcolon}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
|
|
37 |
\isanewline
|
|
38 |
\isamarkupfalse%
|
|
39 |
\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isamarkupfalse%
|
|
40 |
\isanewline
|
|
41 |
\isamarkupfalse%
|
|
42 |
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
|
43 |
\isanewline
|
|
44 |
\isamarkupfalse%
|
|
45 |
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymor}\ C{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymor}\ {\isacharparenleft}B\ {\isasymor}\ C{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
|
46 |
\isanewline
|
|
47 |
\isamarkupfalse%
|
|
48 |
\isacommand{lemma}\ K{\isacharcolon}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
|
|
49 |
\isanewline
|
|
50 |
\isamarkupfalse%
|
|
51 |
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymor}\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymand}\ A{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
|
52 |
\isanewline
|
|
53 |
\isamarkupfalse%
|
|
54 |
\isacommand{lemma}\ S{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B\ {\isasymlongrightarrow}\ C{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymlongrightarrow}\ C{\isachardoublequote}\isamarkupfalse%
|
|
55 |
\isanewline
|
|
56 |
\isamarkupfalse%
|
|
57 |
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}B\ {\isasymlongrightarrow}\ C{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymlongrightarrow}\ C{\isachardoublequote}\isamarkupfalse%
|
|
58 |
\isanewline
|
|
59 |
\isamarkupfalse%
|
|
60 |
\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ {\isasymnot}\ A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
|
|
61 |
\isanewline
|
|
62 |
\isamarkupfalse%
|
|
63 |
\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ {\isasymnot}\ {\isasymnot}\ A{\isachardoublequote}\isamarkupfalse%
|
|
64 |
\isanewline
|
|
65 |
\isamarkupfalse%
|
|
66 |
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymnot}\ A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymnot}\ B\ {\isasymlongrightarrow}\ A{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
|
67 |
\isanewline
|
|
68 |
\isamarkupfalse%
|
|
69 |
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
|
|
70 |
\isanewline
|
|
71 |
\isamarkupfalse%
|
|
72 |
\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymor}\ {\isasymnot}\ A{\isachardoublequote}\isamarkupfalse%
|
|
73 |
\isanewline
|
|
74 |
\isamarkupfalse%
|
|
75 |
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isacharparenright}\ {\isacharequal} {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
|
76 |
\isamarkupfalse%
|
|
77 |
\isanewline
|
|
78 |
\isamarkupfalse%
|
|
79 |
\end{isabellebody}%
|
|
80 |
%%% Local Variables:
|
|
81 |
%%% mode: latex
|
|
82 |
%%% TeX-master: "root"
|
|
83 |
%%% End:
|