git.shemshak.org - ~bandali/bndl.org/blob - static/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)