Solutions to Tutorial 4: Number Theory 1

Logical System

Solutions

Theorem 1

 
1 x=x =I
2 (∀x)(x=x) 1 UG

Theorem 2

 
1     x=y Ass
2     x=y 1 R
3     y=x 2,1 =E
 
4 (x=y)⊃(y=x) 3 ⊃I
5 (∀y)((x=y)⊃(y=x)) 4 UG
6 (∀x)(∀y)((x=y)⊃(y=x)) 5 UG

Theorem 3

 
1     (x=y)∧(y=z) Ass
2     x=y 1 ∧E
3     y=z 1 ∧E
4     x=z 3,2 =E
 
5 ((x=y)∧(y=z))⊃(x=z) 4 ⊃I
6 (∀z)(((x=y)∧(y=z))⊃(x=z)) 5 UG
7 (∀y)(∀z)(((x=y)∧(y=z))⊃(x=z)) 6 UG
8 (∀x)(∀y)(∀z)(((x=y)∧(y=z))⊃(x=z)) 7 UG

Theorem 4

 
1     x=y Ass
2     (x+z)=(x+z) =I
3     (x+z)=(y+z) 2,1 =E
 
4 (x=y)⊃((x+z)=(y+z)) 3 ⊃I

Theorem 5

1     (∀x)(∀y)((x'=y')⊃(x=y)) Ass
2     (∀x)∼(x'=0) Ass
3     (∀x)((x+0)=x) Ass
4     (∀x)(∀y)((x+y')=(x+y)') Ass
5     (∀x)((x.0)=0) Ass
6     (∀x)(∀y)((x.y')=((x.y)+x)) Ass
7     (∀y)((x+y')=(x+y)') 4 UI
8     (x+0')=(x+0)' 7 UI
9     (x+0)=x 3 UI
10     (x+0')=x' 8,9 =E

 

Theorem 6

1     (∀x)(∀y)((x'=y')⊃(x=y)) Ass
2     (∀x)∼(x'=0) Ass
3     (∀x)((x+0)=x) Ass
4     (∀x)(∀y)((x+y')=(x+y)') Ass
5     (∀x)((x.0)=0) Ass
6     (∀x)(∀y)((x.y')=((x.y)+x)) Ass
7     ((0=(0+0))∧(∀n)((n=(0+n))⊃(n'=(0+n'))))⊃(∀n)(n=(0+n)) Induction
8     (0+0)=0 3 UI
9     (0+0)=(0+0) =I
10     0=(0+0) 9,8 =E
11         n=(0+n) Ass
12         (∀y)((0+y')=(0+y)') 4 UI
13         (0+n')=(0+n)' 12 UI
14         (0+n')=n' 13,11 =E
15         n'=n' =I
16         n'=(0+n') 15,14 =E
     
17     (n=(0+n))⊃(n'=(0+n')) 16 ⊃I
18     (∀n)((n=(0+n))⊃(n'=(0+n'))) 17 UG
19     (0=(0+0))∧(∀n)((n=(0+n))⊃(n'=(0+n'))) 10,18 ∧I
20     (∀n)(n=(0+n)) 7,19 ⊃E
21     x=(0+x) 20 UI

The following were done in an earlier format, they will be replaced (in the fullness of time!).

Theorem 7
1 |(∀x)(∀y)((x'=y')⊃(x=y))                Ass
2 |(∀x)~(x'=0)                                     Ass
3 |(∀x)((x+0)=x)                                Ass
4 |(∀x)(∀y)((x+y')=(x+y)')               Ass
5 |(∀x)((x.0)=0)                                 Ass
6 |_(∀x)(∀y)((x.y')=((x.y)+x))        Ass
7 |(((x'+0)=(x+0)')∧(∀n)(((x'+n)=(x+n)')⊃((x'+n')=(x+n')')))⊃(∀n)((x'+n)=(x+n)')     Induction
8 |(x'+0)=x'   3 UI
9 |(x+0)=x     3 UI Open
10 |(x'+0)=(x+0)'  8,9 IE
11 | ˚_(x'+n)=(x+n)'     Ass
12 | |(∀y)((x'+y')=(x'+y)')  4 UI
13 | |(x'+n')=(x'+n)'   12 UI
14 | |(x'+n')=(x+n)''   13,11 IE
15 | |(∀y)((x+y')=(x+y)')    4 UI
16 | |(x+n')=(x+n)'     15 UI
17 | |(x'+n')=(x+n')'   14,16 IE
18 |((x'+n)=(x+n)')⊃((x'+n')=(x+n')')  17 ⊃I
19 |(∀n)(((x'+n)=(x+n)')⊃((x'+n')=(x+n')'))     18 UG Close
20 |((x'+0)=(x+0)')∧(∀n)(((x'+n)=(x+n)')⊃((x'+n')=(x+n')'))   10,19 ∧I
21 |(∀n)((x'+n)=(x+n)')     7,20 ⊃E
22 |(x'+y)=(x+y)'  21 UI

Theorem 8
1 |(∀x)(∀y)((x'=y')⊃(x=y))  Ass
2 |(∀x)~(x'=0)  Ass
3 |(∀x)((x+0)=x)    Ass
4 |(∀x)(∀y)((x+y')=(x+y)')  Ass
5 |(∀x)((x.0)=0)   Ass
6 |_(∀x)(∀y)((x.y')=((x.y)+x))  Ass
7 |(((x+0)=(0+x))∧(∀n)(((x+n)=(n+x))⊃((
   |x+n')=(n'+x))))⊃(∀n)((x+n)=(n+x))   Induction
8 |x=(0+x)     Theorem 6
9 |(x+0)=x     3 UI Open
10 |(x+0)=(0+x)    8,9 IE
11 | ˚_(x+n)=(n+x)   Ass
12 |((x+n)=(n+x))⊃((x+n)=(n+x))    11 ⊃I
I was testing something here so take no notice of lines
11 and 12.

13 | ˚_(x+n)=(n+x)   Ass
14 | |(∀y)((x+y')=(x+y)')    4 UI
15 | |(x+n')=(x+n)'     14 UI
16 | |(∀x)(∀y)((x'+y)=(x+y)')     Th. 7 Clos
17 | |(∀y)((n'+y)=(n+y)')    16 UI
18 | |(n'+x)=(n+x)'     17 UI
19 | |(x+n')=(n+x)'     15,13 IE
20 | |(x+n')=(n'+x)     19,18 IE
21 |((x+n)=(n+x))⊃((x+n')=(n'+x))  20 ⊃I
22 |(∀n)(((x+n)=(n+x))⊃((x+n')=(n'+x)))     21 UG Close
23 |((x+0)=(0+x))∧(∀n)(((x+n)=(n+x))⊃((x
|+n')=(n'+x)))     10,22 ∧I
24 |(∀n)((x+n)=(n+x))   7,23 ⊃E
25 |(x+y)=(y+x)    24 UI

Theorem 9
1 |(∀x)(∀y)((x'=y')⊃(x=y))  Ass
2 |(∀x)~(x'=0)  Ass
3 |(∀x)((x+0)=x)    Ass
4 |(∀x)(∀y)((x+y')=(x+y)')  Ass
5 |(∀x)((x.0)=0)   Ass
6 |_(∀x)(∀y)((x.y')=((x.y)+x))  Ass
7 |((((x+y)+0)=(x+(y+0)))∧(∀n)((((x+y)+
|n)=(x+(y+n)))⊃(((x+y)+n')=(x+(y+n')))
|))⊃(∀n)(((x+y)+n)=(x+(y+n)))     Induction
8 |((x+y)+0)=(x+y)   3 UI
9 |(y+0)=y     3 UI
10 |((x+y)+0)=(x+(y+0))  8,9 IE
11 | ˚_((x+y)+n)=(x+(y+n))     Ass
These next few lines are to change variables on Ax 4
to avoid capture when substituting (x+y) in.

12 | |(∀y)((v+y')=(v+y)')    4 UI
13 | |(v+w')=(v+w)'     12 UI
14 | |(∀w)((v+w')=(v+w)')    13 UG
15 | |(∀v)(∀w)((v+w')=(v+w)')     14 UG
16 | |(∀w)(((x+y)+w')=((x+y)+w)')  15 UI
17 | |((x+y)+n')=((x+y)+n)'   16 UI
18 | |((x+y)+n')=(x+(y+n))'   17,11 IE
19 | |(∀w)((x+w')=(x+w)')    15 UI
20 | |(x+(y+n)')=(x+(y+n))'   19 UI
21 | |((x+y)+n')=(x+(y+n)')   18,20 IE
22 | |(∀w)((y+w')=(y+w)')    15 UI
23 | |(y+n')=(y+n)'     22 UI
24 | |((x+y)+n')=(x+(y+n'))   21,23 IE
25 |(((x+y)+n)=(x+(y+n)))⊃(((x+y)+n')=(x
|+(y+n')))     24 ⊃I
26 |(∀n)((((x+y)+n)=(x+(y+n)))⊃(((x+y)+n
|')=(x+(y+n'))))   25 UG
27 |(((x+y)+0)=(x+(y+0)))∧(∀n)((((x+y)+n
|)=(x+(y+n)))⊃(((x+y)+n')=(x+(y+n'))))   10,26 ∧I
28 |(∀n)(((x+y)+n)=(x+(y+n)))     7,27 ⊃E
29 |((x+y)+z)=(x+(y+z))  28 UI

Theorem 10
1 |(∀x)(∀y)((x'=y')⊃(x=y))  Ass
2 |(∀x)~(x'=0)  Ass
3 |(∀x)((x+0)=x)    Ass
4 |(∀x)(∀y)((x+y')=(x+y)')  Ass
5 |(∀x)((x.0)=0)   Ass
6 |_(∀x)(∀y)((x.y')=((x.y)+x))  Ass
7 |(((0.0)=0)∧(∀n)(((0.n)=0)⊃((0.n')=0)
|))⊃(∀n)((0.n)=0)   Induction
8 |(0.0)=0    5 UI
9 | ˚_(0.n)=0   Ass
10 | |(∀y)((0.y')=((0.y)+0))    6 UI
11 | |(0.n')=((0.n)+0)     10 UI
12 | |(0.n')=(0+0)   11,9 IE
13 | |(0+0)=0    3 UI
14 | |(0.n')=0    12,13 IE
15 |((0.n)=0)⊃((0.n')=0)     14 ⊃I
16 |(∀n)(((0.n)=0)⊃((0.n')=0))    15 UG
17 |((0.0)=0)∧(∀n)(((0.n)=0)⊃((0.n')=0))    8,16 ∧I
18 |(∀n)((0.n)=0)   7,17 ⊃E
19 |(0.x)=0    18 UI