--- /dev/null
+#+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)
projects / ~bandali / bndl.org / blobdiff