NJEdit

NJEdit 的確好用！以下是 NJEdit 的使用畫面，證明上課給的一個定理 ~~(a | ~a)，滿難 XD：

第一張圖和第二張圖 highlight 的 a 是接在一起的，因為框框太小，只好另開視窗 XD。

Max 上課也證過精神相同的定理（還是根本就是同一個？我沒抄下來 XD），即 p 在 classical logic 裡有效（但可能在 intuitionistic logic 裡無效）時，~~p 會在 intuitionistic logic 有效（我說得對嗎？XD）。Max 證完後說這個太難不會考，我自己做一遍後也覺得最好不要考 XD。

--
暫時想不到更短的證明 XD。

---

It turns out that the proof can be (much) simpler XD. I was obsessed with the thought of using bottom elimination and led myself to a tougher direction. See below for the shorter proof:

另外最新作業 Curry-Howard 的部份我也憑 type system 上課時的印象做了做，不過要等明天上完課才能確切知道 Max 要的是什麼 XD。

--
這樣就不用開兩個視窗，也不用接圖了 XD。