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 smart about it. (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); and Maple will reply 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 fresh variable not found in T or the expression 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.