Nm.agda

{-

A natural deduction presentation of minimal logic (Nm).

Basic proof theory
A.S. Troelstra, H. Schwichtenberg, 2000

-}

module Nm (Value : Set) where


infixr 7 ¬_
infixl 6 _∧_
infixl 6 _∨_
infixr 5 _⊃_
infixr 5 _⊃⊂_

infixl 4 _,_
infixl 3 _∈_
infixr 3 _⊢_


data Formula : Set where
  con : Value → Formula
  _⊃_ : Formula → Formula → Formula
  _∧_ : Formula → Formula → Formula
  _∨_ : Formula → Formula → Formula
  ∇   : (Value → Formula) → Formula
  ∃   : (Value → Formula) → Formula
  ⊥   : Formula

_⊃⊂_ : Formula → Formula → Formula
A ⊃⊂ B = (A ⊃ B) ∧ (B ⊃ A)

¬_ : Formula → Formula
¬ A = A ⊃ ⊥

⊤ : Formula
⊤ = ⊥ ⊃ ⊥


data Context (X : Set) : Set where
  ε   : Context X
  _,_ : Context X → X → Context X

data _∈_ {X : Set}(x : X) : Context X → Set where
  zero : ∀ {Γ}             → x ∈ Γ , x
  suc  : ∀ {Γ y}  → x ∈ Γ  → x ∈ Γ , y


data _⊢_ (Γ : Context Formula) : Formula → Set where
  hyp : ∀ {A}      → A ∈ Γ
                   → Γ ⊢ A
  ⊃I  : ∀ {A B}    → Γ , A ⊢ B
                   → Γ ⊢ A ⊃ B
  ⊃E  : ∀ {A B}    → Γ ⊢ A ⊃ B  → Γ ⊢ A
                   → Γ ⊢ B
  ∧I  : ∀ {A B}    → Γ ⊢ A      → Γ ⊢ B
                   → Γ ⊢ A ∧ B
  ∧Eᴿ : ∀ {A B}    → Γ ⊢ A ∧ B
                   → Γ ⊢ A
  ∧Eᴸ : ∀ {A B}    → Γ ⊢ A ∧ B
                   → Γ ⊢ B
  ∨Iᴿ : ∀ {A B}    → Γ ⊢ A
                   → Γ ⊢ A ∨ B
  ∨Iᴸ : ∀ {A B}    → Γ ⊢ B
                   → Γ ⊢ A ∨ B
  ∨E  : ∀ {A B C}  → Γ ⊢ A ∨ B  → Γ , A ⊢ C  → Γ , B ⊢ C
                   → Γ ⊢ C
  ∇I  : ∀ {P}      → (∀ {x} → Γ ⊢ P x)
                   → Γ ⊢ ∇ P
  ∇E  : ∀ {P x}    → Γ ⊢ ∇ P    → Γ ⊢ con x
                   → Γ ⊢ P x
  ∃I  : ∀ {P x}    → Γ ⊢ P x    → Γ ⊢ con x
                   → Γ ⊢ ∃ P
  ∃E  : ∀ {P x A}  → Γ ⊢ ∃ P    → Γ , P x ⊢ A
                   → Γ ⊢ A


I : ∀ {Γ A}  → Γ ⊢ A ⊃ A
I = ⊃I x
  where
    x = hyp zero

K : ∀ {Γ A B}  → Γ ⊢ A ⊃ B ⊃ A
K = ⊃I (⊃I x)
  where
    x = hyp (suc zero)

S : ∀ {Γ A B C}  → Γ ⊢ (A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C
S = ⊃I (⊃I (⊃I (⊃E (⊃E f x)
                   (⊃E g x))))
  where
    f = hyp (suc (suc zero))
    g = hyp (suc zero)
    x = hyp zero