這裡寫的是 Mathematical Logic and Computation §2.2 定義的 Axiomatic Systems。就像書中講的，這套系統很不好用，也不好學，不過在歷史上我們就是這樣實現的

{-# OPTIONS --safe --without-K --no-level-universe #-}
module ag-L7FN where

open import Agda.Builtin.Equality
open import Data.Product
open import Data.Sum

data Proposition : Set where
  ⊥ : Proposition
  _∧_ _∨_ _⇒_ : Proposition → Proposition → Proposition
infixr  _⇒_
infixl  _∧_ _∨_

variable A B C : Proposition

data ⊢ : Proposition → Set where
  PC1 : ⊢ (A ⇒ (B ⇒ A))
  PC2 : ⊢ ((A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C)))
  PC3 : ⊢ (A ⇒ (B ⇒ A ∧ B))
  PC4 : ⊢ (A ∧ B ⇒ A)
  PC5 : ⊢ (A ∧ B ⇒ B)
  PC6 : ⊢ (A ⇒ A ∨ B)
  PC7 : ⊢ (B ⇒ A ∨ B)
  PC8 : ⊢ ((A ⇒ C) ⇒ ((B ⇒ C) ⇒ (A ∨ B ⇒ C)))
  PC9 : ⊢ (⊥ ⇒ A)

  MP : ⊢ A → ⊢ (A ⇒ B) → ⊢ B

現在我們定義了邏輯語言跟它遵循的公理，我們只打算證明一個案例來了解如何用公理證明，這個問題來自 Mathematical Logic and Computation 的 proposition 2.3.6，由於第四個涉及 context 擴充而這裡沒有處理所以略過

record proposition-2-3-6 : Set where
  field
    I : ⊢ A → ⊢ B → ⊢ (A ∧ B)
    II : ⊢ (A ∧ B) → ⊢ A × ⊢ B
    III : ⊢ A ⊎ ⊢ B → ⊢ (A ∨ B)

  proof : proposition-2-3-6
  proof .I A-holds B-holds = MP B-holds (MP A-holds PC3)
  proof .II A-and-B-holds = MP A-and-B-holds PC4 , MP A-and-B-holds PC5
  proof .III (inj₁ A-holds) = MP A-holds PC6
  proof .III (inj₂ B-holds) = MP B-holds PC7

要感受這種證明風格可以有多繁瑣可以參考這裡

這邊我引入了 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  _⇒_
infixl  _∧_ _∨_

data Context : ℕ → Set where
  ∅ : Context 
  _▸_ : {l : ℕ} → Context l → Proposition → Context (suc l)
infix  _▸_

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  _⊢_

再次證明 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。