有关模态逻辑的自然演绎虽不是模态逻辑研究主流之一，也比不上模态逻辑语义研究的红火，但这也是模态逻辑的一种研究传统——语形和证明论的传统。本文将就这一方面的有关问题进行探讨。首先，主要讨论自然演绎系统创建以来的研究概况和一些文献综述，并集中探讨自然演绎的基本概念和基本性质，对自然演绎的概念等作出界定。接着引入其常用的演算系统——自然演绎系统和矢列演算系统，详细的对这两个主要的自然演算系统构成和性质进行讨论。然后讨论模态逻辑的非主流的研究传统即语形研究的一些概况，并分别研究了它的一些模态系统——主要是正规模态系统如K，T，S4，S5等的自然演算系统或者矢列演算系统的构成和演算性质，在研究中对不同的系统分别使用了不同的方法。并且还详实的研究了这些模态系统的健全性和完全性，给出相关命题的证明。接下来是文章的很重要的一部分，关于古典系统和模态系统的证明论性质的研究。这一部分先讨论证明论概念的性质和研究概况，并研究证明论的一系列很重要的性质如甘岑定理(即切割消去定理)、子公式性质、析取性质等，并在一些古典系统和一些模态系统中得出相应的这些证明论性质来，同时也相应指出了一些模态系统不具有这些证明论性质的情形。