IHm.idr

{-

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

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

-}

module IHm


infixr 5 >>

syntax "!-" [a] = Theorem a


data Formula : Type where
  (>>) : Formula -> Formula -> Formula


data Theorem : Formula -> Type where
  MP  : Theorem (a >> b)  -> Theorem a
     -> Theorem b
  K   : Theorem (a >> b >> a)
  S   : Theorem ((a >> b >> c) >> (a >> b) >> a >> c)


I : !- a >> a
I {a} = MP (MP (S {b = a >> a})
               K)
           K

I' : !- a >> a
I' = MP (MP f K)
        K
  where
    f : Theorem ((a >> (a >> a) >> a) >> (a >> a >> a) >> a >> a)
    f = S