1 |
|
2 (*<*) theory a3 = Main: (*>*) |
|
3 |
|
4 subsection {* Natural deduction -- Propositional Logic \label{psv0304a3} *} |
|
5 |
|
6 text {* In this exercise, we will prove some lemmas of propositional |
|
7 logic with the aid of a calculus of natural deduction. |
|
8 |
|
9 For the proofs, you may only use |
|
10 |
|
11 \begin{itemize} |
|
12 \item the following lemmas: \\ |
|
13 @{text "notI:"}~@{thm notI[of A,no_vars]},\\ |
|
14 @{text "notE:"}~@{thm notE[of A B,no_vars]},\\ |
|
15 @{text "conjI:"}~@{thm conjI[of A B,no_vars]},\\ |
|
16 @{text "conjE:"}~@{thm conjE[of A B C,no_vars]},\\ |
|
17 @{text "disjI1:"}~@{thm disjI1[of A B,no_vars]},\\ |
|
18 @{text "disjI2:"}~@{thm disjI2[of A B,no_vars]},\\ |
|
19 @{text "disjE:"}~@{thm disjE[of A B C,no_vars]},\\ |
|
20 @{text "impI:"}~@{thm impI[of A B,no_vars]},\\ |
|
21 @{text "impE:"}~@{thm impE[of A B C,no_vars]},\\ |
|
22 @{text "mp:"}~@{thm mp[of A B,no_vars]}\\ |
|
23 @{text "iffI:"}~@{thm iffI[of A B,no_vars]}, \\ |
|
24 @{text "iffE:"}~@{thm iffE[of A B C,no_vars]}\\ |
|
25 @{text "classical:"}~@{thm classical[of A,no_vars]} |
|
26 |
|
27 \item the proof methods @{term rule}, @{term erule} and @{term assumption} |
|
28 \end{itemize} |
|
29 *} |
|
30 |
|
31 lemma I: "A \<longrightarrow> A" |
|
32 (*<*) oops (*>*) |
|
33 |
|
34 lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
35 (*<*) oops (*>*) |
|
36 |
|
37 lemma "(A \<and> B) \<longrightarrow> (A \<or> B)" |
|
38 (*<*) oops (*>*) |
|
39 |
|
40 lemma "((A \<or> B) \<or> C) \<longrightarrow> A \<or> (B \<or> C)" |
|
41 (*<*) oops (*>*) |
|
42 |
|
43 lemma K: "A \<longrightarrow> B \<longrightarrow> A" |
|
44 (*<*) oops (*>*) |
|
45 |
|
46 lemma "(A \<or> A) = (A \<and> A)" |
|
47 (*<*) oops (*>*) |
|
48 |
|
49 lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C" |
|
50 (*<*) oops (*>*) |
|
51 |
|
52 lemma "(A \<longrightarrow> B) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> A \<longrightarrow> C" |
|
53 (*<*) oops (*>*) |
|
54 |
|
55 lemma "\<not> \<not> A \<longrightarrow> A" |
|
56 (*<*) oops (*>*) |
|
57 |
|
58 lemma "A \<longrightarrow> \<not> \<not> A" |
|
59 (*<*) oops (*>*) |
|
60 |
|
61 lemma "(\<not> A \<longrightarrow> B) \<longrightarrow> (\<not> B \<longrightarrow> A)" |
|
62 (*<*) oops (*>*) |
|
63 |
|
64 lemma "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" |
|
65 (*<*) oops (*>*) |
|
66 |
|
67 lemma "A \<or> \<not> A" |
|
68 (*<*) oops (*>*) |
|
69 |
|
70 lemma "(\<not> (A \<and> B)) = (\<not> A \<or> \<not> B)" |
|
71 (*<*) oops (*>*) |
|
72 |
|
73 (*<*) end (*>*) |
|
74 |
|