add post-specific copyright years
[~bandali/bndl.org] / static / se212-f19 / se212-t05.org
1 #+title: Predicate Logic
2 #+subtitle: (SE 212 Tutorial 5)
3 #+author: Amin Bandali
4 #+email: bandali@uwaterloo.ca
5 #+date: Wed Oct 9, 2019
6 #+language: en
7 #+options: email:t num:t toc:nil \n:nil ::t |:t ^:t -:t f:t *:t <:t
8 #+options: tex:t d:nil todo:t pri:nil tags:not-in-toc
9 #+select_tags: export
10 #+exclude_tags: noexport
11 #+startup: beamer
12 #+latex_class: beamer
13 # #+latex_class_options: [bigger]
14 #+latex_header: \setbeamercovered{transparent}
15 #+latex: \setbeamertemplate{itemize items}[circle]
16 #+beamer_color_theme: beaver
17
18 * Today’s plan
19 :PROPERTIES:
20 :BEAMER_act: [<+->]
21 :END:
22
23 - do some semantics questions from homework 4
24 - do some ND questions from homework 5
25
26 * =h04q05=
27
28 Provide a counterexample to show that the following argument is not
29 valid and demonstrate that your answer is correct.
30
31 #+begin_example
32 forall y : M . exists x : N . p(g(x), y)
33 |=
34 exists z : M . p(z, z)
35 #+end_example
36
37 * =h04q05= \small{(cont’d)}
38
39 #+begin_example
40 Domain:
41 M = {m1, m2}
42 N = {n1, n2}
43
44 Mapping:
45 Syntax | Meaning
46 --------------------------
47 g(.) | G(n1) := m1
48 | G(n2) := m2
49 --------------------------
50 p(., .) | P(m1, m1) := F
51 | P(m1, m2) := T
52 | P(m2, m1) := T
53 | P(m2, m2) := F
54 #+end_example
55
56 * =h04q05= \small{(cont’d)}
57
58 #+begin_example
59 Premise:
60 [forall y : M . exists x : N . p(g(x), y)]
61 = [exists x: N. p(g(x), ^m1)] AND
62 [exists x: N . p(g(x), ^m2)]
63 = (P(G(n1), m1) OR P(G(n2), m1)) AND
64 (P(G(n1), m2) OR P(G(n2), m2))
65 = (P(m1, m1) OR P(m2, m1)) AND
66 (P(m1, m2) OR P(m2, m2))
67 = (F OR T) AND (T OR F)
68 = T
69 #+end_example
70
71 * =h04q05= \small{(cont’d)}
72
73 #+begin_example
74 Conclusion:
75 [exists z: M . p(z, z)]
76 = P(m1, m1) OR P(m2, m2)
77 = F OR F
78 = F
79 #+end_example
80
81 * =h04q06=
82
83 Express the following sentences in predicate logic. Use types in your
84 formalization. Is the set of formulas consistent? Demonstrate that
85 your answer is correct using the semantics of predicate logic.
86
87 #+begin_example
88 All programmer like some computers.
89 Some programmers use MAC.
90 Therefore, some people who like some computers use MAC.
91 #+end_example
92
93 * =h04q06= \small{(cont’d)}
94
95 All programmer like some computers.\\
96 Some programmers use MAC.\\
97 Therefore, some people who like some computers use MAC.
98
99 #+begin_example
100 Formalization:
101 programmer(x) means x is a programmer
102 usesmac(x) means x uses MAC
103 likes(x, y) means x likes y
104
105 forall x: Person . programmer(x) =>
106 exists y: Computer . likes(x, y),
107 exists x: Person . programmer(x) & usesmac(x)
108 |-
109 exists x: Person .
110 (exists y: Computer . likes(x, y) & usesmac(x))
111 #+end_example
112
113 * =h04q06= \small{(cont’d)}
114
115 These sentences are /consistent/. Here is an interpretation in which
116 all the formulas are T:
117
118 #+begin_example
119 Domain:
120 People = {John}
121 Computer = {MacPro}
122
123 Mapping:
124 Syntax | Meaning
125 -------------------------------------------
126 programmer(.) | programmer(John) = T
127 likes(.,.) | likes(John, MacPro) = T
128 usesmac(.) | usesmac(John) = T
129 #+end_example
130
131 * =h04q06= \small{(cont’d)}
132
133 #+begin_example
134 formula 1:
135 [forall x: Person . programmer(x) =>
136 exists y: Computer . likes(x, y)]
137 = [programmer(^John) =>
138 exists y: Computer . likes(^John, y)]]
139 = programmer(John) IMP likes(John, MacPro)
140 = T IMP T
141 = T
142
143 formula 2:
144 [exists x: Person . programmer(x) & usesmac(x)]
145 = programmer(John) AND usesmac(John)
146 = T AND T
147 = T
148 #+end_example
149
150 * =h04q06= \small{(cont’d)}
151
152 #+begin_example
153 formula 3:
154 [exists x: Person . (exists y: Computer .
155 likes(x, y) & usesmac(x))]
156 = [exists y: Computer .
157 likes(^John, y) & usesmac(^John)]
158 = likes(John, MacPro) AND usesmac(John)
159 = T AND T
160 = T
161 #+end_example
162
163 * =h05q01a=
164
165 If the following arguments are valid, use natural deduction AND
166 semantic tableaux to prove them; otherwise, provide a counterexample.
167
168 #+begin_example
169 forall x . s(x) | t(x),
170 forall x . s(x) => t(x) & k(c, x),
171 forall x . t(x) => m(x)
172 |-
173 m(c)
174 where c is a constant
175 #+end_example
176
177 * =h05q01a= \small{(cont’d)}
178
179 #+begin_example
180 #check ND
181 forall x . s(x) | t(x),
182 forall x . s(x) => t(x) & k(c, x),
183 forall x . t(x) => m(x)
184 |-
185 m(c)
186 #+end_example
187
188 * =h05q01a= \small{(cont’d)}
189
190 #+begin_example
191 1) forall x . s(x) | t(x) premise
192 2) forall x . s(x) => t(x) & k(c, x) premise
193 3) forall x . t(x) => m(x) premise
194 4) s(c) | t(c) by forall_e on 1
195 5) s(c) => t(c) & k(c, c) by forall_e on 2
196 6) t(c) => m(c) by forall_e on 3
197 7) case s(c) {
198 8) t(c) & k(c, c) by imp_e on 5, 7
199 9) t(c) by and_e on 8
200 10) m(c) by imp_e on 6, 9
201 }
202 11) case t(c) {
203 12) m(c) by imp_e on 6, 11
204 }
205 13) m(c) by cases on 4, 7-10, 11-12
206 #+end_example
207
208 * =h05q01b=
209
210 Is this formula a tautology?
211
212 #+begin_example
213 |- (exists x . p(x)) => forall y . p(y)
214 #+end_example
215
216 * =h05q01b= \small{(cont’d)}
217
218 No, this formula is not a tautology. Interpretation:
219
220 #+begin_example
221 1) Domain = {a, b}
222
223 2) Mapping:
224 Syntax | Meaning
225 ----------------------
226 p(.) | P(a) = T
227 | P(b) = F
228
229 Conclusion:
230 [(exists x. p(x)) => forall y. p(y)]
231 = (P(a) OR P(b)) IMP (P(a) AND P(b))
232 = (T OR F) IMP (T AND F)
233 = T IMP F
234 = F
235 #+end_example
236
237 * =h05q01d=
238
239 Is this argument valid?
240
241 #+begin_example
242 forall x . p(x) | q(x),
243 forall x . !p(x)
244 |-
245 forall x . q(x)
246 #+end_example
247
248 * =h05q01d= \small{(cont’d)}
249
250 #+begin_example
251 #check ND
252
253 forall x . p(x) | q(x), forall x . !p(x) |- forall x . q(x)
254
255 1) forall x . p(x) | q(x) premise
256 2) forall x . !p(x) premise
257 3) for every xg {
258 4) p(xg) | q(xg) by forall_e on 1
259 5) case p(xg) {
260 6) !p(xg) by forall_e on 2
261 7) q(xg) by not_e on 5, 6
262 }
263 8) case q(xg) {}
264 9) q(xg) by cases on 4, 5-7, 8-8
265 }
266 10) forall x. q(x) by forall_i on 3-9
267 #+end_example
268
269 * Announcements
270
271 - no tutorial next week (Oct 16) (reading week)
272 - no tutorial the week after (Oct 23) (midterm marking)