Generalized Definitional Reflection and the Inversion Principle
Generalized Definitional Reflection and the Inversion Principle
复制标题
广义定义反射和反演原理
作者：
P. Schroeder
反演原理这个术语可以追溯到洛伦岑，他在20世纪50年代初创造了它。后来普拉维茨和其他人用它来描述自然演绎中引入和消除推理之间的对称关系，有时也称为和谐。在处理任意原子产生系统规则的可逆性时，洛伦岑的反演原理比普拉维茨的自然演绎适用范围要广得多。它与定义反射（definitional reflection）密切相关，定义反射是一种基于规则的原子定义的推理原则，由Hallnäs和Schroeder-Heister提出。在介绍了定义性反射和反演原理之后，证明了反演原理可以从定义性反射中形式化地导出，当后者被看作是建立可容许性的一个原则时。此外，定义反射和反演原理之间的关系进行了研究的背景下，普遍化原则，称为ω-原则，它允许一个通过从所有定义的替代实例的集合的一个矩阵本身。
Abstract.The term inversion principle goes back to Lorenzen who coined it in the early 1950s. It was later used by Prawitz and others to describe the symmetric relationship between introduction and elimination inferences in natural deduction, sometimes also called harmony. In dealing with the invertibility of rules of an arbitrary atomic production system, Lorenzen’s inversion principle has a much wider range than Prawitz’s adaptation to natural deduction. It is closely related to definitional reflection, which is a principle for reasoning on the basis of rule-based atomic definitions, proposed by Hallnäs and Schroeder-Heister. After presenting definitional reflection and the inversion principle, it is shown that the inversion principle can be formally derived from definitional reflection, when the latter is viewed as a principle to establish admissibility. Furthermore, the relationship between definitional reflection and the inversion principle is investigated on the background of a universalization principle, called the ω-principle, which allows one to pass from the set of all defined substitution instances of a sequent to the sequent itself.