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 <=