#+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)