This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of `maximal formula', `segment' and `maximal segment' suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions in normal form have the subformula property.
翻译:本文件研究Negri和von Plato对直觉逻辑的正规化,后者具有一般的介绍和删除规则,阐述了该系统的哲学重要性,制定了适合该系统的`最大公式'、`部分'和`最大部分'的定义,并制定了关于最大公式和最大部分调整减少程序的相应削减程序,还考虑了所用主要方法的替代方法,表明系统中的扣减转换成正常形式,正常形式的扣减具有次形式属性。