Discrete-Math/Exercise 2 at master · A454545/Discrete-Math · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
Theorem (3.11) “¬ connection”: (¬ p ≡ q) ≡ (p ≡ ¬ q)
Proof:
    (¬ p ≡ q) ≡ (p ≡ ¬ q)
  =⟨ “Commutativity of ¬ with ≡” ⟩
    ¬ (p ≡ p) ≡ ¬ (q ≡ q)
  =⟨ “Identity of ≡” ⟩
    ¬ true ≡ ¬ true
  =⟨ “Definition of `false`” ⟩
    false ≡ false
  =⟨ “Identity of ≡” ⟩
    true

Theorem (3.12) “Double negation”: ¬ ¬ p ≡ p
Proof:
    ¬ ¬ p ≡ p
  =⟨ “¬ connection” ⟩
    ¬ p ≡ ¬ p
  =⟨ “Identity of ≡” ⟩
    true

Theorem (3.13) “Negation of `false`”: ¬ false ≡ true
Proof:
    ¬ false ≡ true
  =⟨ “Definition of `false`” ⟩
    ¬ ¬ true ≡ true
  =⟨ “¬ connection” ⟩
    ¬ true ≡ ¬ true
  =⟨ “Identity of ≡” ⟩
    true

Theorem (A2.1.2):   a - b = - (b - a)
Proof:
    a - b = - (b - a)
  =⟨ “Subtraction” ⟩
    a + (- b) = - ((- a) + b)
  =⟨ “Identity of +” ⟩
    0 + (a + (- b)) = - ((- a) + b)
  =⟨ “Unary minus” ⟩
    ((- a) + b) + (- ((- a) + b)) + (a + (- b)) = - ((- a) + b)
  =⟨ “Associativity of +” ⟩
    - ((- a) + b) + (a + (- a)) + (b + (- b)) = - ((- a) + b)
  =⟨ “Unary minus” ⟩
    - ((- a) + b) + 0 + 0 = - ((- a) + b)
  =⟨ “Identity of +” ⟩
    - ((- a) + b) = - ((- a) + b)
  =⟨ “Reflexivity of =” ⟩
    true

Theorem (A2.1.3) “Subtraction of addition”:   a - (b + c) = a - b - c
Proof:
    a - (b + c) = a - b - c
  =⟨ “Subtraction” ⟩
    a + (- (b + c)) = a + (- b) + (- c)
  =⟨ “Identity of +” ⟩
    a + (- (b + c)) = a + (- b) + (- c) + 0
  =⟨ “Unary minus” ⟩
    a + (- (b + c)) = a + (- b) + (- c) + (b + c) + (- (b + c))
  =⟨ “Associativity of +” ⟩
    a + (- (b + c)) = a + b + (- b) + c + (- c) + (- (b + c))
  =⟨ “Unary minus” ⟩
    a + (- (b + c)) = a + 0 + 0 + (- (b + c))
  =⟨ “Identity of +” ⟩
    a + (- (b + c)) = a + (- (b + c))
  =⟨ “Reflexivity of =” ⟩
    true