Chapter 5: Propositional (unquantified) logic
=============================================
Syntax
------
Ignores what the symbols mean.
Treats expressions as strings.
Like the compile phase in Java.


Connectives: ~, /\, \/, ->, <->.
Their names:
  negation, conjunction, disjunction, conditional, biconditional


Propositional Formulas:

  Start with a set PV of Propositional Variables for representing
   propositions (like boolean variables in Java).
  Combine them with the connectives to get the set of Prop. Formulas F.

    Base Case: PV is a subset of F.
    Inductive Step:
      If P, Q in F then ~P, (P /\ Q), (P \/ Q), (P -> Q), (P <-> Q) are in F.
       Note: "~", "(", "/\", etc are meant literally,
        but P and Q stand for arbitrary elements of F.


For example, let PV = {x, y, z}.
 Then some propositional formulas are:
  x
  ~x
  y
  (~x \/ y)
  ~(~x \/ y)
  (z -> ~(~x \/ y))

Can make a parse tree to represent a propositional formula.
 This is what most parsers(!)/compilers/interpreters do.
 For example:

             ->
           /   \
          z     ~
                |
               \/
              /  \
             ~    y
             |
             x

This is called the "abstract syntax", whereas the particulars of parentheses, which
 symbols are used (e.g. /\ versus ^), infix/prefix/postfix are called "surface syntax".

[Note: in class I momentarily forgot the term "abstract syntax", and made up the
 term "structural syntax"]

Note that (x \/ (y \/ z)) is a different propositional formula than ((x \/ y) \/ z),
 in particular they have different parse trees.

Some syntactic conventions save some writing/typing:

  may leave out outermost parentheses
    E.g. z -> ~(~x \/ y)
  /\, \/ take precedence over ->, <->
    E.g. x /\ y -> x \/ z parsed as (x /\ y) -> (x \/ z) 
  /\ before \/
    E.g. x \/ y /\ z parsed as x \/ (y /\ z)
  repetition associates to the right
    E.g. x -> y -> z parsed as x -> (y -> z)


Propositional formulas are built up inductively/recursively.
Let's see how to reason about such inductive/recursive definitions, by proving
 the following:

  The number of variables (where we count repeated occurrences as distinct) is
   one more than the number of binary connectives (where again repetition counts).

Induction is for a predicate of natural numbers, so we number the formulas.
 Two reasonable approaches:

  length of formula

  number of times the inductive step is applied

 The second is nicer to work with, since it more closely matches the definition.

A couple of small points: this assumes that each formula is built *only* by applying
 the inductive step
  1. to base cases
  2. a finite number of times

A shorter equivalent way of saying this is that F is the *smallest* set satisfying
 the base case and inductive step. Pretend we added this to our original definition.
 (If you've done a linear algebra course, this is analogous to defining span(S)
   as the *smallest* set containing S u {0} (base case), and closed under addition and
   scalar multiplication (inductive step)).

Now to our proof.
 For convenience, define v(P), b(P) as the number of variables, binary connectives in P.

  Base Case Suppose P is built from the base case using 0 inductive steps.
  ---------
  Then P is a variable, so v(P) = 1 = 0 + 1 = b(P) + 1.

  Inductive Step Let n in N. Suppose the result is true for all formulas built
  --------------  from < n inductive steps.

  Suppose P is built from n inductive steps.

  Then P is ~Q for some Q, or (Q b R) for some Q, R and binary connective b.

  If P is ~Q, then Q is built from n - 1 < n steps, so Q has one more variable
   than binary connectives. ~Q has no new variables or binary connectives,
   so the result is true for P.

  If P is (Q b R), then Q, R are built from < n steps, so
    v(Q) = b(Q) + 1, v(R) = b(R) + 1.
   P has one more binary connective than (Q b R), and no new variables, so
    v(P) = v(Q) + v(R) = b(Q) + 1 + b(R) + 1 = b(P) + 1

People often don't bother mentioning n if its actual value is irrelevant.
The above type of proof is called structural induction.