ON FLATTENING ELIMINATION RULES
ON FLATTENING ELIMINATION RULES
复制标题
论扁平化淘汰规则
DOI：
10.1017/s1755020313000385
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Schroeder-Heister
中科院分区：
文献类型：
--
作者：
Olkhovikov;G. K. ;Schroeder-Heister
在直觉逻辑的证明论语义中，消去规则可以统一地由引入规则生成。如果引入规则排除假设，则相应的排除规则是更高层次的规则，它允许人们排除作为假设出现的规则。在某些情况下，这些统一生成的消元规则可以等价地替换为仅排出公式或根本不排出任何假设的消元规则-它们可以在Read提出的术语中变平。我们通过一个命题逻辑的例子表明，并不是所有的引入规则都有平坦的消去规则。我们将一般形式的平坦消去规则转化为二阶命题逻辑的公式，并证明我们的例子不等价于任何这样的公式。证明使用命题逻辑和Kripke语义的基本技术。
In proof-theoretic semantics of intuitionistic logic it is well known that elimination rules can be generated from introduction rules in a uniform way. If introduction rules discharge assumptions, the corresponding elimination rule is a rule of higher level, which allows one to discharge rules occurring as assumptions. In some cases, these uniformly generated elimination rules can be equivalently replaced with elimination rules that only discharge formulas or do not discharge any assumption at all—they can be flattened in a terminology proposed by Read. We show by an example from propositional logic that not all introduction rules have flat elimination rules. We translate the general form of flat elimination rules into a formula of second-order propositional logic and demonstrate that our example is not equivalent to any such formula. The proof uses elementary techniques from propositional logic and Kripke semantics.
登录
查看更多内容
DOI：
--
发表时间：
1993
期刊：
Lecture Notes in Computer Science
影响因子：
--
作者：
H. Wansing
通讯作者：
H. Wansing
自然演绎的自然延伸
DOI：
--
发表时间：
1984
期刊：
Journal of Symbolic Logic (JSL)
影响因子：
--
作者：
P. Schroeder
通讯作者：
P. Schroeder
高级规则的演算、命题量化以及证明理论和谐的基本方法
影响因子：
0.7
作者：
Herold;Panzer;Demmers;Kruger;Scharfe;Bartkuhn;Renkawitz
通讯作者：
Renkawitz
证明以及逻辑常数的意义和完备性
影响因子：
1.6
作者：
D. Prawitz
通讯作者：
D. Prawitz
根森马蒂克中的直觉主义逻辑
DOI：
--
发表时间：
1968
期刊：
影响因子：
--
作者：
F. Kutschera
通讯作者：
F. Kutschera