遺忘邏輯

繼昨天卡了一題去年出過的邏輯作業後，今天又卡了一個 ¬¬(φ ∨ ¬φ)，也是去年做過的！（雖然去年也卡很久 XD。截圖還看得到 NJEdit 舊版的介面喔！）今年就改用 Agda 記下來吧：

data ⊥ : Set where

¬_ : Set -> Set
¬ P = P -> ⊥

data _∨_ (φ ψ : Set) : Set where
  inj₁ : φ -> φ ∨ ψ
  inj₂ : ψ -> φ ∨ ψ

thm : {φ : Set} -> ¬ ¬ (φ ∨ ¬ φ)
thm φ∨¬φ→⊥ = φ∨¬φ→⊥ (inj₂ (\φ -> φ∨¬φ→⊥ (inj₁ φ)))

--
超難… 去年怎麼做得出來啊？XD