這邊我引入了 context，另外我沒有定義所有規則，只有定義有用到的部分而已
{-# OPTIONS --safe --without-K --no-level-universe #-} module ag-M036 where open import Agda.Builtin.Equality open import Data.Product open import Data.Sum open import Data.Nat data Proposition : Set where ⊥ : Proposition _∧_ _∨_ _⇒_ : Proposition → Proposition → Proposition infixr 30 _⇒_ infixl 40 _∧_ _∨_ data Context : ℕ → Set where ∅ : Context 0 _▸_ : {l : ℕ} → Context l → Proposition → Context (suc l) infix 20 _▸_ variable A B C : Proposition l : ℕ Γ : Context l data _⊢_ : {l : ℕ} (Γ : Context l) → Proposition → Set where var : Γ ▸ A ⊢ A intro-⇒ : Γ ▸ A ⊢ B ----------- → Γ ⊢ A ⇒ B intro-∧ : Γ ⊢ A → Γ ⊢ B ----------- → Γ ⊢ (A ∧ B) elim-∧₁ : Γ ⊢ (A ∧ B) ----------- → Γ ⊢ A elim-∧₂ : Γ ⊢ (A ∧ B) ----------- → Γ ⊢ B intro-∨₁ : Γ ⊢ A ----------- → Γ ⊢ A ∨ B intro-∨₂ : Γ ⊢ B ----------- → Γ ⊢ A ∨ B elim-∨ : Γ ⊢ A ∨ B → Γ ▸ A ⊢ C → Γ ▸ B ⊢ C ----------- → Γ ⊢ C infix 10 _⊢_
再次證明 2.3.6 的問題
record proposition-2-3-6 : Set where field I : Γ ⊢ A → Γ ⊢ B → Γ ⊢ (A ∧ B) II : Γ ⊢ (A ∧ B) → (Γ ⊢ A) × (Γ ⊢ B) III : (Γ ⊢ A) ⊎ (Γ ⊢ B) → Γ ⊢ (A ∨ B) IV : Γ ⊢ (A ∨ B) → Γ ▸ A ⊢ C → Γ ▸ B ⊢ C → Γ ⊢ C proof : proposition-2-3-6 proof .I A-holds B-holds = intro-∧ A-holds B-holds proof .II A-and-B-holds = elim-∧₁ A-and-B-holds , elim-∧₂ A-and-B-holds proof .III (inj₁ A-holds) = intro-∨₁ A-holds proof .III (inj₂ B-holds) = intro-∨₂ B-holds proof .IV A-or-B-holds GA⊢C GB⊢C = elim-∨ A-or-B-holds GA⊢C GB⊢C
不過當然，可以看到問題幾乎就是用了定義而已，所以我們再找個問題證明看看
I : ∅ ⊢ A ∧ B ⇒ B ∧ A I = intro-⇒ (intro-∧ (elim-∧₂ var) (elim-∧₁ var))
natural deduction 的好處就是把很多直覺的推導過程內建到規則中，幾乎就是我們日常使用的邏輯規則。而它也具有可讀性，它的證明樹的結構接近我們的思考，不需要記誦一堆看起來很任意的 axiom schemas。