Next: Monday, February 14 Up: Lecture Notes Previous: Wednesday, February 9

Friday, February 11

```problems 17, 25 of homework 5 are extra credit and may be turned in later.
Both involve proof by cases.  There's also a problem with rules for xor.

The Rules for <+> were NOT complete.

I should have included the xor elimination rules of the form

P <+> Q               P <+> Q

P                     Q

---------             ---------

~Q                    ~P

as well as the rules provided:

P <+> Q               P <+> Q

~P                    ~Q

---------             ---------

Q                     P

in the notes.  The derivation I claimed for these earlier was because
I reported the xor introduction rules incorrectly!  See March 14
correction to the xor introduction rules.

The demonstration of the other rule goes similarly.  Actually,
there is a simpler proof in which the goal pulled out of the air
is an implication, but this form is instructive and not much longer.

Here are a handy pair of rules that I thought Grantham had, and
which I authorize you to use:

~(A -> B)                 ~(A -> B)

---------                 ---------  negated implication elimination

A                         ~B

Syntax of Quantifiers and Bound Variables generally:

I'm going to begin with an example of notation with bound variables
other than quantifiers.  I'm going to start with the notation for functions
familiar from Maple.

If you have taken Math 170 here (or worked with Maple for some other
reason) you have seen the notation

(x -> x^2)

for the function f such that f(x) = x^2.

I will not write it this way (because I don't want the -> to be
confused with implication:  instead, I will use the notation

(x |-> x^2)

where |-> is the typewriter version of a symbol used for this purpose
in mathematics.

If we write the integral from 0 to 1 of x^2 in Maple, we are offered
two notational variants:

int(x^2,x=0..1);

and

int(x->x^2,0..1);

These both give the expected answer of 1/3 (I tested this!).

The first one has surface syntax more like the usual notation (which
I can't easily reproduce here).  In the usual notation for the integral,
we all know that the variable which appears in the dx is a ``dummy
variable''; it does not stand for any particular value.  The x which
appears in both of the Maple notations for this integral is equally
a ``dummy variable'' (what we call a ``bound variable''); but the second
one brings out an important aspect of variable binding constructions
generally.  In the second one, we see int as being an operation which
acts on two objects -- the function (x |-> x^2) and the range 0..1 (the
set usually written [0,1] in math class).  It is possible to simplify
the treatment of bound variables by regarding the construction of functions
as the only variable binding operator and all other variable binding
operators as operations acting on functions.  We won't do this all the time,
but I want to make you aware of the possibility.

For example, the universal quantifier

(\-/x.Px)

can be interpreted as

(x |-> Px) = (x |-> true)

(this is actually how it is defined in current theories under Watson,
for example).

Disasters with Substitution

Maple gives us a nice notation for functions, but it is not very

(x |-> a) is the constant function taking any x to the value a.

Suppose I replace a with b; I can do this in the Maple command

subs(a=b,x->a);

x->b

(for the sake of honesty, I will use actual Maple notation in Maple
input and output).

But Maple is not very smart:

subs(a=x,x->a);

x->x

Can you see why this is a disaster?

The answer is that x->x is a quite different kind of function from
x->a; it is the identity function!  We should not be allowed to replace
the a in x->a with the letter x -- in fact, any letter x outside x->x
is presumably not a ``dummy variable'' (give a calculus example of this
kind of ``double meaning'').

There is a fix for this problem:

notice that the function x->x^2 and y->y^2 are exactly the same function;
we can uniformly replace the dummy variable in a function (or in any other
expression with a bound variable) with a different letter (as long as
we don't run into ``disasters of substitution''; the letter had better
not be one already in use!)

The correct way to carry out the substitution (x |-> a)[x/a] (there's
my notation for substitution again!) is to first make a change of
bound variable:

(x |-> a) = (y |-> a)

and (y|->a)[x/a] = (y|->x) gives a constant function as we expect.

Consider

(\-/a. (x |-> a)(3) = a)

This says ``for every a, (x|->a)(3) = a; it is a true statement (the
constant function with value a applied to 3 as argument gives a as value).

It is a logical rule that if we have (Aa.P(a)) we can deduce P(x) for
any x.  For example,

(x|->4)(3) = 4

(x|->b)(3) = b

But if we naively replace a with x in this statement we get

(x|->x)(3) = x

in which the left side evaluates to 3, not x.  The point is that one
really does need to be more careful than Maple about substitutions!
The result of replacing a with a (non-dummy) x in the statement above
is NOT (x|->x)(3) = x but something like

(y|->x)(3) = x

where the dummy variable has been renamed to avoid disaster!

General rules:

1.  one can replace the dummy variable x in a function
term (x |-> T) (or any other variable binding term) with any letter
you like, as long as that letter doesn't occur in T.  (notice that T
may stand for a complex term; it is a ``metavariable'').

2.  One may not substitute x (or any expression A containing x) for
anything in (x |-> T) without first changing the dummy variable x to a

There's another problem, which arises if we try to replace
x with 3 in an expression like

x + int(x^2,x=0..1) [using maple notation]

where x occurs both ``free'' (the first occurrence) and ``bound''
(the second occurrence).  We simply don't make any substitution at all
for the dummy variable, and the result of the substitution is

3 + int(x^2,x=0..1)

(the expression 3 + int(3^2,3,0..1) isn't even grammatical!)

By the way, Maple does this wrong if we use Int instead of int
(so that it doesn't evaluate the integral before doing the substitution).

General rule 3:

the result of replacing x with anything in (x|->T) is just
(x|->T).

These rules are ``common sense''; if we really understand what our
constructions with bound variables mean, we will not make these mistakes.
But when we are reasoning with complex expressions, we can sometimes
make these errors.

Some definitions:

all occurrences of the variable x in an expression like (x|->T)
are said to be ``bound'':  the same applies to occurrences in
(\-/x.P(x)), (Ex.P(x)), int(f(x),x=a..b) and so forth.  An occurrence of
a variable which is not bound is said to be free.

The general rules above can be phrased in this way:

the binding variable in any of the expressions above can be
replaced by any variable, as long as this does not cause any
previously free variable to become bound.

substitutions can be carried out normally, unless they would cause
a previously free variable to become bound; in this case, avoid the
problem by renaming the bound variable.  When replacing a variable
with a term, replace only free occurrences of that variable.
```

Randall Holmes
2000-05-05