自然推理系统

指一个没有公理的逻辑演算体系。不同于命题演算和谓词演算公理系统，自然推理系统的出发点里没有公理，除了形成规则之外，它的出发点只是一些变形规则或推演规则。自然推理系统中的变形规则或推演规则较之命题演算和谓词演算更接近于一般的数学思维，所以被称为自然推理系统。
自然推理系统的变形规则可以用一些图式表示。关于每一个逻辑常项，都有两种图式，一种是引入这一常项，另一种是消去这一常项，五个真值联结词的图式如下：

图式横线上的公式为推演的根据，横线下的公式是结论。横线上面有方括号的公式，例如[A]，只是暂时的假设，推理图式中的结沦不再以它为前提。因此，自然推理在证明的任何一步上，都可以引入前提，并且在证明的任何一步上所得到的结论都可以作为后继证明的前提。
关于量词的推理图式如下：

在全称引入图式中的变项x不得在曾经引用本图式的任一被解除公式中作为自由变项出现。
通过上面的图式就可以进行定理的证明。如果证明序列中的每一步都是由推理规则或推理图式得到，则这样的证明称作有效的。有效证明得到的结论称作有效的结论，即该结论是从前提中必然得出的。解除了假设前提而得到的公式都是系统中的定理。自然推理系统满足完全性的要求，即它能把命题逻辑的所有重言式和谓词逻辑的所有普遍有效式都推演出来。