This paper considers a formalisation of classical logic using general introduction rules and general elimination rules. It proposes a definition of `maximal formula', `segment' and `maximal segment' suitable to the system, and gives reduction procedures for them. It is then shown that deductions in the system convert into normal form, i.e. deductions that contain neither maximal formulas nor maximal segments, and that deductions in normal form satisfy the subformula property. Tarski's Rule is treated as a general introduction rule for implication. The general introduction rule for negation has a similar form. Maximal formulas with implication or negation as main operator require reduction procedures of a more intricate kind not present in normalisation for intuitionist logic. The Correction added to the end of the paper corrects an error: Theorem 2 is mistaken, and so is a corollary drawn from it as well as a corollary that was concluded by the same mistake. Luckily this does not affect the main result of the paper.

翻译：本文考虑使用一般引入规则和一般消去规则对经典逻辑进行形式化。它提出了适用于该系统的“最大公式”“段”和“最大段”的定义，并给出了相应的归约程序。随后证明，系统中的推导可转化为正规形式，即既不包含最大公式也不包含最大段的推导，且正规形式的推导满足子公式性质。塔尔斯基规则被视为蕴涵的一种一般引入规则，否定的一般引入规则具有类似形式。以蕴涵或否定为主算子的最大公式需要更复杂的归约程序，这是直觉主义逻辑正规化中不存在的。文末添加的修正纠正了一个错误：定理2是错误的，由此推出的推论以及因相同错误得出的另一个推论也不正确。幸运的是，这并未影响论文的主要结论。