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 2⌈j/2⌉ ≥ j, property of Z+.
8 2(⌈j/2⌉ + 1) = 2⌈j/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 = 4⌈j/2⌉ + 1 ∈ Z+.
23 4⌈j/2⌉ ≥ j, property of Z+.
24 4⌈j/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 = 4⌈j/2⌉ + 3 ∈ Z+.
39 4⌈j/2⌉ ≥ j, property of Z+.
40 4⌈j/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[∀j∈Z+.∃k∈Z+.(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