-
Notifications
You must be signed in to change notification settings - Fork 1
/
predicateLogic.thy~
127 lines (113 loc) · 3.04 KB
/
predicateLogic.thy~
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
(*
ex.thy,v 1.1 2016/09/29 17:37:37 jdf Exp
Original Author: Tjark Weber
Updated to Isabelle 2016 by Jacques Fleuriot
*)
section {* Predicate Logic *}
theory predicateLogic imports Main begin
text {*
We are again talking about proofs in the calculus of Natural Deduction. In
addition to the rules given in the exercise "Propositional Logic", you may
now also use
exI: ?P ?x \<Longrightarrow> \<exists>x. ?P x
exE:\<lbrakk>\<exists>x. ?P x; \<And>x. ?P x \<Longrightarrow> ?Q\<rbrakk> \<Longrightarrow> ?Q
allI: (\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x
allE: \<lbrakk>\<forall>x. ?P x; ?P ?x \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R
Give a proof of the following propositions or an argument why the formula is
not valid:
*}
lemma "(\<exists>x. \<forall>y. P x y) \<longrightarrow> (\<forall>y. \<exists>x. P x y)"
apply (rule impI)
apply (rule allI)
apply (erule exE)
apply (rule exI)
apply (erule allE)
apply assumption
done
lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
apply (rule iffI)
apply (rule impI)
apply (erule exE)
apply (erule allE)
apply (erule impE)
apply assumption+
apply (rule allI)
apply (rule impI)
apply (erule impE)
apply (rule exI)
apply assumption+
done
lemma "((\<forall> x. P x) \<and> (\<forall> x. Q x)) = (\<forall> x. (P x \<and> Q x))"
apply (rule iffI)
apply (rule allI)
apply (erule conjE)
apply (erule allE)+
apply (rule conjI)
apply assumption+
apply (rule conjI)
apply (rule allI)
apply (erule allE)
apply (erule conjE)
apply assumption
apply (rule allI)
apply (erule allE)
apply (erule conjE)
apply assumption
done
lemma "((\<forall> x. P x) \<or> (\<forall> x. Q x)) = (\<forall> x. (P x \<or> Q x))"
apply (rule iffI)
apply (rule allI)
apply (erule disjE)
apply (rule disjI1)
apply (erule allE)
apply assumption
apply (rule disjI2)
apply (erule allE)
apply assumption
apply (rule classical)
(* invalid: only provable one way*)
oops
lemma "((\<exists> x. P x) \<or> (\<exists> x. Q x)) = (\<exists> x. (P x \<or> Q x))"
apply (rule iffI)
apply (erule disjE)
apply (erule exE)
apply (rule exI)
apply (rule disjI1)
apply assumption
apply (erule exE)
apply (rule exI)
apply (rule disjI2)
apply assumption
apply (erule exE)
apply (erule disjE)
apply (rule disjI1)
apply (rule exI)
apply assumption
apply (rule disjI2)
apply (rule exI)
apply assumption
done
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
apply (rule impI)
apply (erule allE)
apply (erule exE)
apply (rule exI)
apply (rule allI)
oops
lemma "(\<not> (\<forall> x. P x)) = (\<exists> x. \<not> P x)"
apply (rule iffI)
prefer 2
apply (erule exE)
apply (rule notI)
apply (erule allE)
apply (erule notE)
apply assumption
apply (rule ccontr)
apply (erule notE)
apply (rule allI)
apply (rule ccontr)
apply (erule notE)
apply (rule exI)
apply assumption
done
end