[SOLVED] CS Solutions to

Solutions to
CSC240 Winter 2021 Homework Assignment 3
Let i Z+ be arbitrary.
1. (a) 1
2 (imod2=0)OR(imod4=1)OR(imod4=3),propertyofZ+.
3 Suppose i mod 2 = 0.
4 element(S, i, 2), by definition of S, 3.
5 Let j Z+ be arbitrary.
6 Let k = 2(j/2 + 1) Z+.
7 2j/2 j, property of Z+.
8 2(j/2 + 1) = 2j/2 + 2 > j, property of Z+, 7.
9 k > j, substitution 6, 8.
10 lt(j, k), by definition of lt, 9.
11 k mod 2 = 0, property of Z+, 6
12 element(S, k, 2), by definition of S.
13 lt(j, k) AND element(S, k, 2), conjunction: 10,12.
14 k Z+.(lt(j, k) AND element(S, k, 2)), direct proof of existential quantification: 6,13.
15 j Z+.k Z+.(lt(j, k) AND element(S, k, 2)), generalization: 5,14.
16 element(S, i, 2) AND j Z+.k Z+.(lt(j, k) AND element(S, k, 2)), conjunction: 4,15.
17 x Z.[element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))],
direct proof of existential quantification: 16, since 2 Z.
18 (i mod 2 = 0) IMPLIES x Z.[element(S, i, x) AND
j Z+.k Z+.(lt(j, k) AND element(S, k, x))], direct proof of implication: 3,17.
19 Suppose i mod 4 = 1.
20 element(S, i, 1), by definition of S, 19.
21 Let j Z+ be arbitrary.
22 Let k = 4j/2 + 1 Z+.
23 4j/2 j, property of Z+.
24 4j/2 + 1 > j, property of Z+, 23.
25 k > j, substitution 22, 24.
26 lt(j, k), by definition of lt, 25.
27 k mod 4 = 1, property of Z+, 22.
28 element(S, k, 1), by definition of S, 27.
29 lt(j, k) AND element(S, k, 1), conjunction: 26,28.
30 k Z+.(lt(j, k) AND element(S, k, 1)), direct proof of existential quantification: 22,29.
31 j Z+.k Z+.(lt(j, k) AND element(S, k, 1)), generalization: 21,30.
32 element(S, i, 1) AND j Z+.k Z+.(lt(j, k) AND element(S, k, 1)), conjunction: 20,31.
33 x Z.[element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))],
direct proof of existential quantification: 32, since 1 Z.
34 (i mod 4 = 1) IMPLIES x Z.[element(S, i, x) AND
j Z+.k Z+.(lt(j, k) AND element(S, k, x))], direct proof of implication: 19,33.
1

35 Suppose i mod 4 = 3.
36 element(S, i, 3), by definition of S, 35.
37 Let j Z+ be arbitrary.
38 Let k = 4j/2 + 3 Z+.
39 4j/2 j, property of Z+.
40 4j/2 + 1 > j, property of Z+, 39.
41 k > j, substitution 38, 40.
42 lt(j, k), by definition of lt, 41.
43 k mod 4 = 3, property of Z+, 38.
44 element(S, k, 3),by definition of S, 43.
45 lt(j, k) AND element(S, k, 3), conjunction: 42,44.
46 k Z+.(lt(j, k) AND element(S, k, 3)), direct proof of existential quantification: 38,45.
47 j Z+.k Z+.(lt(j, k) AND element(S, k, 3)), generalization: 37, 47.
48 element(S, i, 3) AND j Z+.k Z+.(lt(j, k) AND element(S, k, 3)), conjunction: 36,47
49 x Z.[element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))],
direct proof of existential quantification: 49, since 3 Z.
50 (i mod 4 = 3) IMPLIES x Z.[element(S, i, x) AND
j Z+.k Z+, .(lt(j, k) AND element(S, k, x))], direct proof of implication: 35,49.
51 x Z.[element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))],
proof by cases: 2,18,34,50.
52 i Z+.x Z.[element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))],
generalization: 1,51.
53 io(S ), by defintion of io, 52
2

(b) 1 2 3 4 5 6 7 8 9
10 11
12
13
14
15
16
17
18
19
20
21
22
23
24
Let i = 4 Z+.
Let x Z be arbitrary.
Suppose element(S, i, x).
x = 1, by definition of S 1, 3.
Let j = i Z+.
Let k Z+ be arbitrary.
Suppose lt(j, k).
NOT(element(S, k, x)), definition of S 1, 5, 7.
lt(j, k) IMPLIES NOT(element(S, k, x)), direct proof of implication 7, 8. (A IMPLIES NOT(B)) IMPLIES NOT(A AND B), tautology
[lt(j, k) IMPLIES NOT(element(S, k, x))] IMPLIES
[NOT(lt(j, k) AND element(S, k, x))], substitution 10.
NOT(lt(j, k) AND element(S, k, x)), modus ponens 11, 9.
k Z+.NOT(lt(j, k) AND element(S, k, x)), generalization 6, 12.
NOT[k Z+.(lt(j, k) AND element(S, k, x))], negation of quantifier 13 .
j Z+.NOT[k Z+.(lt(j, k) AND element(S, k, x))], construction 5, 14 NOT[jZ+.kZ+.(lt(j,k)ANDelement(S,k,x))], negationofquantifier15.
element(S, i, x) IMPLIES NOT[j Z+.k Z+.(lt(j, k) AND element(S, k, x))],
direct proof of implication 3, 16.
(element(S, i, x) IMPLIES NOT[j Z+.k Z+.(lt(j, k) AND element(S, k, x))]) IMPLIES NOT[(element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))], substitution 10
NOT[(element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))],
modus ponens 18, 17.
x Z.NOT[element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))] generalization 2, 19.
NOT[x Z.[(element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))], negation of quantifier 20.
i Z+.NOT[x Z.[(element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))], construction 1, 21
NOT(i Z+.x Z.[(element(S, i, x) AND j Z+.k Z+.(lt(j, k) AND element(S, k, x))]), negation of quantifier 22.
NOT(io(S)), by defintion of io, 23
3