[Jirka_RA] Exercise 0.3.2 嘅補充說明

[gapry]

題目 : Exercise 0.3.2

以下是 @ceciliachan1979 嘅補充說明

個 example 已經多咗少少嘢，其實真係純粹係個 assumption 度 assume 埋啲你唔需要嘅 hypothesis only。

如果真係要用返 formal language 去寫

你已經有 s(k) -> s(k+1)
你係可以證到

[s(k) -> s(k+1)] -> [s(1) ^ s(2) ^ ... ^ s(k) -> s(k+1)]
= [not s(k) v s(k+1)] -> [not {s(1) ^ s(2) ^ ... ^ s(k)] v s(k+1)            (implication)
= not [not s(k) v s(k+1)] v [not {s(1) ^ s(2) ^ ... ^ s(k)] v s(k+1)         (implication)
= [s(k) ^ not s(k+1)] v [not {s(1) ^ s(2) ^ ... ^ s(k)] v s(k+1)             (de morgan)
= [s(k) ^ not s(k+1)] v [not s(1) v not s(2) v ... v not s(k)] v s(k+1)      (de morgan)
= [s(k) ^ not s(k+1)] v not s(1) v not s(2) v ... v [not s(k) v s(k+1)]      (associativity)
= [s(k) ^ not s(k+1)] v not s(1) v not s(2) v ... v not [ s(k) ^ not s(k+1)] (de morgan)
= True                                                                       (a or not a)

個人話係 你 assume 'a'，可以證到 'x'
你 assume 'a', 'b', 'c', 'd', 'e'，一樣證到 'x'

如果呢點唔係 trivial，加返落去都冇問題嘅。

同樣道理，係反向嘅時候其實都有同樣嘅 logic 位

你已經有 T(k) -> S(k+1)，要證 T(k) -> T(k+1) 其實只係加返一個 T(k) -> T(k)

[T(k) -> S(k+1)] -> [T(k) -> T(k+1)]
= [not T(k) v S(k+1)] -> [not T(k) v T(k+1)]    (implication)
= not [not T(k) v S(k+1)] v [not T(k) v T(k+1)] (implication)
= (T(k) ^ not S(k+1)) v not T(k) v T(k+1)       (de morgan)
= not S(k+1) v not T(k) v T(k+1)                (distribute and cancel the side with T(k) or not T(k) - that term is always true and you can cancel true in disjunction)
= not S(k+1) v not T(k) v (T(k) ^ S(k+1))       (definition of T(k+1))
= not (s(k+1) ^ T(k)) v (T(k) ^ S(k+1))         (de morgan)
= true                                          (a or not a)

個人話係
如果你 base on 前面 n 句，證到第 n + 1 句
咁你 base on 前面 n 句，證到前面 n + 1 句 (因為 base on 前面 n 句，證前面 n 句係 trivial)

個人覺得咁 trivial 嘅嘢唔需要咁 formal