{-

A natural deduction presentation of classical logic (Nc), using de Bruijn indices.

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

-}

module NcB (Value : Set) where


infixr 9 ¬_
infixl 8 _∧_
infixl 8 _∨_
infixr 7 _⊃_
infixr 7 _⊃⊂_

infixl 7 _,_
infixl 5 _∈_
infixr 3 _+_⊢_


data Formula : Set where
  _⊃_ : 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 List (X : Set) : Set where
  ε   : List X
  _,_ : List X → X → List X

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


data _+_⊢_ (V : List Value) (Γ : List Formula) : Formula → Set where
  hyp : ∀ {A}      → A ∈ Γ
                   → V + Γ ⊢ A
  ⊃I  : ∀ {A B}    → V + Γ , A ⊢ B
                   → V + Γ ⊢ A ⊃ B
  ⊃E  : ∀ {A B}    → V + Γ ⊢ A ⊃ B  → V + Γ ⊢ A
                   → V + Γ ⊢ B
  ∧I  : ∀ {A B}    → V + Γ ⊢ A      → V + Γ ⊢ B
                   → V + Γ ⊢ A ∧ B
  ∧Eᴸ : ∀ {A B}    → V + Γ ⊢ A ∧ B
                   → V + Γ ⊢ A
  ∧Eᴿ : ∀ {A B}    → V + Γ ⊢ A ∧ B
                   → V + Γ ⊢ B
  ∨Iᴸ : ∀ {A B}    → V + Γ ⊢ A
                   → V + Γ ⊢ A ∨ B
  ∨Iᴿ : ∀ {A B}    → V + Γ ⊢ B
                   → V + Γ ⊢ A ∨ B
  ∨E  : ∀ {A B C}  → V + Γ ⊢ A ∨ B  → V + Γ , A ⊢ C  → V + Γ , B ⊢ C
                   → V + Γ ⊢ C
  ∇I  : ∀ {P x}    → V , x + Γ ⊢ P x
                   → V + Γ ⊢ ∇ P
  ∇E  : ∀ {P x}    → V + Γ ⊢ ∇ P    → x ∈ V
                   → V + Γ ⊢ P x
  ∃I  : ∀ {P x}    → V + Γ ⊢ P x    → x ∈ V
                   → V + Γ ⊢ ∃ P
  ∃E  : ∀ {P x A}  → V + Γ ⊢ ∃ P    → V + Γ , P x ⊢ A
                   → V + Γ ⊢ A
  ⊥E  : ∀ {A}      → V + Γ , ¬ A ⊢ ⊥
                   → V + Γ ⊢ A


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

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

S : ∀ {V Γ A B C}  → V + Γ ⊢ (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

WTF : ∀ {V Γ P}  → V + Γ ⊢ ¬(∇ \x → ¬(P x)) ⊃ ∃ P
WTF = ⊃I (⊥E (⊃E w
                 (∇I (⊃I (⊃E u
                             (∃I v zero))))))
  where
    w = hyp (suc zero)
    u = hyp (suc zero)
    v = hyp zero