February 15 Notes: There are two more rules. They involve a more finicky treatment of variables. G |- S[a/x] ----------- universal quantifier introduction (generalization) G |- (Ax.S) when a is a variable which does not occur in the premises G. G, S[a/x] |- P --------------- existential quantifier elimination (witness introduction) G, (Ex.S) |- P when a is a variable which does not occur in the premises G. When these rules are used, one should note the introduction of the ``new'' variable a in some way. We will do this by introducing a box in which the local variable a is declared, and outside which it cannot appear. This should be a familiar idea to the computer scientists among us. The proof structures that go with the introduction rules look like this: Goal: (Ax.S) | n. a = a arbitrary object introduction (a is a ``Greek curveball'') | . | . | . | n+i. S[a/x] n+i+1 (Ax.S) universal quantifier introduction This only works if a is a variable which does not occur outside the block (and so, for example, does not occur in S). The line a = a arbitrary object introduction has no content; it is really a comment, but it will be numbered. Rules for equality are introduced below. A technical point is that the variable x in the statement (Ax.S) that we prove is NOT local to the box and may in fact occur in S. Normally, we would not expect it to. Goal: (Ex.S) Goal: S[a/x] . . . n. S[a/x] n+1. (Ex.S) existential quantifier introduction Use of the existential quantifier elimination rule has a characteristic structure: n. (Ex.S) premise . . . | n+i+1. S[x/a] witness introduction, line n (a is a ``lucky charm'') | . | . | . | n+i+j. Q ??? n+i+j+1. Q existential quantifier elimination, lines n+i+j This only works if a is a variable which does not occur outside the block (and so, for example, does not occur in Q). Notice that a new justification, ``witness introduction'' is used for the opening line of the block in which a is introduced. It is important to note that any box beginning with witness intro inside a box beginning with arbitrary object intro must be closed before the box containing it can be closed; it will be pretty clear that one is doing something weird if one tries this (we'll look at an example in class). Use of a universal hypothesis is very simple, and we do not give an explicit example at this point (they will be found in the course of proofs later). The logical rules for equality are also provided: (no premises!) ---------- equality introduction a = a (this gives us an example of an actual axiom) The equality introduction rule is actually redundant, but for accidental reasons; because of the way we write the arbitrary object introduction lines we can actually prove it using the universal quantifier rules, but this seems like cheating. P[t/x] t = u -------- equality elimination P[u/x] Notice that t and u may be complex terms, but x is a variable. Rules like a = b a = b ------- and b = c b = a ---------- a = c can be derived: 1. a = b premise 2. a = a reflexivity of equality 3. (x=a)[a/x] line 2 3. b = a equality elimination, lines 1,3 and 1. a = b premise 2. b = c premise 3. (a=x)[b/x] line 1 3. a = c equality elimination, lines 1,3 The details of substitution are important, so we will, when we are being COMPLETELY formal, write formulas with substitutions on lines, justified by the line they explain. Often we will not be that formal. Here's an interesting proof. 1. (Ax.S) premise | 2. a = a new variable introduction | 3. S[a/x] universal quantifier elimination, line 1 4. (Ay. S[a/x][y/a]) univ. intro. lines 2-3. 5. (Ay. S[y/x]) same as line 4 (we only know this because a does not occur in S). This allows the following rule: (Ax.S) -------- renaming of bound variables, universal (Ay. S[y/x]) where y does not occur in S (actually, it is valid even if y does occur in S!) The Universe is Not Empty Goal: (Ex.x=x) Goal: (Ay.(Ex.x=x)) [this is a weird move...] | 1. a=a arbitrary object introduction | 2. (Ex.x=x) exist. intro. line 1 3. (Ay.(Ex.x=x)) univ. intro. lines 1-2 4. (Ex.x=x) univ. elim. line 3. This proof is so weird that it might be clearer with explicit substitution lines: Goal: (Ex.x=x) Goal: (Ay.(Ex.x=x)) [this is a weird move...] | 1. a=a arbitrary object introduction | 2. (Ex.x=x) exist. intro. line 1 | 2'. (Ex.(x=x))[a/y] line 2 ``clarified'' 3. (Ay.(Ex.x=x)) univ. intro. lines 1-2' 3' (Ex.x=x)[a/y] univ. elim. line 3 4. (Ex.x=x) line 3 clarified. The logic could be modified so that it would apply to nonempty universes of discourse (systems of logic, called ``free logics'' which apply to possibly empty universes of discourse are studied) but it seems fairly harmless (and is technically convenient) to take Something exists to be a logical truth. On Grantham's Greek Curveballs and Lucky Charms Grantham's convention of Greek curveballs and lucky charms is a notational extension of the system described here. It amounts to restricting the letter a introduced in ``arbitrary object elimination'' to be a Greek letter, and restricting the letter a introduced in ``witness introduction'' to be one of the weird symbols Grantham uses as ``lucky charms''. I have no hope of following these conventions here, but I may illustrate them in board examples. Grantham's convention of writing ``lucky charms'' in a way which indicates their dependencies on Greek curveballs already introduced can be instructive (we may sometimes do this) but is not needed: it is sufficient not to write any witness or arbitrary object outside the block in which it is declared. Example Proofs A relation which is symmetric, transitive, and has the property that everything has this relation to something is also reflexive. 1. (Ax.(Ay.(Az. x R y & y R z -> x R z))) premise 2. (Ax.(Ay. x R y -> y R x)) premise 3. (Ax.(Ey. x R y)) premise Goal: (Ax. x R x) | 4. a = a arbitrary object intro | Goal: a R a | 5. (Ey. a R y) univ. elim. line 3 | | 6. a R b witness intro line 5 | | 7. a R b -> b R a univ elim, twice, line 2 | | 8. b R a m. p. lines 6 and 7 | | 9. a R b & b R a c. i. lines 6,8 | | 10. (a R b & b R a) -> a R a univ. elim, thrice, line 1 | | 11. a R a m. p. lines 9,10 | 12. a R a exist. elim. lines 6-11 13. (Ax. x R x) univ. intro. lines 4-12 Look at example 6.2.3 on p. 6-18 -- proof on p. 6-19 and bogus ``proof'' on p. 6-21. Appendix: Formal Definition of Syntax and Substitution I promised in class to put this into the notes. ``formula'' is our abstract notion of ``sentence''. ``term'' is our abstract notion of ``name''. Single letters (or letters with numerical subscripts) have three possible uses: they may be variables (atomic terms), function symbols (term constructors; atomic constants are regarded as 0-ary function symbols) or predicate symbols (``verbs'') (propositional letters are regarded as 0-ary predicate symbols). Definition of Terms (``Noun Phrases'') 1. a variable is a term. letters are variables (if not reserved as constants); if x is a variable and n is a numeral, x_n is a variable. 2. if f is a function symbol of arity n and T_1...T_n are terms, then f(T_1,...,T_n) is a term. Notice that n may be 0; in this case we write f rather than f() (such an f is the name of a constant). 3. if f is an infix function symbol (necessarily of arity 2) then (x f y) is a term. The parentheses may be omitted in the presence of operator precedence conventions. 4. if x is a variable and T is a term, then (x |-> T) is a term (this is provided so that we have an example of variable binding inside terms). Another formal possibility is to have a construction like the set builder {x | P} in which a term is constructed by variable binding from a formula. Definition of Atomic Formulas (``Simple Sentences''). 1. If R is a predicate symbol of arity n and T_1,...,T_n are terms, then R(T_1,...,T_n) is an atomic formula. Notice that n may be 0; in this case we write R rather than R() (R is a propositional letter in this case). The parentheses and commas may be omitted in general if readability is not impaired. 2. if R is an infix predicate symbol (necessarily of arity 2) then (x R y) is a term. The parentheses may be omitted in the presence of operator precedence conventions. Definition of Formulas (``Sentences''). 0. an atomic formula is a formula. 1. If T and U are formulas, then ~T, (T & U), (T | U), (T -> U), (T <-> U), and (T <+> U) are formulas (clauses may be added for other propositional connectives if desired.) 2. If x is a variable and T is a formula, then (Ax.T) and (Ex.T) are formulas. There is a final clause to this whole recursive definition which says that every formula, atomic term, and term can be shown to be a formula, term, or atomic term by applying these rules. Now we provide a completely formal definition of substitution. If T is a formula or term, U is a term, and x is a variable, we define the symbol T[U/x] as follows: T a term 1. if T is the variable x, we have x[U/x] = U. 2. if T is a variable y distinct from x, we have y[U/x] = y. 3. if T is of the form f(T_1,...T_n) we have f(T_1,...T_n)[U/x] = f(T_1[U/x],...T_n[U/x]); make the substitution in each argument. 4. if T is of the form (x |-> A), we have (x |-> A)[U/x] = (x |-> A). 5. if T is of the form (y |-> A), with y different from x, we have (y|-> A)[U/x] = (z |-> A[z/y][U/x]), where z is any variable which does not occur in A or U (all such terms are provably equal, no matter which z is chosen). This is the fancy way to say, ``rename y to a completely new variable z, then carry out the substitution''. If y does not occur in U, then (y|->A[U/x]) works. The set builder construction {x | P} would be handled in the same way, as would constructions like integrals from ordinary mathematics. T an atomic formula 1. R(T_1,...,T_n)[U/x] = R(T_1[U/x],...,T_n[U/x]). 2. (A R B)[U/x] = A[U/x] R B[U/x] T a formula 1. for example, (A & B)[U/x] = (A[U/x] & B[U/x]); similarly for all connectives. 2. (Ax.P)[U/x] = (Ax.P); (Ay.P)[U/x] = (Az.P[z/y][U/x]) where z is any variable which does not occur in P or U (all such formulas are provably equivalent, no matter which z is chosen). This is the fancy way to say, ``rename y to a completely new variable z, then carry out the substitution''. If y does not occur in U, then (Ay.P[U/x]) works. (Ex.P) is handled in the same way.