邏輯公理系統是歷史上花了不少力氣整理出來的一組極簡規則，但卻不方便使用。而 natural deduction 改善並與我們日常的思考方式對齊，使它成為更方便的推理工具。現代我們可以用 agda 表述這些概念並更輕鬆的研究他們

邏輯公理系統 [ag-L7FN]

2026-03-19

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

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

open import MLTT.Sigma
open import MLTT.Plus-Type

data Proposition : 𝓤₀  ̇ where
  ⊥ : Proposition
  _∧_ _∨_ _⇒_ : Proposition → Proposition → Proposition
infixr 30 _⇒_
infixl 40 _∧_ _∨_

variable A B C : Proposition

data ⊢ : Proposition → 𝓤₀  ̇ 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 : 𝓤₀  ̇ 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 (inl A-holds) = MP A-holds PC6
  proof .III (inr B-holds) = MP B-holds PC7

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

natural deduction [ag-M036]

2026-03-19

這邊我引入了 context，另外我沒有定義所有規則，只有定義有用到的部分而已

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

open import MLTT.Sigma
open import MLTT.Plus-Type
open import MLTT.NaturalNumbers

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

data Context : ℕ → Set where
  ∅ : Context 0
  _▸_ : {l : ℕ} → Context l → Proposition → Context (succ 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 (inl A-holds) = intro-∨₁ A-holds
  proof .III (inr 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。

從公理系統到natural deduction [EGRZ]

邏輯公理系統 [ag-L7FN]

natural deduction [ag-M036]