BCI.agda

module BCI.Hilbert.Definition where
open import Common

-- A tree variant of a Hilbert-style proof system with "BCI" as axioms.


data Form : Set where
  var : Atom → Form
  _⇒_ : Form → Form → Form
infixr 10 _⇒_

Cx : Set
Cx = List Form

data _⊢_ : Cx → Form → Set where
  ID : ∀ {A}         → [ A ] ⊢ A
  MP : ∀ {Γ₁ Γ₂ A B} → Γ₁ ⊢ A ⇒ B  → Γ₂ ⊢ A → Γ₁ ⁏ Γ₂ ⊢ B
  EX : ∀ {Γ A B C}   → Γ , B , C ⊢ A → Γ , C , B ⊢ A
  AB : ∀ {A B C}     → ∅ ⊢ (B ⇒ C) ⇒ (A ⇒ B) ⇒ (A ⇒ C)
  AC : ∀ {A B C}     → ∅ ⊢ (A ⇒ B ⇒ C) ⇒ B ⇒ A ⇒ C
  AI : ∀ {A}         → ∅ ⊢ A ⇒ A
infix 5 _⊢_


cong⊢₁ : ∀ {Γ Δ A} → Γ ⊢ A → Γ ≡ Δ → Δ ⊢ A
cong⊢₁ t refl = t

det : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ , A ⊢ B
det t = MP t ID

ded : ∀ {Γ Δ A B} → Γ ⊢ B → Γ ≡ Δ , A → Δ ⊢ A ⇒ B
ded ID refl                            = AI
ded (MP {Γ₂ = ∅} t₁ t₂) eq             = cong⊢₁ (MP (MP AC (ded t₁ eq)) t₂) unit⧺ₗ
ded (MP {Γ₁} {Γ₂ = xs , A} t₁ t₂) refl = cong⊢₁ (MP (MP AB t₁) (ded t₂ refl)) lemma
  where lemma : ∅ ⁏ Γ₁ ⁏ xs ≡ Γ₁ ⁏ xs
        lemma = trans (sym (assoc⧺ {L₁ = ∅} {Γ₁} {xs})) unit⧺ₗ
-- Here comes the trouble.
ded (EX {Γ} {C = C} t) refl = cong⊢₁ (MP (MP AC (ded (ded t refl) refl)) ID) (cong₂ _⁏_ {y = Γ} {u = [ C ]} unit⧺ₗ refl)
ded AB ()
ded AC ()
ded AI ()