The Naturality of Natural Deduction
The Naturality of Natural Deduction
复制标题
自然演绎的自然性
DOI：
10.1007/s11225-017-9772-6
复制
发表时间：
2019
期刊：
影响因子：
0.7
通讯作者：
Paolo Pistone
中科院分区：
文献类型：
--
作者：
Luca Tranchini;Mattia Petrolo;Paolo Pistone
发展罗素的建议，Prawitz展示了如何使用命题直觉主义二阶逻辑NI中的蕴涵和二阶量词推导出通常的自然演绎推理规则。然而，众所周知的是，翻译并不保留身份之间的关系，诱导的置换转换和立即扩展的可定义的连接词派生，至少当方程理论的NI被假定为只包括-和-方程。在NI的范畴解释的基础上，我们引入了一类新的方程，它用范畴术语表示解释NI-导子的变换所满足的自然性条件。我们表明，罗素-Prawitz翻译不保持身份的证明方面的丰富的系统突出的事实，即自然对应于一个广义的置换原则。最后，我们勾勒出这些结果可以用来调查的连接词的属性定义在更高层次的规则的框架。
Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logicNI. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equational theory ofNIis assumed to consist only of- and-equations. On the basis of the categorial interpretation ofNI, we introduce a new class of equations expressing what in categorial terms is a naturality condition satisfied by the transformations interpretingNI-derivations. We show that the Russell–Prawitz translation does preserve identity of proof with respect to the enriched system by highlighting the fact that naturality corresponds to a generalized permutation principle. Finally we sketch how these results could be used to investigate the properties of connectives definable in the framework of higher-level rules.
登录
查看更多内容
罗素-普拉维茨模态
影响因子：
0.5
作者：
P. Aczel
通讯作者：
P. Aczel
自然演绎的自然延伸
DOI：
--
发表时间：
1984
期刊：
Journal of Symbolic Logic (JSL)
影响因子：
--
作者：
P. Schroeder
通讯作者：
P. Schroeder
作为自然变换的范式和免割证明
影响因子：
0.8
作者：
J. Girard;A. Scedrov;P. Scott
通讯作者：
P. Scott
影响因子：
1
作者：
D. Leivant
通讯作者：
D. Leivant
DOI：
--
发表时间：
2009
期刊：
Studia Logica: An International Journal for Symbolic Logic
影响因子：
--
作者：
Fernando Ferreira;Gilda Ferreira
通讯作者：
Gilda Ferreira