Commuting Conversions vs. the Standard Conversions of the “Good” Connectives
Commuting Conversions vs. the Standard Conversions of the “Good” Connectives
复制标题
通勤转换与“好”连接词的标准转换
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Gilda Ferreira
中科院分区：
文献类型：
--
作者：
Fernando Ferreira;Gilda Ferreira
自然演绎演算中引入了通勤转换作为临时手段，以保证正规证明中的子公式性质。在一本著名的书中，让-伊夫·吉拉德对这些转换进行了严厉的评论，他说“人们倾向于认为应该修改自然演绎来纠正这种暴行。”我们提出了将直觉谓词演算嵌入到二阶谓词系统中，而无需进行交换转换。此外，我们还表明，通过一系列标准转换的双向应用，原始微积分的交换转换的还原和转换可以转化为等价推导。
Commuting conversions were introduced in the natural deduction calculus as ad hoc devices for the purpose of guaranteeing the subformula property in normal proofs. In a well known book, Jean-Yves Girard commented harshly on these conversions, saying that ‘one tends to think that natural deduction should be modified to correct such atrocities.’ We present an embedding of the intuitionistic predicate calculus into a second-order predicative system for which there is no need for commuting conversions. Furthermore, we show that the redex and the conversum of a commuting conversion of the original calculus translate into equivalent derivations by means of a series of bidirectional applications of standard conversions.