A natural extension of natural deduction
A natural extension of natural deduction
复制标题
自然演绎的自然延伸
DOI：
--
复制
发表时间：
1984
期刊：
影响因子：
--
通讯作者：
P. Schroeder
中科院分区：
文献类型：
--
作者：
P. Schroeder
自然演绎演算的主要思想之一，如Jakowski和Gentzen所介绍的那样，是假设可以在推导过程中被解除。至于抽象逻辑，这一概念将被扩展到不仅公式而且规则都可以作为可以解除的假设。由此产生的演算和推导与任何有限水平的规则在§1中非正式地介绍，而§§2和3状态所涉及的概念和基本引理的正式定义。在这个框架内，任意n元虚算子的引入和消去规则的标准形式在§4中被激发，被理解为对逻辑符号意义理论的贡献。§5证明了标准直觉联结词的集合{&，}是完备的，也就是说&，足以表示每个具有§4中给出的标准形式的规则的n元直觉算子。第6段对相关方法作了一些评论。关于这里提出的概念到量词逻辑的扩展，参见[11]。
One of the main ideas of calculi of natural deduction, as introduced by Jaśkowski and Gentzen, is that assumptions may be discharged in the course of a derivation. As regards sentential logic, this conception will be extended in so far as not only formulas but also rules may serve as assumptions which can be discharged. The resulting calculi and derivations with rules of any finite level are informally introduced in §1, while §§2 and 3 state formal definitions of the concepts involved and basic lemmata. Within this framework, a standard form for introduction and elimination rules for arbitrary n-ary sentential operators is motivated in §4, understood as a contribution to the theory of meaning for logical signs. §5 proves that the set {&, ∨, ⊃, ⋏} of standard intuitionistic connectives is complete, i.e. &, ∨, ⊃, and ⋏ suffice to express each n-ary sentential operator having rules of the standard form given in §4. §6 makes some remarks on related approaches. For an extension of the conception presented here to quantifier logic, see [11].