X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/cfe6a758127c1ee27e6b287724234518a83e653e..ff620ce6ac85cf10600b3da9a640f6ebc3568444:/se212-f19/se212-t05.org diff --git a/se212-f19/se212-t05.org b/se212-f19/se212-t05.org new file mode 100644 index 0000000..a85896d --- /dev/null +++ b/se212-f19/se212-t05.org @@ -0,0 +1,272 @@ +#+title: Predicate Logic +#+subtitle: (SE 212 Tutorial 5) +#+author: Amin Bandali +#+email: bandali@uwaterloo.ca +#+date: Wed Oct 9, 2019 +#+language: en +#+options: email:t num:t toc:nil \n:nil ::t |:t ^:t -:t f:t *:t <:t +#+options: tex:t d:nil todo:t pri:nil tags:not-in-toc +#+select_tags: export +#+exclude_tags: noexport +#+startup: beamer +#+latex_class: beamer +# #+latex_class_options: [bigger] +#+latex_header: \setbeamercovered{transparent} +#+latex: \setbeamertemplate{itemize items}[circle] +#+beamer_color_theme: beaver + +* Today’s plan +:PROPERTIES: +:BEAMER_act: [<+->] +:END: + +- do some semantics questions from homework 4 +- do some ND questions from homework 5 + +* =h04q05= + +Provide a counterexample to show that the following argument is not +valid and demonstrate that your answer is correct. + +#+begin_example +forall y : M . exists x : N . p(g(x), y) +|= +exists z : M . p(z, z) +#+end_example + +* =h04q05= \small{(cont’d)} + +#+begin_example +Domain: + M = {m1, m2} + N = {n1, n2} + +Mapping: + Syntax | Meaning + -------------------------- + g(.) | G(n1) := m1 + | G(n2) := m2 + -------------------------- + p(., .) | P(m1, m1) := F + | P(m1, m2) := T + | P(m2, m1) := T + | P(m2, m2) := F +#+end_example + +* =h04q05= \small{(cont’d)} + +#+begin_example +Premise: + [forall y : M . exists x : N . p(g(x), y)] + = [exists x: N. p(g(x), ^m1)] AND + [exists x: N . p(g(x), ^m2)] + = (P(G(n1), m1) OR P(G(n2), m1)) AND + (P(G(n1), m2) OR P(G(n2), m2)) + = (P(m1, m1) OR P(m2, m1)) AND + (P(m1, m2) OR P(m2, m2)) + = (F OR T) AND (T OR F) + = T +#+end_example + +* =h04q05= \small{(cont’d)} + +#+begin_example +Conclusion: + [exists z: M . p(z, z)] + = P(m1, m1) OR P(m2, m2) + = F OR F + = F +#+end_example + +* =h04q06= + +Express the following sentences in predicate logic. Use types in your +formalization. Is the set of formulas consistent? Demonstrate that +your answer is correct using the semantics of predicate logic. + +#+begin_example +All programmer like some computers. +Some programmers use MAC. +Therefore, some people who like some computers use MAC. +#+end_example + +* =h04q06= \small{(cont’d)} + +All programmer like some computers.\\ +Some programmers use MAC.\\ +Therefore, some people who like some computers use MAC. + +#+begin_example +Formalization: + programmer(x) means x is a programmer + usesmac(x) means x uses MAC + likes(x, y) means x likes y + +forall x: Person . programmer(x) => + exists y: Computer . likes(x, y), +exists x: Person . programmer(x) & usesmac(x) +|- +exists x: Person . + (exists y: Computer . likes(x, y) & usesmac(x)) +#+end_example + +* =h04q06= \small{(cont’d)} + +These sentences are /consistent/. Here is an interpretation in which +all the formulas are T: + +#+begin_example +Domain: + People = {John} + Computer = {MacPro} + +Mapping: + Syntax | Meaning + ------------------------------------------- + programmer(.) | programmer(John) = T + likes(.,.) | likes(John, MacPro) = T + usesmac(.) | usesmac(John) = T +#+end_example + +* =h04q06= \small{(cont’d)} + +#+begin_example +formula 1: + [forall x: Person . programmer(x) => + exists y: Computer . likes(x, y)] + = [programmer(^John) => + exists y: Computer . likes(^John, y)]] + = programmer(John) IMP likes(John, MacPro) + = T IMP T + = T + +formula 2: + [exists x: Person . programmer(x) & usesmac(x)] + = programmer(John) AND usesmac(John) + = T AND T + = T +#+end_example + +* =h04q06= \small{(cont’d)} + +#+begin_example +formula 3: + [exists x: Person . (exists y: Computer . + likes(x, y) & usesmac(x))] + = [exists y: Computer . + likes(^John, y) & usesmac(^John)] + = likes(John, MacPro) AND usesmac(John) + = T AND T + = T +#+end_example + +* =h05q01a= + +If the following arguments are valid, use natural deduction AND +semantic tableaux to prove them; otherwise, provide a counterexample. + +#+begin_example +forall x . s(x) | t(x), +forall x . s(x) => t(x) & k(c, x), +forall x . t(x) => m(x) +|- +m(c) +where c is a constant +#+end_example + +* =h05q01a= \small{(cont’d)} + +#+begin_example +#check ND +forall x . s(x) | t(x), +forall x . s(x) => t(x) & k(c, x), +forall x . t(x) => m(x) +|- +m(c) +#+end_example + +* =h05q01a= \small{(cont’d)} + +#+begin_example +1) forall x . s(x) | t(x) premise +2) forall x . s(x) => t(x) & k(c, x) premise +3) forall x . t(x) => m(x) premise +4) s(c) | t(c) by forall_e on 1 +5) s(c) => t(c) & k(c, c) by forall_e on 2 +6) t(c) => m(c) by forall_e on 3 +7) case s(c) { + 8) t(c) & k(c, c) by imp_e on 5, 7 + 9) t(c) by and_e on 8 + 10) m(c) by imp_e on 6, 9 +} +11) case t(c) { + 12) m(c) by imp_e on 6, 11 +} +13) m(c) by cases on 4, 7-10, 11-12 +#+end_example + +* =h05q01b= + +Is this formula a tautology? + +#+begin_example +|- (exists x . p(x)) => forall y . p(y) +#+end_example + +* =h05q01b= \small{(cont’d)} + +No, this formula is not a tautology. Interpretation: + +#+begin_example +1) Domain = {a, b} + +2) Mapping: + Syntax | Meaning + ---------------------- + p(.) | P(a) = T + | P(b) = F + +Conclusion: + [(exists x. p(x)) => forall y. p(y)] += (P(a) OR P(b)) IMP (P(a) AND P(b)) += (T OR F) IMP (T AND F) += T IMP F += F +#+end_example + +* =h05q01d= + +Is this argument valid? + +#+begin_example +forall x . p(x) | q(x), +forall x . !p(x) +|- +forall x . q(x) +#+end_example + +* =h05q01d= \small{(cont’d)} + +#+begin_example +#check ND + +forall x . p(x) | q(x), forall x . !p(x) |- forall x . q(x) + +1) forall x . p(x) | q(x) premise +2) forall x . !p(x) premise +3) for every xg { + 4) p(xg) | q(xg) by forall_e on 1 + 5) case p(xg) { + 6) !p(xg) by forall_e on 2 + 7) q(xg) by not_e on 5, 6 + } + 8) case q(xg) {} + 9) q(xg) by cases on 4, 5-7, 8-8 +} +10) forall x. q(x) by forall_i on 3-9 +#+end_example + +* Announcements + +- no tutorial next week (Oct 16) (reading week) +- no tutorial the week after (Oct 23) (midterm marking)