自然演绎的自然性

基于 Russell 的一个建议，Prawitz 展示了如何利用命题直觉主义二阶逻辑 $NI^2$ 中的蕴含词和二阶量词的推理规则，推导出通常的析取、合取与谬误的自然演绎推理规则。然而众所周知，至少在假定 $NI^2$ 的等式理论仅由 $\beta$ 和 $\eta$ 等式组成时，该翻译并不保持由可定义联结词的可置换转换和直接展开所诱导的推导之间的等同关系。基于 $NI^2$ 的范畴解释，我们引入了一类新的等式，这些等式表达了范畴术语中由解释 $NI^2$ 推导的变换所满足的自然性条件。我们通过强调自然性对应于广义置换原则这一事实，证明了 Russell-Prawitz 翻译在丰富系统中确实保持了证明的等同性。我们证明这些结果推广了一些迄今未被注意到的事实，即 Russell-Prawitz 翻译将支配析取（及其他可定义联结词）的等式的特定实例类映射到已包含在 $NI^2$ 的 $\beta\eta$ 等式理论中的等式上。最后，我们将我们的方法与 Ferreira 和 Ferreira 提出的方法进行比较，并表明自然性条件提示了将其方法推广到更广泛的公式类别的可能性。