Predicate (Quantified) Logic
============================
Informal
--------
Domain: Non-empty set D.
  E.g. Z, trees

Predicate: Function from D^n (= D x D x ... D) -> {0, 1}.
  E.g. D = Z, M(x, y, z) is "x = y mod z"
       D = set of people, P(x, y) is "x is y's parent"

Unlike in 165, we'll usually have single domain.

Arity: number of parameters for predicate.
Some special cases:
  1: unary
  2: binary
  3: ternary

Combine predicates with:

  the propositional boolean connectives
  -]x, \-/x: variable ranges over D

Same syntactic conventions as for propositional,
 and -]x, \-/x have highest precedence like ~.

Examples:
  -]x P(x, y): y has a parent.
    this is now unary
  \-/x -]y P(x, y): Everyone has a child.
    this is now a proposition
  \-/x M(0, x, 2): Every integer is even.
    also a proposition

The last example used "0" and "2", called constants.

Free and bound variables
------------------------
Free variable of a formula: occurence that isn't quantified.
Otherwise: bound.

E.g. -]x P(x, y): x is bound, y is free.

E.g. \-/x P(y, x) \/ P(x, y)
  from the syntactic conventions above, this means
    (\-/x P(y, x)) \/ P(x, y)
   and the x in P(y, x) is bound, the x in P(x, y) is free
   and the y in both Ps is free.
  So this is binary (two free variables).

No free variables: (closed) sentence.


Syntax (more formally)
------
First-order language:

  1. Set of constant symbols.
  2. Infinite set of variables.
  3. Set of predicate symbols and their arities.

Then:

  term: constant symbol or variable
  atomic: A(t1, ..., tn) for predicate symbol A and terms t1, ..., tn

First-order formulas of L:

  Smallest set such that:

    1. Atomics are in it.
    2. If E, F are in it then ~E, (E /\ F), (E \/ F), (E -> F), (E <-> F) are in it.
    3. If E is in it and x is a variable, then -]x F, \-/x F are in it.

Comparison with Propositional Logic
-----------------------------------
Atomics are like propositional variables with more structure/detail:

  produce 0 and 1
  but based on other (usually not boolean) variables and constants

Quantifiers remove the dependency on the variables.


Semantics (more formally)
---------
Structure S for language L:

  1. Non-empty domain D.
  2. Meanings of constant symbols: for each c of L, a c^S in D.
  3. Meanings of predicate symbols: for each P of L with arity n, a P^S subset of D^n.
     [Could also take the approach that P^S if function from D^n -> {0, 1}]

Enough to decide meaning of sentences from L.


Valuation of structure S: s:Variables of L -> D.

Interpretation I of L: A structure and a valuation.

Enough to decide truth of all formulas of L:

  For I = (S, s), truth values are defined by:

  1. For term t, t^I = t^S  if t a constant symbol,
                       s(t) if t a variable.
  2. For atomic P(t1, ..., tn), whether (t1^I, ..., tn^I) in P^S.
  3. ~E, (E /\ F), ... as in propositional.
  4. \-/x F:
      for every interpretation (S, s') such that s'(t) = s(t) for all t != x, F^I
      [such an s' is also written s|^x_v where s'(x) = v]
  5. -]x F:
      for some interpretation (S, s') such that s'(t) = s(t) for all t != x, F^I

As in propositional logic, define
  satisfies, falsifies, valid, satisfiable, unsatisfiable.
 Use interpretations instead of truth assignments.

Example:

  =(1, 1) is not a tautology (!)

  Let Structure S have:

    D: {red}
    1^S: red
    =^S: {} (no pairs are equal)

    For (any) interpretation I = (S, s): [=(1, 1)]^I is (1^S, 1^S) in =^S
                                                     is (red, red) in {}
                                                     is false.

We do not however allow redefinitions of the logical operations.
 So, for example, the following are tautologies:

  P \/ ~P
  Q(x) \/ ~Q(x)
  \-/x Q(x) \/ ~\-/x Q(x)

Notice that, by testing against every valuation, checking for validity essentially
 binds the free variables with universal quantifiers.

This matches common convention, for example if someone says:

  sin^2 x + cos^2 x = 1

 they mean it for all x (in R).


Logical Equivalence and Implication
-----------------------------------
E Logically Implies F:
  Every interpretation satisfying E also satisfies F.
E Logically Equivalent To (LEQV) F:
  An interpretation satisfies E iff it satisfies F.

Theorem: E Logically Implies F iff E -> F is valid.
         E LEQV F iff E <-> F is valid.

Wow, that's three slightly different levels of equivalence: iff, LEQV and <->.
Yes, it bothered me too when I first saw it.

The model of propositional logic on the assignment should give you a more concrete feel
 for this kind of thing.

Generalized DeMorgan's Laws
---------------------------
  ~-] x F LEQV \-/x ~F (*)
  ~\-/x F LEQV  -]x ~F (**)

Generalizes DeMorgan's: -] is like \/, \-/ is like /\.

Formal proof of (*):
  An interpretation I = (S, s) satisfies ~-]x F
    iff it falsifies -]x F
    iff there is no d in D so that F is satisfied by (S, s|^x_d)
    iff for every d in D, F is falsified by (S, s|^x_d)
    iff for every d in D, ~F is satisfied by (S, s|^x_d)
    iff \-/x ~F is satisfied by (S, s).

Yes, we used DeMorgan's law at the "meta-level" to reason about our formalization.
Yes, I find it somewhat unsatisfying as well.

In programming, this is related to "reflection" and meta-programming.
About a century ago Goedel did remarkable work by getting *inconsistencies* between levels.
 You'll learn about computing versions of these inconsistencies in 3rd year.

Now we'll prove (**) from (*). We'll use the following results:

  Import of propositional equivalences:
    If P, Q are propositional formulas and P LEQV Q as propositional formulas,
     then P LEQV Q as predicate formulas.

  If P, Q are propositional formulas and P LEQV Q,
   then substituting formulas for their (same) variables produces LEQV formulas.

  If E LEQV F then substituting one for the other in a formula produces a LEQV formula.

Proof of (**):

  ~\-/x F LEQV ~\-/x ~~F (uses all three results: P LEQV ~~P,
                                                  so F LEQV ~~F by 1st substitution
                                                  then substitute ~~F for F)
          LEQV ~~-]x ~F  (from (*) and 2nd kind of substitution)
          LEQV   -]x ~F  (from ... [exercise])

Renaming Variables
------------------
In programming, we can rename variables as long as we're consistent and don't cause
 accidental duplication:

  for x in D {
    Do F // with no y's in it
  }

 is equivalent to

  for y in D {
    Do F' // F with all x's replaced by y
  }

In some languages, and in predicate logic, there are levels of scope allowing for
 the same variable name at different levels:

  for x in D {
    ...
    for z in D {
      ...
      for x in D {
        // in here x means the x from the previous line
      }
      ...
    }
    ...
  }

When we replace the x's we must leave the more local ones alone, i.e. the ones bound in F.

  \-/x F LEQV \-/y F' if F has no y's and F' is F with all free x replaced by y.

  Similarly for -].

Factoring
---------
Let D = {0, 1, 2, ..., 9}.

Consider:

  boolean b = true;

  boolean E = ...;
  for (int x = 0; x < 10; ++x) {
    b = b && E && P(x);
  }

This tests whether \-/x (E /\ P(x))
E doesn't depend on x, so it can be `factored out':


  boolean E = ...;
  boolean b = E;
  for (int x = 0; x < 10; ++x) {
    b = b && E && P(x);
  }

This tests whether E /\ \-/x P(x).


In general, suppose x is not free in E.

Then E /\ \-/x F LEQV \-/x (E /\ F).
Similarly for -], and also for \/.

We must be more careful with implication.
We can factor on the left:

  E -> \-/x F LEQV \-/x (E -> F)
  E ->  -]x F LEQV  -]x (E -> F)

But on the right we must switch quantifiers:

  (\-/x F) -> E LEQV  -]x (F -> E) (*)
  ( -]x F) -> E LEQV \-/x (F -> E) (**)


Let's see why (*) is true.

  Case: \-/x F.

    Then (\-/x F) -> E iff E.
    
    -]x (F -> E) is true iff F -> E for some x,
                         iff E for some x, since F is true for x
                         iff E, since E doesn't depend on x

  Case: ~\-/x F.

    Then (\-/x F) -> E.

    By DeMorgan, -]x ~F, so -]x (F -> E)


We could also have done it by breaking down -> into ~ and \/.