next up previous
Next: Tuesday, March 14, 2000 Up: Lecture Notes Previous: Friday, March 10, 2000

Monday, March 13, 2000

Definition of Even(x) as (Ey.x+x=y) and Odd(x) as (Ey.y+y' =x) given
(other definitions of Odd(x) are reasonable; defining Odd(x) as
~Even(x) is excluded...)

We proved some properties of <=.  Here are some notes from a student.

Reflexivity of <=

Theorem:  (Ax.x<=x)

| 1. a=a          arbitrary object intro
| 2. a+0 = a      axiom 3, univ. elim.
| 3. (Ez.a+z=a)   exist. intro. line 2
| 4. a<=a         line 3, def <=
5. (Ax.x<=x)      univ. intro. lines 1-4

Transitivity of <=

Theorem:  (Axyz.((x<=y & y<=z) -> x<=z))

| 1. a=a, b=b, c=c       arbitrary object intro (for multiple univ. intro.)
| Goal: ((Ew.a+w=b)&(Ej.b+j=c))->Ek.a+k=c

comment:  this goal is obtained by expanding all occurrences of <=
using the definition.

| | 2. ((Ew.a+w=b)&(Ej.b+j=c))  subpremise
| | Goal: (Ek.a+k=c)
| | 3. (Ew.a+w=b)               c.e. line 2
| | 4. (Ej.b+j=c)               c.e. line 2
| | | 5. a + Club = b           witness intro line 3
| | | | 6. b + Heart = c        witness intro line 4
| | | | 7. (a + Club) + Heart) = c   prop. = lines 5,6
| | | | 8. a + (Club + Heart) = c    assoc +, prop =, line 7
| | | | 9. (Ek.a+k=c)           exist. intro. line 8
| | | 10.  (Ek.a+k=c)           exist elim lines 6-9
| | 11. (Ek.a+k=c)              exist. elim. lines 5-10
| 12.  ((Ew.a+w=b)&(Ej.b+j=c))->Ek.a+k=c    imp. intro. lines 2-11
13. Theorem                     univ. elim. lines 1-12 and definition of <=



Randall Holmes
2000-05-05