2008/07/02

遺忘邏輯

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

data ⊥ : Set where

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

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

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

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

Labels:

Blogger yen37/02/2008 6:25 am 說:

因為你去年只有在寫作業,今年你的心思上多了很多事

 

<< 回到主頁