邏輯公理系統

這裡寫的是 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

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

邏輯公理系統 [ag-L7FN]