Chapter 5: Propositional (unquantified) logic
=============================================
Interaction of Syntax and Semantics
-----------------------------------

DNF and CNF forms
-----------------
Let's make up a boolean function of variables x, y, z:

  x  y  z  f(x, y, z)

  0  0  0     1
  0  0  1     0
  0  1  0     1
  0  1  1     1
  1  0  0     0
  1  0  1     1
  1  1  0     0
  1  1  1     0

Let's develop a propositional formula representing f, by considering when f returns 1:

  1st row or 3rd row or 4th row or 6th row
  ~x /\ ~y /\ ~x  \/  ~x /\ y /\ ~z  \/  ~x /\ y /\ z  \/  x /\ ~y /\ z

This is in Disjunctive Normal Form (DNF): a disjunction of conjunctions of
 variables and their negations.

This natural form is one motivation for /\ taking precedence over \/.


We can also develop a formula by considering when f doesn't return 0:

  not 2nd row and not 5th row and not 7th row and not 8th row
  (x \/ y \/ ~z) /\ (~x \/ y \/ z) /\ (~x \/ ~y \/ z) /\ (~x \/ ~y \/ ~z)

This is in Conjunctive Normal Form (CNF).


In particular, we have seen that every boolean function is represented by some
 propositional formula, using only the variables, ~, /\ and \/.

More Practice with Structural Induction
---------------------------------------
Can every boolean function be represented by a propositional formula built
 only from variables, /\ and \/?

Is there some property such formulas all have (an invariant(!) while we build them)
 that not every boolean function has?

Yes: value when all variables are 0 is 0.

More formally, if P is built from variables and /\, \/, and t(v) = 0 for all v,
 then t*(P) = 0.

Proof:

  Base Case: P is some variable v, so t*(P) = t*(v) = t(v) = 0.

  Inductive Step:

    Case P = Q \/ R:

      Then Q, R only built from variables, /\, \/, so t*(Q) = t*(R) = 0,
       so t*(P) = min(t*(Q), t*(R)) = min(0, 0) = 0.

    Case P = Q /\ R:

      Again t*(Q) = t*(R) = 0, so t*(P) = t*(Q) * t*(R) = 0 * 0 = 0.

In particular, P can't represent the constant function 1
 (in particular, it can't be a tautology).

Derivations of Logical Equivalence
----------------------------------
LEQV is an equivalence relation, i.e.

  For all P, Q, R:
    P LEQV P (reflexivity)
    P LEQV Q iff Q LEQV P (symmetry)
    P LEQV Q and Q LEQV R  implies  P LEQV R (transitivity)

 These are standard properties one wants for any kind of `sameness'.


For example, we can verify from truth table that x -> y LEQV ~x \/ y.
Then we also know, for example,

   ~x \/ y LEQV x -> y, by symmetry

By reflexivity we know, for example,

   z /\ x LEQV z /\ x


Also, `sameness' usually results in some kind of substitution result(s).

  If P LEQV Q and R LEQV S then
   substituting R for a variable of P and S for the same variable of Q
   results in LEQV formulas.

This contains two kinds of substitution: `inner' and `outer', which the
 next two examples illustrate:

   ~(z /\ x) \/ y LEQV (z /\ x) -> y [R = S = z /\ x]

   (~x \/ y) /\ x LEQV (x ->y) /\ x  [P = Q = z /\ x]


Section 5.6 of the textbook lists some standard logical equivalences.
 They are actually templates for logically equivalent formulas, since
 P, Q and R there are not propositional variables but formulas.
 The can be verified by truth table via variables, and then substitution
  gives them for aribtrary P, Q and R.
  
Notice that, if we so desired, we could break down any formula into a LEQV
 one using only /\ and ~, or only \/ and ~: <-> is in terms of ->, -> is
 in terms of \/ and ~, and DeMorgan's converts between /\ and \/ since we
 can always force a ~ onto a subformula using ~~P LEQV P.


Let's use all this to show that x \/ y -> z LEQV (x -> z) /\ (y -> z)
 (a fairly useful result about proof by cases):

  x \/ y -> z LEQV ~(x \/ y) \/ z, by (substituting into) -> law
              LEQV ~x /\ ~y \/ z, DeMorgan's
              LEQV (~x \/ z) /\ (~y /\ z), Distributive
              LEQV (x -> z) /\ (y -> z), ->

  So (by transitivity) x \/ y -> z LEQV (x -> z) /\ (y -> z).


Syntactic Conventions Revisited
-------------------------------
Notice that associativity of /\ and \/ means the convention about right
 associating repeated /\ and \/ isn't really important.

But (x -> y) -> z and x -> (y -> z) are not LEQV, so we do need a convention
 if we drop the parentheses. x -> (y -> z) is very common, corresponding to:

  Suppose x. If y then z.


Lots of natural statements are -> or <-> at the `top level', which is why
 -> and <-> have lowest precedence. In Java this might be analoguous to the
 common case of if (->) being `above' a boolean condition involving &&, ||, !:

  if (x || y) {
    return !z
  }


LEQV as <->
-----------
P LEQV Q is defined in terms of the meanings of P and Q
 (via truth assignments, or as boolean functions).

We also saw syntactic manipulations above that preserve these meanings.

So we have two approaches to showing LEQV.

A third approach combines P and Q into one formula syntactically,
 then makes a claim about its meaning:

  Theorem
    P LEQV Q iff P <-> Q a tautology.

  Proof
    P LEQV Q iff t*(P) = t*(Q) for every t
             iff t*(P <-> Q) for every t
             iff P <-> Q is a tautology.

Similarly,

  Theorem
    P Logically Implies Q iff P -> Q is a tautology.