How to Ekman a Crabbé-Tennant
How to Ekman a Crabbé-Tennant
复制标题
如何埃克曼克拉布-坦南特
DOI：
10.1007/s11229-018-02018-3
复制
发表时间：
2018
期刊：
影响因子：
1.5
通讯作者：
Luca Tranchini
中科院分区：
文献类型：
--
作者：
Peter Schroeder-Heister ;Luca Tranchini
发展了Prawitz的早期结果，Tennant在Gentzen的自然演绎框架中提出了一个表达式被视为悖论的标准：悖论表达式产生非正规化推导。追溯到克拉贝和坦南特的两种不同的情况表明，标准过度生成，也就是说，存在直觉上非悖论但未能规范化的推导。坦南特提出的解决方案包括以一般（或并行）形式重新制定自然演绎消除规则。发展Ekman的直觉，我们表明采用一般规则的结果是在推导中隐藏了冗余。一旦设计了去除隐藏冗余的约简，很明显，采用一般消去规则并不能弥补普拉维茨-坦南特分析的过度生成。通过这种方式，我们间接地提供了进一步的支持解决方案的两个过度生成的情况下，在以前的工作。
Developing early results of Prawitz, Tennant proposed a criterion for an expression to count as a paradox in the framework of Gentzen’s natural deduction: paradoxical expressions give rise to non-normalizing derivations. Two distinct kinds of cases, going back to Crabbé and Tennant, show that the criterion overgenerates, that is, there are derivations which are intuitively non-paradoxical but which fail to normalize. Tennant’s proposed solution consists in reformulating natural deduction elimination rules in general (or parallelized) form. Developing intuitions of Ekman we show that the adoption of general rules has the consequence of hiding redundancies within derivations. Once reductions to get rid of the hidden redundancies are devised, it is clear that the adoption of general elimination rules offers no remedy to the overgeneration of the Prawitz–Tennant analysis. In this way, we indirectly provide further support for a solution to one of the two overgeneration cases developed in previous work.
登录
查看更多内容
影响因子：
0.3
作者：
J. Plato
通讯作者：
J. Plato
蕴涵作为规则与蕴涵作为链接：后续微积分的另一种蕴涵左模式
影响因子：
1.5
作者：
P. Schroeder
通讯作者：
P. Schroeder
证明与悖论
DOI：
--
发表时间：
1982
期刊：
影响因子：
--
作者：
N. Tennant
通讯作者：
N. Tennant
结构证明理论
DOI：
10.1017/cbo9780511527340
发表时间：
2001
期刊：
ACM Transactions on Computational Logic (TOCL)
影响因子：
--
作者：
Sara Negri;J. Plato
通讯作者：
J. Plato
剪切的悖论和失败
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
David Ripley
通讯作者：
David Ripley