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: |
|