Skip to main content

PPC + Monadic Modality

deduction/MPPC_natDeduct.lean
inductive MPPC_Form : Type
| top : MPPC_Form
| var : ℕ → MPPC_Form
| and : MPPC_Form → MPPC_Form → MPPC_Form
| impl : MPPC_Form → MPPC_Form → MPPC_Form
| diamond : MPPC_Form → MPPC_Form
deduction/MPPC_natDeduct.lean
| dmap {Φ : MPPC_Hyp}{φ ψ : MPPC_Form}
    : MPPC_derives (insert φ Φ) ψ 
      → MPPC_derives (insert (MPPC_Form.diamond φ) Φ) (MPPC_Form.diamond ψ)
| dpure {Φ : MPPC_Hyp} {φ : MPPC_Form}
    : MPPC_derives Φ φ 
      → MPPC_derives Φ (MPPC_Form.diamond φ)
| djoin {Φ : MPPC_Hyp} {φ : MPPC_Form}
    : MPPC_derives Φ (MPPC_Form.diamond(MPPC_Form.diamond φ)) 
      → MPPC_derives Φ (MPPC_Form.diamond φ)
deduction/MPPC_natDeduct.lean
instance MPPC_diamond : deduction_monadic.has_diamond MPPC_Form :=
{
  diamond := MPPC_Form.diamond,
  dmap := @dmap,
  dpure := @dpure,
  djoin := @djoin,
}