commit another bunch of changes
[~bandali/bndl.org] / se212-f19 / se212-t05.org
CommitLineData
ff620ce6
AB
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
28Provide a counterexample to show that the following argument is not
29valid and demonstrate that your answer is correct.
30
31#+begin_example
32forall y : M . exists x : N . p(g(x), y)
33|=
34exists z : M . p(z, z)
35#+end_example
36
37* =h04q05= \small{(cont’d)}
38
39#+begin_example
40Domain:
41 M = {m1, m2}
42 N = {n1, n2}
43
44Mapping:
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
59Premise:
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
74Conclusion:
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
83Express the following sentences in predicate logic. Use types in your
84formalization. Is the set of formulas consistent? Demonstrate that
85your answer is correct using the semantics of predicate logic.
86
87#+begin_example
88All programmer like some computers.
89Some programmers use MAC.
90Therefore, some people who like some computers use MAC.
91#+end_example
92
93* =h04q06= \small{(cont’d)}
94
95All programmer like some computers.\\
96Some programmers use MAC.\\
97Therefore, some people who like some computers use MAC.
98
99#+begin_example
100Formalization:
101 programmer(x) means x is a programmer
102 usesmac(x) means x uses MAC
103 likes(x, y) means x likes y
104
105forall x: Person . programmer(x) =>
106 exists y: Computer . likes(x, y),
107exists x: Person . programmer(x) & usesmac(x)
108|-
109exists x: Person .
110 (exists y: Computer . likes(x, y) & usesmac(x))
111#+end_example
112
113* =h04q06= \small{(cont’d)}
114
115These sentences are /consistent/. Here is an interpretation in which
116all the formulas are T:
117
118#+begin_example
119Domain:
120 People = {John}
121 Computer = {MacPro}
122
123Mapping:
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
134formula 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
143formula 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
153formula 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
165If the following arguments are valid, use natural deduction AND
166semantic tableaux to prove them; otherwise, provide a counterexample.
167
168#+begin_example
169forall x . s(x) | t(x),
170forall x . s(x) => t(x) & k(c, x),
171forall x . t(x) => m(x)
172|-
173m(c)
174where c is a constant
175#+end_example
176
177* =h05q01a= \small{(cont’d)}
178
179#+begin_example
180#check ND
181forall x . s(x) | t(x),
182forall x . s(x) => t(x) & k(c, x),
183forall x . t(x) => m(x)
184|-
185m(c)
186#+end_example
187
188* =h05q01a= \small{(cont’d)}
189
190#+begin_example
1911) forall x . s(x) | t(x) premise
1922) forall x . s(x) => t(x) & k(c, x) premise
1933) forall x . t(x) => m(x) premise
1944) s(c) | t(c) by forall_e on 1
1955) s(c) => t(c) & k(c, c) by forall_e on 2
1966) t(c) => m(c) by forall_e on 3
1977) 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}
20211) case t(c) {
203 12) m(c) by imp_e on 6, 11
204}
20513) m(c) by cases on 4, 7-10, 11-12
206#+end_example
207
208* =h05q01b=
209
210Is 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
218No, this formula is not a tautology. Interpretation:
219
220#+begin_example
2211) Domain = {a, b}
222
2232) Mapping:
224 Syntax | Meaning
225 ----------------------
226 p(.) | P(a) = T
227 | P(b) = F
228
229Conclusion:
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
239Is this argument valid?
240
241#+begin_example
242forall x . p(x) | q(x),
243forall x . !p(x)
244|-
245forall x . q(x)
246#+end_example
247
248* =h05q01d= \small{(cont’d)}
249
250#+begin_example
251#check ND
252
253forall x . p(x) | q(x), forall x . !p(x) |- forall x . q(x)
254
2551) forall x . p(x) | q(x) premise
2562) forall x . !p(x) premise
2573) 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}
26610) 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)