INm.agda

{-

A natural deduction presentation of minimal implication logic (⊃Nm), or simply-typed λ-calculus (λ⊃).

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

-}

module INm where


infixr 5 _⊃_

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


data Formula : Set where
  _⊃_ : Formula → Formula → 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}  → Γ ⊢ 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