1/2/2021
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
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