IHm.agda

{-

A Hilbert presentation of minimal implication logic (⊃Hm), or simply-typed λ-calculus (λ⊃).

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

-}

module IHm where


infixr 5 _⊃_

infixr 3 ⊢_


data Formula : Set where
  _⊃_ : Formula → Formula → Formula


data ⊢_ : Formula → Set where
  MP  : ∀ {A B}    → ⊢ A ⊃ B  → ⊢ A
                   → ⊢ B
  K   : ∀ {A B}    → ⊢ A ⊃ B ⊃ A
  S   : ∀ {A B C}  → ⊢ (A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C


I : ∀ {A}  → ⊢ A ⊃ A
I {A = A} = MP (MP (S {B = A ⊃ A})
                   K)
               K

I : ∀ {A}  → ⊢ A ⊃ A
I = MP (MP f K)
       K
  where
    f : ∀ {A}  → ⊢ (A ⊃ (A ⊃ A) ⊃ A) ⊃ (A ⊃ A ⊃ A) ⊃ A ⊃ A
    f = S