关于模态化海廷演算的一些语法性质

我们证明了模态化海廷演算~\cite{esa06}允许一种正规公理化。进而我们证明在该演算中，推理规则 $\square\alpha/\alpha$ 是可容许的（命题5.6），但规则 $\square\alpha\rightarrow\alpha/\alpha$ 不是（命题6.1）。最后，我们表明该演算与直觉主义命题演算是断言等价的，这导致了模态化海廷演算的一种有限分离性质的变体。