natural deduction [ag-M036]

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

data Context : ℕ → Set where
  ∅ : Context 
  _▸_ : {l : ℕ} → Context l → Proposition → Context (succ 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 (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。