next up previous
Next: February 16, 2000 Up: Lecture Notes Previous: Monday, February 14

Tuesday, February 15

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.



Randall Holmes
2000-05-05