PropLogMod.agda

record Model : Set₁ where
  field
    Atomic : Set
    True : Atomic → Set

open Model


data Proposition (M : Model) : Set where
  [_] : (A : Atomic M) → Proposition M
  _&_ _=>_ : Proposition M → Proposition M → Proposition M

data Context (A : Set) : Set where
  <> : Context A
  _,_ : Context A → A → Context A

data Member {A : Set} : Context A → A → Set where
  here : ∀ {xs x} → Member (xs , x) x
  there : ∀ {xs x y} → Member xs x → Member (xs , y) x

data Proof (M : Model) : Context (Proposition M) → Proposition M → Set where
  ax : ∀ {G A} → True M A → Proof M G [ A ]
  hyp : ∀ {G P} → Member G P → Proof M G P
  &I : ∀ {G P Q} → Proof M G P → Proof M G Q → Proof M G (P & Q)
  &E1 : ∀ {G P Q} → Proof M G (P & Q) → Proof M G P
  &E2 : ∀ {G P Q} → Proof M G (P & Q) → Proof M G Q
  =>I : ∀ {G P Q} → Proof M (G , P) Q → Proof M G (P => Q)
  =>E : ∀ {G P Q} → Proof M G (P => Q) → Proof M G P → Proof M G Q

data Sat (M : Model) : Proposition M → Set where
  ax : ∀ {A} → True M A → Sat M [ A ]
  &S : ∀ {P Q} → Sat M P → Sat M Q → Sat M (P & Q)
  =>S : ∀ {P Q} → (Sat M P → Sat M Q) → Sat M (P => Q)